1open HolKernel Parse boolLib bossLib
2
3open boolSimps
4
5open pegTheory locationTheory
6
7open rich_listTheory;
8
9val _ = new_theory "pegexec"
10
11val _ = Hol_datatype`
12  kont =
13    ksym of ('atok,'bnt,'cvalue) pegsym => kont => kont
14  | appf1 of ('cvalue -> 'cvalue) => kont
15  | appf2 of ('cvalue -> 'cvalue -> 'cvalue) => kont
16  | returnTo of ('atok # locs) list => 'cvalue option list => kont
17  | poplist of ('cvalue list -> 'cvalue) => kont
18  | listsym of ('atok,'bnt,'cvalue) pegsym =>
19               ('cvalue list -> 'cvalue) =>
20               kont
21  | done
22  | failed
23`
24
25val poplist_aux_def = Define`
26  poplist_aux acc (SOME h::t) = poplist_aux (h::acc) t ���
27  poplist_aux acc (NONE::t) = (acc,t) ���
28  poplist_aux acc [] = (acc,[]) (* should never happen *)
29`;
30
31val poplistval_def = Define`
32  poplistval f l = let (values,rest) = poplist_aux [] l
33                   in
34                     SOME(f values) :: rest
35`;
36
37val _ = Hol_datatype `
38  evalcase = EV of ('atok,'bnt,'cvalue) pegsym =>
39                   ('atok # locs) list => 'cvalue option list =>
40                   ('atok,'bnt,'cvalue) kont =>
41                   ('atok,'bnt,'cvalue) kont
42           | AP of ('atok,'bnt,'cvalue) kont =>
43                   ('atok # locs) list => 'cvalue option list
44           | Result of (('atok # locs) list # 'cvalue) option
45           | Looped
46`;
47
48val coreloop_def = zDefine`
49  coreloop G =
50   OWHILE (��s. case s of Result _ => F
51                       | _ => T)
52          (��s. case s of
53                   EV (empty v) i r k fk => AP k i (SOME v::r)
54                 | EV (any tf) i r k fk =>
55                   (case i of
56                        [] => AP fk i r
57                      | h::t => AP k t (SOME (tf h) :: r))
58                 | EV (tok P tf2) i r k fk =>
59                   (case i of
60                        [] => AP fk i r
61                      | h::t => if P (FST h) then AP k t (SOME (tf2 h)::r)
62                                else AP fk i r)
63                 | EV (nt n tf3) i r k fk =>
64                   if n ��� FDOM G.rules then
65                     EV (G.rules ' n) i r (appf1 tf3 k) fk
66                   else
67                     Result NONE
68                 | EV (seq e1 e2 f) i r k fk =>
69                     EV e1 i r
70                        (ksym e2 (appf2 f k) (returnTo i r fk))
71                        fk
72                 | EV (choice e1 e2 cf) i r k fk =>
73                     EV e1 i r
74                        (appf1 (cf o INL) k)
75                        (returnTo i r (ksym e2 (appf1 (cf o INR) k) fk))
76                 | EV (rpt e lf) i r k fk =>
77                     EV e i (NONE::r) (listsym e lf k) (poplist lf k)
78                 | EV (not e v) i r k fk =>
79                     EV e i r (returnTo i r fk) (returnTo i (SOME v::r) k)
80                 | AP done i r => Result(case r of
81                                             [] => NONE
82                                           | NONE::t => NONE
83                                           | SOME rv::t => SOME(i, rv))
84                 | AP failed i r => Result NONE
85                 | AP (ksym e k fk) i r => EV e i r k fk
86                 | AP (appf1 f1 k) i (SOME v :: r) => AP k i (SOME (f1 v) :: r)
87                 | AP (appf1 _ _) _ _ => Looped
88                 | AP (appf2 f2 k) i (SOME v1 :: SOME v2 :: r) =>
89                     AP k i (SOME (f2 v2 v1) :: r)
90                 | AP (appf2 _ _) _ _ => Looped
91                 | AP (returnTo i r k) i' r' => AP k i r
92                 | AP (listsym e f k) i r =>
93                     EV e i r (listsym e f k) (poplist f k)
94                 | AP (poplist f k) i r => AP k i (poplistval f r)
95                 | Result r => Result r
96                 | Looped => Looped)
97`;
98
99
100val peg_exec_def = zDefine`
101  peg_exec (G:('atok,'bnt,'cvalue)peg) e i r k fk =
102    case coreloop G (EV e i r k fk) of
103        SOME r => r
104      | NONE => Looped
105`
106
107val applykont_def = zDefine`
108  applykont G k i r = case coreloop G (AP k i r) of
109                          SOME r => r
110                        | NONE => Looped
111`
112
113val coreloop_result = store_thm(
114  "coreloop_result",
115  ``coreloop G (Result x) = SOME (Result x)``,
116  simp[coreloop_def, Once whileTheory.OWHILE_THM]);
117
118fun inst_thm def (qs,ths) =
119    def |> SIMP_RULE (srw_ss()) [Once whileTheory.OWHILE_THM, coreloop_def]
120        |> SPEC_ALL
121        |> Q.INST qs
122        |> SIMP_RULE (srw_ss()) []
123        |> SIMP_RULE bool_ss (GSYM peg_exec_def :: GSYM coreloop_def ::
124                              GSYM applykont_def :: coreloop_result ::
125                              optionTheory.option_case_def :: ths)
126
127val peg_exec_thm = inst_thm peg_exec_def
128
129val option_case_COND = prove(
130  ``option_CASE (if P then Q else R) n s =
131    if P then option_CASE Q n s else option_CASE R n s``,
132  SRW_TAC [][]);
133
134val better_peg_execs =
135    map peg_exec_thm [([`e` |-> `empty v`], []),
136                  ([`e` |-> `tok P f`, `i` |-> `[]`], []),
137                  ([`e` |-> `tok P f`, `i` |-> `x::xs`],
138                   [Once COND_RAND, option_case_COND]),
139                  ([`e` |-> `any f`, `i` |-> `[]`], []),
140                  ([`e` |-> `any f`, `i` |-> `x::xs`], []),
141                  ([`e` |-> `seq e1 e2 sf`], []),
142                  ([`e` |-> `choice e1 e2 cf`], []),
143                  ([`e` |-> `not e v`], []),
144                  ([`e` |-> `rpt e lf`], [])]
145
146val better_apply =
147    map (inst_thm applykont_def)
148        [([`k` |-> `ksym e k fk`], []),
149         ([`k` |-> `appf1 f k`, `r` |-> `SOME v::r`], []),
150         ([`k` |-> `appf2 f k`, `r` |-> `SOME v1::SOME v2::r`], []),
151         ([`k` |-> `returnTo i' r' k`], []),
152         ([`k` |-> `done`], []),
153         ([`k` |-> `failed`], []),
154         ([`k` |-> `poplist f k`], []),
155         ([`k` |-> `listsym e f k`], [])]
156
157val peg_nt_thm = save_thm(
158  "peg_nt_thm",
159  peg_exec_thm ([`e` |-> `nt n nfn`], [Once COND_RAND, option_case_COND]))
160
161val peg_exec_thm = save_thm("peg_exec_thm", LIST_CONJ better_peg_execs);
162
163val applykont_thm = save_thm("applykont_thm", LIST_CONJ better_apply);
164
165val _ = computeLib.add_persistent_funs ["peg_exec_thm", "applykont_thm"]
166
167val _ = app (fn s => ignore (remove_ovl_mapping s {Thy = "pegexec", Name = s}))
168            ["AP", "EV"]
169
170val exec_correct0 = prove(
171  ``(���i e r. peg_eval G (i,e) r ���
172             (���j v k fk stk.
173                r = SOME(j,v) ���
174                peg_exec G e i stk k fk = applykont G k j (SOME v :: stk)) ���
175             (���k fk stk.
176                r = NONE ��� peg_exec G e i stk k fk = applykont G fk i stk)) ���
177    (���i e j vlist.
178      peg_eval_list G (i,e) (j,vlist) ���
179      ���f k stk vs.
180          peg_exec G e i (MAP SOME vs ++ (NONE::stk))
181                     (listsym e f k)
182                     (poplist f k) =
183          applykont G k j (SOME (f (REVERSE vs ++ vlist)) :: stk))``,
184  ho_match_mp_tac peg_eval_strongind' >>
185  simp[peg_exec_thm, peg_nt_thm, applykont_thm] >>
186  rpt conj_tac
187  >- ((* rpt - no elements succeed *)
188      map_every qx_gen_tac [`e`, `f`, `i`, `j`, `vlist`] >> strip_tac >>
189      map_every qx_gen_tac [`k`, `stk`] >>
190      first_x_assum (qspecl_then [`f`, `k`, `stk`, `[]`] mp_tac) >>
191      simp[])
192  >- ((* poplistval works *)
193      rpt strip_tac >> rpt AP_TERM_TAC >> rpt (pop_assum (K ALL_TAC)) >>
194      simp[poplistval_def] >>
195      qmatch_abbrev_tac `
196        (��(values,rest). SOME (f values)::rest)
197        (poplist_aux [] (MAP SOME vs ++ [NONE] ++ stk)) =
198        SOME (f (REVERSE vs))::stk` >>
199      qsuff_tac `���a. poplist_aux a (MAP SOME vs ++ [NONE] ++ stk) =
200                     (REVERSE vs ++ a, stk)` >- simp[] >>
201      Induct_on `vs` >> simp[poplist_aux_def])
202  >- ((* rpt - some elements succeed *)
203      map_every qx_gen_tac [`e`, `i0`, `i1`, `j`, `v`, `vs`] >> strip_tac >>
204      map_every qx_gen_tac [`f`, `k`, `stk`, `vs'`] >>
205      first_x_assum (qspecl_then [`f`, `k`, `stk`, `v::vs'`] mp_tac) >>
206      simp[] >>
207      simp_tac bool_ss [GSYM listTheory.APPEND_ASSOC, listTheory.APPEND]))
208
209val exec_correct = save_thm(
210  "exec_correct",
211  exec_correct0 |> SIMP_RULE (srw_ss() ++ DNF_ss) [])
212
213val pegexec_succeeds = save_thm(
214  "pegexec_succeeds",
215  exec_correct |> CONJUNCTS |> hd |> SPEC_ALL
216               |> Q.INST [`k` |-> `done`, `fk` |-> `failed`, `stk` |-> `[]`]
217               |> SIMP_RULE (srw_ss()) [applykont_thm])
218
219val pegexec_fails = save_thm(
220  "pegexec_fails",
221  exec_correct |> CONJUNCTS |> tl |> hd |> SPEC_ALL
222               |> Q.INST [`k` |-> `done`, `fk` |-> `failed`, `stk` |-> `[]`]
223               |> SIMP_RULE (srw_ss()) [applykont_thm])
224
225val pair_CASES = pairTheory.pair_CASES
226val option_CASES = optionTheory.option_nchotomy
227val list_CASES = listTheory.list_CASES
228
229val pegexec = store_thm(
230  "pegexec",
231  ``peg_eval G (s,e) r ��� peg_exec G e s [] done failed = Result r``,
232  metis_tac [option_CASES, pair_CASES, pegexec_fails, pegexec_succeeds]);
233
234val peg_eval_executed = store_thm(
235  "peg_eval_executed",
236  ``wfG G ��� e ��� Gexprs G ���
237    (peg_eval G (s,e) r ��� peg_exec G e s [] done failed = Result r)``,
238  strip_tac >> eq_tac
239  >- (`r = NONE ��� ���s' v. r = SOME (s',v)`
240        by metis_tac[option_CASES, pair_CASES] >>
241      simp[pegexec_fails, pegexec_succeeds]) >>
242  strip_tac >>
243  `���r'. peg_eval G (s,e) r'` by metis_tac[peg_eval_total] >>
244  first_assum (assume_tac o MATCH_MP (CONJUNCT1 peg_deterministic)) >>
245  simp[] >> first_x_assum (assume_tac o MATCH_MP pegexec) >> fs[]);
246
247val destResult_def = Define`destResult (Result r) = r`
248val _ = export_rewrites ["destResult_def"]
249
250val pegparse_def = Define`
251  pegparse G s =
252    if wfG G then destResult (peg_exec G G.start s [] done failed)
253    else NONE
254`;
255
256val pegparse_eq_SOME = store_thm(
257  "pegparse_eq_SOME",
258  ``pegparse G s = SOME (s',v) ��� wfG G ��� peg_eval G (s,G.start) (SOME(s',v))``,
259  Tactical.REVERSE (Cases_on `wfG G`) >- simp[pegparse_def] >>
260  `���r. peg_eval G (s,G.start) r`
261    by metis_tac [peg_eval_total, start_IN_Gexprs] >>
262  first_assum (assume_tac o MATCH_MP (CONJUNCT1 peg_deterministic)) >>
263  simp[] >>
264  `r = NONE ��� ���s2 v2. r = SOME (s2,v2)` by metis_tac [option_CASES, pair_CASES]
265  >- rw[pegparse_def, pegexec_fails] >>
266  rw[pegparse_def] >> first_x_assum (assume_tac o MATCH_MP pegexec_succeeds) >>
267  simp[] >> metis_tac[]);
268
269val pegparse_eq_NONE = store_thm(
270  "pegparse_eq_NONE",
271  ``pegparse G s = NONE ��� ��wfG G ��� peg_eval G (s,G.start) NONE``,
272  Cases_on `wfG G` >> simp[pegparse_def] >>
273  `���r. peg_eval G (s,G.start) r`
274    by metis_tac [peg_eval_total, start_IN_Gexprs] >>
275  first_assum (assume_tac o MATCH_MP (CONJUNCT1 peg_deterministic)) >>
276  simp[] >>
277  `r = NONE ��� ���s2 v2. r = SOME (s2,v2)` by metis_tac [option_CASES, pair_CASES]
278  >- rw[pegexec_fails] >>
279  rw[] >> first_x_assum (assume_tac o MATCH_MP pegexec_succeeds) >>
280  simp[]);
281
282val peg_exec_total = store_thm(
283  "peg_exec_total",
284  ``wfG G ==> ���r. peg_exec G G.start i [] done failed = Result r``,
285  strip_tac >>
286  `���pr. peg_eval G (i, G.start) pr` by simp[peg_eval_total, start_IN_Gexprs] >>
287  pop_assum mp_tac >> simp[peg_eval_executed, start_IN_Gexprs]);
288
289val option_case_EQ = prove(
290  ``option_CASE x n s = v ��� x = NONE ��� n = v ��� ���v0. x = SOME v0 ��� v = s v0``,
291  Cases_on `x` >> simp[] >> metis_tac[]);
292
293(*
294   |- wfG G ���
295      ���r.
296        coreloop G (pegexec$EV G.start i [] done failed) = SOME (Result r)
297*)
298val coreloop_total = save_thm(
299  "coreloop_total",
300  peg_exec_total |> SIMP_RULE (srw_ss()) [peg_exec_def, option_case_EQ])
301
302
303val _ = export_theory()
304
305