gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
--- 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)
--- 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