haftmann@33967
|
1 |
(* Title: HOL/Tools/Datatype/datatype_case.ML
|
berghofe@22779
|
2 |
Author: Konrad Slind, Cambridge University Computer Laboratory
|
wenzelm@29266
|
3 |
Author: Stefan Berghofer, TU Muenchen
|
berghofe@22779
|
4 |
|
haftmann@33967
|
5 |
Datatype package: nested case expressions on datatypes.
|
berghofe@22779
|
6 |
*)
|
berghofe@22779
|
7 |
|
berghofe@22779
|
8 |
signature DATATYPE_CASE =
|
berghofe@22779
|
9 |
sig
|
haftmann@33967
|
10 |
datatype config = Error | Warning | Quiet
|
haftmann@33967
|
11 |
type info = Datatype_Aux.info
|
haftmann@33967
|
12 |
val make_case: (string * typ -> info option) ->
|
bulwahn@32671
|
13 |
Proof.context -> config -> string list -> term -> (term * term) list ->
|
krauss@44094
|
14 |
term
|
haftmann@33967
|
15 |
val dest_case: (string -> info option) -> bool ->
|
berghofe@22779
|
16 |
string list -> term -> (term * (term * term) list) option
|
haftmann@33967
|
17 |
val strip_case: (string -> info option) -> bool ->
|
berghofe@22779
|
18 |
term -> (term * (term * term) list) option
|
haftmann@33967
|
19 |
val case_tr: bool -> (theory -> string * typ -> info option) ->
|
haftmann@33967
|
20 |
Proof.context -> term list -> term
|
haftmann@33967
|
21 |
val case_tr': (theory -> string -> info option) ->
|
berghofe@22779
|
22 |
string -> Proof.context -> term list -> term
|
berghofe@22779
|
23 |
end;
|
berghofe@22779
|
24 |
|
haftmann@33967
|
25 |
structure Datatype_Case : DATATYPE_CASE =
|
berghofe@22779
|
26 |
struct
|
berghofe@22779
|
27 |
|
bulwahn@32671
|
28 |
datatype config = Error | Warning | Quiet;
|
haftmann@33967
|
29 |
type info = Datatype_Aux.info;
|
bulwahn@32671
|
30 |
|
berghofe@22779
|
31 |
exception CASE_ERROR of string * int;
|
berghofe@22779
|
32 |
|
berghofe@22779
|
33 |
fun match_type thy pat ob = Sign.typ_match thy (pat, ob) Vartab.empty;
|
berghofe@22779
|
34 |
|
krauss@44096
|
35 |
(* Get information about datatypes *)
|
berghofe@22779
|
36 |
|
haftmann@32896
|
37 |
fun ty_info tab sT =
|
wenzelm@42930
|
38 |
(case tab sT of
|
haftmann@33967
|
39 |
SOME ({descr, case_name, index, sorts, ...} : info) =>
|
berghofe@22779
|
40 |
let
|
berghofe@22779
|
41 |
val (_, (tname, dts, constrs)) = nth descr index;
|
haftmann@33967
|
42 |
val mk_ty = Datatype_Aux.typ_of_dtyp descr sorts;
|
wenzelm@35124
|
43 |
val T = Type (tname, map mk_ty dts);
|
berghofe@22779
|
44 |
in
|
berghofe@22779
|
45 |
SOME {case_name = case_name,
|
berghofe@22779
|
46 |
constructors = map (fn (cname, dts') =>
|
wenzelm@35845
|
47 |
Const (cname, Logic.varifyT_global (map mk_ty dts' ---> T))) constrs}
|
berghofe@22779
|
48 |
end
|
wenzelm@42930
|
49 |
| NONE => NONE);
|
berghofe@22779
|
50 |
|
berghofe@22779
|
51 |
|
krauss@44096
|
52 |
(*Each pattern carries with it a tag i, which denotes the clause it
|
krauss@44096
|
53 |
came from. i = ~1 indicates that the clause was added by pattern
|
krauss@44096
|
54 |
completion.*)
|
berghofe@22779
|
55 |
|
wenzelm@29281
|
56 |
fun add_row_used ((prfx, pats), (tm, tag)) =
|
krauss@44093
|
57 |
fold Term.add_free_names (tm :: pats @ map Free prfx);
|
berghofe@22779
|
58 |
|
krauss@44096
|
59 |
(*try to preserve names given by user*)
|
berghofe@22779
|
60 |
fun default_names names ts =
|
berghofe@22779
|
61 |
map (fn ("", Free (name', _)) => name' | (name, _) => name) (names ~~ ts);
|
berghofe@22779
|
62 |
|
wenzelm@35124
|
63 |
fun strip_constraints (Const (@{syntax_const "_constrain"}, _) $ t $ tT) =
|
berghofe@22779
|
64 |
strip_constraints t ||> cons tT
|
berghofe@22779
|
65 |
| strip_constraints t = (t, []);
|
berghofe@22779
|
66 |
|
wenzelm@35124
|
67 |
fun mk_fun_constrain tT t =
|
wenzelm@35124
|
68 |
Syntax.const @{syntax_const "_constrain"} $ t $
|
wenzelm@35363
|
69 |
(Syntax.const @{type_syntax fun} $ tT $ Syntax.const @{type_syntax dummy});
|
berghofe@22779
|
70 |
|
berghofe@22779
|
71 |
|
krauss@44096
|
72 |
(*Produce an instance of a constructor, plus fresh variables for its arguments.*)
|
berghofe@22779
|
73 |
fun fresh_constr ty_match ty_inst colty used c =
|
berghofe@22779
|
74 |
let
|
berghofe@22779
|
75 |
val (_, Ty) = dest_Const c
|
berghofe@22779
|
76 |
val Ts = binder_types Ty;
|
berghofe@22779
|
77 |
val names = Name.variant_list used
|
wenzelm@35845
|
78 |
(Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
|
berghofe@22779
|
79 |
val ty = body_type Ty;
|
berghofe@22779
|
80 |
val ty_theta = ty_match ty colty handle Type.TYPE_MATCH =>
|
berghofe@22779
|
81 |
raise CASE_ERROR ("type mismatch", ~1)
|
berghofe@22779
|
82 |
val c' = ty_inst ty_theta c
|
berghofe@22779
|
83 |
val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts)
|
wenzelm@42930
|
84 |
in (c', gvars) end;
|
berghofe@22779
|
85 |
|
berghofe@22779
|
86 |
|
krauss@44096
|
87 |
(*Goes through a list of rows and picks out the ones beginning with a
|
krauss@44096
|
88 |
pattern with constructor = name.*)
|
berghofe@22779
|
89 |
fun mk_group (name, T) rows =
|
wenzelm@42930
|
90 |
let val k = length (binder_types T) in
|
krauss@44097
|
91 |
fold (fn (row as ((prfx, p :: ps), rhs as (_, i))) =>
|
wenzelm@42930
|
92 |
fn ((in_group, not_in_group), (names, cnstrts)) =>
|
wenzelm@42930
|
93 |
(case strip_comb p of
|
wenzelm@42930
|
94 |
(Const (name', _), args) =>
|
wenzelm@42930
|
95 |
if name = name' then
|
wenzelm@42930
|
96 |
if length args = k then
|
wenzelm@42930
|
97 |
let val (args', cnstrts') = split_list (map strip_constraints args)
|
wenzelm@42930
|
98 |
in
|
krauss@44097
|
99 |
((((prfx, args' @ ps), rhs) :: in_group, not_in_group),
|
wenzelm@42930
|
100 |
(default_names names args', map2 append cnstrts cnstrts'))
|
wenzelm@42930
|
101 |
end
|
wenzelm@42930
|
102 |
else raise CASE_ERROR
|
wenzelm@42930
|
103 |
("Wrong number of arguments for constructor " ^ name, i)
|
wenzelm@42930
|
104 |
else ((in_group, row :: not_in_group), (names, cnstrts))
|
wenzelm@42930
|
105 |
| _ => raise CASE_ERROR ("Not a constructor pattern", i)))
|
berghofe@22779
|
106 |
rows (([], []), (replicate k "", replicate k [])) |>> pairself rev
|
berghofe@22779
|
107 |
end;
|
berghofe@22779
|
108 |
|
krauss@44096
|
109 |
|
krauss@44096
|
110 |
(* Partitioning *)
|
krauss@44096
|
111 |
|
berghofe@22779
|
112 |
fun partition _ _ _ _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
|
berghofe@22779
|
113 |
| partition ty_match ty_inst type_of used constructors colty res_ty
|
krauss@44097
|
114 |
(rows as (((prfx, _ :: ps), _) :: _)) =
|
berghofe@22779
|
115 |
let
|
krauss@44098
|
116 |
fun part [] [] = []
|
krauss@44098
|
117 |
| part [] ((_, (_, i)) :: _) =
|
berghofe@22779
|
118 |
raise CASE_ERROR ("Not a constructor pattern", i)
|
krauss@44098
|
119 |
| part (c :: cs) rows =
|
berghofe@22779
|
120 |
let
|
berghofe@22779
|
121 |
val ((in_group, not_in_group), (names, cnstrts)) =
|
berghofe@22779
|
122 |
mk_group (dest_Const c) rows;
|
berghofe@22779
|
123 |
val used' = fold add_row_used in_group used;
|
berghofe@22779
|
124 |
val (c', gvars) = fresh_constr ty_match ty_inst colty used' c;
|
berghofe@22779
|
125 |
val in_group' =
|
berghofe@22779
|
126 |
if null in_group (* Constructor not given *)
|
berghofe@22779
|
127 |
then
|
berghofe@22779
|
128 |
let
|
krauss@44097
|
129 |
val Ts = map type_of ps;
|
berghofe@22779
|
130 |
val xs = Name.variant_list
|
wenzelm@29281
|
131 |
(fold Term.add_free_names gvars used')
|
krauss@44097
|
132 |
(replicate (length ps) "x")
|
berghofe@22779
|
133 |
in
|
berghofe@22779
|
134 |
[((prfx, gvars @ map Free (xs ~~ Ts)),
|
krauss@44095
|
135 |
(Const (@{const_syntax undefined}, res_ty), ~1))]
|
berghofe@22779
|
136 |
end
|
berghofe@22779
|
137 |
else in_group
|
berghofe@22779
|
138 |
in
|
krauss@44098
|
139 |
{constructor = c',
|
krauss@44098
|
140 |
new_formals = gvars,
|
krauss@44098
|
141 |
names = names,
|
krauss@44098
|
142 |
constraints = cnstrts,
|
krauss@44098
|
143 |
group = in_group'} :: part cs not_in_group
|
berghofe@22779
|
144 |
end
|
krauss@44098
|
145 |
in part constructors rows end;
|
berghofe@22779
|
146 |
|
krauss@44093
|
147 |
fun v_to_prfx (prfx, Free v::pats) = (v::prfx,pats)
|
berghofe@22779
|
148 |
| v_to_prfx _ = raise CASE_ERROR ("mk_case: v_to_prfx", ~1);
|
berghofe@22779
|
149 |
|
berghofe@22779
|
150 |
|
krauss@44096
|
151 |
(* Translation of pattern terms into nested case expressions. *)
|
krauss@44096
|
152 |
|
berghofe@22779
|
153 |
fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
|
berghofe@22779
|
154 |
let
|
wenzelm@44206
|
155 |
val name = singleton (Name.variant_list used) "a";
|
berghofe@22779
|
156 |
fun expand constructors used ty ((_, []), _) =
|
berghofe@22779
|
157 |
raise CASE_ERROR ("mk_case: expand_var_row", ~1)
|
krauss@44097
|
158 |
| expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
|
berghofe@22779
|
159 |
if is_Free p then
|
berghofe@22779
|
160 |
let
|
berghofe@22779
|
161 |
val used' = add_row_used row used;
|
berghofe@22779
|
162 |
fun expnd c =
|
berghofe@22779
|
163 |
let val capp =
|
berghofe@22779
|
164 |
list_comb (fresh_constr ty_match ty_inst ty used' c)
|
krauss@44097
|
165 |
in ((prfx, capp :: ps), (subst_free [(p, capp)] rhs, tag))
|
berghofe@22779
|
166 |
end
|
berghofe@22779
|
167 |
in map expnd constructors end
|
berghofe@22779
|
168 |
else [row]
|
krauss@44098
|
169 |
fun mk _ [] = raise CASE_ERROR ("no rows", ~1)
|
krauss@44098
|
170 |
| mk [] (((_, []), (tm, tag)) :: _) = (* Done *)
|
krauss@44094
|
171 |
([tag], tm)
|
krauss@44098
|
172 |
| mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) =
|
krauss@44098
|
173 |
mk path [row]
|
krauss@44098
|
174 |
| mk (u :: us) (rows as ((_, _ :: _), _) :: _) =
|
krauss@44095
|
175 |
let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
|
wenzelm@42930
|
176 |
(case Option.map (apfst head_of) (find_first (not o is_Free o fst) col0) of
|
berghofe@22779
|
177 |
NONE =>
|
berghofe@22779
|
178 |
let
|
berghofe@22779
|
179 |
val rows' = map (fn ((v, _), row) => row ||>
|
krauss@44096
|
180 |
apfst (subst_free [(v, u)]) |>> v_to_prfx) (col0 ~~ rows);
|
krauss@44098
|
181 |
in mk us rows' end
|
wenzelm@42930
|
182 |
| SOME (Const (cname, cT), i) =>
|
wenzelm@42930
|
183 |
(case ty_info tab (cname, cT) of
|
wenzelm@42930
|
184 |
NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i)
|
wenzelm@42930
|
185 |
| SOME {case_name, constructors} =>
|
wenzelm@42930
|
186 |
let
|
wenzelm@42930
|
187 |
val pty = body_type cT;
|
krauss@44097
|
188 |
val used' = fold Term.add_free_names us used;
|
wenzelm@42930
|
189 |
val nrows = maps (expand constructors used' pty) rows;
|
wenzelm@42930
|
190 |
val subproblems = partition ty_match ty_inst type_of used'
|
wenzelm@42930
|
191 |
constructors pty range_ty nrows;
|
krauss@44098
|
192 |
val (pat_rect, dtrees) = split_list (map (fn {new_formals, group, ...} =>
|
krauss@44098
|
193 |
mk (new_formals @ us) group) subproblems)
|
wenzelm@42930
|
194 |
val case_functions = map2
|
wenzelm@42930
|
195 |
(fn {new_formals, names, constraints, ...} =>
|
wenzelm@42930
|
196 |
fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
|
wenzelm@42930
|
197 |
Abs (if s = "" then name else s, T,
|
wenzelm@42930
|
198 |
abstract_over (x, t)) |>
|
wenzelm@42930
|
199 |
fold mk_fun_constrain cnstrts)
|
wenzelm@42930
|
200 |
(new_formals ~~ names ~~ constraints))
|
wenzelm@42930
|
201 |
subproblems dtrees;
|
wenzelm@42930
|
202 |
val types = map type_of (case_functions @ [u]);
|
wenzelm@42930
|
203 |
val case_const = Const (case_name, types ---> range_ty)
|
wenzelm@42930
|
204 |
val tree = list_comb (case_const, case_functions @ [u])
|
krauss@44094
|
205 |
in (flat pat_rect, tree) end)
|
berghofe@22779
|
206 |
| SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
|
wenzelm@42930
|
207 |
Syntax.string_of_term ctxt t, i))
|
berghofe@22779
|
208 |
end
|
krauss@44098
|
209 |
| mk _ _ = raise CASE_ERROR ("Malformed row matrix", ~1)
|
wenzelm@42930
|
210 |
in mk end;
|
berghofe@22779
|
211 |
|
berghofe@22779
|
212 |
fun case_error s = error ("Error in case expression:\n" ^ s);
|
berghofe@22779
|
213 |
|
krauss@44096
|
214 |
(*Repeated variable occurrences in a pattern are not allowed.*)
|
berghofe@22779
|
215 |
fun no_repeat_vars ctxt pat = fold_aterms
|
berghofe@22779
|
216 |
(fn x as Free (s, _) => (fn xs =>
|
berghofe@22779
|
217 |
if member op aconv xs x then
|
berghofe@22779
|
218 |
case_error (quote s ^ " occurs repeatedly in the pattern " ^
|
wenzelm@24920
|
219 |
quote (Syntax.string_of_term ctxt pat))
|
berghofe@22779
|
220 |
else x :: xs)
|
berghofe@22779
|
221 |
| _ => I) pat [];
|
berghofe@22779
|
222 |
|
bulwahn@32671
|
223 |
fun gen_make_case ty_match ty_inst type_of tab ctxt config used x clauses =
|
berghofe@22779
|
224 |
let
|
wenzelm@35124
|
225 |
fun string_of_clause (pat, rhs) =
|
wenzelm@35124
|
226 |
Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
|
berghofe@22779
|
227 |
val _ = map (no_repeat_vars ctxt o fst) clauses;
|
berghofe@22779
|
228 |
val rows = map_index (fn (i, (pat, rhs)) =>
|
krauss@44095
|
229 |
(([], [pat]), (rhs, i))) clauses;
|
wenzelm@35124
|
230 |
val rangeT =
|
wenzelm@35124
|
231 |
(case distinct op = (map (type_of o snd) clauses) of
|
berghofe@22779
|
232 |
[] => case_error "no clauses given"
|
berghofe@22779
|
233 |
| [T] => T
|
berghofe@22779
|
234 |
| _ => case_error "all cases must have the same result type");
|
berghofe@22779
|
235 |
val used' = fold add_row_used rows used;
|
krauss@44094
|
236 |
val (tags, case_tm) = mk_case tab ctxt ty_match ty_inst type_of
|
krauss@44098
|
237 |
used' rangeT [x] rows
|
berghofe@22779
|
238 |
handle CASE_ERROR (msg, i) => case_error (msg ^
|
berghofe@22779
|
239 |
(if i < 0 then ""
|
berghofe@22779
|
240 |
else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
|
wenzelm@35124
|
241 |
val _ =
|
krauss@44095
|
242 |
(case subtract (op =) tags (map (snd o snd) rows) of
|
wenzelm@42930
|
243 |
[] => ()
|
wenzelm@42930
|
244 |
| is =>
|
wenzelm@42930
|
245 |
(case config of Error => case_error | Warning => warning | Quiet => fn _ => {})
|
wenzelm@42930
|
246 |
("The following clauses are redundant (covered by preceding clauses):\n" ^
|
wenzelm@42930
|
247 |
cat_lines (map (string_of_clause o nth clauses) is)));
|
berghofe@22779
|
248 |
in
|
krauss@44094
|
249 |
case_tm
|
berghofe@22779
|
250 |
end;
|
berghofe@22779
|
251 |
|
berghofe@22779
|
252 |
fun make_case tab ctxt = gen_make_case
|
wenzelm@43232
|
253 |
(match_type (Proof_Context.theory_of ctxt)) Envir.subst_term_types fastype_of tab ctxt;
|
berghofe@22779
|
254 |
val make_case_untyped = gen_make_case (K (K Vartab.empty))
|
berghofe@22779
|
255 |
(K (Term.map_types (K dummyT))) (K dummyT);
|
berghofe@22779
|
256 |
|
berghofe@22779
|
257 |
|
berghofe@22779
|
258 |
(* parse translation *)
|
berghofe@22779
|
259 |
|
nipkow@24349
|
260 |
fun case_tr err tab_of ctxt [t, u] =
|
wenzelm@42930
|
261 |
let
|
wenzelm@43232
|
262 |
val thy = Proof_Context.theory_of ctxt;
|
wenzelm@43232
|
263 |
val intern_const_syntax = Consts.intern_syntax (Proof_Context.consts_of ctxt);
|
wenzelm@35256
|
264 |
|
wenzelm@42930
|
265 |
(* replace occurrences of dummy_pattern by distinct variables *)
|
wenzelm@42930
|
266 |
(* internalize constant names *)
|
wenzelm@44206
|
267 |
(* FIXME proper name context!? *)
|
wenzelm@42930
|
268 |
fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
|
wenzelm@42930
|
269 |
let val (t', used') = prep_pat t used
|
wenzelm@42930
|
270 |
in (c $ t' $ tT, used') end
|
wenzelm@42930
|
271 |
| prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
|
wenzelm@44206
|
272 |
let val x = singleton (Name.variant_list used) "x"
|
wenzelm@42930
|
273 |
in (Free (x, T), x :: used) end
|
wenzelm@42930
|
274 |
| prep_pat (Const (s, T)) used =
|
wenzelm@42930
|
275 |
(Const (intern_const_syntax s, T), used)
|
wenzelm@42930
|
276 |
| prep_pat (v as Free (s, T)) used =
|
wenzelm@43232
|
277 |
let val s' = Proof_Context.intern_const ctxt s in
|
wenzelm@42930
|
278 |
if Sign.declared_const thy s' then
|
wenzelm@42930
|
279 |
(Const (s', T), used)
|
wenzelm@42930
|
280 |
else (v, used)
|
wenzelm@42930
|
281 |
end
|
wenzelm@42930
|
282 |
| prep_pat (t $ u) used =
|
wenzelm@42930
|
283 |
let
|
wenzelm@42930
|
284 |
val (t', used') = prep_pat t used;
|
wenzelm@43230
|
285 |
val (u', used'') = prep_pat u used';
|
wenzelm@42930
|
286 |
in
|
wenzelm@42930
|
287 |
(t' $ u', used'')
|
wenzelm@42930
|
288 |
end
|
wenzelm@42930
|
289 |
| prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
|
wenzelm@42930
|
290 |
fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
|
wenzelm@42930
|
291 |
let val (l', cnstrts) = strip_constraints l
|
wenzelm@42930
|
292 |
in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts) end
|
wenzelm@42930
|
293 |
| dest_case1 t = case_error "dest_case1";
|
wenzelm@42930
|
294 |
fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
|
wenzelm@42930
|
295 |
| dest_case2 t = [t];
|
wenzelm@42938
|
296 |
val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
|
krauss@44094
|
297 |
val case_tm = make_case_untyped (tab_of thy) ctxt
|
wenzelm@42930
|
298 |
(if err then Error else Warning) []
|
wenzelm@42930
|
299 |
(fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
|
wenzelm@42930
|
300 |
(flat cnstrts) t) cases;
|
wenzelm@42930
|
301 |
in case_tm end
|
nipkow@24349
|
302 |
| case_tr _ _ _ ts = case_error "case_tr";
|
berghofe@22779
|
303 |
|
berghofe@22779
|
304 |
|
krauss@44096
|
305 |
(* Pretty printing of nested case expressions *)
|
berghofe@22779
|
306 |
|
berghofe@22779
|
307 |
(* destruct one level of pattern matching *)
|
berghofe@22779
|
308 |
|
wenzelm@44206
|
309 |
(* FIXME proper name context!? *)
|
berghofe@22779
|
310 |
fun gen_dest_case name_of type_of tab d used t =
|
wenzelm@42930
|
311 |
(case apfst name_of (strip_comb t) of
|
berghofe@22779
|
312 |
(SOME cname, ts as _ :: _) =>
|
berghofe@22779
|
313 |
let
|
berghofe@22779
|
314 |
val (fs, x) = split_last ts;
|
berghofe@22779
|
315 |
fun strip_abs i t =
|
berghofe@22779
|
316 |
let
|
berghofe@22779
|
317 |
val zs = strip_abs_vars t;
|
berghofe@22779
|
318 |
val _ = if length zs < i then raise CASE_ERROR ("", 0) else ();
|
berghofe@22779
|
319 |
val (xs, ys) = chop i zs;
|
berghofe@22779
|
320 |
val u = list_abs (ys, strip_abs_body t);
|
wenzelm@29270
|
321 |
val xs' = map Free (Name.variant_list (OldTerm.add_term_names (u, used))
|
berghofe@22779
|
322 |
(map fst xs) ~~ map snd xs)
|
berghofe@22779
|
323 |
in (xs', subst_bounds (rev xs', u)) end;
|
berghofe@22779
|
324 |
fun is_dependent i t =
|
berghofe@22779
|
325 |
let val k = length (strip_abs_vars t) - i
|
wenzelm@42930
|
326 |
in k < 0 orelse exists (fn j => j >= k) (loose_bnos (strip_abs_body t)) end;
|
berghofe@22779
|
327 |
fun count_cases (_, _, true) = I
|
berghofe@22779
|
328 |
| count_cases (c, (_, body), false) =
|
berghofe@22779
|
329 |
AList.map_default op aconv (body, []) (cons c);
|
wenzelm@35392
|
330 |
val is_undefined = name_of #> equal (SOME @{const_name undefined});
|
berghofe@22779
|
331 |
fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body)
|
wenzelm@42930
|
332 |
in
|
wenzelm@42930
|
333 |
(case ty_info tab cname of
|
berghofe@22779
|
334 |
SOME {constructors, case_name} =>
|
berghofe@22779
|
335 |
if length fs = length constructors then
|
berghofe@22779
|
336 |
let
|
berghofe@22779
|
337 |
val cases = map (fn (Const (s, U), t) =>
|
berghofe@22779
|
338 |
let
|
berghofe@22779
|
339 |
val k = length (binder_types U);
|
berghofe@22779
|
340 |
val p as (xs, _) = strip_abs k t
|
berghofe@22779
|
341 |
in
|
berghofe@22779
|
342 |
(Const (s, map type_of xs ---> type_of x),
|
berghofe@22779
|
343 |
p, is_dependent k t)
|
berghofe@22779
|
344 |
end) (constructors ~~ fs);
|
berghofe@22779
|
345 |
val cases' = sort (int_ord o swap o pairself (length o snd))
|
berghofe@22779
|
346 |
(fold_rev count_cases cases []);
|
berghofe@22779
|
347 |
val R = type_of t;
|
wenzelm@35124
|
348 |
val dummy =
|
wenzelm@35392
|
349 |
if d then Const (@{const_name dummy_pattern}, R)
|
wenzelm@44206
|
350 |
else Free (singleton (Name.variant_list used) "x", R);
|
berghofe@22779
|
351 |
in
|
wenzelm@42930
|
352 |
SOME (x,
|
wenzelm@42930
|
353 |
map mk_case
|
wenzelm@42930
|
354 |
(case find_first (is_undefined o fst) cases' of
|
wenzelm@42930
|
355 |
SOME (_, cs) =>
|
wenzelm@42930
|
356 |
if length cs = length constructors then [hd cases]
|
wenzelm@42930
|
357 |
else filter_out (fn (_, (_, body), _) => is_undefined body) cases
|
wenzelm@42930
|
358 |
| NONE => case cases' of
|
wenzelm@42930
|
359 |
[] => cases
|
wenzelm@42930
|
360 |
| (default, cs) :: _ =>
|
wenzelm@42930
|
361 |
if length cs = 1 then cases
|
wenzelm@42930
|
362 |
else if length cs = length constructors then
|
wenzelm@42930
|
363 |
[hd cases, (dummy, ([], default), false)]
|
wenzelm@42930
|
364 |
else
|
wenzelm@42930
|
365 |
filter_out (fn (c, _, _) => member op aconv cs c) cases @
|
wenzelm@42930
|
366 |
[(dummy, ([], default), false)]))
|
berghofe@22779
|
367 |
end handle CASE_ERROR _ => NONE
|
berghofe@22779
|
368 |
else NONE
|
wenzelm@42930
|
369 |
| _ => NONE)
|
berghofe@22779
|
370 |
end
|
wenzelm@42930
|
371 |
| _ => NONE);
|
berghofe@22779
|
372 |
|
berghofe@22779
|
373 |
val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
|
wenzelm@43162
|
374 |
val dest_case' = gen_dest_case (try (dest_Const #> fst #> Lexicon.unmark_const)) (K dummyT);
|
berghofe@22779
|
375 |
|
berghofe@22779
|
376 |
|
berghofe@22779
|
377 |
(* destruct nested patterns *)
|
berghofe@22779
|
378 |
|
haftmann@29623
|
379 |
fun strip_case'' dest (pat, rhs) =
|
wenzelm@42930
|
380 |
(case dest (Term.add_free_names pat []) rhs of
|
berghofe@22779
|
381 |
SOME (exp as Free _, clauses) =>
|
wenzelm@29266
|
382 |
if member op aconv (OldTerm.term_frees pat) exp andalso
|
berghofe@22779
|
383 |
not (exists (fn (_, rhs') =>
|
wenzelm@29266
|
384 |
member op aconv (OldTerm.term_frees rhs') exp) clauses)
|
berghofe@22779
|
385 |
then
|
haftmann@29623
|
386 |
maps (strip_case'' dest) (map (fn (pat', rhs') =>
|
berghofe@22779
|
387 |
(subst_free [(exp, pat')] pat, rhs')) clauses)
|
berghofe@22779
|
388 |
else [(pat, rhs)]
|
wenzelm@42930
|
389 |
| _ => [(pat, rhs)]);
|
berghofe@22779
|
390 |
|
wenzelm@35124
|
391 |
fun gen_strip_case dest t =
|
wenzelm@42930
|
392 |
(case dest [] t of
|
berghofe@22779
|
393 |
SOME (x, clauses) =>
|
haftmann@29623
|
394 |
SOME (x, maps (strip_case'' dest) clauses)
|
wenzelm@42930
|
395 |
| NONE => NONE);
|
berghofe@22779
|
396 |
|
berghofe@22779
|
397 |
val strip_case = gen_strip_case oo dest_case;
|
berghofe@22779
|
398 |
val strip_case' = gen_strip_case oo dest_case';
|
berghofe@22779
|
399 |
|
berghofe@22779
|
400 |
|
berghofe@22779
|
401 |
(* print translation *)
|
berghofe@22779
|
402 |
|
berghofe@22779
|
403 |
fun case_tr' tab_of cname ctxt ts =
|
berghofe@22779
|
404 |
let
|
wenzelm@43232
|
405 |
val thy = Proof_Context.theory_of ctxt;
|
berghofe@22779
|
406 |
fun mk_clause (pat, rhs) =
|
wenzelm@42930
|
407 |
let val xs = Term.add_frees pat [] in
|
wenzelm@35124
|
408 |
Syntax.const @{syntax_const "_case1"} $
|
berghofe@22779
|
409 |
map_aterms
|
wenzelm@43156
|
410 |
(fn Free p => Syntax_Trans.mark_boundT p
|
wenzelm@43162
|
411 |
| Const (s, _) => Syntax.const (Lexicon.mark_const s)
|
berghofe@22779
|
412 |
| t => t) pat $
|
berghofe@22779
|
413 |
map_aterms
|
wenzelm@29266
|
414 |
(fn x as Free (s, T) =>
|
wenzelm@43156
|
415 |
if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
|
berghofe@22779
|
416 |
| t => t) rhs
|
wenzelm@42930
|
417 |
end;
|
wenzelm@35124
|
418 |
in
|
wenzelm@42930
|
419 |
(case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
|
wenzelm@35124
|
420 |
SOME (x, clauses) =>
|
wenzelm@35124
|
421 |
Syntax.const @{syntax_const "_case_syntax"} $ x $
|
wenzelm@35124
|
422 |
foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
|
wenzelm@35124
|
423 |
(map mk_clause clauses)
|
wenzelm@42930
|
424 |
| NONE => raise Match)
|
berghofe@22779
|
425 |
end;
|
berghofe@22779
|
426 |
|
berghofe@22779
|
427 |
end;
|