--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Apr 09 13:15:21 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Apr 09 18:22:11 2014 +0200
@@ -7,9 +7,10 @@
signature BNF_FP_N2M =
sig
- val construct_mutualized_fp: BNF_Util.fp_kind -> typ list -> BNF_FP_Def_Sugar.fp_sugar list ->
- binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
- BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory
+ val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
+ BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list ->
+ typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
+ BNF_FP_Util.fp_result * local_theory
end;
structure BNF_FP_N2M : BNF_FP_N2M =
@@ -46,7 +47,7 @@
Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
end;
-fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
+fun construct_mutualized_fp fp cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
(absT_infos : absT_info list) lthy =
let
fun of_fp_res get =
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Apr 09 13:15:21 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Apr 09 18:22:11 2014 +0200
@@ -10,7 +10,7 @@
val unfold_lets_splits: term -> term
val dest_map: Proof.context -> string -> term -> term * term list
- val mutualize_fp_sugars: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
+ val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory ->
(BNF_FP_Def_Sugar.fp_sugar list
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
@@ -109,7 +109,7 @@
|> map_filter I;
(* TODO: test with sort constraints on As *)
-fun mutualize_fp_sugars fp bs fpTs callers callssss fp_sugars0 no_defs_lthy0 =
+fun mutualize_fp_sugars fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy0 =
let
val thy = Proof_Context.theory_of no_defs_lthy0;
@@ -225,7 +225,7 @@
val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
- fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
+ fp_bnf (construct_mutualized_fp fp cliques fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
no_defs_lthy0;
val fp_abs_inverses = map #abs_inverse fp_absT_infos;
@@ -401,7 +401,7 @@
val (num_groups, perm_Ts, perm_gen_Ts) = gather_types lthy [] 0 [] [] sorted_actual_Ts;
val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts;
- val missing_Ts = subtract (op =) actual_Ts perm_Ts;
+ val missing_Ts = fold (remove1 (op =)) actual_Ts perm_Ts;
val Ts = actual_Ts @ missing_Ts;
val nn = length Ts;
@@ -424,10 +424,12 @@
val perm_callssss = map2 (indexify_callsss o #ctrs o #ctr_sugar) perm_fp_sugars0 perm_callssss0;
+ val perm_cliques = [] (*###*)
+
val ((perm_fp_sugars, fp_sugar_thms), lthy) =
if num_groups > 1 then
- mutualize_fp_sugars fp perm_bs perm_frozen_gen_Ts perm_callers perm_callssss perm_fp_sugars0
- lthy
+ mutualize_fp_sugars fp perm_cliques perm_bs perm_frozen_gen_Ts perm_callers perm_callssss
+ perm_fp_sugars0 lthy
else
((perm_fp_sugars0, (NONE, NONE)), lthy);
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Apr 09 13:15:21 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Apr 09 18:22:11 2014 +0200
@@ -81,7 +81,9 @@
Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp;
(* put nested types before the types that nest them, as needed for N2M *)
- val descr = reindex_desc (orig_descr' @ flat (rev nested_descrs));
+ val descrs = burrow reindex_desc (orig_descr' :: rev nested_descrs);
+ val (cliques, descr) =
+ split_list (flat (map_index (fn (i, descr) => map (pair i) descr) descrs));
val dest_dtyp = Datatype_Aux.typ_of_dtyp descr;
@@ -108,7 +110,7 @@
val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
if nn > nn_fp then
- mutualize_fp_sugars Least_FP compat_bs Ts callers callssss fp_sugars0 lthy
+ mutualize_fp_sugars Least_FP cliques compat_bs Ts callers callssss fp_sugars0 lthy
else
((fp_sugars0, (NONE, NONE)), lthy);