1structure pegLib :> pegLib = 2struct 3 4open HolKernel Parse boolLib 5 6fun add_peg_compset cs = 7 (computeLib.add_thms 8 [grammarTheory.isTOK_def 9 ,grammarTheory.language_def 10 ,grammarTheory.derive_def 11 ,grammarTheory.ptree_fringe_def 12 ,grammarTheory.complete_ptree_def 13 ,grammarTheory.ptree_head_def 14 ,grammarTheory.ptree_size_def 15 ,pegTheory.subexprs_def 16 ,pegTheory.wfG_def 17 ,pegTheory.Gexprs_def 18 ,pegexecTheory.poplist_aux_def 19 ,pegexecTheory.poplistval_def 20 ,pegexecTheory.pegparse_def 21 ,pegexecTheory.destResult_def 22 ,pegexecTheory.applykont_thm 23 ,pegexecTheory.peg_exec_thm 24 ] cs; 25 List.app (computeLib.add_datatype_info cs o valOf o TypeBase.fetch) 26 [``:('a,'b)grammar$symbol`` 27 ,``:('a,'b)grammar`` 28 ,``:('a,'b,'locs)parsetree`` 29 ,``:('a,'b,'c)pegsym`` 30 ,``:('a,'b,'c)peg`` 31 ,``:('a,'b,'c)kont`` 32 ,``:('a,'b,'c)evalcase`` 33 ]) 34 35fun derive_compset_distincts ty = 36 let 37 val ax = TypeBase.axiom_of ty 38 val th = Prim_rec.prove_constructors_distinct ax |> hd |> valOf 39 in 40 CONJ th (GSYM th) 41 end 42 43val peg_rules_t = prim_mk_const{Thy = "peg", Name = "peg_rules"} 44 45fun strip_insert t = let 46 open pred_setSyntax 47 fun recurse acc t = 48 case Lib.total dest_insert t of 49 NONE => acc 50 | SOME (e,s) => recurse (e::acc) s 51in 52 recurse [] t 53end 54 55fun derive_lookup_ths {pegth, ntty, simp} = 56 let 57 open finite_mapSyntax pred_setTheory finite_mapTheory 58 val pegc = lhs (concl pegth) 59 val nt_thm = pegexecTheory.peg_nt_thm |> Q.GEN `n` |> Q.GEN `G` |> ISPEC pegc 60 val NT_ty = sumSyntax.mk_sum (ntty, numSyntax.num) 61 val mkNT_t = Term.inst [alpha |-> ntty, beta |-> numSyntax.num] 62 sumSyntax.inl_tm 63 val Grules_t = mk_icomb(peg_rules_t, pegc) 64 val fdomrules_t = mk_fdom Grules_t 65 val fdom_thm = simp[pegth, FUPDATE_LIST] fdomrules_t 66 val cs = strip_insert (rhs (concl fdom_thm)) 67 fun fdom c = 68 AP_TERM (mk_icomb(pred_setSyntax.in_tm, c)) fdom_thm 69 |> CONV_RULE 70 (RAND_CONV 71 (PURE_REWRITE_CONV [IN_INSERT, OR_CLAUSES, REFL_CLAUSE])) 72 val fdoms = map fdom cs 73 fun fapp c = 74 mk_fapply(Grules_t, c) 75 |> simp[pegth, FUPDATE_LIST, FAPPLY_FUPDATE_THM] 76 val fapps = map fapp cs 77 fun final c = CONV_RULE 78 (RAND_CONV 79 (PURE_REWRITE_CONV (COND_CLAUSES :: fdoms @ fapps))) 80 (SPEC c nt_thm) 81 in 82 {lookups = map final cs, fdom_thm = fdom_thm, applieds = fapps} 83 end 84 85 86 87 88end 89