# HG changeset patch
# User panny
# Date 1382116712 -7200
# Node ID 496f9af15b39d985f4e09419b201c09e3cbba8aa
# Parent  a179353111db7746d8eaa4019fa74cfe317e816f# Parent  eb5d58c990490e828d48db7d903dc6c421e9d1d1
merge

diff -r a179353111db -r 496f9af15b39 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Oct 18 19:03:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Oct 18 19:18:32 2013 +0200
@@ -232,7 +232,6 @@
   | flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) =
     p :: flat_corec_predss_getterss qss fss @ flat_corec_preds_predsss_gettersss ps qsss fsss;
 
-fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
 fun mk_uncurried2_fun f xss =
   mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat_rec_arg_args xss);
 
diff -r a179353111db -r 496f9af15b39 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 19:03:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 19:18:32 2013 +0200
@@ -172,27 +172,30 @@
   let
     fun subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
       | subst bound_Ts (t as g' $ y) =
-        if not (member (op =) ctr_args y) then
-          pairself (subst bound_Ts) (g', y) |> op $
-        else
-          let
-            val maybe_mutual_y' = AList.lookup (op =) mutual_calls y;
-            val maybe_nested_y' = AList.lookup (op =) nested_calls y;
-            val (g, g_args) = strip_comb g';
-            val ctr_pos = try (get_ctr_pos o the) (free_name g) |> the_default ~1;
-            val _ = ctr_pos < 0 orelse length g_args >= ctr_pos orelse
-              primrec_error_eqn "too few arguments in recursive call" t;
-          in
-            if ctr_pos >= 0 then
-              list_comb (the maybe_mutual_y', g_args)
-            else if is_some maybe_nested_y' then
-              (if has_call g' then t else y)
-              |> massage_nested_rec_call lthy has_call
-                (rewrite_map_arg get_ctr_pos) bound_Ts y (the maybe_nested_y')
-              |> (if has_call g' then I else curry (op $) g')
-            else
-              t
-          end
+        let val y_head = head_of y in
+          if not (member (op =) ctr_args y_head) then
+            pairself (subst bound_Ts) (g', y) |> op $
+          else
+            let
+              val maybe_mutual_y' = AList.lookup (op =) mutual_calls y;
+              val maybe_nested_y_head' = AList.lookup (op =) nested_calls y_head;
+              val (g, g_args) = strip_comb g';
+              val ctr_pos = try (get_ctr_pos o the) (free_name g) |> the_default ~1;
+              val _ = ctr_pos < 0 orelse length g_args >= ctr_pos orelse
+                primrec_error_eqn "too few arguments in recursive call" t;
+            in
+              if ctr_pos >= 0 then
+                list_comb (the maybe_mutual_y', g_args)
+              else if is_some maybe_nested_y_head' then
+                (if has_call g' then t else y)
+                |> massage_nested_rec_call lthy has_call
+                  (rewrite_map_arg get_ctr_pos) bound_Ts y_head (the maybe_nested_y_head')
+                |> (if has_call g' then I else curry (op $) g')
+              else
+                t
+            end
+            |> tap (fn t => tracing ("*** " ^ Syntax.string_of_term lthy t)) (*###*)
+        end
       | subst _ t = t
   in
     subst [] t
@@ -583,7 +586,7 @@
       else apfst SOME (dissect_coeqn_disc seq fun_names basic_ctr_specss
           (SOME (abstract (List.rev fun_args) rhs)) maybe_code_rhs prems disc_concl matchedsss);
 
-    val sel_concls = (sels ~~ ctr_args)
+    val sel_concls = sels ~~ ctr_args
       |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg));
 
 (*
@@ -838,7 +841,8 @@
       map_filter (try (fn Sel x => x)) eqns_data
       |> partition_eq ((op =) o pairself #fun_name)
       |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
-      |> map (flat o snd)      |> map2 (fold o find_corec_calls has_call) basic_ctr_specss
+      |> map (flat o snd)
+      |> map2 (fold o find_corec_calls has_call) basic_ctr_specss
       |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
         (ctr, map (K []) sels))) basic_ctr_specss);
 
diff -r a179353111db -r 496f9af15b39 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Oct 18 19:03:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Oct 18 19:18:32 2013 +0200
@@ -215,6 +215,19 @@
     SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt
   | NONE => invalid_map ctxt);
 
+fun expand_to_comp bound_Ts f t =
+  let
+    val (g, xs) = Term.strip_comb t;
+    val m = length xs;
+    val j = Term.maxidx_of_term t;
+    val us = map2 (fn k => fn x => Var ((Name.uu, j + k), fastype_of1 (bound_Ts, x))) (1 upto m) xs;
+    val u_tuple = HOLogic.mk_tuple us;
+    val unc_g = mk_tupled_fun u_tuple g us;
+    val x_tuple = HOLogic.mk_tuple xs;
+  in
+    (HOLogic.mk_comp (f, unc_g), x_tuple)
+  end;
+
 fun map_flattened_map_args ctxt s map_args fs =
   let
     val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs;
@@ -261,6 +274,11 @@
         if t2 = y then
           massage_map yU yT (elim_y t1) $ y'
           handle AINT_NO_MAP t' => invalid_map ctxt t'
+        else if head_of t2 = y then
+          let val (u1, u2) = expand_to_comp bound_Ts t1 t2 in
+            if has_call u2 then unexpected_rec_call ctxt u2
+            else massage_call u1 $ u2
+          end
         else
           ill_formed_rec_call ctxt t
       | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
@@ -446,17 +464,17 @@
     if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
   end;
 
-fun expand_ctr_term ctxt s Ts t =
+fun expand_to_ctr_term ctxt s Ts t =
   (case ctr_sugar_of ctxt s of
     SOME {ctrs, casex, ...} =>
     Term.list_comb (mk_case Ts (Type (s, Ts)) casex, map (mk_ctr Ts) ctrs) $ t
-  | NONE => raise Fail "expand_ctr_term");
+  | NONE => raise Fail "expand_to_ctr_term");
 
 fun expand_corec_code_rhs ctxt has_call bound_Ts t =
   (case fastype_of1 (bound_Ts, t) of
     Type (s, Ts) =>
     massage_let_if_case ctxt has_call (fn _ => fn t =>
-      if can (dest_ctr ctxt s) t then t else expand_ctr_term ctxt s Ts t) bound_Ts t
+      if can (dest_ctr ctxt s) t then t else expand_to_ctr_term ctxt s Ts t) bound_Ts t
   | _ => raise Fail "expand_corec_code_rhs");
 
 fun massage_corec_code_rhs ctxt massage_ctr =
diff -r a179353111db -r 496f9af15b39 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Oct 18 19:03:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Oct 18 19:18:32 2013 +0200
@@ -139,6 +139,7 @@
   val mk_sumTN_balanced: typ list -> typ
 
   val mk_convol: term * term -> term
+  val mk_tupled_fun: term -> term -> term list -> term
 
   val Inl_const: typ -> typ -> term
   val Inr_const: typ -> typ -> term
@@ -381,6 +382,9 @@
     val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU);
   in Const (@{const_name convol}, convolT) $ f $ g end;
 
+fun mk_tupled_fun x f xs =
+  if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs));
+
 fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
 fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;