1structure PrecAnalysis :> PrecAnalysis = 2struct 3 4open HOLgrammars term_grammar_dtype 5 6type lspec = listspec 7type rel = HOLgrammars.rule_element 8type mlsp = HOLgrammars.mini_lspec 9 10infix |> 11fun (x |> f) = f x 12 13fun listfld_tok ppels = 14 case ppels of 15 [] => raise Fail "No TOK in list field pp-element list" 16 | RE (TOK s) :: _ => s 17 | RE TM :: _ => raise Fail "TM in list field pp-element list" 18 | ListForm _ :: _ => raise Fail "ListForm in list field pp-element list" 19 | _ :: rest => listfld_tok rest 20 21fun listform_left ({leftdelim,...} : lspec) = listfld_tok leftdelim 22fun listform_right ({rightdelim,...} : lspec) = listfld_tok rightdelim 23 24fun rel_equalities rels = 25 let 26 fun recurse rels (A as (lastopt, acc)) = 27 case (lastopt, rels) of 28 (_, []) => acc 29 | (SOME(_, true), TM :: _) => raise Fail "Two TM elements in a row" 30 | (SOME(tk1,false), TM :: rest) => recurse rest (SOME(tk1,true), acc) 31 | (SOME(tk1, tmp), TOK tk2::rest) => 32 recurse rest (SOME(tk2,false), (tk1,tmp,tk2)::acc) 33 | (SOME(tk1, true), ListTM _ :: rest) => 34 raise Fail "rel_equalities: TM before ListTM" 35 | (SOME(tk1, false), ListTM{sep,...} :: TOK tk2 :: rest) => 36 recurse rest (SOME (tk2,false), 37 (tk1,true,sep) :: (sep,true,sep) :: 38 (sep,false,tk2) :: (sep,true,tk2) :: 39 (tk1,true,tk2) :: (tk1,false,tk2) :: acc) 40 | (_, ListTM _ :: ListTM _ :: _) => 41 raise Fail "rel_equalities: two ListTMs in a row" 42 | (_, ListTM _ :: TM :: _) => 43 raise Fail "rel_equalities: ListTM followed by TM" 44 | (_, [ListTM _]) => raise Fail "rel_equalities: last ListTM" 45 | (NONE, TM :: _) => raise Fail "rel_equalities: initial TM" 46 | (NONE, TOK tk :: rest) => recurse rest (SOME(tk,false), acc) 47 | (NONE, ListTM _ :: _) => raise Fail "rel_equalities: initial ListTM" 48 in 49 recurse rels (NONE, []) 50 end 51 52fun ppel_equalities ppels = rel_equalities (term_grammar.rule_elements ppels) 53fun rule_equalities (rr : rule_record) = ppel_equalities (#elements rr) 54 55type rell_transform = rule_element list -> rule_element list 56 57fun mkrels_infix rels = TM :: (rels @ [TM]) 58fun mkrels_suffix rels = TM :: rels 59fun mkrels_prefix rels = rels @ [TM] 60fun mkrels_closefix rels = rels 61 62fun check_for_listreductions check rels = 63 let 64 val rev = List.rev 65 fun recurse A left_opt sep_opt p rels = 66 (* left_opt is candidate left-delimiter, sep_opt candidate separator 67 Invariant: 68 left_opt = SOME l ==> TOK l was seen earlier as candidate leftdelim 69 sep_opt = SOME s ==> 70 ?l. left_opt = SOME l /\ TOK s followed a TM after the l was 71 seen and there have been no other TOKs seen since, and 72 check(l,s) = NONE 73 (p <=> last thing seen was TM) 74 *) 75 case rels of 76 [] => rev A 77 | [TM] => rev A 78 | [TOK tk1] => (* tk1 may end a list *) 79 let 80 in 81 case sep_opt of 82 SOME s => 83 (case check(s, tk1) of 84 NONE => 85 (case check(valOf left_opt, tk1) of 86 NONE => rev A 87 | SOME lp => 88 rev ((valOf left_opt, tk1, lp) :: A)) 89 | SOME lp => rev ((s,tk1,lp)::A)) 90 | NONE => 91 (case left_opt of 92 NONE => rev A 93 | SOME l => (case check(l,tk1) of 94 NONE => rev A 95 | SOME lp => rev ((l,tk1,lp) :: A))) 96 end 97 | TOK tk1 :: TM :: rest => 98 let 99 in 100 case sep_opt of 101 SOME s => 102 (if s = tk1 andalso p then 103 recurse A left_opt sep_opt true rest 104 else 105 case check (valOf left_opt, tk1) of 106 NONE => 107 (case check (s, tk1) of 108 NONE => 109 if p then 110 recurse A (SOME s) (SOME tk1) true rest 111 else 112 recurse A (SOME tk1) NONE true rest 113 | SOME lp => 114 recurse ((s,tk1,lp)::A) (SOME tk1) NONE 115 true rest) 116 | SOME lp => recurse ((valOf left_opt, tk1, lp)::A) 117 (SOME tk1) NONE true rest) 118 | NONE => 119 (case left_opt of 120 NONE => recurse A (SOME tk1) NONE true rest 121 | SOME l => 122 (case check (l, tk1) of 123 NONE => if p then 124 recurse A left_opt (SOME tk1) true rest 125 else 126 recurse A (SOME tk1) NONE true rest 127 | SOME lp => 128 recurse ((l,tk1,lp)::A) (SOME tk1) NONE 129 true rest)) 130 end 131 | TOK tk1 :: TOK tk2 :: rest => 132 (case sep_opt of 133 SOME s => 134 if s = tk1 andalso p then 135 case check (valOf left_opt, tk2) of 136 NONE => 137 (case check(tk1,tk2) of 138 NONE => recurse A (SOME tk2) NONE false rest 139 | SOME lp => 140 recurse ((tk1,tk2,lp)::A) (SOME tk2) NONE 141 false rest) 142 | SOME lp => 143 recurse ((valOf left_opt, tk2, lp)::A) 144 (SOME tk2) NONE false rest 145 else 146 (case check(s,tk1) of 147 NONE => 148 if p then 149 case check(s,tk2) of 150 NONE => 151 (case check (tk1,tk2) of 152 NONE => recurse A (SOME tk2) NONE false rest 153 | SOME lp => 154 recurse ((tk1,tk2,lp)::A) (SOME tk2) 155 NONE false rest) 156 | SOME lp => 157 (* s is the left, tk1 is the sep, tk2 right *) 158 recurse ((s,tk2,lp)::A) (SOME tk2) NONE false 159 rest 160 else 161 (case check (tk1,tk2) of 162 NONE => recurse A (SOME tk2) NONE false rest 163 | SOME lp => 164 recurse ((tk1,tk2,lp)::A) (SOME tk2) 165 NONE false rest) 166 | SOME lp => 167 recurse ((s,tk1,lp)::A) (SOME tk1) NONE 168 false (TOK tk2 :: rest)) 169 | NONE => (* no sep *) 170 let 171 val f = case check(tk1,tk2) of 172 NONE => (fn A => A) 173 | SOME lp => (fn A => (tk1,tk2,lp) :: A) 174 in 175 case left_opt of 176 NONE => recurse (f A) (SOME tk2) NONE false rest 177 | SOME l => 178 (case check(l,tk1) of 179 NONE => 180 if p then (* tk1 might be sep and tk2 rdelim *) 181 case check(l,tk2) of 182 NONE => 183 recurse (f A) (SOME tk2) NONE false rest 184 | SOME lp => 185 recurse ((l,tk2,lp)::A) (SOME tk2) NONE false 186 rest 187 else 188 recurse (f A) (SOME tk2) NONE false rest 189 | SOME lp => 190 recurse (f ((l,tk1,lp)::A)) (SOME tk2) NONE false 191 rest) 192 end) 193 | TM :: rest => (* p must be false as two TMs in a row is impossible *) 194 recurse A left_opt sep_opt true rest 195 | _ => raise Fail "check_for_listreductions: impossible rhs" 196 in 197 recurse [] NONE NONE false rels 198 end 199 200fun rev2 (l1, l2, c) = (List.rev l1, List.rev l2, c) 201fun c1 x (l1, l2, c) = (x::l1, l2, c) 202fun c2 x (l1, l2, c) = (l1, x::l2, c) 203fun inc (l1, l2, c) = (l1, l2, c + 1) 204fun ap1 f (x,y,z) = (f x, y, z) 205 206fun remove_listrels lsps rels = 207 let 208 fun recurse (A as (outrels, listbits, tmc)) lsps rels = 209 case lsps of 210 [] => ap1 (fn l => l @ rels) (rev2 A) 211 | (ld,rd,lsp:mini_lspec)::more_lsps => 212 (case rels of 213 [] => rev2 A 214 | TM :: rrest => recurse (A |> inc |> c1 TM) lsps rrest 215 | (rel as TOK tk) :: more_rels => 216 if tk <> ld then recurse (c1 rel A) lsps more_rels 217 else (* tk = ld *) 218 let 219 val {sep,...} = lsp 220 in 221 case more_rels of 222 TOK tk' :: later_rels => 223 if tk' = rd then 224 recurse 225 (A |> c1 rel |> c1 TM |> c2 (lsp,[])) 226 more_lsps 227 more_rels 228 else 229 (* probably an error; can't be sep as no TM first*) 230 recurse (c1 rel A) more_lsps more_rels 231 | TM :: (inter_rels as (TOK sep' :: later_rels)) => 232 if sep = sep' then 233 consume_list 234 (A |> c1 rel |> c1 TM |> inc) (lsp, [#3 A]) rd 235 more_lsps later_rels 236 else if sep' = rd then 237 recurse 238 (A |> c1 rel |> c1 TM |> inc |> c2 (lsp, [#3 A])) 239 more_lsps inter_rels 240 else (* probably an error *) 241 recurse (A |> c1 rel |> c1 TM |> inc) 242 lsps 243 inter_rels 244 | _ => raise Fail "remove_listrels: malformed RHS" 245 end 246 | _ => raise Fail "remove_listrels: malformed RHS(2)") 247 and consume_list A (curr as (lsp, idxs)) rdelim lsps rels = 248 case rels of 249 [] => (* probably an error *) rev2 (A |> c2 (lsp, List.rev idxs)) 250 | TM :: rest => consume_list (A |> inc) (lsp, #3 A :: idxs) 251 rdelim lsps rest 252 | TOK t :: rest => 253 if t = rdelim then 254 recurse (A |> c2 (lsp, List.rev idxs)) lsps rels 255 else (* it's assumed to be the sep *) 256 consume_list A curr rdelim lsps rest 257 | _ => raise Fail "consume_list: malformed RHS" 258 val (x, y, _) = recurse ([], [], 0) lsps rels 259 in 260 (x,y) 261 end 262 263end 264