more general, reliable N2M
authorblanchet
Tue Mar 22 07:57:02 2016 +0100 (2016-03-22)
changeset 62688a3cccaef566a
parent 62687 1c4842b32bfb
child 62689 9b8b3db6ac03
more general, reliable N2M
src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
     1.1 --- a/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy	Tue Mar 22 07:57:02 2016 +0100
     1.2 +++ b/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy	Tue Mar 22 07:57:02 2016 +0100
     1.3 @@ -102,7 +102,7 @@
     1.4  codatatype 'a M = CM "('a, 'a M) M0"
     1.5  codatatype 'a N = CN "('a N, 'a) N0"
     1.6  codatatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0"
     1.7 -         and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
     1.8 +       and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
     1.9  codatatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0"
    1.10  
    1.11  primcorec
    1.12 @@ -144,12 +144,6 @@
    1.13  datatype_compat ttttree
    1.14  *)
    1.15  
    1.16 -datatype ('a,'b)complex = 
    1.17 -  C1 nat "'a ttree" 
    1.18 -| C2 "('a,'b)complex list tree tree" 'b "('a,'b)complex" "('a,'b)complex2 ttree list"
    1.19 -and ('a,'b)complex2 = D1 "('a,'b)complex ttree"
    1.20 -datatype_compat complex complex2
    1.21 -
    1.22  datatype 'a F = F1 'a | F2 "'a F"
    1.23  datatype 'a G = G1 'a | G2 "'a G F"
    1.24  datatype H = H1 | H2 "H G"
    1.25 @@ -167,7 +161,6 @@
    1.26  context linorder
    1.27  begin
    1.28  
    1.29 -(* slow *)
    1.30  primrec
    1.31    f1_tl :: "(nat, 'a) t l \<Rightarrow> nat" and
    1.32    f1_t :: "(nat, 'a) t \<Rightarrow> nat"
    1.33 @@ -176,7 +169,7 @@
    1.34    "f1_tl (C t ts) = f1_t t + f1_tl ts" |
    1.35    "f1_t (T n _ ts) = n + f1_tl ts"
    1.36  
    1.37 -(* should be fast *)
    1.38 +(* should hit cache *)
    1.39  primrec
    1.40    f2_t :: "(nat, 'b) t \<Rightarrow> nat" and
    1.41    f2_tl :: "(nat, 'b) t l \<Rightarrow> nat"
    1.42 @@ -187,7 +180,7 @@
    1.43  
    1.44  end
    1.45  
    1.46 -(* should be fast *)
    1.47 +(* should hit cache *)
    1.48  primrec
    1.49    g1_t :: "('a, int) t \<Rightarrow> nat" and
    1.50    g1_tl :: "('a, int) t l \<Rightarrow> nat"
    1.51 @@ -196,7 +189,7 @@
    1.52    "g1_tl N = 0" |
    1.53    "g1_tl (C _ ts) = g1_tl ts"
    1.54  
    1.55 -(* should be fast *)
    1.56 +(* should hit cache *)
    1.57  primrec
    1.58    g2_t :: "(int, int) t \<Rightarrow> nat" and
    1.59    g2_tl :: "(int, int) t l \<Rightarrow> nat"
    1.60 @@ -223,7 +216,6 @@
    1.61    ('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" and
    1.62    ('a, 'b) t2 = T2 "('a, 'b) t1"
    1.63  
    1.64 -(* slow *)
    1.65  primrec
    1.66    h1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
    1.67    h1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
    1.68 @@ -235,7 +227,7 @@
    1.69    "h1_tl2 (C2 t ts) = h1_t1 t + h1_tl1 ts" |
    1.70    "h1_t1 (T1 n _ ts) = n + h1_tl1 ts"
    1.71  
    1.72 -(* should be fast *)
    1.73 +(* should hit cache *)
    1.74  primrec
    1.75    h2_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
    1.76    h2_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
    1.77 @@ -247,7 +239,7 @@
    1.78    "h2_tl2 (C2 t ts) = h2_t1 t + h2_tl1 ts" |
    1.79    "h2_t1 (T1 n _ ts) = n + h2_tl1 ts"
    1.80  
    1.81 -(* should be fast *)
    1.82 +(* should hit cache *)
    1.83  primrec
    1.84    h3_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
    1.85    h3_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
    1.86 @@ -259,7 +251,7 @@
    1.87    "h3_tl2 (C2 t ts) = h3_t1 t + h3_tl1 ts" |
    1.88    "h3_t1 (T1 n _ ts) = n + h3_tl1 ts"
    1.89  
    1.90 -(* should be fast *)
    1.91 +(* should hit cache *)
    1.92  primrec
    1.93    i1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
    1.94    i1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
    1.95 @@ -273,7 +265,7 @@
    1.96    "i1_t1 (T1 n _ ts) = n + i1_tl1 ts" |
    1.97    "i1_t2 (T2 t) = i1_t1 t"
    1.98  
    1.99 -(* should be fast *)
   1.100 +(* should hit cache *)
   1.101  primrec
   1.102    j1_t2 :: "(nat, 'a) t2 \<Rightarrow> nat" and
   1.103    j1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" and
   1.104 @@ -292,7 +284,6 @@
   1.105  datatype 'a l4 = N4 | C4 'a "'a l4"
   1.106  datatype ('a, 'b) t3 = T3 'a 'b "('a, 'b) t3 l3" "('a, 'b) t3 l4"
   1.107  
   1.108 -(* slow *)
   1.109  primrec
   1.110    k1_tl3 :: "(nat, 'a) t3 l3 \<Rightarrow> nat" and
   1.111    k1_tl4 :: "(nat, 'a) t3 l4 \<Rightarrow> nat" and
   1.112 @@ -304,7 +295,7 @@
   1.113    "k1_tl4 (C4 t ts) = k1_t3 t + k1_tl4 ts" |
   1.114    "k1_t3 (T3 n _ ts us) = n + k1_tl3 ts + k1_tl4 us"
   1.115  
   1.116 -(* should be fast *)
   1.117 +(* should hit cache *)
   1.118  primrec
   1.119    k2_tl4 :: "(nat, int) t3 l4 \<Rightarrow> nat" and
   1.120    k2_tl3 :: "(nat, int) t3 l3 \<Rightarrow> nat" and
   1.121 @@ -321,7 +312,6 @@
   1.122  datatype ('a, 'b) l6 = N6 | C6 'a 'b "('a, 'b) l6"
   1.123  datatype ('a, 'b, 'c) t4 = T4 'a 'b "(('a, 'b, 'c) t4, 'b) l5" "(('a, 'b, 'c) t4, 'c) l6"
   1.124  
   1.125 -(* slow *)
   1.126  primrec
   1.127    l1_tl5 :: "((nat, 'a, 'b) t4, 'a) l5 \<Rightarrow> nat" and
   1.128    l1_tl6 :: "((nat, 'a, 'b) t4, 'b) l6 \<Rightarrow> nat" and
   1.129 @@ -342,7 +332,6 @@
   1.130  context linorder
   1.131  begin
   1.132  
   1.133 -(* slow *)
   1.134  primcorec
   1.135    f1_cotcol :: "nat \<Rightarrow> (nat, 'a) cot col" and
   1.136    f1_cot :: "nat \<Rightarrow> (nat, 'a) cot"
   1.137 @@ -351,7 +340,7 @@
   1.138    "_ \<Longrightarrow> f1_cotcol n = C (f1_cot n) (f1_cotcol n)" |
   1.139    "f1_cot n = T n undefined (f1_cotcol n)"
   1.140  
   1.141 -(* should be fast *)
   1.142 +(* should hit cache *)
   1.143  primcorec
   1.144    f2_cotcol :: "nat \<Rightarrow> (nat, 'b) cot col" and
   1.145    f2_cot :: "nat \<Rightarrow> (nat, 'b) cot"
   1.146 @@ -362,7 +351,7 @@
   1.147  
   1.148  end
   1.149  
   1.150 -(* should be fast *)
   1.151 +(* should hit cache *)
   1.152  primcorec
   1.153    g1_cot :: "int \<Rightarrow> (int, 'a) cot" and
   1.154    g1_cotcol :: "int \<Rightarrow> (int, 'a) cot col"
   1.155 @@ -371,7 +360,7 @@
   1.156    "n = 0 \<Longrightarrow> g1_cotcol n = N" |
   1.157    "_ \<Longrightarrow> g1_cotcol n = C (g1_cot n) (g1_cotcol n)"
   1.158  
   1.159 -(* should be fast *)
   1.160 +(* should hit cache *)
   1.161  primcorec
   1.162    g2_cot :: "int \<Rightarrow> (int, int) cot" and
   1.163    g2_cotcol :: "int \<Rightarrow> (int, int) cot col"
   1.164 @@ -389,7 +378,6 @@
   1.165    ('a, 'b) cot1 = T1 'a 'b "('a, 'b) cot1 col1" and
   1.166    ('a, 'b) cot2 = T2 "('a, 'b) cot1"
   1.167  
   1.168 -(* slow *)
   1.169  primcorec
   1.170    h1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   1.171    h1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
   1.172 @@ -399,7 +387,7 @@
   1.173    "h1_cotcol2 n = C2 (h1_cot1 n) (h1_cotcol1 n)" |
   1.174    "h1_cot1 n = T1 n undefined (h1_cotcol1 n)"
   1.175  
   1.176 -(* should be fast *)
   1.177 +(* should hit cache *)
   1.178  primcorec
   1.179    h2_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   1.180    h2_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
   1.181 @@ -409,7 +397,7 @@
   1.182    "h2_cotcol2 n = C2 (h2_cot1 n) (h2_cotcol1 n)" |
   1.183    "h2_cot1 n = T1 n undefined (h2_cotcol1 n)"
   1.184  
   1.185 -(* should be fast *)
   1.186 +(* should hit cache *)
   1.187  primcorec
   1.188    h3_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
   1.189    h3_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   1.190 @@ -419,7 +407,7 @@
   1.191    "h3_cotcol2 n = C2 (h3_cot1 n) (h3_cotcol1 n)" |
   1.192    "h3_cot1 n = T1 n undefined (h3_cotcol1 n)"
   1.193  
   1.194 -(* should be fast *)
   1.195 +(* should hit cache *)
   1.196  primcorec
   1.197    i1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
   1.198    i1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   1.199 @@ -431,7 +419,7 @@
   1.200    "i1_cot1 n = T1 n undefined (i1_cotcol1 n)" |
   1.201    "i1_cot2 n = T2 (i1_cot1 n)"
   1.202  
   1.203 -(* should be fast *)
   1.204 +(* should hit cache *)
   1.205  primcorec
   1.206    j1_cot2 :: "nat \<Rightarrow> (nat, 'a) cot2" and
   1.207    j1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" and
   1.208 @@ -448,7 +436,6 @@
   1.209  codatatype 'a col4 = N4 | C4 'a "'a col4"
   1.210  codatatype ('a, 'b) cot3 = T3 'a 'b "('a, 'b) cot3 col3" "('a, 'b) cot3 col4"
   1.211  
   1.212 -(* slow *)
   1.213  primcorec
   1.214    k1_cotcol3 :: "nat \<Rightarrow> (nat, 'a) cot3 col3" and
   1.215    k1_cotcol4 :: "nat \<Rightarrow> (nat, 'a) cot3 col4" and
   1.216 @@ -458,7 +445,7 @@
   1.217    "k1_cotcol4 n = C4 (k1_cot3 n) (k1_cotcol4 n)" |
   1.218    "k1_cot3 n = T3 n undefined (k1_cotcol3 n) (k1_cotcol4 n)"
   1.219  
   1.220 -(* should be fast *)
   1.221 +(* should hit cache *)
   1.222  primcorec
   1.223    k2_cotcol4 :: "nat \<Rightarrow> (nat, 'a) cot3 col4" and
   1.224    k2_cotcol3 :: "nat \<Rightarrow> (nat, 'a) cot3 col3" and
   1.225 @@ -468,4 +455,10 @@
   1.226    "k2_cotcol3 n = C3 (k2_cot3 n) (k2_cotcol3 n)" |
   1.227    "k2_cot3 n = T3 n undefined (k2_cotcol3 n) (k2_cotcol4 n)"
   1.228  
   1.229 +datatype ('a,'b)complex =
   1.230 +  C1 nat "'a ttree"
   1.231 +| C2 "('a,'b)complex list tree tree" 'b "('a,'b)complex" "('a,'b)complex2 ttree list"
   1.232 +and ('a,'b)complex2 = D1 "('a,'b)complex ttree"
   1.233 +datatype_compat complex complex2
   1.234 +
   1.235  end
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Mar 22 07:57:02 2016 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Mar 22 07:57:02 2016 +0100
     2.3 @@ -400,44 +400,38 @@
     2.4          else
     2.5            not_co_datatype0 T
     2.6        | not_co_datatype T = not_co_datatype0 T;
     2.7 -    fun not_mutually_nested_rec Ts1 Ts2 =
     2.8 -      error (qsotys Ts1 ^ " is neither mutually " ^ co_prefix fp ^ "recursive with " ^ qsotys Ts2 ^
     2.9 -        " nor nested " ^ co_prefix fp ^ "recursive through " ^
    2.10 -        (if Ts1 = Ts2 andalso length Ts1 = 1 then "itself" else qsotys Ts2));
    2.11  
    2.12      val sorted_actual_Ts =
    2.13        sort (prod_ord int_ord Term_Ord.typ_ord o apply2 (`Term.size_of_typ)) actual_Ts;
    2.14  
    2.15      fun the_ctrs_of (Type (s, Ts)) = map (mk_ctr Ts) (#ctrs (the (ctr_sugar_of lthy s)));
    2.16  
    2.17 +    fun gen_rhss_in gen_Ts rho (subTs as Type (_, sub_tyargs) :: _) =
    2.18 +      let
    2.19 +        fun maybe_insert (T, Type (_, gen_tyargs)) =
    2.20 +            member (op =) subTs T ? insert (op =) gen_tyargs
    2.21 +          | maybe_insert _ = I;
    2.22 +
    2.23 +        val gen_ctrs = maps the_ctrs_of gen_Ts;
    2.24 +        val gen_ctr_Ts = maps (binder_types o fastype_of) gen_ctrs;
    2.25 +        val ctr_Ts = map (Term.typ_subst_atomic rho) gen_ctr_Ts;
    2.26 +      in
    2.27 +        (case fold (fold_subtype_pairs maybe_insert) (ctr_Ts ~~ gen_ctr_Ts) [] of
    2.28 +          [] => [map (typ_subst_nonatomic (map swap rho)) sub_tyargs]
    2.29 +        | gen_tyargss => gen_tyargss)
    2.30 +      end;
    2.31 +
    2.32      fun the_fp_sugar_of (T as Type (T_name, _)) =
    2.33        (case fp_sugar_of lthy T_name of
    2.34          SOME (fp_sugar as {fp = fp', ...}) => if fp = fp' then fp_sugar else not_co_datatype T
    2.35        | NONE => not_co_datatype T);
    2.36  
    2.37 -    fun gen_rhss_in gen_Ts rho subTs =
    2.38 -      let
    2.39 -        fun maybe_insert (T, Type (_, gen_tyargs)) =
    2.40 -            if member (op =) subTs T then insert (op =) gen_tyargs else I
    2.41 -          | maybe_insert _ = I;
    2.42 -
    2.43 -        val ctrs = maps the_ctrs_of gen_Ts;
    2.44 -        val gen_ctr_Ts = maps (binder_types o fastype_of) ctrs;
    2.45 -        val ctr_Ts = map (Term.typ_subst_atomic rho) gen_ctr_Ts;
    2.46 -      in
    2.47 -        fold (fold_subtype_pairs maybe_insert) (ctr_Ts ~~ gen_ctr_Ts) []
    2.48 -      end;
    2.49 -
    2.50      fun gather_types _ _ rev_seens gen_seen [] = (rev rev_seens, gen_seen)
    2.51        | gather_types lthy rho rev_seens gen_seen ((T as Type (_, tyargs)) :: Ts) =
    2.52          let
    2.53            val {T = Type (_, tyargs0), fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T;
    2.54            val mutual_Ts = map (retypargs tyargs) mutual_Ts0;
    2.55  
    2.56 -          val rev_seen = flat rev_seens;
    2.57 -          val _ = null rev_seens orelse exists (exists_strict_subtype_in rev_seen) mutual_Ts orelse
    2.58 -            not_mutually_nested_rec mutual_Ts rev_seen;
    2.59 -
    2.60            fun fresh_tyargs () =
    2.61              let
    2.62                val (unsorted_gen_tyargs, lthy') =
    2.63 @@ -451,7 +445,7 @@
    2.64              end;
    2.65  
    2.66            val (rho', gen_tyargs, gen_seen', lthy') =
    2.67 -            if exists (exists_subtype_in rev_seen) mutual_Ts then
    2.68 +            if exists (exists_subtype_in (flat rev_seens)) mutual_Ts then
    2.69                (case gen_rhss_in gen_seen rho mutual_Ts of
    2.70                  [] => fresh_tyargs ()
    2.71                | gen_tyargs :: gen_tyargss_tl =>