--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 01 16:17:47 2014 +0200
@@ -183,7 +183,7 @@
fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res
ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss common_co_inducts co_inductss
- co_rec_thmss disc_co_recss sel_co_recsss rel_injectss rel_distinctss noted =
+ co_rec_thmss co_rec_discss co_rec_selsss rel_injectss rel_distinctss noted =
let
val fp_sugars =
map_index (fn (kk, T) =>
@@ -193,8 +193,8 @@
ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk,
co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk, maps = nth mapss kk,
common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
- co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk,
- sel_co_recss = nth sel_co_recsss kk, rel_injects = nth rel_injectss kk,
+ co_rec_thms = nth co_rec_thmss kk, co_rec_discs = nth co_rec_discss kk,
+ co_rec_selss = nth co_rec_selsss kk, rel_injects = nth rel_injectss kk,
rel_distincts = nth rel_distinctss kk}
|> morph_fp_sugar (substitute_noted_thm noted)) Ts;
in
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Sep 01 16:17:47 2014 +0200
@@ -11,12 +11,12 @@
val unfold_splits_lets: term -> term
val dest_map: Proof.context -> string -> term -> term * term list
- val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
- term list list list list -> BNF_FP_Util.fp_sugar list -> local_theory ->
+ val mutualize_fp_sugars: BNF_Util.fp_kind -> bool -> int list -> binding list -> typ list ->
+ term list -> term list list list list -> BNF_FP_Util.fp_sugar list -> local_theory ->
(BNF_FP_Util.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 list ->
+ val nested_to_mutual_fps: BNF_Util.fp_kind -> bool -> binding list -> typ list -> term list ->
(term * term list list) list list -> local_theory ->
(typ list * int list * BNF_FP_Util.fp_sugar list
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
@@ -113,7 +113,8 @@
|> map_filter I;
(* TODO: test with sort constraints on As *)
-fun mutualize_fp_sugars fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy0 =
+fun mutualize_fp_sugars fp need_co_inducts_recs cliques bs fpTs callers callssss
+ (fp_sugars0 as fp_sugars01 :: _) no_defs_lthy0 =
let
val thy = Proof_Context.theory_of no_defs_lthy0;
@@ -227,74 +228,93 @@
val fp_absT_infos = map #absT_info fp_sugars0;
- val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
- dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
- fp_bnf (construct_mutualized_fp fp cliques fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
- no_defs_lthy0;
+ val (fp_res, fp_nesting_bnfs, live_nesting_bnfs, common_co_inducts, pre_bnfs, absT_infos,
+ co_recs, co_rec_defs, co_inductss, co_rec_thmss, co_rec_disc_thmss, co_rec_sel_thmsss,
+ fp_sugar_thms, lthy) =
+ if need_co_inducts_recs then
+ let
+ val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
+ dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
+ fp_bnf (construct_mutualized_fp fp cliques fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
+ no_defs_lthy0;
- val fp_abs_inverses = map #abs_inverse fp_absT_infos;
- val fp_type_definitions = map #type_definition fp_absT_infos;
+ val fp_abs_inverses = map #abs_inverse fp_absT_infos;
+ val fp_type_definitions = map #type_definition fp_absT_infos;
- val abss = map #abs absT_infos;
- val reps = map #rep absT_infos;
- val absTs = map #absT absT_infos;
- val repTs = map #repT absT_infos;
- val abs_inverses = map #abs_inverse absT_infos;
+ val abss = map #abs absT_infos;
+ val reps = map #rep absT_infos;
+ val absTs = map #absT absT_infos;
+ val repTs = map #repT absT_infos;
+ val abs_inverses = map #abs_inverse absT_infos;
- val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
- val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
+ val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
+ val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
- val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
- mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
+ val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
+ mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
- fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
+ fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
- val ((co_recs, co_rec_defs), lthy) =
- fold_map2 (fn b =>
- if fp = Least_FP then define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps
- else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss)
- fp_bs xtor_co_recs lthy
- |>> split_list;
+ val ((co_recs, co_rec_defs), lthy) =
+ fold_map2 (fn b =>
+ if fp = Least_FP then
+ define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps
+ else
+ define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss)
+ fp_bs xtor_co_recs lthy
+ |>> split_list;
- val ((common_co_inducts, co_inductss, co_rec_thmss, corec_disc_thmss, corec_sel_thmsss),
- fp_sugar_thms) =
- if fp = Least_FP then
- derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
- xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
- fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs
- lthy
- |> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
- ([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
- ||> (fn info => (SOME info, NONE))
+ val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss,
+ co_rec_sel_thmsss), fp_sugar_thms) =
+ if fp = Least_FP then
+ derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
+ xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
+ fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs
+ co_rec_defs lthy
+ |> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
+ ([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
+ ||> (fn info => (SOME info, NONE))
+ else
+ derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types)
+ xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs
+ Cs Xs ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses
+ (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs
+ (Proof_Context.export lthy no_defs_lthy) lthy
+ |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _,
+ (corec_sel_thmsss, _)) =>
+ (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
+ corec_disc_thmss, corec_sel_thmsss))
+ ||> (fn info => (NONE, SOME info));
+ in
+ (fp_res, fp_nesting_bnfs, live_nesting_bnfs, common_co_inducts, pre_bnfs, absT_infos,
+ co_recs, co_rec_defs, transpose co_inductss', co_rec_thmss, co_rec_disc_thmss,
+ co_rec_sel_thmsss, fp_sugar_thms, lthy)
+ end
else
- derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
- dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
- mss ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
- ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy
- |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _,
- (corec_sel_thmsss, _)) =>
- (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
- corec_disc_thmss, corec_sel_thmsss))
- ||> (fn info => (NONE, SOME info));
+ (#fp_res fp_sugars01, [], [], #common_co_inducts fp_sugars01, map #pre_bnf fp_sugars0,
+ map #absT_info fp_sugars0, map #co_rec fp_sugars0, map #co_rec_def fp_sugars0,
+ map #co_inducts fp_sugars0, map #co_rec_thms fp_sugars0, map #co_rec_discs fp_sugars0,
+ map #co_rec_selss fp_sugars0, (NONE, NONE), no_defs_lthy);
val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
- co_rec_def maps co_inducts co_rec_thms corec_disc_thms corec_sel_thmss
+ co_rec_def maps co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
({rel_injects, rel_distincts, ...} : fp_sugar) =
- {T = T, BT = Term.dummyT (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res,
- fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info,
- fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
- ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
- co_rec_def = co_rec_def, maps = maps, common_co_inducts = common_co_inducts,
- co_inducts = co_inducts, co_rec_thms = co_rec_thms, disc_co_recs = corec_disc_thms,
- sel_co_recss = corec_sel_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
+ {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
+ pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs,
+ live_nesting_bnfs = live_nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs,
+ ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
+ common_co_inducts = common_co_inducts, co_inducts = co_inducts,
+ co_rec_thms = co_rec_thms, co_rec_discs = co_rec_disc_thms,
+ co_rec_selss = co_rec_sel_thmss, rel_injects = rel_injects,
+ rel_distincts = rel_distincts}
|> morph_fp_sugar phi;
val target_fp_sugars =
map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
- co_recs co_rec_defs mapss (transpose co_inductss) co_rec_thmss corec_disc_thmss
- corec_sel_thmsss fp_sugars0;
+ co_recs co_rec_defs mapss co_inductss co_rec_thmss co_rec_disc_thmss co_rec_sel_thmsss
+ fp_sugars0;
val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
in
@@ -320,7 +340,8 @@
val impossible_caller = Bound ~1;
-fun nested_to_mutual_fps fp actual_bs actual_Ts actual_callers actual_callssss0 lthy =
+fun nested_to_mutual_fps fp need_co_inducts_recs 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;
@@ -336,7 +357,7 @@
fun not_mutually_nested_rec Ts1 Ts2 =
error (qsotys Ts1 ^ " is neither mutually recursive with " ^ qsotys Ts2 ^
" nor nested recursive through " ^
- (if Ts1 = Ts2 andalso can the_single Ts1 then "itself" else qsotys Ts2));
+ (if Ts1 = Ts2 andalso length Ts1 = 1 then "itself" else qsotys Ts2));
val sorted_actual_Ts =
sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts;
@@ -440,11 +461,11 @@
val perm_callssss = map2 (indexify_callsss o #ctrs o #ctr_sugar) perm_fp_sugars0 perm_callssss0;
val ((perm_fp_sugars, fp_sugar_thms), lthy) =
- if can the_single perm_Tss then
+ if length perm_Tss = 1 then
((perm_fp_sugars0, (NONE, NONE)), lthy)
else
- mutualize_fp_sugars fp perm_cliques perm_bs perm_frozen_gen_Ts perm_callers perm_callssss
- perm_fp_sugars0 lthy;
+ mutualize_fp_sugars fp need_co_inducts_recs perm_cliques perm_bs perm_frozen_gen_Ts
+ perm_callers perm_callssss perm_fp_sugars0 lthy;
val fp_sugars = unpermute perm_fp_sugars;
in
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Sep 01 16:17:47 2014 +0200
@@ -50,8 +50,8 @@
common_co_inducts: thm list,
co_inducts: thm list,
co_rec_thms: thm list,
- disc_co_recs: thm list,
- sel_co_recss: thm list list,
+ co_rec_discs: thm list,
+ co_rec_selss: thm list list,
rel_injects: thm list,
rel_distincts: thm list};
@@ -282,14 +282,14 @@
common_co_inducts: thm list,
co_inducts: thm list,
co_rec_thms: thm list,
- disc_co_recs: thm list,
- sel_co_recss: thm list list,
+ co_rec_discs: thm list,
+ co_rec_selss: thm list list,
rel_injects: thm list,
rel_distincts: thm list};
fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
- co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, rel_injects, rel_distincts} : fp_sugar) =
+ co_inducts, co_rec_thms, co_rec_discs, co_rec_selss, rel_injects, rel_distincts} : fp_sugar) =
{T = Morphism.typ phi T,
BT = Morphism.typ phi BT,
X = Morphism.typ phi X,
@@ -309,8 +309,8 @@
common_co_inducts = map (Morphism.thm phi) common_co_inducts,
co_inducts = map (Morphism.thm phi) co_inducts,
co_rec_thms = map (Morphism.thm phi) co_rec_thms,
- disc_co_recs = map (Morphism.thm phi) disc_co_recs,
- sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss,
+ co_rec_discs = map (Morphism.thm phi) co_rec_discs,
+ co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss,
rel_injects = map (Morphism.thm phi) rel_injects,
rel_distincts = map (Morphism.thm phi) rel_distincts};
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 01 16:17:47 2014 +0200
@@ -377,7 +377,7 @@
val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
- nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
+ nested_to_mutual_fps Greatest_FP true bs res_Ts callers callssss0 lthy0;
val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 16:17:47 2014 +0200
@@ -1,13 +1,25 @@
(* Title: HOL/Tools/BNF/bnf_lfp_compat.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2013
+ Copyright 2013, 2014
-Compatibility layer with the old datatype package ("datatype_compat").
+Compatibility layer with the old datatype package.
*)
signature BNF_LFP_COMPAT =
sig
- val datatype_compat_cmd : string list -> local_theory -> local_theory
+ val get_all: theory -> bool -> Old_Datatype_Aux.info Symtab.table
+ val get_info: theory -> bool -> string -> Old_Datatype_Aux.info option
+ val the_info: theory -> bool -> string -> Old_Datatype_Aux.info
+ val the_spec: theory -> bool -> string -> (string * sort) list * (string * typ list) list
+ val the_descr: theory -> bool -> string list ->
+ Old_Datatype_Aux.descr * (string * sort) list * string list * string
+ * (string list * string list) * (typ list * typ list)
+ val get_constrs: theory -> bool -> string -> (string * typ) list option
+ val interpretation: (Old_Datatype_Aux.config -> string list -> theory -> theory) -> theory ->
+ theory
+ val add_datatype: Old_Datatype_Aux.config -> Old_Datatype_Aux.spec list -> theory ->
+ string list * theory
+ val datatype_compat_cmd: string list -> local_theory -> local_theory
end;
structure BNF_LFP_Compat : BNF_LFP_COMPAT =
@@ -21,8 +33,6 @@
val compatN = "compat_";
-val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
-
fun reindex_desc desc =
let
val kks = map fst desc;
@@ -40,8 +50,8 @@
map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc
end;
-(* TODO: graceful failure for local datatypes -- perhaps by making the command global *)
-fun datatype_compat_cmd raw_fpT_names0 lthy =
+fun mk_infos_of_mutually_recursive_new_datatypes unfold_nesting need_co_inducts_recs check_names
+ raw_fpT_names0 lthy =
let
val thy = Proof_Context.theory_of lthy;
@@ -61,9 +71,9 @@
val fpTs0 as Type (_, var_As) :: _ = #Ts (#fp_res (lfp_sugar_of (hd fpT_names0)));
val fpT_names = map (fst o dest_Type) fpTs0;
- val _ = eq_set (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
+ val _ = check_names (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
- val (As_names, _) = lthy |> Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As);
+ val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) lthy;
val As = map2 (fn s => fn TVar (_, S) => TFree (s, S)) As_names var_As;
val fpTs = map (fn s => Type (s, As)) fpT_names;
@@ -78,8 +88,11 @@
val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names;
val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
val all_infos = Old_Datatype_Data.get_all thy;
- val (orig_descr' :: nested_descrs, _) =
- Old_Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp;
+ val (orig_descr' :: nested_descrs) =
+ if unfold_nesting then
+ fst (Old_Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp)
+ else
+ [orig_descr];
fun cliquify_descr [] = []
| cliquify_descr [entry] = [[entry]]
@@ -124,11 +137,11 @@
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;
- val common_name = compatN ^ mk_common_name b_names;
- val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
+ val ((fp_sugars, (lfp_sugar_thms, _)), lthy') =
if nn > nn_fp then
- mutualize_fp_sugars Least_FP cliques compat_bs Ts callers callssss fp_sugars0 lthy
+ mutualize_fp_sugars Least_FP need_co_inducts_recs cliques compat_bs Ts callers callssss
+ fp_sugars0 lthy
else
((fp_sugars0, (NONE, NONE)), lthy);
@@ -148,12 +161,113 @@
split_asm = split_asm});
val infos = map_index mk_info (take nn_fp fp_sugars);
+ in
+ (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy')
+ end;
+
+fun infos_of_new_datatype_mutual_cluster lthy unfold_nesting raw_fpt_names01 =
+ mk_infos_of_mutually_recursive_new_datatypes unfold_nesting false subset [raw_fpt_names01] lthy
+ |> #5;
+
+fun get_all thy unfold_nesting =
+ let
+ val lthy = Named_Target.theory_init thy;
+ val old_info_tab = Old_Datatype_Data.get_all thy;
+ val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy
+ |> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s));
+ val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy unfold_nesting) new_T_names;
+ in
+ fold (if unfold_nesting then Symtab.default else Symtab.update) new_infos old_info_tab
+ end;
+
+fun get_one get_old get_new thy unfold_nesting x =
+ let val (get_fst, get_snd) = (get_new thy unfold_nesting, get_old thy) |> unfold_nesting ? swap in
+ (case get_fst x of NONE => get_snd x | res => res)
+ end;
+
+fun get_info_of_new_datatype thy unfold_nesting T_name =
+ let val lthy = Named_Target.theory_init thy in
+ AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy unfold_nesting T_name) T_name
+ end;
+
+val get_info = get_one Old_Datatype_Data.get_info get_info_of_new_datatype;
+
+fun the_info thy unfold_nesting T_name =
+ (case get_info thy unfold_nesting T_name of
+ SOME info => info
+ | NONE => error ("Unknown datatype " ^ quote T_name));
+
+fun the_spec thy unfold_nesting T_name =
+ let
+ val {descr, index, ...} = the_info thy unfold_nesting T_name;
+ val (_, Ds, ctrs0) = the (AList.lookup (op =) descr index);
+ val Ts = map Old_Datatype_Aux.dest_DtTFree Ds;
+ val ctrs = map (apsnd (map (Old_Datatype_Aux.typ_of_dtyp descr))) ctrs0;
+ in (Ts, ctrs) end;
+
+fun the_descr thy unfold_nesting (T_names0 as T_name01 :: _) =
+ let
+ fun not_mutually_recursive ss =
+ error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes");
+
+ val info = the_info thy unfold_nesting T_name01;
+ val descr = #descr info;
+
+ val (_, Ds, _) = the (AList.lookup (op =) descr (#index info));
+ val vs = map Old_Datatype_Aux.dest_DtTFree Ds;
+
+ fun is_DtTFree (Old_Datatype_Aux.DtTFree _) = true
+ | is_DtTFree _ = false;
+
+ val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
+ val protoTs as (dataTs, _) = chop k descr
+ |> (pairself o map)
+ (fn (_, (T_name, Ds, _)) => (T_name, map (Old_Datatype_Aux.typ_of_dtyp descr) Ds));
+
+ val T_names = map fst dataTs;
+ val _ = eq_set (op =) (T_names, T_names0) orelse not_mutually_recursive T_names0
+
+ val (Ts, Us) = (pairself o map) Type protoTs;
+
+ val names = map Long_Name.base_name T_names;
+ val (auxnames, _) = Name.make_context names
+ |> fold_map (Name.variant o Old_Datatype_Aux.name_of_typ) Us;
+ val prefix = space_implode "_" names;
+ in
+ (descr, vs, T_names, prefix, (names, auxnames), (Ts, Us))
+ end;
+
+fun get_constrs thy unfold_nesting T_name =
+ try (the_spec thy unfold_nesting) T_name
+ |> Option.map (fn (Ts, ctrs) =>
+ let
+ fun subst (v, S) = TVar ((v, 0), S);
+ fun subst_ty (TFree v) = subst v
+ | subst_ty ty = ty;
+ val dataT = Type (T_name, map subst Ts);
+ fun mk_ctr_typ Ts = map (Term.map_atyps subst_ty) Ts ---> dataT;
+ in
+ map (apsnd mk_ctr_typ) ctrs
+ end);
+
+fun interpretation f thy = Old_Datatype_Data.interpretation f thy;
+
+fun add_datatype config specs thy = ([], thy);
+
+val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
+
+fun datatype_compat_cmd raw_fpT_names0 lthy =
+ let
+ val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') =
+ mk_infos_of_mutually_recursive_new_datatypes true true eq_set raw_fpT_names0 lthy;
val all_notes =
(case lfp_sugar_thms of
NONE => []
| SOME ((induct_thms, induct_thm, induct_attrs), (rec_thmss, _)) =>
let
+ val common_name = compatN ^ mk_common_name b_names;
+
val common_notes =
(if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
|> filter_out (null o #2)
@@ -179,7 +293,7 @@
Old_Datatype_Data.register infos
#> Old_Datatype_Data.interpretation_data (Old_Datatype_Aux.default_config, map fst infos);
in
- lthy
+ lthy'
|> Local_Theory.raw_theory register_interpret
|> Local_Theory.notes all_notes
|> snd
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Sep 01 16:17:47 2014 +0200
@@ -31,7 +31,7 @@
val ((missing_arg_Ts, perm0_kks,
fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
(lfp_sugar_thms, _)), lthy) =
- nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0;
+ nested_to_mutual_fps Least_FP true bs arg_Ts callers callssss0 lthy0;
val Ts = map #T fp_sugars;
val Xs = map #X fp_sugars;