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