support indirect corecursion

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 04 23:57:38 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 05 01:58:48 2013 +0200
@@ -536,6 +536,9 @@
 fun build_corec_args_discs disc_eqns ctr_specs =
   if null disc_eqns then I else
     let
+(*val _ = tracing ("d/p:\<cdot> " ^ space_implode "\n    \<cdot> " (map ((op ^) o
+ apfst (Syntax.string_of_term @{context}) o apsnd (curry (op ^) " / " o @{make_string}))
+  (ctr_specs |> map_filter (fn {disc, pred = SOME pred, ...} => SOME (disc, pred) | _ => NONE))));*)
       val conds = map #cond disc_eqns;
       val fun_args = #fun_args (hd disc_eqns);
       val args =
@@ -544,14 +547,15 @@
           fst (split_last conds)
         else if length disc_eqns = length ctr_specs - 1 then
           let val n = 0 upto length ctr_specs - 1
-              |> the o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns)) (*###*) in
+              |> the(*###*) o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns)) in
             if n = length ctr_specs - 1 then
               conds
             else
               split_last conds
               ||> HOLogic.mk_not
-              |>> chop n
-              |> (fn ((l, r), x) => l @ (x :: r))
+              |> `(uncurry (fold (curry HOLogic.mk_conj o HOLogic.mk_not)))
+              ||> chop n o fst
+              |> (fn (x, (l, r)) => l @ (x :: r))
           end
         else
           0 upto length ctr_specs - 1
@@ -570,11 +574,12 @@
 fun build_corec_arg_no_call sel_eqns sel = find_first (equal sel o #sel) sel_eqns
   |> try (fn SOME sel_eqn => (#fun_args sel_eqn, #rhs_term sel_eqn))
   |> the_default ([], undef_const)
-  |-> abs_tuple;
+  |-> abs_tuple
+  |> K;
 
 fun build_corec_arg_direct_call lthy has_call sel_eqns sel =
   let
-    val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns
+    val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
     fun rewrite is_end U T t =
       if U = @{typ bool} then @{term True} |> has_call t ? K @{term False} (* stop? *)
       else if is_end = has_call t then undef_const
@@ -587,8 +592,33 @@
       abs_tuple (#fun_args (the maybe_sel_eqn)) oo massage (#rhs_term (the maybe_sel_eqn))
   end;
 
-fun build_corec_arg_indirect_call sel_eqns sel =
-  primrec_error "indirect corecursion not implemented yet";
+fun build_corec_arg_indirect_call lthy has_call sel_eqns sel =
+  let
+    val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
+    fun rewrite _ _ =
+      let
+        fun subst (Abs (v, T, b)) = Abs (v, T, subst b)
+          | subst (t as _ $ _) =
+            let val (u, vs) = strip_comb t in
+              if is_Free u andalso has_call u then
+                Const (@{const_name Inr}, dummyT) $ (*HOLogic.mk_tuple vs*)
+                  (try (foldr1 (fn (x, y) => Const (@{const_name Pair}, dummyT) $ x $ y)) vs
+                    |> the_default (hd vs))
+              else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
+                list_comb (u |> map_types (K dummyT), map subst vs)
+              else
+                list_comb (subst u, map subst vs)
+            end
+          | subst t = t;
+      in
+        subst
+      end;
+    fun massage rhs_term t = massage_indirect_corec_call
+      lthy has_call rewrite [] (fastype_of t |> range_type) rhs_term;
+  in
+    if is_none maybe_sel_eqn then I else
+      abs_tuple (#fun_args (the maybe_sel_eqn)) o massage (#rhs_term (the maybe_sel_eqn))
+  end;
 
 fun build_corec_args_sel lthy has_call all_sel_eqns ctr_spec =
   let val sel_eqns = filter (equal (#ctr ctr_spec) o #ctr) all_sel_eqns in
@@ -596,9 +626,9 @@
       let
         val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec;
 
-val _ = tracing ("sels / calls:\n    \<cdot> " ^ space_implode "\n    \<cdot> " (map ((op ^) o
- apfst (Syntax.string_of_term @{context}) o apsnd (curry (op ^) " / " o @{make_string}))
-  (sel_call_list)));
+(*val _ = tracing ("s/c:\<cdot> " ^ space_implode "\n    \<cdot> " (map ((op ^) o
+ apfst (Syntax.string_of_term lthy) o apsnd (curry (op ^) " / " o @{make_string}))
+  sel_call_list));*)
 
         val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list;
         val direct_calls' = map_filter (try (apsnd (fn Direct_Corec n => n))) sel_call_list;
@@ -606,12 +636,12 @@
       in
         I
         #> fold (fn (sel, n) => nth_map n
-          (build_corec_arg_no_call sel_eqns sel |> K)) no_calls'
+          (build_corec_arg_no_call sel_eqns sel)) no_calls'
         #> fold (fn (sel, (q, g, h)) =>
           let val f = build_corec_arg_direct_call lthy has_call sel_eqns sel in
             nth_map h (f false) o nth_map g (f true) o nth_map q (f true) end) direct_calls'
         #> fold (fn (sel, n) => nth_map n
-          (build_corec_arg_indirect_call sel_eqns sel |> K)) indirect_calls'
+          (build_corec_arg_indirect_call lthy has_call sel_eqns sel)) indirect_calls'
       end
   end;
 
@@ -652,18 +682,19 @@
       |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts;
 
 val _ = tracing ("corecursor arguments:\n    \<cdot> " ^
- space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) corec_args));
+ space_implode "\n    \<cdot> " (map (Syntax.string_of_term lthy) corec_args));
 
     fun uneq_pairs_rev xs = xs (* FIXME \<exists>? *)
       |> these o try (split_last #> (fn (ys, y) => uneq_pairs_rev ys @ map (pair y) ys));
     val proof_obligations = if sequential then [] else
-      maps (uneq_pairs_rev o map (fn {fun_args, cond, ...} => (fun_args, cond))) disc_eqnss
+      disc_eqnss
+      |> maps (uneq_pairs_rev o map (fn {fun_args, cond, ...} => (fun_args, cond)))
       |> map (fn ((fun_args, x), (_, y)) => [x, HOLogic.mk_not y]
         |> map (HOLogic.mk_Trueprop o curry subst_bounds (List.rev fun_args))
         |> curry list_comb @{const ==>});
 
 val _ = tracing ("proof obligations:\n    \<cdot> " ^
- space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) proof_obligations));
+ space_implode "\n    \<cdot> " (map (Syntax.string_of_term lthy) proof_obligations));
 
   in
     map (list_comb o rpair corec_args) corecs

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 04 23:57:38 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 05 01:58:48 2013 +0200
@@ -198,11 +198,11 @@
 fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts res_U t =
   let
     val typof = curry fastype_of1 bound_Ts;
-    val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o fst);
+    val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
 
     fun check_and_massage_direct_call U T t =
       if has_call t then factor_out_types ctxt massage_direct_call dest_sumT U T t
-      else build_map_Inl (U, T) $ t;
+      else build_map_Inl (T, U) $ t;
 
     fun check_and_massage_unapplied_direct_call U T t =
       let val var = Var ((Name.uu, Term.maxidx_of_term t + 1), domain_type (typof t)) in
@@ -241,11 +241,11 @@
               | NONE =>
                 (case t of
                   t1 $ t2 =>
-                  if has_call t2 then
+                  (if has_call t2 then
                     check_and_massage_direct_call U T t
                   else
                     massage_map U T t1 $ t2
-                    handle AINT_NO_MAP _ => check_and_massage_direct_call U T t
+                    handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
                 | _ => check_and_massage_direct_call U T t))
             | _ => ill_formed_corec_call ctxt t))
         U T