580 (* FIXME: because of "@ Xs", the output could contain type variables that are not in the |
580 (* FIXME: because of "@ Xs", the output could contain type variables that are not in the |
581 input; also, "fp_sort" should put the "resBs" first and in the order in which they appear *) |
581 input; also, "fp_sort" should put the "resBs" first and in the order in which they appear *) |
582 fun fp_sort Ass = |
582 fun fp_sort Ass = |
583 subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs; |
583 subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs; |
584 |
584 |
585 val common_name = mk_common_name (map Binding.name_of bs); |
|
586 |
|
587 fun raw_qualify base_b = |
585 fun raw_qualify base_b = |
588 Binding.prefix_name rawN |
586 let val (_, qs, n) = Binding.dest base_b; |
589 #> fold_rev (fn (s, mand) => Binding.qualify mand s) (#2 (Binding.dest base_b)); |
587 in |
|
588 Binding.prefix_name rawN |
|
589 #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)]) |
|
590 end; |
590 |
591 |
591 val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list) |
592 val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list) |
592 (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs) bs rhsXs |
593 (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs) bs rhsXs |
593 (empty_unfolds, lthy)); |
594 (empty_unfolds, lthy)); |
594 |
595 |
595 fun qualify i = |
596 fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1)))); |
596 let val namei = common_name ^ nonzero_string_of_int i; |
|
597 in Binding.qualify true namei end; |
|
598 |
597 |
599 val Ass = map (map dest_TFree) livess; |
598 val Ass = map (map dest_TFree) livess; |
600 val resDs = fold (subtract (op =)) Ass resBs; |
599 val resDs = fold (subtract (op =)) Ass resBs; |
601 val Ds = fold (fold Term.add_tfreesT) deadss []; |
600 val Ds = fold (fold Term.add_tfreesT) deadss []; |
602 |
601 |
603 val timer = time (timer "Construction of BNFs"); |
602 val timer = time (timer "Construction of BNFs"); |
604 |
603 |
605 val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) = |
604 val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) = |
606 normalize_bnfs qualify Ass Ds fp_sort bnfs unfold_set lthy; |
605 normalize_bnfs norm_qualify Ass Ds fp_sort bnfs unfold_set lthy; |
607 |
606 |
608 val Dss = map3 (append oo map o nth) livess kill_poss deadss; |
607 val Dss = map3 (append oo map o nth) livess kill_poss deadss; |
609 |
608 |
|
609 val pre_qualify = Binding.qualify false o Binding.name_of; |
|
610 |
610 val ((pre_bnfs, deadss), lthy'') = |
611 val ((pre_bnfs, deadss), lthy'') = |
611 fold_map3 (seal_bnf unfold_set') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy' |
612 fold_map3 (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) |
|
613 bs Dss bnfs' lthy' |
612 |>> split_list; |
614 |>> split_list; |
613 |
615 |
614 val timer = time (timer "Normalization & sealing of BNFs"); |
616 val timer = time (timer "Normalization & sealing of BNFs"); |
615 |
617 |
616 val res = construct_fp bs resBs (map TFree resDs, deadss) pre_bnfs lthy''; |
618 val res = construct_fp bs resBs (map TFree resDs, deadss) pre_bnfs lthy''; |