# HG changeset patch # User blanchet # Date 1409592480 -7200 # Node ID 1abeda3c3bc275cae17211fb6a6d6a1d37356214 # Parent 5e9170812356abb5c47601d3410823353f0cd7b7 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat' diff -r 5e9170812356 -r 1abeda3c3bc2 src/HOL/BNF_Examples/Compat.thy --- a/src/HOL/BNF_Examples/Compat.thy Mon Sep 01 18:42:02 2014 +0200 +++ b/src/HOL/BNF_Examples/Compat.thy Mon Sep 01 19:28:00 2014 +0200 @@ -58,7 +58,7 @@ datatype_compat s ML \ get_descrs @{theory} (1, 1, 1) @{type_name s}; \ -ML \ get_descrs @{theory} (0, 3, 1) @{type_name x}; \ +ML \ get_descrs @{theory} (0, 1, 1) @{type_name x}; \ datatype_compat x @@ -66,7 +66,7 @@ datatype_new 'a tttre = TTTre 'a "'a tttre lst lst lst" -ML \ get_descrs @{theory} (0, 4, 1) @{type_name tttre}; \ +ML \ get_descrs @{theory} (0, 1, 1) @{type_name tttre}; \ datatype_compat tttre @@ -74,7 +74,7 @@ datatype_new 'a ftre = FEmp | FTre "'a \ 'a ftre lst" -ML \ get_descrs @{theory} (0, 2, 1) @{type_name ftre}; \ +ML \ get_descrs @{theory} (0, 1, 1) @{type_name ftre}; \ datatype_compat ftre @@ -82,7 +82,7 @@ datatype_new 'a btre = BTre 'a "'a btre lst" "'a btre lst" -ML \ get_descrs @{theory} (0, 3, 1) @{type_name btre}; \ +ML \ get_descrs @{theory} (0, 1, 1) @{type_name btre}; \ datatype_compat btre @@ -100,7 +100,7 @@ datatype_new 'a tre = Tre 'a "'a tre lst" -ML \ get_descrs @{theory} (0, 2, 1) @{type_name tre}; \ +ML \ get_descrs @{theory} (0, 1, 1) @{type_name tre}; \ datatype_compat tre @@ -124,7 +124,7 @@ ML \ get_descrs @{theory} (2, 2, 2) @{type_name f}; \ ML \ get_descrs @{theory} (2, 2, 2) @{type_name g}; \ -ML \ get_descrs @{theory} (0, 3, 1) @{type_name h}; \ +ML \ get_descrs @{theory} (0, 1, 1) @{type_name h}; \ datatype_compat h @@ -187,7 +187,7 @@ datatype_new tree = Tree "tree foo" -ML \ get_descrs @{theory} (0, 3, 1) @{type_name tree}; \ +ML \ get_descrs @{theory} (0, 1, 1) @{type_name tree}; \ datatype_compat tree diff -r 5e9170812356 -r 1abeda3c3bc2 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Sep 01 18:42:02 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Sep 01 19:28:00 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 -> bool -> 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 -> 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 -> bool -> binding list -> typ list -> term 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_Util.fp_sugar list * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) @@ -113,8 +113,8 @@ |> map_filter I; (* TODO: test with sort constraints on As *) -fun mutualize_fp_sugars fp need_co_inducts_recs cliques bs fpTs callers callssss - (fp_sugars0 as fp_sugars01 :: _) no_defs_lthy0 = +fun mutualize_fp_sugars fp cliques bs fpTs callers callssss (fp_sugars0 as fp_sugars01 :: _) + no_defs_lthy0 = let val thy = Proof_Context.theory_of no_defs_lthy0; @@ -228,73 +228,58 @@ val fp_absT_infos = map #absT_info fp_sugars0; - 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 ((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 ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss, - co_rec_sel_thmsss), fp_sugar_thms) = + val ((co_recs, co_rec_defs), lthy) = + fold_map2 (fn b => 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)) + define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps 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 - (#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); + 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, 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)); val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0; @@ -313,8 +298,8 @@ 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 co_inductss co_rec_thmss co_rec_disc_thmss co_rec_sel_thmsss - fp_sugars0; + co_recs co_rec_defs mapss (transpose 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 @@ -340,8 +325,7 @@ val impossible_caller = Bound ~1; -fun nested_to_mutual_fps fp need_co_inducts_recs actual_bs actual_Ts actual_callers actual_callssss0 - lthy = +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; @@ -464,8 +448,8 @@ if length perm_Tss = 1 then ((perm_fp_sugars0, (NONE, NONE)), lthy) else - mutualize_fp_sugars fp need_co_inducts_recs perm_cliques perm_bs perm_frozen_gen_Ts - perm_callers perm_callssss perm_fp_sugars0 lthy; + mutualize_fp_sugars fp 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 5e9170812356 -r 1abeda3c3bc2 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 01 18:42:02 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 01 19:28:00 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 true bs res_Ts callers callssss0 lthy0; + 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; diff -r 5e9170812356 -r 1abeda3c3bc2 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 18:42:02 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 19:28:00 2014 +0200 @@ -62,8 +62,7 @@ map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc end; -fun mk_infos_of_mutually_recursive_new_datatypes nesting_pref need_co_inducts_recs check_names - fpT_names0 lthy = +fun mk_infos_of_mutually_recursive_new_datatypes nesting_pref check_names fpT_names0 lthy = let val thy = Proof_Context.theory_of lthy; @@ -146,8 +145,7 @@ val ((fp_sugars, (lfp_sugar_thms, _)), lthy') = if nn > nn_fp then - mutualize_fp_sugars Least_FP need_co_inducts_recs cliques compat_bs Ts callers callssss - fp_sugars0 lthy + mutualize_fp_sugars Least_FP cliques compat_bs Ts callers callssss fp_sugars0 lthy else ((fp_sugars0, (NONE, NONE)), lthy); @@ -171,16 +169,9 @@ (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') end; -fun infos_of_new_datatype_mutual_cluster lthy nesting_pref fpT_name = - let - fun infos_of nesting_pref = - #5 (mk_infos_of_mutually_recursive_new_datatypes nesting_pref false subset [fpT_name] lthy); - in - infos_of nesting_pref - handle ERROR _ => - (if nesting_pref = Unfold_Nesting then infos_of Keep_Nesting else []) - handle ERROR _ => [] - end; +fun infos_of_new_datatype_mutual_cluster lthy fpT_name = + #5 (mk_infos_of_mutually_recursive_new_datatypes Keep_Nesting subset [fpT_name] lthy) + handle ERROR _ => []; fun get_all thy nesting_pref = let @@ -188,23 +179,20 @@ 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 nesting_pref) new_T_names; + val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy) new_T_names; in fold (if nesting_pref = Keep_Nesting then Symtab.update else Symtab.default) new_infos old_info_tab end; fun get_one get_old get_new thy nesting_pref x = - let - val (get_fst, get_snd) = - (get_old thy, get_new thy nesting_pref) |> nesting_pref = Keep_Nesting ? swap - in + let val (get_fst, get_snd) = (get_old thy, get_new thy) |> nesting_pref = Keep_Nesting ? swap in (case get_fst x of NONE => get_snd x | res => res) end; -fun get_info_of_new_datatype thy nesting_pref T_name = +fun get_info_of_new_datatype thy T_name = let val lthy = Proof_Context.init_global thy in - AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy nesting_pref T_name) T_name + AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy T_name) T_name end; val get_info = get_one Old_Datatype_Data.get_info get_info_of_new_datatype; @@ -293,7 +281,7 @@ fun datatype_compat fpT_names lthy = let val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') = - mk_infos_of_mutually_recursive_new_datatypes Unfold_Nesting true eq_set fpT_names lthy; + mk_infos_of_mutually_recursive_new_datatypes Unfold_Nesting eq_set fpT_names lthy; val all_notes = (case lfp_sugar_thms of diff -r 5e9170812356 -r 1abeda3c3bc2 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Sep 01 18:42:02 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Sep 01 19:28:00 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 true bs arg_Ts callers 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;