--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Apr 07 15:14:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Apr 07 15:14:14 2015 +0200
@@ -51,7 +51,8 @@
val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
typ list -> term -> term
val massage_nested_corec_call: Proof.context -> (term -> bool) ->
- (typ list -> typ -> typ -> term -> term) -> typ list -> typ -> term -> term
+ (typ list -> typ -> typ -> term -> term) -> (typ -> typ -> term) -> typ list -> typ -> term ->
+ term
val expand_to_ctr_term: Proof.context -> string -> typ list -> term -> term
val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) ->
typ list -> term -> term
@@ -305,17 +306,15 @@
fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T;
-fun massage_nested_corec_call ctxt has_call raw_massage_call bound_Ts U t0 =
+fun massage_nested_corec_call ctxt has_call massage_call wrap_noncall bound_Ts U t0 =
let
fun check_no_call t = if has_call t then unexpected_corec_call ctxt [t0] t else ();
- val build_map_Inl = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd);
-
fun massage_mutual_call bound_Ts (Type (@{type_name fun}, [_, U2]))
(Type (@{type_name fun}, [T1, T2])) t =
Abs (Name.uu, T1, massage_mutual_call bound_Ts U2 T2 (incr_boundvars 1 t $ Bound 0))
| massage_mutual_call bound_Ts U T t =
- if has_call t then raw_massage_call bound_Ts T U t else build_map_Inl (T, U) $ t;
+ if has_call t then massage_call bound_Ts T U t else wrap_noncall T U $ t;
fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t =
(case try (dest_map ctxt s) t of
@@ -345,9 +344,10 @@
val j = Term.maxidx_of_term t + 1;
val var = Var ((Name.uu, j), domain_type (fastype_of1 (bound_Ts, t)));
in
- Term.lambda var (Term.incr_boundvars 1 (massage_call bound_Ts U T (betapply (t, var))))
+ Term.lambda var (Term.incr_boundvars 1 (massage_any_call bound_Ts U T
+ (betapply (t, var))))
end)
- and massage_call bound_Ts U T =
+ and massage_any_call bound_Ts U T =
massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
if has_call t then
(case U of
@@ -361,7 +361,7 @@
val arg_Ts = map typof args;
in
Term.list_comb (f',
- @{map 3} (massage_call bound_Ts) (binder_types f'_T) arg_Ts args)
+ @{map 3} (massage_any_call bound_Ts) (binder_types f'_T) arg_Ts args)
end
| NONE =>
(case t of
@@ -370,7 +370,7 @@
val U' = curried_type U;
val T' = curried_type T;
in
- Const (@{const_name case_prod}, U' --> U) $ massage_call bound_Ts U' T' t'
+ Const (@{const_name case_prod}, U' --> U) $ massage_any_call bound_Ts U' T' t'
end
| t1 $ t2 =>
(if has_call t2 then
@@ -379,15 +379,15 @@
massage_map bound_Ts U T t1 $ t2
handle NO_MAP _ => massage_mutual_call bound_Ts U T t)
| Abs (s, T', t') =>
- Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')
+ Abs (s, T', massage_any_call (T' :: bound_Ts) (range_type U) (range_type T) t')
| _ => massage_mutual_call bound_Ts U T t))
| _ => ill_formed_corec_call ctxt t)
else
- build_map_Inl (T, U) $ t) bound_Ts;
+ wrap_noncall T U $ t) bound_Ts;
val T = fastype_of1 (bound_Ts, t0);
in
- if has_call t0 then massage_call bound_Ts U T t0 else build_map_Inl (T, U) $ t0
+ if has_call t0 then massage_any_call bound_Ts U T t0 else wrap_noncall T U $ t0
end;
fun expand_to_ctr_term ctxt s Ts t =
@@ -894,7 +894,7 @@
NONE => I
| SOME {fun_args, rhs_term, ...} =>
let
- fun massage_leaf bound_Ts T U t0 =
+ fun massage_call bound_Ts T U t0 =
let
val U2 =
(case try dest_sumT U of
@@ -919,11 +919,14 @@
rewrite bound_Ts t0
end;
+ fun wrap_noncall T U = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd) (T, U);
+
val bound_Ts = List.rev (map fastype_of fun_args);
fun build t =
rhs_term
- |> massage_nested_corec_call ctxt has_call massage_leaf bound_Ts (range_type (fastype_of t))
+ |> massage_nested_corec_call ctxt has_call massage_call wrap_noncall bound_Ts
+ (range_type (fastype_of t))
|> abs_tuple_balanced fun_args;
in
build