146 |
146 |
147 ML {* |
147 ML {* |
148 fun non_rec_binds l = |
148 fun non_rec_binds l = |
149 let |
149 let |
150 fun is_non_rec (SOME (f, false), _, _) = SOME f |
150 fun is_non_rec (SOME (f, false), _, _) = SOME f |
151 | is_non_rec _ = NONE |
|
152 in |
|
153 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
|
154 end |
|
155 *} |
|
156 |
|
157 ML {* |
|
158 fun all_binds l = |
|
159 let |
|
160 fun is_non_rec (SOME (f, _), _, _) = SOME f |
|
161 | is_non_rec _ = NONE |
151 | is_non_rec _ = NONE |
162 in |
152 in |
163 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
153 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
164 end |
154 end |
165 *} |
155 *} |
264 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
254 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
265 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
255 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
266 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
256 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
267 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
257 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
268 val fv_frees = map Free (fv_names ~~ fv_types); |
258 val fv_frees = map Free (fv_names ~~ fv_types); |
269 val all_bns = all_binds bindsall; |
|
270 val nr_bns = non_rec_binds bindsall; |
259 val nr_bns = non_rec_binds bindsall; |
271 val rel_bns = filter (fn (bn, _, _) => bn mem all_bns) bns; |
260 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
272 val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); |
261 val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); |
273 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
262 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
274 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
263 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
275 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
264 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
276 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
265 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
305 if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else |
294 if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else |
306 (* TODO we do not know what to do with non-atomizable things *) |
295 (* TODO we do not know what to do with non-atomizable things *) |
307 @{term "{} :: atom set"} |
296 @{term "{} :: atom set"} |
308 | fv_bind args (SOME (f, _), i, _) = f $ (nth args i); |
297 | fv_bind args (SOME (f, _), i, _) = f $ (nth args i); |
309 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
298 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
|
299 fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE |
|
300 | find_nonrec_binder _ _ = NONE |
310 fun find_compound_binder j (SOME (f, r), i, _) = if i = j then SOME (f, r) else NONE |
301 fun find_compound_binder j (SOME (f, r), i, _) = if i = j then SOME (f, r) else NONE |
311 | find_compound_binder _ _ = NONE |
302 | find_compound_binder _ _ = NONE |
312 fun fv_arg ((dt, x), arg_no) = |
303 fun fv_arg ((dt, x), arg_no) = |
313 case get_first (find_compound_binder arg_no) bindcs of |
304 case get_first (find_nonrec_binder arg_no) bindcs of |
314 SOME (f, is_rec) => |
305 SOME f => |
315 (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of |
306 (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of |
316 SOME fv_bn => |
307 SOME fv_bn => fv_bn $ x |
317 if is_rec then |
|
318 let |
|
319 val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
|
320 val sub = fv_binds args relevant |
|
321 in |
|
322 mk_diff (fv_bn $ x) sub |
|
323 end |
|
324 else fv_bn $ x |
|
325 | NONE => error "bn specified in a non-rec binding but not in bn list") |
308 | NONE => error "bn specified in a non-rec binding but not in bn list") |
326 | NONE => |
309 | NONE => |
327 let |
310 let |
328 val arg = |
311 val arg = |
329 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
312 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |