# HG changeset patch # User blanchet # Date 1383626888 -3600 # Node ID d1478807f287721dada865e23187c6da02239429 # Parent 04cd231e2b9e396bee840619e0defe7a32b73335 generalize types when synthetizing n2m (co)recursors, to facilitate reuse diff -r 04cd231e2b9e -r d1478807f287 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Tue Nov 05 05:48:08 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Tue Nov 05 05:48:08 2013 +0100 @@ -295,10 +295,19 @@ | check_enrich_with_mutuals _ (T :: _) = not_co_datatype T; val perm_Ts = check_enrich_with_mutuals [] perm_actual_Ts; - val missing_Ts = perm_Ts |> subtract (op =) actual_Ts; val Ts = actual_Ts @ missing_Ts; + fun generalize_type (T as Type (s, Ts)) (seen_lthy as (seen, lthy)) = + (case AList.lookup (op =) seen T of + SOME U => (U, seen_lthy) + | NONE => + if exists_subtype_in Ts T then fold_map generalize_type Ts seen_lthy |>> curry Type s + else mk_TFrees 1 lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy)))) + | generalize_type T seen_lthy = (T, seen_lthy); + + val (perm_Us, _) = fold_map generalize_type perm_Ts ([], lthy); + val nn = length Ts; val kks = 0 upto nn - 1; @@ -318,7 +327,7 @@ val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices; val ((perm_fp_sugars, fp_sugar_thms), lthy) = - mutualize_fp_sugars has_nested fp perm_bs perm_Ts get_perm_indices perm_callssss + mutualize_fp_sugars has_nested fp perm_bs perm_Us get_perm_indices perm_callssss perm_fp_sugars0 lthy; val fp_sugars = unpermute perm_fp_sugars;