# HG changeset patch
# User blanchet
# Date 1382289808 -7200
# Node ID 402fcacb5c8893ef7513afde7ba795f32d23a5ef
# Parent  41bd81a1c98e809b0d18e32eb217429ecba6da90
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation

diff -r 41bd81a1c98e -r 402fcacb5c88 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 19:20:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 19:23:28 2013 +0200
@@ -168,7 +168,7 @@
     subst (SOME ~1)
   end;
 
-fun subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls t =
+fun subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls =
   let
     fun try_nested_rec bound_Ts y t =
       AList.lookup (op =) nested_calls y
@@ -176,9 +176,12 @@
         massage_nested_rec_call lthy has_call (rewrite_map_arg get_ctr_pos) bound_Ts y y' t);
 
     fun subst bound_Ts (t as g' $ y) =
-        let val y_head = head_of y in
+        let
+          fun subst_rec () = subst bound_Ts g' $ subst bound_Ts y;
+          val y_head = head_of y;
+        in
           if not (member (op =) ctr_args y_head) then
-            subst bound_Ts g' $ subst bound_Ts y
+            subst_rec ()
           else
             (case try_nested_rec bound_Ts y_head t of
               SOME t' => t'
@@ -190,16 +193,21 @@
                    primrec_error_eqn "too few arguments in recursive call" t;
                    (case AList.lookup (op =) mutual_calls y of
                      SOME y' => list_comb (y', g_args)
-                   | NONE => t))
-                | NONE => t)
+                   | NONE => subst_rec ()))
+                | NONE => subst_rec ())
               end)
         end
       | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
       | subst _ t = t
+
+    fun subst' t =
+      if has_call t then
+        (* FIXME detect this case earlier? *)
+        primrec_error_eqn "recursive call not directly applied to constructor argument" t
+      else
+        try_nested_rec [] (head_of t) t |> the_default t
   in
-    subst [] t
-    |> tap (fn u => has_call u andalso (* FIXME detect this case earlier *)
-      primrec_error_eqn "recursive call not directly applied to constructor argument" t)
+    subst' o subst []
   end;
 
 fun build_rec_arg lthy (funs_data : eqn_data list list) has_call (ctr_spec : rec_ctr_spec)
diff -r 41bd81a1c98e -r 402fcacb5c88 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sun Oct 20 19:20:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sun Oct 20 19:23:28 2013 +0200
@@ -274,17 +274,20 @@
         handle AINT_NO_MAP _ => massage_mutual_fun U T t;
 
     fun massage_call (t as t1 $ t2) =
-        if t2 = y then
-          massage_map yU yT (elim_y t1) $ y'
-          handle AINT_NO_MAP t' => invalid_map ctxt t'
+        if has_call t then
+          if t2 = y then
+            massage_map yU yT (elim_y t1) $ y'
+            handle AINT_NO_MAP t' => invalid_map ctxt t'
+          else
+            let val (g, xs) = Term.strip_comb t2 in
+              if g = y then
+                if exists has_call xs then unexpected_rec_call ctxt t2
+                else Term.list_comb (massage_call (mk_compN bound_Ts (length xs) (t1, y)), xs)
+              else
+                ill_formed_rec_call ctxt t
+            end
         else
-          let val (g, xs) = Term.strip_comb t2 in
-            if g = y then
-              if exists has_call xs then unexpected_rec_call ctxt t2
-              else Term.list_comb (massage_call (mk_compN bound_Ts (length xs) (t1, y)), xs)
-            else
-              ill_formed_rec_call ctxt t
-          end
+          elim_y t
       | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
   in
     massage_call