1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Thu Sep 19 11:27:32 2013 +0200
1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Thu Sep 19 12:20:12 2013 +0200
1.3 @@ -583,25 +583,23 @@
1.4 fun build_corec_arg_indirect_call lthy has_call sel_eqns sel =
1.5 let
1.6 val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
1.7 - fun rewrite _ _ =
1.8 - let
1.9 - fun subst (Abs (v, T, b)) = Abs (v, T, subst b)
1.10 - | subst t =
1.11 - let val (u, vs) = strip_comb t in
1.12 - if is_Free u andalso has_call u then
1.13 - Const (@{const_name Inr}, dummyT) $
1.14 - (if null vs then HOLogic.unit
1.15 - else foldr1 (fn (x, y) => Const (@{const_name Pair}, dummyT) $ x $ y) vs)
1.16 - else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
1.17 - list_comb (u |> map_types (K dummyT), map subst vs)
1.18 - else
1.19 - list_comb (subst u, map subst vs)
1.20 - end;
1.21 - in
1.22 - subst
1.23 - end;
1.24 - fun massage rhs_term t = massage_indirect_corec_call
1.25 - lthy has_call rewrite [] (range_type (fastype_of t)) rhs_term;
1.26 + fun rewrite (Abs (v, T, b)) = Abs (v, T, rewrite b)
1.27 + | rewrite t =
1.28 + let val (u, vs) = strip_comb t in
1.29 + if is_Free u andalso has_call u then
1.30 + Const (@{const_name Inr}, dummyT) $
1.31 + (if null vs then HOLogic.unit
1.32 + else foldr1 (fn (x, y) => Const (@{const_name Pair}, dummyT) $ x $ y) vs)
1.33 + else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
1.34 + list_comb (u |> map_types (K dummyT), map rewrite vs)
1.35 + else if null vs then
1.36 + u
1.37 + else
1.38 + list_comb (rewrite u, map rewrite vs)
1.39 + end;
1.40 + fun massage rhs_term t =
1.41 + massage_indirect_corec_call lthy has_call (K (K rewrite)) [] (range_type (fastype_of t))
1.42 + rhs_term;
1.43 in
1.44 if is_none maybe_sel_eqn then I else
1.45 abs_tuple (#fun_args (the maybe_sel_eqn)) o massage (#rhs_term (the maybe_sel_eqn))
2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Thu Sep 19 11:27:32 2013 +0200
2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Thu Sep 19 12:20:12 2013 +0200
2.3 @@ -150,7 +150,7 @@
2.4 permute_like (op aconv) flat_fs fs flat_fs'
2.5 end;
2.6
2.7 -fun massage_indirect_rec_call ctxt has_call massage_unapplied_direct_call bound_Ts y y' =
2.8 +fun massage_indirect_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
2.9 let
2.10 val typof = curry fastype_of1 bound_Ts;
2.11 val build_map_fst = build_map ctxt (fst_const o fst);
2.12 @@ -161,11 +161,9 @@
2.13 fun y_of_y' () = build_map_fst (yU, yT) $ y';
2.14 val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
2.15
2.16 - fun check_and_massage_unapplied_direct_call U T t =
2.17 - if has_call t then
2.18 - factor_out_types ctxt massage_unapplied_direct_call HOLogic.dest_prodT U T t
2.19 - else
2.20 - HOLogic.mk_comp (t, build_map_fst (U, T));
2.21 + fun massage_direct_fun U T t =
2.22 + if has_call t then factor_out_types ctxt raw_massage_fun HOLogic.dest_prodT U T t
2.23 + else HOLogic.mk_comp (t, build_map_fst (U, T));
2.24
2.25 fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
2.26 (case try (dest_map ctxt s) t of
2.27 @@ -184,7 +182,7 @@
2.28 if has_call t then unexpected_rec_call ctxt t else t
2.29 else
2.30 massage_map U T t
2.31 - handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t;
2.32 + handle AINT_NO_MAP _ => massage_direct_fun U T t;
2.33
2.34 fun massage_call (t as t1 $ t2) =
2.35 if t2 = y then
2.36 @@ -221,21 +219,21 @@
2.37 fld
2.38 end;
2.39
2.40 -fun massage_direct_corec_call ctxt has_call massage_direct_call U t =
2.41 - massage_let_and_if ctxt has_call massage_direct_call U t;
2.42 +fun massage_direct_corec_call ctxt has_call raw_massage_call U t =
2.43 + massage_let_and_if ctxt has_call raw_massage_call U t;
2.44
2.45 -fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts U t =
2.46 +fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
2.47 let
2.48 val typof = curry fastype_of1 bound_Ts;
2.49 val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
2.50
2.51 - fun check_and_massage_direct_call U T t =
2.52 - if has_call t then factor_out_types ctxt massage_direct_call dest_sumT U T t
2.53 + fun massage_direct_call U T t =
2.54 + if has_call t then factor_out_types ctxt raw_massage_call dest_sumT U T t
2.55 else build_map_Inl (T, U) $ t;
2.56
2.57 - fun check_and_massage_unapplied_direct_call U T t =
2.58 + fun massage_direct_fun U T t =
2.59 let val var = Var ((Name.uu, Term.maxidx_of_term t + 1), domain_type (typof t)) in
2.60 - Term.lambda var (check_and_massage_direct_call U T (t $ var))
2.61 + Term.lambda var (massage_direct_call U T (t $ var))
2.62 end;
2.63
2.64 fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
2.65 @@ -255,7 +253,7 @@
2.66 if has_call t then unexpected_corec_call ctxt t else t
2.67 else
2.68 massage_map U T t
2.69 - handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t;
2.70 + handle AINT_NO_MAP _ => massage_direct_fun U T t;
2.71
2.72 fun massage_call U T =
2.73 massage_let_and_if ctxt has_call (fn t =>
2.74 @@ -271,12 +269,12 @@
2.75 (case t of
2.76 t1 $ t2 =>
2.77 (if has_call t2 then
2.78 - check_and_massage_direct_call U T t
2.79 + massage_direct_call U T t
2.80 else
2.81 massage_map U T t1 $ t2
2.82 - handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
2.83 + handle AINT_NO_MAP _ => massage_direct_call U T t)
2.84 | Abs (s, T', t') => Abs (s, T', massage_call (range_type U) (range_type T) t')
2.85 - | _ => check_and_massage_direct_call U T t))
2.86 + | _ => massage_direct_call U T t))
2.87 | _ => ill_formed_corec_call ctxt t)
2.88 else
2.89 build_map_Inl (T, U) $ t) U