thread mutual cliques through
authorblanchet
Wed Apr 09 18:22:11 2014 +0200 (2014-04-09)
changeset 56484c451cf8b29c8
parent 56483 5b82c58b665c
child 56485 008634379465
thread mutual cliques through
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 09 13:15:21 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 09 18:22:11 2014 +0200
     1.3 @@ -7,9 +7,10 @@
     1.4  
     1.5  signature BNF_FP_N2M =
     1.6  sig
     1.7 -  val construct_mutualized_fp: BNF_Util.fp_kind -> typ list -> BNF_FP_Def_Sugar.fp_sugar list ->
     1.8 -    binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
     1.9 -    BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory
    1.10 +  val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
    1.11 +    BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list ->
    1.12 +    typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
    1.13 +    BNF_FP_Util.fp_result * local_theory
    1.14  end;
    1.15  
    1.16  structure BNF_FP_N2M : BNF_FP_N2M =
    1.17 @@ -46,7 +47,7 @@
    1.18      Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
    1.19    end;
    1.20  
    1.21 -fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
    1.22 +fun construct_mutualized_fp fp cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
    1.23      (absT_infos : absT_info list) lthy =
    1.24    let
    1.25      fun of_fp_res get =
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Apr 09 13:15:21 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Apr 09 18:22:11 2014 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4    val unfold_lets_splits: term -> term
     2.5    val dest_map: Proof.context -> string -> term -> term * term list
     2.6  
     2.7 -  val mutualize_fp_sugars: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
     2.8 +  val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
     2.9      term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory ->
    2.10      (BNF_FP_Def_Sugar.fp_sugar list
    2.11       * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
    2.12 @@ -109,7 +109,7 @@
    2.13    |> map_filter I;
    2.14  
    2.15  (* TODO: test with sort constraints on As *)
    2.16 -fun mutualize_fp_sugars fp bs fpTs callers callssss fp_sugars0 no_defs_lthy0 =
    2.17 +fun mutualize_fp_sugars fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy0 =
    2.18    let
    2.19      val thy = Proof_Context.theory_of no_defs_lthy0;
    2.20  
    2.21 @@ -225,7 +225,7 @@
    2.22  
    2.23          val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
    2.24                 dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
    2.25 -          fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
    2.26 +          fp_bnf (construct_mutualized_fp fp cliques fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
    2.27              no_defs_lthy0;
    2.28  
    2.29          val fp_abs_inverses = map #abs_inverse fp_absT_infos;
    2.30 @@ -401,7 +401,7 @@
    2.31      val (num_groups, perm_Ts, perm_gen_Ts) = gather_types lthy [] 0 [] [] sorted_actual_Ts;
    2.32      val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts;
    2.33  
    2.34 -    val missing_Ts = subtract (op =) actual_Ts perm_Ts;
    2.35 +    val missing_Ts = fold (remove1 (op =)) actual_Ts perm_Ts;
    2.36      val Ts = actual_Ts @ missing_Ts;
    2.37  
    2.38      val nn = length Ts;
    2.39 @@ -424,10 +424,12 @@
    2.40  
    2.41      val perm_callssss = map2 (indexify_callsss o #ctrs o #ctr_sugar) perm_fp_sugars0 perm_callssss0;
    2.42  
    2.43 +    val perm_cliques = [] (*###*)
    2.44 +
    2.45      val ((perm_fp_sugars, fp_sugar_thms), lthy) =
    2.46        if num_groups > 1 then
    2.47 -        mutualize_fp_sugars fp perm_bs perm_frozen_gen_Ts perm_callers perm_callssss perm_fp_sugars0
    2.48 -          lthy
    2.49 +        mutualize_fp_sugars fp perm_cliques perm_bs perm_frozen_gen_Ts perm_callers perm_callssss
    2.50 +          perm_fp_sugars0 lthy
    2.51        else
    2.52          ((perm_fp_sugars0, (NONE, NONE)), lthy);
    2.53  
     3.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Apr 09 13:15:21 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Apr 09 18:22:11 2014 +0200
     3.3 @@ -81,7 +81,9 @@
     3.4        Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp;
     3.5  
     3.6      (* put nested types before the types that nest them, as needed for N2M *)
     3.7 -    val descr = reindex_desc (orig_descr' @ flat (rev nested_descrs));
     3.8 +    val descrs = burrow reindex_desc (orig_descr' :: rev nested_descrs);
     3.9 +    val (cliques, descr) =
    3.10 +      split_list (flat (map_index (fn (i, descr) => map (pair i) descr) descrs));
    3.11  
    3.12      val dest_dtyp = Datatype_Aux.typ_of_dtyp descr;
    3.13  
    3.14 @@ -108,7 +110,7 @@
    3.15  
    3.16      val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
    3.17        if nn > nn_fp then
    3.18 -        mutualize_fp_sugars Least_FP compat_bs Ts callers callssss fp_sugars0 lthy
    3.19 +        mutualize_fp_sugars Least_FP cliques compat_bs Ts callers callssss fp_sugars0 lthy
    3.20        else
    3.21          ((fp_sugars0, (NONE, NONE)), lthy);
    3.22