# HG changeset patch # User blanchet # Date 1458629822 -3600 # Node ID a3cccaef566a5b311921934c0273924758d98a8e # Parent 1c4842b32bfb3251cf9957d73bc4c6426bc6811b more general, reliable N2M diff -r 1c4842b32bfb -r a3cccaef566a src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy --- a/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy Tue Mar 22 07:57:02 2016 +0100 +++ b/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy Tue Mar 22 07:57:02 2016 +0100 @@ -102,7 +102,7 @@ codatatype 'a M = CM "('a, 'a M) M0" codatatype 'a N = CN "('a N, 'a) N0" codatatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0" - and ('a, 'b) L = CL "('b, ('a, 'b) K) L0" + and ('a, 'b) L = CL "('b, ('a, 'b) K) L0" codatatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0" primcorec @@ -144,12 +144,6 @@ datatype_compat ttttree *) -datatype ('a,'b)complex = - C1 nat "'a ttree" -| C2 "('a,'b)complex list tree tree" 'b "('a,'b)complex" "('a,'b)complex2 ttree list" -and ('a,'b)complex2 = D1 "('a,'b)complex ttree" -datatype_compat complex complex2 - datatype 'a F = F1 'a | F2 "'a F" datatype 'a G = G1 'a | G2 "'a G F" datatype H = H1 | H2 "H G" @@ -167,7 +161,6 @@ context linorder begin -(* slow *) primrec f1_tl :: "(nat, 'a) t l \ nat" and f1_t :: "(nat, 'a) t \ nat" @@ -176,7 +169,7 @@ "f1_tl (C t ts) = f1_t t + f1_tl ts" | "f1_t (T n _ ts) = n + f1_tl ts" -(* should be fast *) +(* should hit cache *) primrec f2_t :: "(nat, 'b) t \ nat" and f2_tl :: "(nat, 'b) t l \ nat" @@ -187,7 +180,7 @@ end -(* should be fast *) +(* should hit cache *) primrec g1_t :: "('a, int) t \ nat" and g1_tl :: "('a, int) t l \ nat" @@ -196,7 +189,7 @@ "g1_tl N = 0" | "g1_tl (C _ ts) = g1_tl ts" -(* should be fast *) +(* should hit cache *) primrec g2_t :: "(int, int) t \ nat" and g2_tl :: "(int, int) t l \ nat" @@ -223,7 +216,6 @@ ('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" and ('a, 'b) t2 = T2 "('a, 'b) t1" -(* slow *) primrec h1_tl1 :: "(nat, 'a) t1 l1 \ nat" and h1_tl2 :: "(nat, 'a) t1 l2 \ nat" and @@ -235,7 +227,7 @@ "h1_tl2 (C2 t ts) = h1_t1 t + h1_tl1 ts" | "h1_t1 (T1 n _ ts) = n + h1_tl1 ts" -(* should be fast *) +(* should hit cache *) primrec h2_tl1 :: "(nat, 'a) t1 l1 \ nat" and h2_tl2 :: "(nat, 'a) t1 l2 \ nat" and @@ -247,7 +239,7 @@ "h2_tl2 (C2 t ts) = h2_t1 t + h2_tl1 ts" | "h2_t1 (T1 n _ ts) = n + h2_tl1 ts" -(* should be fast *) +(* should hit cache *) primrec h3_tl2 :: "(nat, 'a) t1 l2 \ nat" and h3_tl1 :: "(nat, 'a) t1 l1 \ nat" and @@ -259,7 +251,7 @@ "h3_tl2 (C2 t ts) = h3_t1 t + h3_tl1 ts" | "h3_t1 (T1 n _ ts) = n + h3_tl1 ts" -(* should be fast *) +(* should hit cache *) primrec i1_tl2 :: "(nat, 'a) t1 l2 \ nat" and i1_tl1 :: "(nat, 'a) t1 l1 \ nat" and @@ -273,7 +265,7 @@ "i1_t1 (T1 n _ ts) = n + i1_tl1 ts" | "i1_t2 (T2 t) = i1_t1 t" -(* should be fast *) +(* should hit cache *) primrec j1_t2 :: "(nat, 'a) t2 \ nat" and j1_t1 :: "(nat, 'a) t1 \ nat" and @@ -292,7 +284,6 @@ datatype 'a l4 = N4 | C4 'a "'a l4" datatype ('a, 'b) t3 = T3 'a 'b "('a, 'b) t3 l3" "('a, 'b) t3 l4" -(* slow *) primrec k1_tl3 :: "(nat, 'a) t3 l3 \ nat" and k1_tl4 :: "(nat, 'a) t3 l4 \ nat" and @@ -304,7 +295,7 @@ "k1_tl4 (C4 t ts) = k1_t3 t + k1_tl4 ts" | "k1_t3 (T3 n _ ts us) = n + k1_tl3 ts + k1_tl4 us" -(* should be fast *) +(* should hit cache *) primrec k2_tl4 :: "(nat, int) t3 l4 \ nat" and k2_tl3 :: "(nat, int) t3 l3 \ nat" and @@ -321,7 +312,6 @@ datatype ('a, 'b) l6 = N6 | C6 'a 'b "('a, 'b) l6" datatype ('a, 'b, 'c) t4 = T4 'a 'b "(('a, 'b, 'c) t4, 'b) l5" "(('a, 'b, 'c) t4, 'c) l6" -(* slow *) primrec l1_tl5 :: "((nat, 'a, 'b) t4, 'a) l5 \ nat" and l1_tl6 :: "((nat, 'a, 'b) t4, 'b) l6 \ nat" and @@ -342,7 +332,6 @@ context linorder begin -(* slow *) primcorec f1_cotcol :: "nat \ (nat, 'a) cot col" and f1_cot :: "nat \ (nat, 'a) cot" @@ -351,7 +340,7 @@ "_ \ f1_cotcol n = C (f1_cot n) (f1_cotcol n)" | "f1_cot n = T n undefined (f1_cotcol n)" -(* should be fast *) +(* should hit cache *) primcorec f2_cotcol :: "nat \ (nat, 'b) cot col" and f2_cot :: "nat \ (nat, 'b) cot" @@ -362,7 +351,7 @@ end -(* should be fast *) +(* should hit cache *) primcorec g1_cot :: "int \ (int, 'a) cot" and g1_cotcol :: "int \ (int, 'a) cot col" @@ -371,7 +360,7 @@ "n = 0 \ g1_cotcol n = N" | "_ \ g1_cotcol n = C (g1_cot n) (g1_cotcol n)" -(* should be fast *) +(* should hit cache *) primcorec g2_cot :: "int \ (int, int) cot" and g2_cotcol :: "int \ (int, int) cot col" @@ -389,7 +378,6 @@ ('a, 'b) cot1 = T1 'a 'b "('a, 'b) cot1 col1" and ('a, 'b) cot2 = T2 "('a, 'b) cot1" -(* slow *) primcorec h1_cotcol1 :: "nat \ (nat, 'a) cot1 col1" and h1_cotcol2 :: "nat \ (nat, 'a) cot1 col2" and @@ -399,7 +387,7 @@ "h1_cotcol2 n = C2 (h1_cot1 n) (h1_cotcol1 n)" | "h1_cot1 n = T1 n undefined (h1_cotcol1 n)" -(* should be fast *) +(* should hit cache *) primcorec h2_cotcol1 :: "nat \ (nat, 'a) cot1 col1" and h2_cotcol2 :: "nat \ (nat, 'a) cot1 col2" and @@ -409,7 +397,7 @@ "h2_cotcol2 n = C2 (h2_cot1 n) (h2_cotcol1 n)" | "h2_cot1 n = T1 n undefined (h2_cotcol1 n)" -(* should be fast *) +(* should hit cache *) primcorec h3_cotcol2 :: "nat \ (nat, 'a) cot1 col2" and h3_cotcol1 :: "nat \ (nat, 'a) cot1 col1" and @@ -419,7 +407,7 @@ "h3_cotcol2 n = C2 (h3_cot1 n) (h3_cotcol1 n)" | "h3_cot1 n = T1 n undefined (h3_cotcol1 n)" -(* should be fast *) +(* should hit cache *) primcorec i1_cotcol2 :: "nat \ (nat, 'a) cot1 col2" and i1_cotcol1 :: "nat \ (nat, 'a) cot1 col1" and @@ -431,7 +419,7 @@ "i1_cot1 n = T1 n undefined (i1_cotcol1 n)" | "i1_cot2 n = T2 (i1_cot1 n)" -(* should be fast *) +(* should hit cache *) primcorec j1_cot2 :: "nat \ (nat, 'a) cot2" and j1_cot1 :: "nat \ (nat, 'a) cot1" and @@ -448,7 +436,6 @@ codatatype 'a col4 = N4 | C4 'a "'a col4" codatatype ('a, 'b) cot3 = T3 'a 'b "('a, 'b) cot3 col3" "('a, 'b) cot3 col4" -(* slow *) primcorec k1_cotcol3 :: "nat \ (nat, 'a) cot3 col3" and k1_cotcol4 :: "nat \ (nat, 'a) cot3 col4" and @@ -458,7 +445,7 @@ "k1_cotcol4 n = C4 (k1_cot3 n) (k1_cotcol4 n)" | "k1_cot3 n = T3 n undefined (k1_cotcol3 n) (k1_cotcol4 n)" -(* should be fast *) +(* should hit cache *) primcorec k2_cotcol4 :: "nat \ (nat, 'a) cot3 col4" and k2_cotcol3 :: "nat \ (nat, 'a) cot3 col3" and @@ -468,4 +455,10 @@ "k2_cotcol3 n = C3 (k2_cot3 n) (k2_cotcol3 n)" | "k2_cot3 n = T3 n undefined (k2_cotcol3 n) (k2_cotcol4 n)" +datatype ('a,'b)complex = + C1 nat "'a ttree" +| C2 "('a,'b)complex list tree tree" 'b "('a,'b)complex" "('a,'b)complex2 ttree list" +and ('a,'b)complex2 = D1 "('a,'b)complex ttree" +datatype_compat complex complex2 + end diff -r 1c4842b32bfb -r a3cccaef566a src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Mar 22 07:57:02 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Mar 22 07:57:02 2016 +0100 @@ -400,44 +400,38 @@ else not_co_datatype0 T | not_co_datatype T = not_co_datatype0 T; - fun not_mutually_nested_rec Ts1 Ts2 = - error (qsotys Ts1 ^ " is neither mutually " ^ co_prefix fp ^ "recursive with " ^ qsotys Ts2 ^ - " nor nested " ^ co_prefix fp ^ "recursive through " ^ - (if Ts1 = Ts2 andalso length Ts1 = 1 then "itself" else qsotys Ts2)); val sorted_actual_Ts = sort (prod_ord int_ord Term_Ord.typ_ord o apply2 (`Term.size_of_typ)) actual_Ts; fun the_ctrs_of (Type (s, Ts)) = map (mk_ctr Ts) (#ctrs (the (ctr_sugar_of lthy s))); + fun gen_rhss_in gen_Ts rho (subTs as Type (_, sub_tyargs) :: _) = + let + fun maybe_insert (T, Type (_, gen_tyargs)) = + member (op =) subTs T ? insert (op =) gen_tyargs + | maybe_insert _ = I; + + val gen_ctrs = maps the_ctrs_of gen_Ts; + val gen_ctr_Ts = maps (binder_types o fastype_of) gen_ctrs; + val ctr_Ts = map (Term.typ_subst_atomic rho) gen_ctr_Ts; + in + (case fold (fold_subtype_pairs maybe_insert) (ctr_Ts ~~ gen_ctr_Ts) [] of + [] => [map (typ_subst_nonatomic (map swap rho)) sub_tyargs] + | gen_tyargss => gen_tyargss) + end; + fun the_fp_sugar_of (T as Type (T_name, _)) = (case fp_sugar_of lthy T_name of SOME (fp_sugar as {fp = fp', ...}) => if fp = fp' then fp_sugar else not_co_datatype T | NONE => not_co_datatype T); - fun gen_rhss_in gen_Ts rho subTs = - let - fun maybe_insert (T, Type (_, gen_tyargs)) = - if member (op =) subTs T then insert (op =) gen_tyargs else I - | maybe_insert _ = I; - - val ctrs = maps the_ctrs_of gen_Ts; - val gen_ctr_Ts = maps (binder_types o fastype_of) ctrs; - val ctr_Ts = map (Term.typ_subst_atomic rho) gen_ctr_Ts; - in - fold (fold_subtype_pairs maybe_insert) (ctr_Ts ~~ gen_ctr_Ts) [] - end; - fun gather_types _ _ rev_seens gen_seen [] = (rev rev_seens, gen_seen) | gather_types lthy rho rev_seens gen_seen ((T as Type (_, tyargs)) :: Ts) = let val {T = Type (_, tyargs0), fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T; val mutual_Ts = map (retypargs tyargs) mutual_Ts0; - val rev_seen = flat rev_seens; - val _ = null rev_seens orelse exists (exists_strict_subtype_in rev_seen) mutual_Ts orelse - not_mutually_nested_rec mutual_Ts rev_seen; - fun fresh_tyargs () = let val (unsorted_gen_tyargs, lthy') = @@ -451,7 +445,7 @@ end; val (rho', gen_tyargs, gen_seen', lthy') = - if exists (exists_subtype_in rev_seen) mutual_Ts then + if exists (exists_subtype_in (flat rev_seens)) mutual_Ts then (case gen_rhss_in gen_seen rho mutual_Ts of [] => fresh_tyargs () | gen_tyargs :: gen_tyargss_tl =>