# HG changeset patch # User blanchet # Date 1409581067 -7200 # Node ID 9608028d8f43e2dd3b64083d3aa872e79cba9242 # Parent 1a9ac371e5a086c3bf5f107e1cfe24a29f161194 more compatibility between old- and new-style datatypes diff -r 1a9ac371e5a0 -r 9608028d8f43 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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 diff -r 1a9ac371e5a0 -r 9608028d8f43 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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 diff -r 1a9ac371e5a0 -r 9608028d8f43 src/HOL/Tools/BNF/bnf_fp_util.ML --- 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}; diff -r 1a9ac371e5a0 -r 9608028d8f43 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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; diff -r 1a9ac371e5a0 -r 9608028d8f43 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- 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 diff -r 1a9ac371e5a0 -r 9608028d8f43 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- 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;