1open HolKernel Parse boolLib bossLib
2
3open pegexecTheory
4
5val _ = new_theory "pegSample"
6
7val _ = Hol_datatype`tok = Plus | Times | Number of num | LParen | RParen`
8
9local open stringTheory in end
10
11val _ = Hol_datatype `
12  expr = XN of num
13       | XPlus of expr => expr
14       | XTimes of expr => expr
15       | XList of expr list`;
16
17val ty = ty_antiq ``:(tok, string, expr) pegsym``
18val lift_number_def = Define`
19  lift_number (Number n,l) = XN n
20`;
21
22val nrule = ``tok (��t. case t of Number n => T | _ => F) lift_number : ^ty``
23val paren_rule =
24  ``seq (tok ((=) LParen) (K (XN 0)))
25        (seq (nt (INL "expr") I) (tok ((=) RParen) (K (XN 0))) K)
26        (K I) : ^ty``
27
28val termpair =
29  ``(INL "term" : string inf,
30     choice ^nrule ^paren_rule (\s. case s of INL e => e | INR e => e))``
31
32val leftassoc_def = Define`
33  leftassoc f (XList []) b = b ���
34  leftassoc f (XList (h::t)) b = FOLDL f h (t ++ [b])
35`;
36
37val factorpair = ``(INL "factor" : string inf,
38                    seq (rpt (seq (nt (INL "term") I)
39                                  (tok ((=) Times) (K ARB))
40                                  K)
41                             XList)
42                        (nt (INL "term") I)
43                        (leftassoc XTimes) : ^ty)``
44
45val exprpair = ``(INL "expr" : string inf,
46                  seq (rpt (seq (nt (INL "factor") I)
47                                (tok ((=) Plus) (K ARB))
48                                K)
49                           XList)
50                      (nt (INL "factor") I)
51                      (leftassoc XPlus): ^ty)``
52
53val rules = ``FEMPTY |+ ^exprpair |+ ^factorpair |+ ^termpair``
54
55val G = ``<| start := nt (INL "expr") I; rules := ^rules |>``
56
57val testexp = ``[Number 3; Plus; Number 4; Times; Number 5]``
58
59open lcsymtacs
60val _ = let
61  open computeLib
62in
63  set_skip the_compset ``evalcase_CASE`` (SOME 1);
64  set_skip the_compset ``option_CASE`` (SOME 1);
65  set_skip the_compset ``COND`` (SOME 1)
66end
67
68(* with eval_def directly: 1.155s;
69   with "optimised" tail-recursive form: 0.213s *)
70val result1 = save_thm(
71  "result1",
72  time EVAL ``peg_exec ^G (nt (INL "expr") I)
73                      (map_loc [Number 1; Plus; Number 2; Times; Number 4] 0) []
74                      done failed``)
75
76(* As of 5a18cdc17ff, takes 1.983s (ugh) *)
77val result2 = save_thm(
78  "result2",
79  time EVAL ``peg_exec ^G (nt (INL "expr") I)
80                      (map_loc [Number 1; Plus; Number 2; Times; Number 4;
81                       Times; LParen; Number 3; Plus; Number 1; RParen] 0)
82                      [] done failed``)
83
84val G_def = zDefine`G = <| start := nt (INL "expr") I; rules := ^rules |>`
85
86val Grules = store_thm(
87  "Grules",
88  ``G.rules ' (INL "expr") = ^(#2 (pairSyntax.dest_pair exprpair)) ���
89    G.rules ' (INL "factor") = ^(#2 (pairSyntax.dest_pair factorpair)) ���
90    G.rules ' (INL "term") = ^(#2 (pairSyntax.dest_pair termpair)) ���
91    INL "expr" ��� FDOM G.rules ���
92    INL "term" ��� FDOM G.rules ���
93    INL "factor" ��� FDOM G.rules``,
94  simp[G_def, finite_mapTheory.FAPPLY_FUPDATE_THM]);
95val _ = computeLib.add_persistent_funs ["Grules"]
96
97(* on a machine running PolyML 5.4.1, and where result2 takes 0.084s,
98   the following takes 0.028s
99
100   One further optimisation would be partially evaluate the actual
101   nt values against exec theorem and put the result into the compset
102*)
103val result2' = save_thm(
104  "result2'",
105  time EVAL ``peg_exec G (nt (INL "expr") I)
106                      (map_loc [Number 1; Plus; Number 2; Times; Number 4;
107                       Times; LParen; Number 3; Plus; Number 1; RParen] 0)
108                      [] done failed``)
109
110
111val _ = export_theory()
112
113