1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 21:40:41 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 22:42:54 2013 +0100
     1.3 @@ -264,14 +264,20 @@
     1.4  fun indexify_callsss fp_sugar callsss =
     1.5    let
     1.6      val {ctrs, ...} = of_fp_sugar #ctr_sugars fp_sugar;
     1.7 -    fun do_ctr ctr =
     1.8 +    fun indexify_ctr ctr =
     1.9        (case AList.lookup Term.aconv_untyped callsss ctr of
    1.10          NONE => replicate (num_binder_types (fastype_of ctr)) []
    1.11        | SOME callss => map (map (Envir.beta_eta_contract o unfold_let)) callss);
    1.12    in
    1.13 -    map do_ctr ctrs
    1.14 +    map indexify_ctr ctrs
    1.15    end;
    1.16  
    1.17 +fun retypargs tyargs (Type (s, _)) = Type (s, tyargs);
    1.18 +
    1.19 +fun fold_subtype_pairs f (T as Type (s, Ts), U as Type (s', Us)) =
    1.20 +    f (T, U) #> (if s = s' then fold (fold_subtype_pairs f) (Ts ~~ Us) else I)
    1.21 +  | fold_subtype_pairs f TU = f TU;
    1.22 +
    1.23  fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
    1.24    let
    1.25      val qsoty = quote o Syntax.string_of_typ lthy;
    1.26 @@ -292,23 +298,70 @@
    1.27      val perm_actual_Ts as Type (_, tyargs0) :: _ =
    1.28        sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts;
    1.29  
    1.30 +    fun the_ctrs_of (Type (s, Ts)) = map (mk_ctr Ts) (#ctrs (the (ctr_sugar_of lthy s)));
    1.31 +
    1.32      fun the_fp_sugar_of (T as Type (T_name, _)) =
    1.33        (case fp_sugar_of lthy T_name of
    1.34          SOME (fp_sugar as {fp = fp', ...}) => if fp = fp' then fp_sugar else not_co_datatype T
    1.35        | NONE => not_co_datatype T);
    1.36  
    1.37 -    fun check_enrich_with_mutuals _ [] = []
    1.38 -      | check_enrich_with_mutuals seen ((T as Type (_, tyargs)) :: Ts) =
    1.39 +    fun gen_rhss_in gen_Ts rho subTs =
    1.40 +      let
    1.41 +        fun maybe_insert (T, Type (_, gen_tyargs)) =
    1.42 +            if member (op =) subTs T then insert (op =) gen_tyargs else I
    1.43 +          | maybe_insert _ = I;
    1.44 +
    1.45 +        val ctrs = maps the_ctrs_of gen_Ts;
    1.46 +        val gen_ctr_Ts = maps (binder_types o fastype_of) ctrs;
    1.47 +        val ctr_Ts = map (Term.typ_subst_atomic rho) gen_ctr_Ts;
    1.48 +      in
    1.49 +        fold (fold_subtype_pairs maybe_insert) (ctr_Ts ~~ gen_ctr_Ts) []
    1.50 +      end;
    1.51 +
    1.52 +    fun check_enrich_with_mutuals _ _ seen gen_seen [] = (seen, gen_seen)
    1.53 +      | check_enrich_with_mutuals lthy rho seen gen_seen ((T as Type (_, tyargs)) :: Ts) =
    1.54          let
    1.55 -          val {fp_res = {Ts = Ts', ...}, ...} = the_fp_sugar_of T
    1.56 -          val mutual_Ts = map (fn Type (s, _) => Type (s, tyargs)) Ts';
    1.57 -          val (seen', Ts') = List.partition (member (op =) mutual_Ts) Ts;
    1.58 +          val {fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T;
    1.59 +          val mutual_Ts = map (retypargs tyargs) mutual_Ts0;
    1.60 +
    1.61 +          fun fresh_tyargs () =
    1.62 +            let
    1.63 +              (* The name "'z" is unlikely to clash with the context, yielding more cache hits. *)
    1.64 +              val (gen_tyargs, lthy') =
    1.65 +                variant_tfrees (replicate (length tyargs) "z") lthy
    1.66 +                |>> map Logic.varifyT_global;
    1.67 +              val rho' = (gen_tyargs ~~ tyargs) @ rho;
    1.68 +            in
    1.69 +              (rho', gen_tyargs, gen_seen, lthy')
    1.70 +            end;
    1.71 +
    1.72 +          val (rho', gen_tyargs, gen_seen', lthy') =
    1.73 +            if exists (exists_subtype_in seen) mutual_Ts then
    1.74 +              (case gen_rhss_in gen_seen rho mutual_Ts of
    1.75 +                [] => fresh_tyargs ()
    1.76 +              | [gen_tyargs] => (rho, gen_tyargs, gen_seen, lthy)
    1.77 +              | gen_tyargss as gen_tyargs :: gen_tyargss_tl =>
    1.78 +                let
    1.79 +                  val unify_pairs = split_list (maps (curry (op ~~) gen_tyargs) gen_tyargss_tl);
    1.80 +                  val mgu = Type.raw_unifys unify_pairs Vartab.empty;
    1.81 +                  val gen_tyargs' = map (Envir.subst_type mgu) gen_tyargs;
    1.82 +                  val gen_seen' = map (Envir.subst_type mgu) gen_seen;
    1.83 +                in
    1.84 +                  (rho, gen_tyargs', gen_seen', lthy)
    1.85 +                end)
    1.86 +            else
    1.87 +              fresh_tyargs ();
    1.88 +
    1.89 +          val gen_mutual_Ts = map (retypargs gen_tyargs) mutual_Ts0;
    1.90 +          val Ts' = filter_out (member (op =) mutual_Ts) Ts;
    1.91          in
    1.92 -          mutual_Ts @ check_enrich_with_mutuals (seen @ T :: seen') Ts'
    1.93 +          check_enrich_with_mutuals lthy' rho' (seen @ mutual_Ts) (gen_seen' @ gen_mutual_Ts) Ts'
    1.94          end
    1.95 -      | check_enrich_with_mutuals _ (T :: _) = not_co_datatype T;
    1.96 +      | check_enrich_with_mutuals _ _ _ _ (T :: _) = not_co_datatype T;
    1.97  
    1.98 -    val perm_Ts = check_enrich_with_mutuals [] perm_actual_Ts;
    1.99 +    val (perm_Ts, perm_gen_Ts) = check_enrich_with_mutuals lthy [] [] [] perm_actual_Ts;
   1.100 +    val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts;
   1.101 +
   1.102      val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
   1.103      val Ts = actual_Ts @ missing_Ts;
   1.104  
   1.105 @@ -334,7 +387,7 @@
   1.106      val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
   1.107  
   1.108      val ((perm_fp_sugars, fp_sugar_thms), lthy) =
   1.109 -      mutualize_fp_sugars has_nested fp perm_bs perm_Ts get_perm_indices perm_callssss
   1.110 +      mutualize_fp_sugars has_nested fp perm_bs perm_frozen_gen_Ts get_perm_indices perm_callssss
   1.111          perm_fp_sugars0 lthy;
   1.112  
   1.113      val fp_sugars = unpermute perm_fp_sugars;