1open HolKernel Parse boolLib bossLib;
2
3open optionTheory listTheory
4
5open lcsymtacs
6
7(* simple (infixes + function application via juxtaposition) precedence
8   parser
9
10   This is all that is needed to handle the precedence parsing done by
11   SML, where one can assume that handling of parentheses has already
12   been done, and there are only binary infixes to worry about.
13
14*)
15
16val _ = new_theory "precparser";
17
18val _ = ParseExtras.tight_equality()
19
20val bool_case_eq = prove_case_eq_thm{
21  case_def= TypeBase.case_def_of ``:bool``,
22  nchotomy = TypeBase.nchotomy_of ``:bool``
23};
24
25val option_case_eq = prove_case_eq_thm{
26  case_def= option_case_def,
27  nchotomy = option_CASES
28               |> ONCE_REWRITE_RULE [DISJ_COMM]
29};
30
31val sum_case_eq = prove_case_eq_thm {
32  case_def = sumTheory.sum_case_def,
33  nchotomy = sumTheory.sum_CASES
34};
35
36val list_case_eq = prove_case_eq_thm{
37  case_def = listTheory.list_case_def,
38  nchotomy = listTheory.list_CASES
39};
40
41
42val _ = Datatype`tokrel = Reduce | Shift`
43
44val tokrel_case_eq = prove_case_eq_thm {
45  case_def = theorem "tokrel_case_def",
46  nchotomy = theorem "tokrel_nchotomy"
47};
48
49val _ = Datatype`
50  pMachine = <| rules : 'tok # 'tok -> tokrel option ; (* stk tok , strm tok *)
51                reduce : 'trm -> 'tok -> 'trm -> 'trm option ;
52                lift : 'tok -> 'trm ;
53                isOp : 'tok -> bool ;
54                mkApp : 'trm -> 'trm -> 'trm option |>
55`;
56
57
58(* stack is list of tokens + terms *)
59val precparse1_def = Define`
60  precparse1 pM (stk, strm) =
61     case strm of
62         [] =>
63           (case stk of
64               INR tm2 :: INL opn :: INR tm1 :: rest =>
65                 OPTION_MAP (��r. (INR r :: rest, [])) (pM.reduce tm1 opn tm2)
66             | _ => NONE)
67       | tok :: strm_rest =>
68         if pM.isOp tok then
69           case stk of
70               INR tm2 :: INL opn :: INR tm1 :: stk_rest =>
71               (case pM.rules (opn, tok) of
72                    SOME Shift => SOME(INL tok :: stk, strm_rest)
73                  | SOME Reduce =>
74                      OPTION_MAP (��r. (INR r :: stk_rest, tok :: strm_rest))
75                                 (pM.reduce tm1 opn tm2)
76                  | NONE => NONE)
77             | [INR tm] => SOME([INL tok; INR tm], strm_rest)
78             | _ => NONE
79         else
80           case stk of
81               [] => SOME([INR (pM.lift tok)], strm_rest)
82             | INR ftm :: stk_rest =>
83                 OPTION_MAP (��r. (INR r :: stk_rest, strm_rest))
84                            (pM.mkApp ftm (pM.lift tok))
85             | INL _ :: _ => SOME(INR (pM.lift tok) :: stk, strm_rest)
86`;
87
88val wfStk_def = Define`
89  (wfStk [] ��� T) ���
90  (wfStk [INR _] ��� T) ���
91  (wfStk [INL _] ��� F) ���
92  (wfStk (INL _ :: INR tm :: rest) ��� wfStk (INR tm :: rest)) ���
93  (wfStk (INR _ :: INL t :: rest) ��� wfStk (INL t :: rest)) ���
94  (wfStk _ ��� F)
95`;
96val _ = export_rewrites ["wfStk_def"]
97
98val wfStk_ignores_hdvalues = store_thm(
99  "wfStk_ignores_hdvalues[simp]",
100  ``wfStk (INL l::t) = wfStk (INL ARB :: t) ���
101    wfStk (INR r::t) = wfStk (INR ARB :: t)``,
102  Cases_on `t` >> simp[] >> rename1 `wfStk (INL ARB :: el2 :: tl)` >>
103  Cases_on `el2` >> simp[]);
104
105val precparse1_preserves_wfStk = store_thm(
106  "precparse1_preserves_wfStk",
107  ``wfStk stk0 ��� precparse1 pM (stk0, strm0) = SOME (stk, strm) ���
108    wfStk stk``,
109  Cases_on `strm0` >> Cases_on `stk0` >>
110  dsimp[precparse1_def, list_case_eq, sum_case_eq, bool_case_eq,
111        option_case_eq, tokrel_case_eq] >>
112  rw[] >> fs[]);
113
114val LT_SUC = store_thm(
115  "LT_SUC",
116  ``x < SUC y ��� (x = 0) ��� ���m. x = SUC m ��� m < y``,
117  Cases_on `x` >> simp[]);
118
119val wfStk_ALT = store_thm(
120  "wfStk_ALT",
121  ``wfStk l ��� (l ��� [] ��� ���opn. LAST l ��� INL opn) ���
122              (���i. i + 1 < LENGTH l ��� ISR (EL i l) ��� ISR (EL (i + 1) l))``,
123  Induct_on `l` >> simp[] >> Cases >> simp[] >> rename1 `wfStk (_ :: stk)` >>
124  Cases_on `stk` >> simp[] >> fs[] >> rename1 `wfStk (_ :: el2 :: stk)` >>
125  Cases_on `el2` >> simp[] >- (disj2_tac >> qexists_tac `0` >> simp[]) >>
126  simp[DECIDE ``x + 1 < SUC y ��� x < y``] >>
127  dsimp[LT_SUC, DECIDE ``x + 1 = SUC x``])
128
129val precparse1_reduces = store_thm(
130  "precparse1_reduces",
131  ``precparse1 pM (stk0,strm0) = SOME (stk,strm) ���
132      LENGTH strm < LENGTH strm0 ��� strm = strm0 ��� LENGTH stk < LENGTH stk0``,
133  Cases_on `strm0` >> Cases_on `stk0` >>
134  dsimp[precparse1_def, list_case_eq, sum_case_eq, bool_case_eq,
135        option_case_eq, tokrel_case_eq] >> rw[] >> simp[]);
136
137val isFinal_def = Define`
138  (isFinal ([INR _],[]) ��� T) ���
139  (isFinal _ ��� F)
140`;
141val _ = export_rewrites ["isFinal_def"]
142
143
144val precparse_def = tDefine "precparse" `
145  precparse pM (stk0,strm0) =
146     if isFinal (stk0,strm0) then SOME (OUTR (HD stk0))
147     else
148       case precparse1 pM (stk0, strm0) of
149           NONE => NONE
150         | SOME (stk, strm) => precparse pM (stk, strm)
151` (WF_REL_TAC
152    `inv_image (measure LENGTH LEX measure LENGTH) (��(_,y,z). (z,y))` >>
153   metis_tac[precparse1_reduces]);
154
155(* test case
156local open stringTheory finite_mapTheory in end
157val _ = Datatype`ast = Plus ast ast | Times ast ast | App ast ast | C char`
158val fm = ``FLOOKUP (FEMPTY |+ ((#"+",#"*"), Shift) |+ ((#"*",#"+"), Reduce)
159                      |+ ((#"+",#"+"), Reduce) |+ ((#"*",#"*"), Reduce))``
160
161val isOp = ``��c. c = #"*" ��� c = #"+"``
162val reduce = ``��tm1 c tm2. if c = #"*" then SOME (Times tm1 tm2)
163                           else SOME (Plus tm1 tm2)``
164val lift = ``C``
165
166val m = ``<| rules :=  ^fm ;
167             reduce := ^reduce ;
168             lift := C;
169             isOp := ^isOp;
170             mkApp := ��t1 t2. SOME (App t1 t2) |>``
171
172EVAL ``precparse ^m ([],"3*fx*7+9")``;
173EVAL ``precparse ^m ([],"3+fx*7+9")``;
174EVAL ``precparse ^m ([],"fxy")``;
175EVAL ``precparse ^m ([],"x*2")``;
176EVAL ``precparse ^m ([],"3++7")`` (* fails *);
177*)
178
179val _ = export_theory();
180