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