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