1structure parsePMATCH :> parsePMATCH = 2struct 3 4open Lib HolKernel Parse term_grammar 5 6fun case_element s (e : pp_element) = 7 case e of 8 RE (TOK s') => s = s' 9 | PPBlock(els,_) => case_elements s els 10 | _ => false 11and case_elements s (els : pp_element list) = List.exists (case_element s) els 12 13fun case_rulerecord s fixity (rr : rule_record, acc) = 14 let 15 val {block_style,elements,paren_style,term_name,...} = rr 16 in 17 if case_elements s elements then 18 {block_style = block_style, fixity = fixity, 19 paren_style = paren_style, pp_elements = elements, 20 term_name = term_name} :: acc 21 else acc 22 end 23 24type add_record = { block_style : PhraseBlockStyle * block_info, 25 fixity : term_grammar.fixity, 26 paren_style : ParenStyle, 27 pp_elements : pp_element list, 28 term_name : string } 29fun ar_elements_fupd 30 f 31 ({block_style,fixity,paren_style,pp_elements,term_name} : add_record) = 32 { block_style = block_style, fixity = fixity, paren_style = paren_style, 33 pp_elements = f pp_elements, term_name = term_name } 34fun ar_name_fupd 35 (f : string -> string) 36 ({block_style,fixity,paren_style,pp_elements,term_name} : add_record) = 37 { block_style = block_style, fixity = fixity, paren_style = paren_style, 38 pp_elements = pp_elements, term_name = f term_name } 39 40fun case_rules s ((precopt, r : grammar_rule),acc) : add_record list 41 = 42 case (precopt, r) of 43 (_, CLOSEFIX rrs) => 44 List.foldl (case_rulerecord s Closefix) acc rrs 45 | (SOME prec, INFIX (STD_infix (rrs, ass))) => 46 List.foldl (case_rulerecord s (Infix(ass,prec))) acc rrs 47 | (SOME prec, PREFIX (STD_prefix rrs)) => 48 List.foldl (case_rulerecord s (Prefix prec)) acc rrs 49 | (SOME prec, SUFFIX (STD_suffix rrs)) => 50 List.foldl (case_rulerecord s (Suffix prec)) acc rrs 51 | _ => acc 52 53fun grammar_tok_rules tok G = List.foldl (case_rules tok) [] (rules G) 54 55fun map_tok_element f e = 56 case e of 57 RE (TOK s) => RE (TOK (f s)) 58 | PPBlock(els, bi) => PPBlock(map_tok_elements f els, bi) 59 | _ => e 60and map_tok_elements f els = map (map_tok_element f) els 61 62fun map_tok_add_record f = ar_elements_fupd (map_tok_elements f) 63 64val PMATCH_case_special = GrammarSpecials.mk_case_special "PMATCH" 65val PMATCH_endbinding = 66 GrammarSpecials.mk_fakeconst_name {fake = ".|", 67 original = SOME{Thy = "patternMatches", 68 Name = "endbinding"}} 69val PMATCH_when = 70 GrammarSpecials.mk_fakeconst_name {fake = "when", 71 original = SOME{Thy = "patternMatches", 72 Name = "when"}} 73 74val endbinding_ar = {block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 75 fixity = Infix(NONASSOC, 13), 76 paren_style = OnlyIfNecessary, 77 pp_elements = [RE (TOK ".|")], 78 term_name = PMATCH_endbinding} 79val when_ar = {block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 80 fixity = Infix(NONASSOC, 14), 81 paren_style = OnlyIfNecessary, 82 pp_elements = [RE (TOK "when")], 83 term_name = PMATCH_when} 84 85fun mk_dtcase ar = map_tok_add_record (fn "case" => "dtcase" | s => s) ar 86fun mk_pmcase ar = ar_name_fupd (K PMATCH_case_special) ar 87 88 89(* ---------------------------------------------------------------------- 90 pmatch absyn to preterm-in-env conversion 91 ---------------------------------------------------------------------- *) 92 93open Absyn Parse_support Parse_supportENV 94 95fun strip_casesplit a = 96 let 97 fun recurse acc a = 98 case a of 99 APP(_, APP(_, QIDENT(_, "bool", csplit), a1), a2) => 100 if csplit = GrammarSpecials.case_split_special then 101 recurse (recurse acc a2) a1 102 else 103 a::acc 104 | _ => a::acc 105 in 106 recurse [] a 107 end 108 109val noloc = locn.Loc_None 110val cons_pt = Parse_support.make_qconst noloc ("list", "CONS") 111val nil_pt = Parse_support.make_qconst noloc ("list", "NIL") 112val PMATCH_ROW_pt = 113 Parse_support.make_qconst noloc ("patternMatches", "PMATCH_ROW") 114val unit_pty = Pretype.Tyop{Thy = "one", Tyop = "one", Args = []} 115val bool_pty = Pretype.Tyop{Thy = "min", Tyop = "bool", Args = []} 116 117fun mk_ptlist pts = 118 case pts of 119 [] => nil_pt 120 | h::t => Parse_support.list_make_comb noloc [cons_pt, h, mk_ptlist t] 121 122type env = Parse_supportENV.env 123fun push bvs = fupd_scope (fn s => bvs @ s) 124fun popn n = fupd_scope (fn s => List.drop(s,n)) 125 126fun ptlist_mk_comb [] = raise Fail "ptlist_mk_comb: empty list" 127 | ptlist_mk_comb [t] = t 128 | ptlist_mk_comb (f::x::xs) = 129 ptlist_mk_comb (Preterm.Comb{Locn = noloc, Rand = x, Rator = f} :: xs) 130 131val UNCURRY_pty = Pretype.fromType (type_of pairSyntax.uncurry_tm) 132open Preterm errormonad 133val mkUNCURRY = 134 lift (fn pty => Const {Locn=noloc, Name="UNCURRY", Thy="pair", Ty=pty}) 135 (Pretype.rename_typevars [] UNCURRY_pty) 136 137fun ptmkabs((vnm,vty),b) = 138 Abs{Body = b, Bvar = Preterm.Var{Locn=noloc,Name=vnm,Ty=vty}, Locn = noloc} 139fun ptmkcomb(f,x) = Preterm.Comb{Rator = f, Rand = x, Locn = noloc} 140fun tuplify vs body = 141 case vs of 142 [] => return body 143 | [x] => return (ptmkabs(x,body)) 144 | [x,y] => lift (fn pt => ptmkcomb(pt, ptmkabs(x,ptmkabs(y,body)))) 145 mkUNCURRY 146 | v::rest => lift2 (fn body' => fn pt => ptmkcomb(pt, ptmkabs(v, body'))) 147 (tuplify rest body) 148 mkUNCURRY 149 150val pty_to_string = PP.pp_to_string 70 Pretype.pp_pretype 151(* 152fun envdiag msg E = () 153 print (msg ^ ": " ^ 154 String.concatWith ", " 155 (map (fn (n,ty) => n ^ ": " ^ pty_to_string ty) 156 (frees E)) ^ "\n") *) 157 158fun extract_fvs ptm = 159 let 160 open Preterm Pretype 161 fun recurse tyopt acc ptm = 162 case (ptm, tyopt) of 163 (Var{Name,Ty,...}, NONE) => return ((Name, Ty) :: acc) 164 | (Var{Name,...}, SOME Ty) => return ((Name, Ty) :: acc) 165 | (Constrained {Ptm,Ty,...}, _) => recurse (SOME Ty) acc Ptm 166 | (Comb{Rator = Comb{Rator = Const {Name = ",", Thy = "pair", ...}, 167 Rand = arg1, ...}, 168 Rand = arg2, ...}, _) => 169 (case tyopt of 170 SOME (Tyop{Thy = "pair", Tyop = "prod", Args = [ty1,ty2]}) => 171 recurse (SOME ty2) acc arg2 >- 172 (fn a => recurse (SOME ty1) a arg1) 173 | _ => recurse NONE acc arg2 >- (fn a => recurse NONE a arg1)) 174 | (Comb{Rator = arg1, Rand = arg2, ...}, _) => 175 recurse NONE acc arg2 >- (fn a => recurse NONE a arg1) 176 | (Antiq{Tm,...}, _) => 177 term_to_preterm [] Tm >- 178 (fn pt => recurse (SOME (fromType (type_of Tm))) acc pt) 179 | _ => return acc 180 in 181 recurse NONE [] ptm 182 end 183 184fun update_ptyE (old:env) = fupd_ptyE (K (#ptyE old)) 185 186fun mk_row recursor a E = 187 case a of 188 APP(l1, APP(l2, IDENT (l3, arr), lh), rh) => 189 let 190 (* val _ = envdiag "mk_row entry" E *) 191 val _ = arr = GrammarSpecials.case_arrow_special orelse 192 raise mk_HOL_ERRloc "parsePMATCH" "pmatch_transform" l1 193 "No arrow" 194 val (bvs_opt, lhbody) = 195 case lh of 196 APP(_, APP(_, IDENT (_, bvsplit), bvs), body) => 197 if bvsplit = PMATCH_endbinding then (SOME bvs, body) 198 else (NONE, lh) 199 | _ => (NONE, lh) 200 val (pat, guard_opt) = 201 case lhbody of 202 APP(_, APP(_, IDENT(_, gdsplit), pat), gd) => 203 if gdsplit = PMATCH_when then 204 (pat, SOME gd) 205 else (lhbody, NONE) 206 | _ => (lhbody, NONE) 207 val bvsE = 208 case bvs_opt of 209 NONE => NONE 210 | SOME a => 211 let 212 val (bv_ptm, E') = recursor a (update_ptyE E empty_env) 213 in 214 SOME (smash (extract_fvs bv_ptm) (#ptyE E'), E') 215 end 216 217 val (patStartE,pop_count) = 218 case bvsE of 219 NONE => (update_ptyE E empty_env,0) 220 | SOME (vs,bv_env) => (push vs (update_ptyE bv_env E), length vs) 221 222 val (pat_ptm, patfrees, patE0) = 223 let 224 val (pat_ptm, E') = recursor pat patStartE 225 in 226 (pat_ptm, 227 Lib.set_diff (frees E') (frees patStartE), 228 popn pop_count E') 229 end 230 val (allvars0, patE) = 231 case bvsE of 232 NONE => (List.rev patfrees, update_ptyE patE0 E) 233 | SOME (vs, _) => 234 (vs @ List.filter (fn(nm,_) => String.isPrefix "_" nm) patfrees, 235 patE0) 236 val allvars = if null allvars0 then [("_", unit_pty)] else allvars0 237 val allpop_count = length allvars 238 val (guard_ptm, guardE) = 239 case guard_opt of 240 NONE => (Preterm.Const{Thy="bool", Name = "T", Locn = noloc, 241 Ty = bool_pty}, patE) 242 | SOME ga => 243 let 244 val (g, E') = recursor ga (push allvars patE) 245 in 246 (g, popn allpop_count E') 247 end 248 val (rh_ptm, rhE) = let 249 val (pt, E') = recursor rh (push allvars guardE) 250 in 251 (pt, popn allpop_count E') 252 end 253 val (prow_pt,penultE) = PMATCH_ROW_pt rhE 254 val tupled_argsM = mmap (tuplify allvars) [pat_ptm, guard_ptm, rh_ptm] 255 val (tupled_args, ptyE) = 256 case tupled_argsM (#ptyE penultE) of 257 Some(ptyE', pts) => (pts, ptyE') 258 | Error e => raise mkExn e 259 (* val _ = envdiag "mk_row exit" rhE *) 260 in 261 (ptlist_mk_comb (prow_pt :: tupled_args), fupd_ptyE (K ptyE) penultE) 262 end 263 | _ => raise mk_HOL_ERRloc "parsePMATCH" "pmatch_transform" 264 (locn_of_absyn a) 265 "No arrow" 266 267fun pmatch_case G recursor a = 268 case a of 269 APP(l1, APP(l2, IDENT(l3, c), arg1), arg2) => 270 let 271 open Parse_support 272 val arg1 = recursor arg1 273 val pmatch_pt = make_qconst noloc ("patternMatches", "PMATCH") 274 val rows = map (mk_row recursor) (strip_casesplit arg2) 275 in 276 list_make_comb l1 [pmatch_pt, arg1, mk_ptlist rows] 277 end 278 | _ => raise Fail "pmatch_case: should never happen" 279 280(* ---------------------------------------------------------------------- 281 Functions to modify grammars so that they do or don't use new 282 pmatch case expressions 283 ---------------------------------------------------------------------- *) 284 285fun add_pmatch actions (G:'a) = 286 let 287 val {get, arule : add_record -> 'a -> 'a, rmtmtok, 288 add_ptmproc: string * int -> preterm_processor -> 'a -> 'a, 289 addup, up} = 290 actions 291 val crules = grammar_tok_rules "case" (get G) 292 val dtcrules0 = grammar_tok_rules "dtcase" (get G) 293 val do_dtc = null dtcrules0 294 val do_pm = 295 case crules of 296 [] => raise mk_HOL_ERR "parsePMATCH" "ADD_PMATCH" 297 "No existing case rules?" 298 | c :: _ => #term_name c <> PMATCH_case_special 299 val _ = set_trace "pp_cases_dt" 1 300 val G = 301 if do_pm then rmtmtok {term_name = GrammarSpecials.core_case_special, 302 tok = "case"} G 303 else G 304 val G = 305 if do_dtc then 306 List.foldl (fn (ar, G) => arule (mk_dtcase ar) G) G crules 307 else G 308 val G = 309 if do_pm then 310 List.foldl (fn (ar, G) => arule (mk_pmcase ar) G) G crules 311 else G 312 val G = if do_pm then 313 G |> arule when_ar |> arule endbinding_ar 314 else G 315 val G = if do_pm then 316 G |> add_ptmproc (PMATCH_case_special, 2) pmatch_case 317 else G 318 val G = if do_pm then G |> addup up else G 319 in 320 G 321 end 322 323 324 325end 326