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