150 |
150 |
151 (* Translation of pattern terms into nested case expressions. *) |
151 (* Translation of pattern terms into nested case expressions. *) |
152 |
152 |
153 fun mk_case tab ctxt ty_match ty_inst type_of used range_ty = |
153 fun mk_case tab ctxt ty_match ty_inst type_of used range_ty = |
154 let |
154 let |
155 val name = Name.variant used "a"; |
155 val name = singleton (Name.variant_list used) "a"; |
156 fun expand constructors used ty ((_, []), _) = |
156 fun expand constructors used ty ((_, []), _) = |
157 raise CASE_ERROR ("mk_case: expand_var_row", ~1) |
157 raise CASE_ERROR ("mk_case: expand_var_row", ~1) |
158 | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) = |
158 | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) = |
159 if is_Free p then |
159 if is_Free p then |
160 let |
160 let |
262 val thy = Proof_Context.theory_of ctxt; |
262 val thy = Proof_Context.theory_of ctxt; |
263 val intern_const_syntax = Consts.intern_syntax (Proof_Context.consts_of ctxt); |
263 val intern_const_syntax = Consts.intern_syntax (Proof_Context.consts_of ctxt); |
264 |
264 |
265 (* replace occurrences of dummy_pattern by distinct variables *) |
265 (* replace occurrences of dummy_pattern by distinct variables *) |
266 (* internalize constant names *) |
266 (* internalize constant names *) |
|
267 (* FIXME proper name context!? *) |
267 fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used = |
268 fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used = |
268 let val (t', used') = prep_pat t used |
269 let val (t', used') = prep_pat t used |
269 in (c $ t' $ tT, used') end |
270 in (c $ t' $ tT, used') end |
270 | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used = |
271 | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used = |
271 let val x = Name.variant used "x" |
272 let val x = singleton (Name.variant_list used) "x" |
272 in (Free (x, T), x :: used) end |
273 in (Free (x, T), x :: used) end |
273 | prep_pat (Const (s, T)) used = |
274 | prep_pat (Const (s, T)) used = |
274 (Const (intern_const_syntax s, T), used) |
275 (Const (intern_const_syntax s, T), used) |
275 | prep_pat (v as Free (s, T)) used = |
276 | prep_pat (v as Free (s, T)) used = |
276 let val s' = Proof_Context.intern_const ctxt s in |
277 let val s' = Proof_Context.intern_const ctxt s in |
303 |
304 |
304 (* Pretty printing of nested case expressions *) |
305 (* Pretty printing of nested case expressions *) |
305 |
306 |
306 (* destruct one level of pattern matching *) |
307 (* destruct one level of pattern matching *) |
307 |
308 |
|
309 (* FIXME proper name context!? *) |
308 fun gen_dest_case name_of type_of tab d used t = |
310 fun gen_dest_case name_of type_of tab d used t = |
309 (case apfst name_of (strip_comb t) of |
311 (case apfst name_of (strip_comb t) of |
310 (SOME cname, ts as _ :: _) => |
312 (SOME cname, ts as _ :: _) => |
311 let |
313 let |
312 val (fs, x) = split_last ts; |
314 val (fs, x) = split_last ts; |
343 val cases' = sort (int_ord o swap o pairself (length o snd)) |
345 val cases' = sort (int_ord o swap o pairself (length o snd)) |
344 (fold_rev count_cases cases []); |
346 (fold_rev count_cases cases []); |
345 val R = type_of t; |
347 val R = type_of t; |
346 val dummy = |
348 val dummy = |
347 if d then Const (@{const_name dummy_pattern}, R) |
349 if d then Const (@{const_name dummy_pattern}, R) |
348 else Free (Name.variant used "x", R); |
350 else Free (singleton (Name.variant_list used) "x", R); |
349 in |
351 in |
350 SOME (x, |
352 SOME (x, |
351 map mk_case |
353 map mk_case |
352 (case find_first (is_undefined o fst) cases' of |
354 (case find_first (is_undefined o fst) cases' of |
353 SOME (_, cs) => |
355 SOME (_, cs) => |