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