1open HolKernel Parse boolLib bossLib; 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