correct most general type for mutual recursion when several identical types are involved
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Feb 27 11:41:32 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Feb 27 13:04:57 2014 +0100
@@ -9,12 +9,14 @@
sig
type fp_sugar =
{T: typ,
+ X: typ,
fp: BNF_Util.fp_kind,
fp_res_index: int,
fp_res: BNF_FP_Util.fp_result,
pre_bnf: BNF_Def.bnf,
nested_bnfs: BNF_Def.bnf list,
nesting_bnfs: BNF_Def.bnf list,
+ ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
co_iters: term list,
@@ -61,9 +63,8 @@
* (string * term list * term list list
* ((term list list * term list list list) * typ list) list) option)
* Proof.context
- val mk_coiter_fun_arg_types: typ list list list -> typ list -> int list -> term ->
- typ list list
- * (typ list list list list * typ list list list * typ list list list list * typ list)
+ val repair_nullary_single_ctr: typ list list -> typ list list
+ val mk_coiter_p_pred_types: typ list -> int list -> typ list list
val define_iters: string list ->
(typ list list * typ list list list list * term list list * term list list list list) list ->
(string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
@@ -115,12 +116,14 @@
type fp_sugar =
{T: typ,
+ X: typ,
fp: fp_kind,
fp_res_index: int,
fp_res: fp_result,
pre_bnf: bnf,
nested_bnfs: bnf list,
nesting_bnfs: bnf list,
+ ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
co_iters: term list,
@@ -131,16 +134,18 @@
disc_co_iterss: thm list list,
sel_co_itersss: thm list list list};
-fun morph_fp_sugar phi ({T, fp, fp_res, fp_res_index, pre_bnf, nested_bnfs, nesting_bnfs, ctr_defs,
- ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, co_iter_thmss, disc_co_iterss,
- sel_co_itersss} : fp_sugar) =
+fun morph_fp_sugar phi ({T, X, fp, fp_res, fp_res_index, pre_bnf, nested_bnfs, nesting_bnfs,
+ ctrXs_Tss, ctr_defs, ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, co_iter_thmss,
+ disc_co_iterss, sel_co_itersss} : fp_sugar) =
{T = Morphism.typ phi T,
+ X = Morphism.typ phi X,
fp = fp,
fp_res = morph_fp_result phi fp_res,
fp_res_index = fp_res_index,
pre_bnf = morph_bnf phi pre_bnf,
nested_bnfs = map (morph_bnf phi) nested_bnfs,
nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+ ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
ctr_defs = map (Morphism.thm phi) ctr_defs,
ctr_sugar = morph_ctr_sugar phi ctr_sugar,
co_iters = map (Morphism.term phi) co_iters,
@@ -178,17 +183,17 @@
Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)));
-fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
- ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss disc_co_itersss
- sel_co_iterssss lthy =
+fun register_fp_sugars Xs fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctrXs_Tsss
+ ctr_defss ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss
+ disc_co_itersss sel_co_iterssss lthy =
(0, lthy)
|> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
- register_fp_sugar s {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk,
+ register_fp_sugar s {T = T, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
pre_bnf = nth pre_bnfs kk, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs,
- ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, co_iters = nth co_iterss kk,
- maps = nth mapss kk, common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
- co_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk,
- sel_co_itersss = nth sel_co_iterssss kk}
+ ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk,
+ co_iters = nth co_iterss kk, maps = nth mapss kk, common_co_inducts = common_co_inducts,
+ co_inducts = nth co_inductss kk, co_iter_thmss = nth co_iter_thmsss kk,
+ disc_co_iterss = nth disc_co_itersss kk, sel_co_itersss = nth sel_co_iterssss kk}
lthy)) Ts
|> snd;
@@ -381,13 +386,13 @@
([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy)
end;
+(*avoid "'a itself" arguments in coiterators*)
+fun repair_nullary_single_ctr [[]] = [[@{typ unit}]]
+ | repair_nullary_single_ctr Tss = Tss;
+
fun mk_coiter_fun_arg_types0 ctr_Tsss Cs ns fun_Ts =
let
- (*avoid "'a itself" arguments in coiterators*)
- fun repair_arity [[]] = [[@{typ unit}]]
- | repair_arity Tss = Tss;
-
- val ctr_Tsss' = map repair_arity ctr_Tsss;
+ val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss;
val f_sum_prod_Ts = map range_type fun_Ts;
val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
val f_Tsss = map2 (map2 (dest_tupleT o length)) ctr_Tsss' f_prod_Tss;
@@ -400,10 +405,6 @@
fun mk_coiter_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
-fun mk_coiter_fun_arg_types ctr_Tsss Cs ns dtor_coiter =
- (mk_coiter_p_pred_types Cs ns,
- mk_coiter_fun_arg_types0 ctr_Tsss Cs ns (binder_fun_types (fastype_of dtor_coiter)));
-
fun mk_coiters_args_types ctr_Tsss Cs ns dtor_coiter_fun_Tss lthy =
let
val p_Tss = mk_coiter_p_pred_types Cs ns;
@@ -1385,9 +1386,9 @@
|> Spec_Rules.add Spec_Rules.Equational (map un_fold_of iterss, flat fold_thmss)
|> Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss)
|> Local_Theory.notes (common_notes @ notes) |> snd
- |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
- iterss mapss [induct_thm] (map single induct_thms) (transpose [fold_thmss, rec_thmss])
- (replicate nn []) (replicate nn [])
+ |> register_fp_sugars Xs Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctrXs_Tsss
+ ctr_defss ctr_sugars iterss mapss [induct_thm] (map single induct_thms)
+ (transpose [fold_thmss, rec_thmss]) (replicate nn []) (replicate nn [])
end;
fun derive_note_coinduct_coiters_thms_for_types
@@ -1450,8 +1451,8 @@
|> add_spec_rules un_fold_of sel_unfold_thmss unfold_thmss
|> add_spec_rules co_rec_of sel_corec_thmss corec_thmss
|> Local_Theory.notes (common_notes @ notes) |> snd
- |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
- ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
+ |> register_fp_sugars Xs Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctrXs_Tsss
+ ctr_defss ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
(transpose [coinduct_thms, strong_coinduct_thms])
(transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
(transpose [sel_unfold_thmsss, sel_corec_thmsss])
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Feb 27 11:41:32 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Feb 27 13:04:57 2014 +0100
@@ -10,12 +10,12 @@
val unfold_lets_splits: term -> term
val dest_map: Proof.context -> string -> term -> term * term list
- val mutualize_fp_sugars: BNF_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
+ val mutualize_fp_sugars: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory ->
(BNF_FP_Def_Sugar.fp_sugar list
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
* local_theory
- val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
+ val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
(term * term list list) list list -> local_theory ->
(typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
@@ -103,8 +103,13 @@
fun key_of_fp_eqs fp fpTs fp_eqs =
Type (fp_case fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs);
+fun get_indices callers t =
+ callers
+ |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
+ |> map_filter I;
+
(* TODO: test with sort constraints on As *)
-fun mutualize_fp_sugars fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
+fun mutualize_fp_sugars fp bs fpTs callers callssss fp_sugars0 no_defs_lthy0 =
let
val thy = Proof_Context.theory_of no_defs_lthy0;
@@ -112,6 +117,8 @@
fun incompatible_calls ts =
error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ commas (map qsotm ts));
+ fun mutual_self_call caller t =
+ error ("Unsupported mutual self-call " ^ qsotm t ^ " from " ^ qsotm caller);
fun nested_self_call t =
error ("Unsupported nested self-call " ^ qsotm t);
@@ -146,7 +153,7 @@
||>> variant_tfrees fp_b_names;
fun check_call_dead live_call call =
- if null (get_indices call) then () else incompatible_calls [live_call, call];
+ if null (get_indices callers call) then () else incompatible_calls [live_call, call];
fun freeze_fpTs_type_based_default (T as Type (s, Ts)) =
(case filter (curry (op =) T o snd) (map_index I fpTs) of
@@ -154,31 +161,36 @@
| _ => Type (s, map freeze_fpTs_type_based_default Ts))
| freeze_fpTs_type_based_default T = T;
- fun freeze_fpTs_mutual_call calls T =
- (case fold (union (op =)) (map get_indices calls) [] of
- [] => freeze_fpTs_type_based_default T
- | [kk] => nth Xs kk
+ fun freeze_fpTs_mutual_call kk fpT calls T =
+ (case fold (union (op =)) (map (get_indices callers) calls) [] of
+ [] => if T = fpT then nth Xs kk else freeze_fpTs_type_based_default T
+ | [kk'] =>
+ if T = fpT andalso kk' <> kk then
+ mutual_self_call (nth callers kk)
+ (the (find_first (not o null o get_indices callers) calls))
+ else
+ nth Xs kk'
| _ => incompatible_calls calls);
- fun freeze_fpTs_map (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls))
+ fun freeze_fpTs_map kk (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls))
(Type (s, Ts)) =
if Ts' = Ts then
nested_self_call live_call
else
(List.app (check_call_dead live_call) dead_calls;
- Type (s, map2 (freeze_fpTs_call fpT)
+ Type (s, map2 (freeze_fpTs_call kk fpT)
(flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] (transpose callss)) Ts))
- and freeze_fpTs_call fpT calls (T as Type (s, _)) =
+ and freeze_fpTs_call kk fpT calls (T as Type (s, _)) =
(case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
([], _) =>
(case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of
- ([], _) => freeze_fpTs_mutual_call calls T
- | callsp => freeze_fpTs_map fpT callsp T)
- | callsp => freeze_fpTs_map fpT callsp T)
- | freeze_fpTs_call _ _ T = T;
+ ([], _) => freeze_fpTs_mutual_call kk fpT calls T
+ | callsp => freeze_fpTs_map kk fpT callsp T)
+ | callsp => freeze_fpTs_map kk fpT callsp T)
+ | freeze_fpTs_call _ _ _ T = T;
val ctr_Tsss = map (map binder_types) ctr_Tss;
- val ctrXs_Tsss = map3 (map2 o map2 o freeze_fpTs_call) fpTs callssss ctr_Tsss;
+ val ctrXs_Tsss = map4 (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss;
val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
val ns = map length ctr_Tsss;
@@ -254,11 +266,12 @@
val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
- fun mk_target_fp_sugar T kk pre_bnf ctr_defs ctr_sugar co_iters maps co_inducts un_fold_thms
- co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss sel_corec_thmss =
- {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
- nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctr_defs = ctr_defs,
- ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps,
+ fun mk_target_fp_sugar T X kk pre_bnf ctrXs_Tss ctr_defs ctr_sugar co_iters maps co_inducts
+ un_fold_thms co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss
+ sel_corec_thmss =
+ {T = T, X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
+ nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctrXs_Tss = ctrXs_Tss,
+ ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps,
common_co_inducts = common_co_inducts, co_inducts = co_inducts,
co_iter_thmss = [un_fold_thms, co_rec_thms],
disc_co_iterss = [disc_unfold_thms, disc_corec_thms],
@@ -266,9 +279,9 @@
|> morph_fp_sugar phi;
val target_fp_sugars =
- map14 mk_target_fp_sugar fpTs kks pre_bnfs ctr_defss ctr_sugars co_iterss mapss
- (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss disc_corec_thmss
- sel_unfold_thmsss sel_corec_thmsss;
+ map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs ctrXs_Tsss ctr_defss ctr_sugars co_iterss
+ mapss (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss
+ disc_corec_thmss sel_unfold_thmsss sel_corec_thmsss;
val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
in
@@ -292,7 +305,9 @@
f (T, U) #> (if s = s' then fold (fold_subtype_pairs f) (Ts ~~ Us) else I)
| fold_subtype_pairs f TU = f TU;
-fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
+val impossible_caller = Bound ~1;
+
+fun nested_to_mutual_fps fp actual_bs actual_Ts actual_callers actual_callssss0 lthy =
let
val qsoty = quote o Syntax.string_of_typ lthy;
val qsotys = space_implode " or " o map qsoty;
@@ -391,23 +406,23 @@
val common_name = mk_common_name (map Binding.name_of actual_bs);
val bs = pad_list (Binding.name common_name) nn actual_bs;
+ val callers = pad_list impossible_caller nn actual_callers;
fun permute xs = permute_like (op =) Ts perm_Ts xs;
fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs;
val perm_bs = permute bs;
+ val perm_callers = permute callers;
val perm_kks = permute kks;
val perm_callssss0 = permute callssss0;
val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
val perm_callssss = map2 (indexify_callsss o #ctrs o #ctr_sugar) perm_fp_sugars0 perm_callssss0;
- val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
-
val ((perm_fp_sugars, fp_sugar_thms), lthy) =
if num_groups > 1 then
- mutualize_fp_sugars fp perm_bs perm_frozen_gen_Ts get_perm_indices perm_callssss
- perm_fp_sugars0 lthy
+ mutualize_fp_sugars fp perm_bs perm_frozen_gen_Ts perm_callers perm_callssss perm_fp_sugars0
+ lthy
else
((perm_fp_sugars0, (NONE, NONE)), lthy);
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Feb 27 11:41:32 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Feb 27 13:04:57 2014 +0100
@@ -38,7 +38,6 @@
val mk_compN: int -> typ list -> term * term -> term
val mk_comp: typ list -> term * term -> term
- val get_free_indices: ((binding * typ) * 'a) list -> term -> int list
val mk_co_iter: theory -> fp_kind -> typ -> typ list -> term -> term
val mk_conjunctN: int -> int -> thm
@@ -109,10 +108,6 @@
val mk_comp = mk_compN 1;
-fun get_free_indices fixes t = map (fst #>> Binding.name_of #> Free) fixes
- |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
- |> map_filter I;
-
fun mk_co_iter thy fp fpT Cs t =
let
val ((f_Cs, prebody), body) = strip_type (fastype_of t) |>> split_last;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Feb 27 11:41:32 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Feb 27 13:04:57 2014 +0100
@@ -370,33 +370,44 @@
(case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => [])
| map_thms_of_typ _ _ = [];
-fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
+fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
let
val thy = Proof_Context.theory_of lthy0;
- val ((missing_res_Ts, perm0_kks,
- fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
- common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
- nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy0;
+ val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, co_iters = coiter1 :: _,
+ common_co_inducts = common_coinduct_thms, ...} :: _,
+ (_, gfp_sugar_thms)), lthy) =
+ nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
val indices = map #fp_res_index fp_sugars;
val perm_indices = map #fp_res_index perm_fp_sugars;
- val perm_ctrss = map (#ctrs o #ctr_sugar) perm_fp_sugars;
- val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
- val perm_gfpTs = map (body_type o fastype_of o hd) perm_ctrss;
+ val perm_gfpTs = map #T perm_fp_sugars;
+ val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars;
val nn0 = length res_Ts;
val nn = length perm_gfpTs;
val kks = 0 upto nn - 1;
- val perm_ns = map length perm_ctr_Tsss;
+ val perm_ns' = map length perm_ctrXs_Tsss';
+
+ val perm_Ts = map #T perm_fp_sugars;
+ val perm_Xs = map #X perm_fp_sugars;
+ val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o #co_iters) perm_fp_sugars;
+ val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs);
- val perm_Cs = map (fn {fp_res, fp_res_index, ...} => domain_type (body_fun_type (fastype_of
- (co_rec_of (nth (#xtor_co_iterss fp_res) fp_res_index))))) perm_fp_sugars;
- val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) =
- mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1);
+ fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)]
+ | zip_corecT U =
+ (case AList.lookup (op =) Xs_TCs U of
+ SOME (T, C) => [T, C]
+ | NONE => [U]);
+
+ val perm_p_Tss = mk_coiter_p_pred_types perm_Cs perm_ns';
+ val perm_f_Tssss =
+ map2 (fn C => map (map (map (curry (op -->) C) o zip_corecT))) perm_Cs perm_ctrXs_Tsss';
+ val perm_q_Tssss =
+ map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) perm_f_Tssss;
val (perm_p_hss, h) = indexedd perm_p_Tss 0;
val (perm_q_hssss, h') = indexedddd perm_q_Tssss h;
@@ -915,7 +926,8 @@
val fun_names = map Binding.name_of bs;
val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
- val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
+ val frees = map (fst #>> Binding.name_of #> Free) fixes;
+ val has_call = exists_subterm (member (op =) frees);
val eqns_data =
fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) (tag_list 0 (map snd specs))
of_specs_opt []
@@ -936,7 +948,7 @@
val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
strong_coinduct_thms), lthy') =
- corec_specs_of bs arg_Ts res_Ts (get_free_indices fixes) callssss lthy;
+ corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
val corec_specs = take actual_nn corec_specs';
val ctr_specss = map #ctr_specs corec_specs;
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Feb 27 11:41:32 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Feb 27 13:04:57 2014 +0100
@@ -99,8 +99,6 @@
| NONE => error ("Unsupported recursion via type constructor " ^ quote s ^
" not corresponding to new-style datatype (cf. \"datatype_new\")"));
- fun get_var_indices (Var ((_, kk), _)) = [kk];
-
val (Tparentss_kkssss, _) = nested_Tparentss_indicessss_of [] fpT1 0;
val Tparentss = map fst Tparentss_kkssss;
val Ts = map (fst o hd) Tparentss;
@@ -110,14 +108,6 @@
val ctrss0 = map (#ctrs o #ctr_sugar) fp_sugars0;
val ctr_Tsss0 = map (map (binder_types o fastype_of)) ctrss0;
- fun apply_comps n kk =
- mk_partial_compN n (replicate n @{typ unit} ---> @{typ unit})
- (Var ((Name.uu, kk), @{typ "unit => unit"}));
-
- val callssss =
- map2 (map2 (map2 (fn kks => fn ctr_T => map (apply_comps (num_binder_types ctr_T)) kks)))
- kkssss ctr_Tsss0;
-
val b_names = Name.variant_list [] (map base_name_of_typ Ts);
val compat_b_names = map (prefix compatN) b_names;
val compat_bs = map Binding.name compat_b_names;
@@ -126,9 +116,18 @@
val nn_fp = length fpTs;
val nn = length Ts;
+ val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1);
+
+ fun apply_comps n kk =
+ mk_partial_compN n (replicate n @{typ unit} ---> @{typ unit}) (nth callers kk);
+
+ val callssss =
+ map2 (map2 (map2 (fn kks => fn ctr_T => map (apply_comps (num_binder_types ctr_T)) kks)))
+ kkssss ctr_Tsss0;
+
val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
if nn > nn_fp then
- mutualize_fp_sugars Least_FP compat_bs Ts get_var_indices callssss fp_sugars0 lthy
+ mutualize_fp_sugars Least_FP compat_bs Ts callers callssss fp_sugars0 lthy
else
((fp_sugars0, (NONE, NONE)), lthy);
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Feb 27 11:41:32 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Feb 27 13:04:57 2014 +0100
@@ -21,9 +21,9 @@
type lfp_rec_extension =
{nested_simps: thm list,
is_new_datatype: Proof.context -> string -> bool,
- get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) ->
- (term * term list list) list list -> local_theory ->
- typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
+ get_basic_lfp_sugars: binding list -> typ list -> term list ->
+ (term * term list list) list list -> local_theory ->
+ typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
term -> term -> term -> term};
@@ -92,9 +92,9 @@
type lfp_rec_extension =
{nested_simps: thm list,
is_new_datatype: Proof.context -> string -> bool,
- get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) ->
- (term * term list list) list list -> local_theory ->
- typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
+ get_basic_lfp_sugars: binding list -> typ list -> term list ->
+ (term * term list list) list list -> local_theory ->
+ typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
term -> term -> term -> term};
@@ -118,22 +118,22 @@
SOME {is_new_datatype, ...} => is_new_datatype ctxt
| NONE => K false);
-fun get_basic_lfp_sugars bs arg_Ts get_indices callssss lthy =
+fun get_basic_lfp_sugars bs arg_Ts callers callssss lthy =
(case Data.get (Proof_Context.theory_of lthy) of
- SOME {get_basic_lfp_sugars, ...} => get_basic_lfp_sugars bs arg_Ts get_indices callssss lthy
- | NONE => error "Not implemented yet");
+ SOME {get_basic_lfp_sugars, ...} => get_basic_lfp_sugars bs arg_Ts callers callssss lthy
+ | NONE => error "Functionality not loaded yet");
fun rewrite_nested_rec_call ctxt =
(case Data.get (Proof_Context.theory_of ctxt) of
SOME {rewrite_nested_rec_call, ...} => rewrite_nested_rec_call ctxt);
-fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
+fun rec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
let
val thy = Proof_Context.theory_of lthy0;
val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, nested_map_idents, nested_map_comps,
induct_thm, n2m, lthy) =
- get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0;
+ get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0;
val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
@@ -427,7 +427,8 @@
|> map (fn (x, y) => the_single y
handle List.Empty => raise PRIMREC ("missing equations for function " ^ quote x, []));
- val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
+ val frees = map (fst #>> Binding.name_of #> Free) fixes;
+ val has_call = exists_subterm (member (op =) frees);
val arg_Ts = map (#rec_type o hd) funs_data;
val res_Ts = map (#res_type o hd) funs_data;
val callssss = funs_data
@@ -444,7 +445,7 @@
| (b, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", []));
val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy) =
- rec_specs_of bs arg_Ts res_Ts (get_free_indices fixes) callssss lthy0;
+ rec_specs_of bs arg_Ts res_Ts frees callssss lthy0;
val actual_nn = length funs_data;
@@ -469,7 +470,8 @@
|> map_filter (try (fn (x, [y]) =>
(#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
|> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) =>
- mk_primrec_tac lthy' num_extra_args nested_map_idents nested_map_comps def_thms rec_thm
+ mk_primrec_tac lthy' num_extra_args nested_map_idents nested_map_comps def_thms
+ rec_thm
|> K |> Goal.prove_sorry lthy' [] [] user_eqn
(* for code extraction from proof terms: *)
|> singleton (Proof_Context.export lthy' lthy)
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Feb 27 11:41:32 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Feb 27 13:04:57 2014 +0100
@@ -26,26 +26,26 @@
{T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_defs = ctr_defs,
ctr_sugar = ctr_sugar, recx = co_rec_of iters, rec_thms = co_rec_of iter_thmss};
-fun get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0 =
+fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
let
val ((missing_arg_Ts, perm0_kks,
fp_sugars as {nested_bnfs, co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)),
lthy) =
- nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy0;
+ nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0;
val Ts = map #T fp_sugars;
+ val Xs = map #X fp_sugars;
val Cs = map (body_type o fastype_of o co_rec_of o #co_iters) fp_sugars;
- val Ts_Cs = Ts ~~ Cs;
+ val Xs_TCs = Xs ~~ (Ts ~~ Cs);
- fun zip_recT (T as Type (s, Ts)) =
- (case AList.lookup (op =) Ts_Cs T of
- SOME C => [T, C]
- | NONE => [Type (s, map (HOLogic.mk_tupleT o zip_recT) Ts)])
- | zip_recT T = [T];
+ fun zip_recT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_recT) Us)]
+ | zip_recT U =
+ (case AList.lookup (op =) Xs_TCs U of
+ SOME (T, C) => [T, C]
+ | NONE => [U]);
- val ctrss = map (#ctrs o #ctr_sugar) fp_sugars;
- val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
- val fun_arg_Tssss = map (map (map zip_recT)) ctr_Tsss;
+ val ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
+ val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_Tsss;
val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs;
val nested_map_comps = map map_comp_of_bnf nested_bnfs;
--- a/src/HOL/Tools/BNF/bnf_util.ML Thu Feb 27 11:41:32 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Feb 27 13:04:57 2014 +0100
@@ -31,10 +31,18 @@
val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list
- val map14:
- ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> 'o) ->
+ val map14: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+ 'o) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
+ val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+ 'o -> 'p) ->
+ 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
+ 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list
+ val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+ 'o -> 'p -> 'q) ->
+ 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
+ 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list
val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
@@ -202,6 +210,21 @@
map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s
| map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+fun map15 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
+ | map15 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+ (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) =
+ f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ::
+ map15 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s
+ | map15 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
+fun map16 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
+ | map16 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+ (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s)
+ (x16::x16s) =
+ f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 ::
+ map16 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s
+ | map16 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
fun fold_map4 _ [] [] [] [] acc = ([], acc)
| fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
let