# HG changeset patch
# User blanchet
# Date 1397060531 -7200
# Node ID c451cf8b29c8cda58e9b6d6ddb439b8e94be16a4
# Parent  5b82c58b665c259318b2a9d37179abc4b8c91248
thread mutual cliques through

diff -r 5b82c58b665c -r c451cf8b29c8 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- 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 =
diff -r 5b82c58b665c -r c451cf8b29c8 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- 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);
 
diff -r 5b82c58b665c -r c451cf8b29c8 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- 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);