1open HolKernel Parse boolLib bossLib lcsymtacs;
2
3open simpleSexpTheory pegTheory pegLib
4
5val _ = new_theory "simpleSexpPEG";
6
7val tokeq_def = Define`tokeq t = tok ((=) t) (K (SX_SYM [t]))`
8val grabWS_def = Define`
9  grabWS s = rpt (tok isSpace (K arb_sexp)) (K arb_sexp) ~> s
10`;
11
12val peg0_tokeq = store_thm(
13  "peg0_tokeq[simp]",
14  ``peg0 G (tokeq t) = F``,
15  simp[tokeq_def])
16
17val pnt_def = Define`pnt ntsym = nt (mkNT ntsym) I`
18
19val replace_nil_def= Define`
20  (replace_nil (SX_SYM s) z = if s = "nil" then z else SX_SYM s) ���
21  (replace_nil (SX_CONS x y) z = SX_CONS x (replace_nil y z)) ���
22  (replace_nil x y = x)
23`;
24
25(* have to use these versions of choicel and pegf below because the
26   versions from pegTheory use ARB in their definitions.
27   Logically, the ARBs are harmless, but they completely mess with the
28   CakeML translator.
29*)
30val choicel_def = Define`
31  choicel [] = not (empty arb_sexp) arb_sexp ���
32  choicel (h::t) = choice h (choicel t) (��s. case s of INL x => x | INR y => y)
33`;
34
35val pegf_def = Define`pegf sym f = seq sym (empty arb_sexp) (��l1 l2. f l1)`;
36
37val peg_eval_choicel_NIL = store_thm(
38  "peg_eval_choicel_NIL[simp]",
39  ``peg_eval G (i0, choicel []) x = (x = NONE)``,
40  simp[choicel_def, Once peg_eval_cases]);
41
42val peg_eval_choicel_CONS = store_thm(
43  "peg_eval_choicel_CONS",
44  ``���x. peg_eval G (i0, choicel (h::t)) x ���
45          peg_eval G (i0, h) x ��� x <> NONE ���
46          peg_eval G (i0,h) NONE ��� peg_eval G (i0, choicel t) x``,
47  simp[choicel_def, SimpLHS, Once peg_eval_cases] >>
48  simp[pairTheory.FORALL_PROD, optionTheory.FORALL_OPTION]);
49
50val peg0_choicel = store_thm(
51  "peg0_choicel[simp]",
52  ``(peg0 G (choicel []) = F) ���
53    (peg0 G (choicel (h::t)) ��� peg0 G h ��� pegfail G h ��� peg0 G (choicel t))``,
54  simp[choicel_def])
55
56val peg0_pegf = store_thm(
57  "peg0_pegf[simp]",
58  ``peg0 G (pegf s f) = peg0 G s``,
59  simp[pegf_def])
60
61val sexpPEG_def = zDefine`
62  sexpPEG : (char, sexpNT, sexp) peg = <|
63    start := pnt sxnt_sexp ;
64    rules :=
65    FEMPTY |++
66    [(mkNT sxnt_sexp, pnt sxnt_WSsexp <~ rpt (tok isSpace (K arb_sexp)) (K arb_sexp));
67     (mkNT sxnt_sexp0,
68      choicel [
69        pnt sxnt_sexpnum ;
70        tokeq #"(" ~> pnt sxnt_sexpseq ;
71        tokeq #"\"" ~> pnt sxnt_strcontents <~ tokeq #"\"" ;
72        pegf (tokeq #"'" ~> grabWS (pnt sxnt_sexp0))
73             (��s. ��� SX_SYM "quote"; s���) ;
74        pnt sxnt_sexpsym
75      ]);
76     (mkNT sxnt_sexpseq,
77      choicel [
78        pegf (grabWS (tokeq #")")) (K (SX_SYM "nil"));
79        seq (grabWS (pnt sxnt_sexp0))
80            (seq (rpt (grabWS (pnt sxnt_sexp0))
81                      (FOLDR SX_CONS (SX_SYM "nil")))
82                 (choicel [
83                     pegf (grabWS (tokeq #")")) (K (SX_SYM "nil"));
84                     grabWS (tokeq #".") ~>
85                        grabWS (pnt sxnt_sexp0)
86                     <~ grabWS (tokeq #")")
87                     ])
88                 replace_nil)
89            SX_CONS
90     ]);
91     (mkNT sxnt_WSsexp,
92      rpt (tok isSpace (K arb_sexp)) (K arb_sexp) ~> pnt sxnt_sexp0);
93     (mkNT sxnt_sexpnum,
94        seq (pnt sxnt_digit)
95            (rpt (pnt sxnt_digit)
96                 (UNCURRY SX_CONS o (SX_NUM ## SX_NUM) o
97                  FOLDL (��(l,n) d. (10*l, 10*n + destSXNUM d)) (1,0)))
98            (��s1. (��(l,n). SX_NUM (destSXNUM s1 * l + n))
99                  o (destSXNUM ## destSXNUM) o destSXCONS)) ;
100     (mkNT sxnt_digit, tok isDigit (��(c,l). SX_NUM (ORD c - ORD #"0"))) ;
101     (mkNT sxnt_sexpsym,
102      seq (tok valid_first_symchar (��(c,l). SX_SYM [c]))
103          (rpt (tok valid_symchar (��(c,l). SX_SYM [c]))
104               (SX_SYM o FOLDR (��s a. destSXSYM s ++ a) []))
105          (��s1 s2. SX_SYM (destSXSYM s1 ++ destSXSYM s2)));
106     (mkNT sxnt_strcontents,
107      rpt (pnt sxnt_strchar) (SX_STR o FOLDR (��s a. destSXSYM s ++ a) []));
108     (mkNT sxnt_strchar,
109      choicel [
110        tokeq #"\\" ~> pnt sxnt_escapedstrchar ;
111        pnt sxnt_normstrchar
112      ]);
113     (mkNT sxnt_escapedstrchar, choicel [tokeq #"\\"; tokeq #"\""]);
114     (mkNT sxnt_normstrchar,
115      tok (��c. isPrint c ��� c ��� #"\"" ��� c ��� #"\\") (��(c,l). SX_SYM [c]))
116    ]
117  |>
118`;
119
120val sexpPEG_start = save_thm(
121  "sexpPEG_start[simp]",
122  SIMP_CONV(srw_ss())[sexpPEG_def]``sexpPEG.start``)
123val ds = derive_compset_distincts ``:sexpNT``
124val {lookups,fdom_thm,applieds} = derive_lookup_ths {pegth = sexpPEG_def, ntty = ``:sexpNT``, simp = SIMP_CONV (srw_ss())}
125val sexpPEG_exec_thm = save_thm("sexpPEG_exec_thm",LIST_CONJ(sexpPEG_start::ds::lookups))
126val _ = computeLib.add_persistent_funs["sexpPEG_exec_thm"];
127val _ = save_thm("FDOM_sexpPEG", fdom_thm);
128val _ = save_thm("sexpPEG_applied", LIST_CONJ applieds);
129
130val frange_image = prove(
131  ``FRANGE fm = IMAGE (FAPPLY fm) (FDOM fm)``,
132  simp[finite_mapTheory.FRANGE_DEF, pred_setTheory.EXTENSION] >> metis_tac[]);
133
134val sexpPEG_range =
135    SIMP_CONV (srw_ss())
136              (fdom_thm :: frange_image :: applieds)
137              ``FRANGE sexpPEG.rules``
138
139val wfpeg_rwts = wfpeg_cases
140                   |> ISPEC ``sexpPEG``
141                   |> (fn th => map (fn t => Q.SPEC t th)
142                                    [`seq e1 e2 f`, `choice e1 e2 f`, `tok P f`,
143                                     `any f`, `empty v`, `not e v`, `rpt e f`,
144                                     `choicel []`, `choicel (h::t)`, `tokeq t`,
145                                     `pegf e f`
146                      ])
147                   |> map (CONV_RULE
148                             (RAND_CONV (SIMP_CONV (srw_ss())
149                                [choicel_def, tokeq_def, ignoreL_def,
150                                 ignoreR_def, pegf_def, grabWS_def])))
151
152
153val wfpeg_pnt = wfpeg_cases
154                  |> ISPEC ``sexpPEG``
155                  |> Q.SPEC `pnt n`
156                  |> CONV_RULE (RAND_CONV (SIMP_CONV (srw_ss()) [pnt_def]))
157
158val peg0_rwts = peg0_cases
159                  |> ISPEC ``sexpPEG`` |> CONJUNCTS
160                  |> map (fn th => map (fn t => Q.SPEC t th)
161                                       [`tok P f`, `choice e1 e2 f`, `seq e1 e2 f`,
162                                        `tokeq t`, `empty l`, `not e v`, `rpt e f`])
163                  |> List.concat
164                  |> map (CONV_RULE
165                            (RAND_CONV (SIMP_CONV (srw_ss())
166                                                  [tokeq_def])))
167
168val wfpeg_grabWS =
169  SIMP_CONV (srw_ss()) (grabWS_def::ignoreL_def::wfpeg_rwts @ peg0_rwts)
170                       ``wfpeg sexpPEG (grabWS e)``
171
172
173val pegfail_t = ``pegfail``
174val peg0_rwts = let
175  fun filterthis th = let
176    val c = concl th
177    val (l,r) = dest_eq c
178    val (f,_) = strip_comb l
179  in
180    not (same_const pegfail_t f) orelse is_const r
181  end
182in
183  List.filter filterthis peg0_rwts
184end
185
186val pegnt_case_ths = peg0_cases
187                      |> ISPEC ``sexpPEG`` |> CONJUNCTS
188                      |> map (Q.SPEC `pnt n`)
189                      |> map (CONV_RULE (RAND_CONV (SIMP_CONV (srw_ss()) [pnt_def])))
190
191fun pegnt(t,acc) = let
192  val th =
193      prove(``��peg0 sexpPEG (pnt ^t)``,
194            simp (fdom_thm::choicel_def::ignoreL_def::ignoreR_def::applieds @ pegnt_case_ths) >>
195            simp(peg0_rwts @ acc))
196  val nm = "peg0_" ^ term_to_string t
197  val th' = save_thm(nm, SIMP_RULE bool_ss [pnt_def] th)
198  val _ = export_rewrites [nm]
199in
200  th::acc
201end
202
203val npeg0_rwts =
204    List.foldl pegnt []
205   [``sxnt_symchars``, ``sxnt_symchar``,
206    ``sxnt_strchar``, ``sxnt_sexpsym``, ``sxnt_sexpstr``,
207    ``sxnt_sexpnum``,  ``sxnt_normstrchar``,
208    ``sxnt_grabWS``, ``sxnt_first_symchar``, ``sxnt_escapedstrchar``,
209    ``sxnt_escapablechar``, ``sxnt_digit``,``sxnt_WS``]
210
211val npeg0_sexp0 = Q.prove(
212  `��peg0 sexpPEG (pnt sxnt_sexp0)`,
213  simp pegnt_case_ths >> simp[fdom_thm] >>
214  simp applieds >> simp[ignoreL_def,ignoreR_def] >>
215  simp npeg0_rwts)
216
217val npeg0_WSsexp = Q.prove(
218  `��peg0 sexpPEG (pnt sxnt_WSsexp)`,
219  simp pegnt_case_ths >> simp[fdom_thm] >>
220  simp applieds >> simp[ignoreL_def] >>
221  simp (npeg0_sexp0::peg0_rwts))
222
223val npeg0_rwts = npeg0_WSsexp::npeg0_sexp0::npeg0_rwts
224
225val peg0_grabWS = Q.prove(
226  `peg0 sexpPEG (grabWS e) = peg0 sexpPEG e`,
227  simp(ignoreL_def::grabWS_def::peg0_rwts));
228
229fun wfnt(t,acc) = let
230  val th =
231    prove(``wfpeg sexpPEG (pnt ^t)``,
232          SIMP_TAC (srw_ss())
233                   (applieds @
234                    [wfpeg_pnt, fdom_thm, ignoreL_def, ignoreR_def,
235                     checkAhead_def]) THEN
236          fs(peg0_grabWS :: wfpeg_grabWS :: wfpeg_rwts @ npeg0_rwts @
237             peg0_rwts @ acc))
238in
239  th::acc
240end;
241
242val topo_nts =
243  [``sxnt_sexpsym``,
244   ``sxnt_escapedstrchar``,
245   ``sxnt_normstrchar``,
246   ``sxnt_strchar``,
247   ``sxnt_strcontents``,
248   ``sxnt_digit``,
249   ``sxnt_sexpnum``,
250   ``sxnt_sexp0``,
251   ``sxnt_WSsexp``,
252   ``sxnt_sexpseq``,
253   ``sxnt_sexp``]
254
255val wfpeg_thm = LIST_CONJ (List.foldl wfnt [] topo_nts)
256
257val subexprs_pnt = prove(
258  ``subexprs (pnt n) = {pnt n}``,
259  simp[subexprs_def, pnt_def]);
260
261val Gexprs_sexpPEG = save_thm(
262  "Gexprs_sexpPEG",
263  ``Gexprs sexpPEG``
264    |> SIMP_CONV (srw_ss())
265         [Gexprs_def, subexprs_def,
266          subexprs_pnt, sexpPEG_start, sexpPEG_range,
267          ignoreR_def, ignoreL_def,
268          choicel_def, tokeq_def, pegf_def, grabWS_def,
269          checkAhead_def,
270          pred_setTheory.INSERT_UNION_EQ
271         ])
272
273val wfG_sexpPEG = store_thm(
274  "wfG_sexpPEG",
275  ``wfG sexpPEG``,
276  rw[wfG_def,Gexprs_sexpPEG] >>
277  srw_tac[boolSimps.DNF_ss][] >>
278  simp(wfpeg_thm :: wfpeg_rwts @ npeg0_rwts));
279
280val _ = export_theory();
281