276 in |
276 in |
277 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
277 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
278 end |
278 end |
279 *} |
279 *} |
280 |
280 |
281 ML AList.lookup |
|
282 |
|
283 (* We assume no bindings in the type on which bn is defined *) |
281 (* We assume no bindings in the type on which bn is defined *) |
284 (* TODO: currently works only with current fv_bn function *) |
282 (* TODO: currently works only with current fv_bn function *) |
285 ML {* |
283 ML {* |
286 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn (fvbn, (bn, ith_dtyp, args_in_bns)) = |
284 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn (fvbn, (bn, ith_dtyp, args_in_bns)) = |
287 let |
285 let |
294 val args = map Free (names ~~ Ts); |
292 val args = map Free (names ~~ Ts); |
295 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
293 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
296 fun fv_arg ((dt, x), arg_no) = |
294 fun fv_arg ((dt, x), arg_no) = |
297 let |
295 let |
298 val ty = fastype_of x |
296 val ty = fastype_of x |
299 val _ = tracing (PolyML.makestring args_in_bn); |
297 (* val _ = tracing ("B 1" ^ PolyML.makestring args_in_bn);*) |
300 val _ = tracing (PolyML.makestring bn_fvbn); |
298 (* val _ = tracing ("B 2" ^ PolyML.makestring bn_fvbn);*) |
301 in |
299 in |
302 case AList.lookup (op=) args_in_bn arg_no of |
300 case AList.lookup (op=) args_in_bn arg_no of |
303 SOME NONE => @{term "{} :: atom set"} |
301 SOME NONE => @{term "{} :: atom set"} |
304 | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x |
302 | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x |
305 | NONE => |
303 | NONE => |
418 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
416 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
419 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
417 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
420 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
418 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
421 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
419 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
422 val fv_frees = map Free (fv_names ~~ fv_types); |
420 val fv_frees = map Free (fv_names ~~ fv_types); |
423 val nr_bns = non_rec_binds bindsall; |
421 (* TODO: We need a transitive closure, but instead we do this hack considering |
|
422 all binding functions as recursive or not *) |
|
423 val nr_bns = |
|
424 if (non_rec_binds bindsall) = [] then [] |
|
425 else map (fn (bn, _, _) => bn) bns; |
424 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
426 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
425 val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns; |
427 val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns; |
426 val fvbns = map snd bn_fv_bns; |
428 val fvbns = map snd bn_fv_bns; |
427 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
429 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
428 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
430 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |