--- 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);