1open HolKernel Parse boolLib bossLib;
2
3local open stringLib in end
4
5open grammarLib
6open monadsyntax lcsymtacs pegTheory
7
8val _ = new_theory "simpleSexp";
9
10val _ = temp_add_monadsyntax()
11
12val _ = overload_on ("monad_bind", ``OPTION_BIND``)
13val _ = overload_on ("monad_unitbind", ``OPTION_IGNORE_BIND``)
14val _ = temp_overload_on ("return", ``SOME``)
15val _ = temp_overload_on ("SOME", ``SOME``)
16
17val _ = computeLib.add_persistent_funs ["option.OPTION_BIND_def",
18                                        "option.OPTION_IGNORE_BIND_def",
19                                        "option.OPTION_GUARD_def",
20                                        "option.OPTION_CHOICE_def"]
21
22val _ = overload_on ("assert", ``option$OPTION_GUARD : bool -> unit option``)
23val _ = overload_on ("++", ``option$OPTION_CHOICE``)
24
25
26val _ = Datatype`
27  sexp = SX_CONS sexp sexp
28       | SX_SYM string
29       | SX_NUM num
30       | SX_STR string
31`;
32
33val _ = add_numeral_form(#"s", SOME "SX_NUM")
34val _ = overload_on ("nil", ``SX_SYM "nil"``)
35val _ = add_rule { block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)),
36                   fixity = Closefix,
37                   paren_style = OnlyIfNecessary,
38                   pp_elements = [Parse.TOK "���", TM, HardSpace 1,
39                                  Parse.TOK "���", BreakSpace(1, 0), TM,
40                                  Parse.TOK "���"],
41                   term_name = "SX_CONS" }
42val _ = add_listform { block_info = (PP.INCONSISTENT, 0),
43                       cons = "SX_CONS", leftdelim = [Parse.TOK "���"],
44                       nilstr = "nil", rightdelim = [Parse.TOK "���"],
45                       separator = [Parse.TOK ";", BreakSpace(1,0)]}
46
47val _ = overload_on ("���", ``��s. ��� SX_SYM "quote" ; s ���``)
48
49val valid_first_symchar_def = Define`
50  valid_first_symchar c ��� isGraph c ��� c ��� {#"'"; #"("; #")"; #"."; #"\""} ��� ��isDigit c`;
51
52val valid_symchar_def =  Define`
53  valid_symchar c ��� isGraph c ��� c ��� {#"'"; #"("; #")"}`;
54
55val valid_symbol_def = Define`
56   (valid_symbol "" ��� F) ���
57   (valid_symbol (c::cs) ��� valid_first_symchar c ��� EVERY valid_symchar cs)`;
58
59val valid_sexp_def = Define`
60  (valid_sexp (SX_SYM s) ��� valid_symbol s) ���
61  (valid_sexp (SX_CONS s1 s2) ��� valid_sexp s1 ��� valid_sexp s2) ���
62  (valid_sexp (SX_STR s) ��� EVERY isPrint s) ���
63  (valid_sexp s ��� T)`;
64val _ = export_rewrites["valid_first_symchar_def","valid_symchar_def","valid_symbol_def","valid_sexp_def"];
65
66val arb_sexp_def = Define`arb_sexp = SX_NUM 0`;
67
68val destSXNUM_def = Define`
69  destSXNUM (SX_NUM n) = n ���
70  destSXNUM _ = 0
71`;
72
73val destSXSYM_def = Define`
74  destSXSYM (SX_SYM s) = s ���
75  destSXSYM _ = ""
76`;
77
78val destSXCONS_def = Define`
79  destSXCONS (SX_CONS a d) = (a,d) ���
80  destSXCONS _ = (arb_sexp, arb_sexp)
81`;
82
83val strip_sxcons_def = Define`
84  strip_sxcons s =
85    case s of
86        SX_CONS h t => OPTION_MAP (CONS h) (strip_sxcons t)
87      | SX_SYM s => if s = "nil" then SOME []
88                    else NONE
89      | _ => NONE
90`;
91
92val sxMEM_def = Define`
93  sxMEM e s ��� ���l. strip_sxcons s = SOME l ��� MEM e l
94`;
95
96val sexp_size_def = definition"sexp_size_def";
97
98val sxMEM_sizelt = store_thm(
99  "sxMEM_sizelt",
100  ``���s1 s2. sxMEM s1 s2 ��� sexp_size s1 < sexp_size s2``,
101  dsimp[sxMEM_def] >> Induct_on `s2` >>
102  dsimp[Once strip_sxcons_def, sexp_size_def] >> rpt strip_tac >>
103  res_tac >> simp[]);
104
105val dstrip_sexp_def = Define`
106  (dstrip_sexp (SX_CONS sym args) =
107     case sym of
108         SX_SYM s => OPTION_MAP (��t. (s, t)) (strip_sxcons args)
109       | _ => NONE) ���
110  (dstrip_sexp _ = NONE)
111`;
112
113val tokmap = List.foldl (fn ((s,t), acc) => Binarymap.insert(acc, s, t))
114                        (Binarymap.mkDict String.compare)
115  [("(", ``#"("``), (")", ``#")"``), ("'", ``#"'"``),
116   ("\"", ``#"\""``), ("\\", ``#"\\"``), (".", ``#"."``)]
117
118fun toklookup s =
119  Binarymap.find(tokmap, s)
120  handle Binarymap.NotFound => raise Fail ("No tok def for "^s)
121
122val ginfo = { tokmap = toklookup,
123              tokty = ``:char``, nt_tyname = "sexpNT", start = "sexp",
124              gname = "sexpG", mkntname = (fn s => "sxnt_" ^ s) }
125
126
127val sexpG_def = mk_grammar_def ginfo `
128  sexp ::= WSsexp grabWS ;
129  WSsexp ::= grabWS sexp0 ;
130  grabWS ::= WS grabWS | ;
131  WS ::= ^(``{ c | isSpace c }``) ;
132  sexp0 ::= sexpsym | sexpnum | sexpstr | "(" sexpseq grabWS ")"
133         | "(" sexp "." sexp ")" | "'" WSsexp ;
134
135  sexpseq ::= WSsexp sexpseq | ;
136
137  sexpnum ::= sexpnum digit | digit ;
138  digit ::= ^(``{ c | isDigit c}``);
139
140  sexpstr ::= "\"" strcontents "\"" ;
141  strcontents ::= | strchar strcontents ;
142  strchar ::= normstrchar | escapedstrchar ;
143  normstrchar ::= ^(``{ c | isPrint c ��� c ��� #"\\" ��� c ��� #"\"" }``) ;
144  escapedstrchar ::= "\\" escapablechar ;
145  escapablechar ::= "\\" | "\"" ;
146
147  sexpsym ::= first_symchar symchars ;
148  first_symchar ::= ^(``{ c | valid_first_symchar c }``)
149 ;
150  symchars ::= symchar symchars | ;
151  symchar ::= ^(``{ c | valid_symchar c }``);
152`;
153
154val _ = type_abbrev("NT", ``:sexpNT inf``)
155val _ = overload_on("mkNT", ``INL : sexpNT -> NT``)
156val _ = overload_on ("TK", ``TOK : char -> (char,sexpNT)symbol``)
157
158
159val ptree_digit_def = Define`
160  (ptree_digit (Lf _) = NONE) ���
161  (ptree_digit (Nd (ntm,_) args) =
162     if ntm ��� mkNT sxnt_digit then NONE
163     else
164       case args of
165           [Lf tksym] =>
166             do
167               c <- destTOK tksym ;
168               return (ORD c - ORD #"0")
169             od
170         | _ => NONE)
171`;
172
173val ptree_sexpnum_def = Define`
174  (ptree_sexpnum (Lf _) = NONE) ���
175  (ptree_sexpnum (Nd (ntm,_) args) =
176     if ntm ��� mkNT sxnt_sexpnum then NONE
177     else
178       case args of
179           [d] => ptree_digit d
180         | [sn; d] =>
181             do
182                dn <- ptree_digit d ;
183                snn <- ptree_sexpnum sn ;
184                return (10 * snn + dn)
185             od
186         | _ => NONE)
187`;
188
189
190val ptree_WS_def = Define`
191  (ptree_WS (Lf _) = NONE) ���
192  (ptree_WS (Nd (ntm,_) args) =
193   if ntm ��� mkNT sxnt_WS then NONE
194   else
195     case args of
196       [c] => return ()
197     | _ => NONE)`;
198
199val ptree_grabWS_def = Define`
200  (ptree_grabWS (Lf _) = NONE) ���
201  (ptree_grabWS (Nd (ntm,_) args) =
202   if ntm ��� mkNT sxnt_grabWS then NONE
203   else
204     case args of
205       [w; g] =>
206         do
207           ptree_WS w;
208           ptree_grabWS g;
209           return ()
210         od
211     | _ => NONE)`;
212
213val ptree_normstrchar_def = Define`
214  (ptree_normstrchar (Lf _) = NONE) ���
215  (ptree_normstrchar (Nd (ntm,_) args) =
216   if ntm ��� mkNT sxnt_normstrchar then NONE
217   else
218     case args of
219       [Lf(TK c,_)] => return c
220     | _ => NONE)`;
221
222val ptree_escapablechar_def = Define`
223  (ptree_escapablechar (Lf _) = NONE) ���
224  (ptree_escapablechar (Nd (ntm,_) args) =
225   if ntm ��� mkNT sxnt_escapablechar then NONE
226   else
227     case args of
228       [Lf(TK c,_)] => return c
229     | _ => NONE)`;
230
231val ptree_escapedstrchar_def = Define`
232  (ptree_escapedstrchar (Lf _) = NONE) ���
233  (ptree_escapedstrchar (Nd (ntm,_) args) =
234   if ntm ��� mkNT sxnt_escapedstrchar then NONE
235   else
236     case args of
237       [Lf(TK#"\\",_) ; c] => ptree_escapablechar c
238     | _      => NONE)`;
239
240val ptree_strchar_def = Define`
241  (ptree_strchar (Lf _) = NONE) ���
242  (ptree_strchar (Nd (ntm,_) args) =
243   if ntm ��� mkNT sxnt_strchar then NONE
244   else
245     case args of
246       [c] => ptree_normstrchar c ++ ptree_escapedstrchar c
247     | _   => NONE)`;
248
249val ptree_strcontents_def = Define`
250  (ptree_strcontents (Lf _) = NONE) ���
251  (ptree_strcontents (Nd (ntm,_) args) =
252   if ntm ��� mkNT sxnt_strcontents then NONE
253   else
254     case args of
255       [] => return ""
256     | [sc; ss] =>
257       do
258         c <- ptree_strchar sc;
259         s <- ptree_strcontents ss;
260         return (c::s)
261       od
262     | _ => NONE)`;
263
264val ptree_sexpstr_def = Define`
265  (ptree_sexpstr (Lf _) = NONE) ���
266  (ptree_sexpstr (Nd (ntm,_) args) =
267   if ntm ��� mkNT sxnt_sexpstr then NONE
268   else
269     case args of
270       [Lf(TK#"\"",_) ; s; Lf(TK#"\"",_)] => ptree_strcontents s
271     | _ => NONE)`;
272
273val ptree_first_symchar_def = Define`
274  (ptree_first_symchar (Lf _) = NONE) ���
275  (ptree_first_symchar (Nd (ntm,_) args) =
276   if ntm ��� mkNT sxnt_first_symchar then NONE
277   else
278     case args of
279       [Lf(TK c,_)] => return c
280     | _ => NONE)`;
281
282val ptree_symchar_def = Define`
283  (ptree_symchar (Lf _) = NONE) ���
284  (ptree_symchar (Nd (ntm,_) args) =
285   if ntm ��� mkNT sxnt_symchar then NONE
286   else
287     case args of
288       [Lf(TK c,_)] => return c
289     | _ => NONE)`;
290
291val ptree_symchars_def = Define`
292  (ptree_symchars (Lf _) = NONE) ���
293  (ptree_symchars (Nd (ntm,_) args) =
294   if ntm ��� mkNT sxnt_symchars then NONE
295   else
296     case args of
297       [f;s] =>
298         do
299           c <- ptree_symchar f;
300           cs <- ptree_symchars s;
301           return (c::cs)
302         od
303     | _ => NONE)`;
304
305val ptree_sexpsym_def = Define`
306  (ptree_sexpsym (Lf _) = NONE) ���
307  (ptree_sexpsym (Nd (ntm,_) args) =
308   if ntm ��� mkNT sxnt_sexpsym then NONE
309   else
310     case args of
311       [f;s] =>
312         do
313           c <- ptree_first_symchar f;
314           cs <- ptree_symchars s;
315           return (c::cs)
316         od
317     | _ => NONE)`;
318
319val ptree_sexp_def = Define`
320  (ptree_sexp (Lf _) = NONE) ���
321  (ptree_sexp (Nd (ntm,_) args) =
322   if ntm ��� mkNT sxnt_sexp then NONE
323   else
324     case args of
325         [w; g] => do ptree_grabWS g; ptree_WSsexp w od
326     |   _      => NONE) ���
327  (ptree_WSsexp (Lf _) = NONE) ���
328  (ptree_WSsexp (Nd (ntm,_) args) =
329   if ntm ��� mkNT sxnt_WSsexp then NONE
330   else
331     case args of
332       [g; s] => do ptree_grabWS g; ptree_sexp0 s od
333     | _      => NONE) ���
334  (ptree_sexp0 (Lf _) = NONE) ���
335  (ptree_sexp0 (Nd (ntm,_) args) =
336   if ntm ��� mkNT sxnt_sexp0 then NONE
337   else
338     case args of
339       [s] =>
340         do x <- ptree_sexpsym s; return (SX_SYM x) od ++
341         do x <- ptree_sexpnum s; return (SX_NUM x) od ++
342         do x <- ptree_sexpstr s; return (SX_STR x) od
343     | [Lf (TK#"'",_) ;w] => ptree_WSsexp w
344     | [Lf (TK#"(",_) ; s; g; Lf (TK#")",_) ] =>
345         do
346           ptree_grabWS g;
347           ptree_sexpseq s
348         od
349     | [Lf (TK#"(",_); sa; Lf (TK#".",_) ; sd; Lf (TK#")",_) ] =>
350         do
351           a <- ptree_sexp sa;
352           d <- ptree_sexp sd;
353           return (SX_CONS a d)
354         od
355     | _ => NONE) ���
356  (ptree_sexpseq (Lf _) = NONE) ���
357  (ptree_sexpseq (Nd (ntm,_) args) =
358   if ntm ��� mkNT sxnt_sexpseq then NONE
359   else
360     case args of
361       [] => return nil
362     | [w; s] =>
363         do
364           x <- ptree_WSsexp w;
365           r <- ptree_sexpseq s;
366           return (SX_CONS x r)
367         od
368     | _ => NONE)`;
369
370
371val _ = export_theory()
372