# HG changeset patch
# User blanchet
# Date 1347131066 -7200
# Node ID 73f9aede57a4efb516f693c8efe81a045e8857f1
# Parent  7c9a3c67c55d06643802c9f1451276c207ba1228
correctly curry recursor arguments

diff -r 7c9a3c67c55d -r 73f9aede57a4 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -23,6 +23,11 @@
 
 fun retype_free (Free (s, _)) T = Free (s, T);
 
+fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
+fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs;
+fun mk_doubly_uncurried_fun f xss =
+  mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss);
+
 fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters";
 
 fun merge_type_arg_constrained ctxt (T, c) (T', c') =
@@ -242,6 +247,10 @@
         val mss = map (map length) ctr_Tsss;
         val Css = map2 replicate ns Cs;
 
+        fun dest_rec_pair (T as Type (@{type_name prod}, Us as [_, U])) =
+            if member (op =) Cs U then Us else [T]
+          | dest_rec_pair T = [T];
+
         fun sugar_datatype no_defs_lthy =
           let
             val fp_y_Ts = map domain_type (fst (split_last (binder_types (fastype_of fp_iter))));
@@ -253,7 +262,8 @@
             val fp_z_Ts = map domain_type (fst (split_last (binder_types (fastype_of fp_rec))));
             val z_prod_Tss = map2 dest_sumTN ns fp_z_Ts;
             val z_Tsss = map2 (map2 dest_tupleT) mss z_prod_Tss;
-            val h_Tss = map2 (map2 (curry (op --->))) z_Tsss Css;
+            val z_Tssss = map (map (map dest_rec_pair)) z_Tsss;
+            val h_Tss = map2 (map2 (fold_rev (curry (op --->)))) z_Tssss Css;
             val rec_T = flat h_Tss ---> fp_T --> C;
 
             val ((gss, ysss), _) =
@@ -262,9 +272,9 @@
               ||>> mk_Freesss "x" y_Tsss;
 
             val hss = map2 (map2 retype_free) gss h_Tss;
-            val (zsss, _) =
+            val (zssss, _) =
               no_defs_lthy
-              |> mk_Freesss "x" z_Tsss;
+              |> mk_Freessss "x" z_Tssss;
 
             val iter_binder = Binding.suffix_name ("_" ^ iterN) b;
             val rec_binder = Binding.suffix_name ("_" ^ recN) b;
@@ -277,7 +287,8 @@
                 Term.list_comb (fp_iter, map2 (mk_sum_caseN oo map2 mk_uncurried_fun) gss ysss));
             val rec_spec =
               mk_Trueprop_eq (fold (fn hs => fn t => Term.list_comb (t, hs)) hss rec_free,
-                Term.list_comb (fp_rec, map2 (mk_sum_caseN oo map2 mk_uncurried_fun) hss zsss));
+                Term.list_comb (fp_rec,
+                  map2 (mk_sum_caseN oo map2 mk_doubly_uncurried_fun) hss zssss));
 
             val (([raw_iter, raw_rec], [raw_iter_def, raw_rec_def]), (lthy', lthy)) = no_defs_lthy
               |> apfst split_list o fold_map (fn (b, spec) =>
diff -r 7c9a3c67c55d -r 73f9aede57a4 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -91,8 +91,6 @@
   val dest_sumTN: int -> typ -> typ list
   val dest_tupleT: int -> typ -> typ list
 
-  val mk_uncurried_fun: term -> term list -> term
-
   val mk_Field: term -> term
   val mk_union: term * term -> term
 
@@ -232,8 +230,6 @@
   | dest_tupleT 1 T = [T]
   | dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T';
 
-fun mk_uncurried_fun f xs = HOLogic.tupled_lambda (HOLogic.mk_tuple xs) (Term.list_comb (f, xs));
-
 fun mk_Field r =
   let val T = fst (dest_relT (fastype_of r));
   in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;
diff -r 7c9a3c67c55d -r 73f9aede57a4 src/HOL/Codatatype/Tools/bnf_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -50,6 +50,8 @@
   val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context
   val mk_Freesss: string -> typ list list list -> Proof.context ->
     term list list list * Proof.context
+  val mk_Freessss: string -> typ list list list list -> Proof.context ->
+    term list list list list * Proof.context
   val mk_Frees': string -> typ list -> Proof.context ->
     (term list * (string * typ) list) * Proof.context
   val mk_Freess': string -> typ list list -> Proof.context ->
@@ -274,6 +276,7 @@
 fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
 fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
 fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss;
+fun mk_Freessss x Tssss = fold_map2 mk_Freesss (mk_names (length Tssss) x) Tssss;
 fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
 fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;