--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Mon Oct 14 09:17:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Mon Oct 14 09:31:42 2013 +0200
@@ -168,13 +168,13 @@
subst (SOME ~1)
end;
-fun subst_rec_calls lthy get_ctr_pos has_call ctr_args direct_calls indirect_calls t =
+fun subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls t =
let
fun subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
| subst bound_Ts (t as g' $ y) =
let
- val maybe_direct_y' = AList.lookup (op =) direct_calls y;
- val maybe_indirect_y' = AList.lookup (op =) indirect_calls y;
+ 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
@@ -183,11 +183,11 @@
if not (member (op =) ctr_args y) then
pairself (subst bound_Ts) (g', y) |> (op $)
else if ctr_pos >= 0 then
- list_comb (the maybe_direct_y', g_args)
- else if is_some maybe_indirect_y' 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_indirect_rec_call lthy has_call
- (rewrite_map_arg get_ctr_pos) bound_Ts y (the maybe_indirect_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
@@ -208,25 +208,25 @@
val ctr_args = #ctr_args eqn_data;
val calls = #calls ctr_spec;
- val n_args = fold (curry (op +) o (fn Direct_Rec _ => 2 | _ => 1)) calls 0;
+ val n_args = fold (curry (op +) o (fn Mutual_Rec _ => 2 | _ => 1)) calls 0;
val no_calls' = tag_list 0 calls
- |> map_filter (try (apsnd (fn No_Rec n => n | Direct_Rec (n, _) => n)));
- val direct_calls' = tag_list 0 calls
- |> map_filter (try (apsnd (fn Direct_Rec (_, n) => n)));
- val indirect_calls' = tag_list 0 calls
- |> map_filter (try (apsnd (fn Indirect_Rec n => n)));
+ |> map_filter (try (apsnd (fn No_Rec n => n | Mutual_Rec (n, _) => n)));
+ val mutual_calls' = tag_list 0 calls
+ |> map_filter (try (apsnd (fn Mutual_Rec (_, n) => n)));
+ val nested_calls' = tag_list 0 calls
+ |> map_filter (try (apsnd (fn Nested_Rec n => n)));
- fun make_direct_type _ = dummyT; (* FIXME? *)
+ fun make_mutual_type _ = dummyT; (* FIXME? *)
val rec_res_type_list = map (fn (x :: _) => (#rec_type x, #res_type x)) funs_data;
- fun make_indirect_type (Type (Tname, Ts)) = Type (Tname, Ts |> map (fn T =>
+ fun make_nested_type (Type (Tname, Ts)) = Type (Tname, Ts |> map (fn T =>
let val maybe_res_type = AList.lookup (op =) rec_res_type_list T in
if is_some maybe_res_type
then HOLogic.mk_prodT (T, the maybe_res_type)
- else make_indirect_type T end))
- | make_indirect_type T = T;
+ else make_nested_type T end))
+ | make_nested_type T = T;
val args = replicate n_args ("", dummyT)
|> Term.rename_wrt_term t
@@ -235,22 +235,22 @@
nth_map arg_idx (K (nth ctr_args ctr_arg_idx)))
no_calls'
|> fold (fn (ctr_arg_idx, arg_idx) =>
- nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_direct_type)))
- direct_calls'
+ nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_mutual_type)))
+ mutual_calls'
|> fold (fn (ctr_arg_idx, arg_idx) =>
- nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_indirect_type)))
- indirect_calls';
+ nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_nested_type)))
+ nested_calls';
val fun_name_ctr_pos_list =
map (fn (x :: _) => (#fun_name x, length (#left_args x))) funs_data;
val get_ctr_pos = try (the o AList.lookup (op =) fun_name_ctr_pos_list) #> the_default ~1;
- val direct_calls = map (apfst (nth ctr_args) o apsnd (nth args)) direct_calls';
- val indirect_calls = map (apfst (nth ctr_args) o apsnd (nth args)) indirect_calls';
+ val mutual_calls = map (apfst (nth ctr_args) o apsnd (nth args)) mutual_calls';
+ val nested_calls = map (apfst (nth ctr_args) o apsnd (nth args)) nested_calls';
val abstractions = args @ #left_args eqn_data @ #right_args eqn_data;
in
t
- |> subst_rec_calls lthy get_ctr_pos has_call ctr_args direct_calls indirect_calls
+ |> subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls
|> fold_rev lambda abstractions
end;
@@ -671,7 +671,7 @@
|> the_default undef_const
|> K;
-fun build_corec_args_direct_call lthy has_call (sel_eqns : co_eqn_data_sel list) sel =
+fun build_corec_args_mutual_call lthy has_call (sel_eqns : co_eqn_data_sel list) sel =
let
val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
in
@@ -683,7 +683,7 @@
fun rewrite_g _ t = if has_call t then undef_const else t;
fun rewrite_h bound_Ts t =
if has_call t then mk_tuple1 bound_Ts (snd (strip_comb t)) else undef_const;
- fun massage f _ = massage_direct_corec_call lthy has_call f bound_Ts rhs_term
+ fun massage f _ = massage_mutual_corec_call lthy has_call f bound_Ts rhs_term
|> abs_tuple fun_args;
in
(massage rewrite_q,
@@ -692,7 +692,7 @@
end
end;
-fun build_corec_arg_indirect_call lthy has_call (sel_eqns : co_eqn_data_sel list) sel =
+fun build_corec_arg_nested_call lthy has_call (sel_eqns : co_eqn_data_sel list) sel =
let
val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
in
@@ -714,7 +714,7 @@
if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t;
fun massage t =
rhs_term
- |> massage_indirect_corec_call lthy has_call rewrite bound_Ts (range_type (fastype_of t))
+ |> massage_nested_corec_call lthy has_call rewrite bound_Ts (range_type (fastype_of t))
|> abs_tuple fun_args;
in
massage
@@ -729,16 +729,16 @@
val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec;
val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list;
- val direct_calls' = map_filter (try (apsnd (fn Direct_Corec n => n))) sel_call_list;
- val indirect_calls' = map_filter (try (apsnd (fn Indirect_Corec n => n))) sel_call_list;
+ val mutual_calls' = map_filter (try (apsnd (fn Mutual_Corec n => n))) sel_call_list;
+ val nested_calls' = map_filter (try (apsnd (fn Nested_Corec n => n))) sel_call_list;
in
I
#> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls'
#> fold (fn (sel, (q, g, h)) =>
- let val (fq, fg, fh) = build_corec_args_direct_call lthy has_call sel_eqns sel in
- nth_map q fq o nth_map g fg o nth_map h fh end) direct_calls'
+ let val (fq, fg, fh) = build_corec_args_mutual_call lthy has_call sel_eqns sel in
+ nth_map q fq o nth_map g fg o nth_map h fh end) mutual_calls'
#> fold (fn (sel, n) => nth_map n
- (build_corec_arg_indirect_call lthy has_call sel_eqns sel)) indirect_calls'
+ (build_corec_arg_nested_call lthy has_call sel_eqns sel)) nested_calls'
end
end;
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Mon Oct 14 09:17:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Mon Oct 14 09:31:42 2013 +0200
@@ -10,14 +10,14 @@
sig
datatype rec_call =
No_Rec of int |
- Direct_Rec of int (*before*) * int (*after*) |
- Indirect_Rec of int
+ Mutual_Rec of int (*before*) * int (*after*) |
+ Nested_Rec of int
datatype corec_call =
Dummy_No_Corec of int |
No_Corec of int |
- Direct_Corec of int (*stop?*) * int (*end*) * int (*continue*) |
- Indirect_Corec of int
+ Mutual_Corec of int (*stop?*) * int (*end*) * int (*continue*) |
+ Nested_Corec of int
type rec_ctr_spec =
{ctr: term,
@@ -57,12 +57,12 @@
val s_disjs: term list -> term
val s_dnf: term list list -> term list
- val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
+ val massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
typ list -> term -> term -> term -> term
val unfold_let: term -> term
- val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
+ val massage_mutual_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
typ list -> term -> term
- val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
+ val massage_nested_corec_call: Proof.context -> (term -> bool) ->
(typ list -> typ -> typ -> term -> term) -> typ list -> typ -> term -> term
val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) ->
@@ -92,14 +92,14 @@
datatype rec_call =
No_Rec of int |
- Direct_Rec of int * int |
- Indirect_Rec of int;
+ Mutual_Rec of int * int |
+ Nested_Rec of int;
datatype corec_call =
Dummy_No_Corec of int |
No_Corec of int |
- Direct_Corec of int * int * int |
- Indirect_Corec of int;
+ Mutual_Corec of int * int * int |
+ Nested_Corec of int;
type rec_ctr_spec =
{ctr: term,
@@ -210,7 +210,7 @@
permute_like (op aconv) flat_fs fs flat_fs'
end;
-fun massage_indirect_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
+fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
let
val typof = curry fastype_of1 bound_Ts;
val build_map_fst = build_map ctxt (fst_const o fst);
@@ -221,7 +221,7 @@
fun y_of_y' () = build_map_fst (yU, yT) $ y';
val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
- fun massage_direct_fun U T t =
+ fun massage_mutual_fun U T t =
if has_call t then factor_out_types ctxt raw_massage_fun HOLogic.dest_prodT U T t
else HOLogic.mk_comp (t, build_map_fst (U, T));
@@ -242,7 +242,7 @@
if has_call t then unexpected_rec_call ctxt t else t
else
massage_map U T t
- handle AINT_NO_MAP _ => massage_direct_fun U T t;
+ handle AINT_NO_MAP _ => massage_mutual_fun U T t;
fun massage_call (t as t1 $ t2) =
if t2 = y then
@@ -341,24 +341,24 @@
massage_rec
end;
-val massage_direct_corec_call = massage_let_if_case;
+val massage_mutual_corec_call = massage_let_if_case;
fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T;
-fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
+fun massage_nested_corec_call ctxt has_call raw_massage_call bound_Ts U t =
let
val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
- fun massage_direct_call bound_Ts U T t =
+ fun massage_mutual_call bound_Ts U T t =
if has_call t then factor_out_types ctxt (raw_massage_call bound_Ts) dest_sumT U T t
else build_map_Inl (T, U) $ t;
- fun massage_direct_fun bound_Ts U T t =
+ fun massage_mutual_fun bound_Ts U T t =
let
val var = Var ((Name.uu, Term.maxidx_of_term t + 1),
domain_type (fastype_of1 (bound_Ts, t)));
in
- Term.lambda var (massage_direct_call bound_Ts U T (t $ var))
+ Term.lambda var (massage_mutual_call bound_Ts U T (t $ var))
end;
fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t =
@@ -379,7 +379,7 @@
if has_call t then unexpected_corec_call ctxt t else t
else
massage_map bound_Ts U T t
- handle AINT_NO_MAP _ => massage_direct_fun bound_Ts U T t;
+ handle AINT_NO_MAP _ => massage_mutual_fun bound_Ts U T t;
fun massage_call bound_Ts U T =
massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
@@ -407,13 +407,13 @@
end
| t1 $ t2 =>
(if has_call t2 then
- massage_direct_call bound_Ts U T t
+ massage_mutual_call bound_Ts U T t
else
massage_map bound_Ts U T t1 $ t2
- handle AINT_NO_MAP _ => massage_direct_call bound_Ts U T t)
+ handle AINT_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')
- | _ => massage_direct_call bound_Ts U 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;
@@ -521,8 +521,8 @@
| offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) =
length ctrs + offset_of_ctr (n - 1) ctr_sugars;
- fun call_of [i] [T] = (if exists_subtype_in Cs T then Indirect_Rec else No_Rec) i
- | call_of [i, i'] _ = Direct_Rec (i, i');
+ fun call_of [i] [T] = (if exists_subtype_in Cs T then Nested_Rec else No_Rec) i
+ | call_of [i, i'] _ = Mutual_Rec (i, i');
fun mk_ctr_spec ctr offset fun_arg_Tss rec_thm =
let
@@ -613,10 +613,10 @@
val perm_Cs' = map substCT perm_Cs;
fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] =
- (if exists_subtype_in Cs T then Indirect_Corec
+ (if exists_subtype_in Cs T then Nested_Corec
else if nullary then Dummy_No_Corec
else No_Corec) g_i
- | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
+ | call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i');
fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss discI sel_thms collapse corec_thm
disc_corec sel_corecs =