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