# HG changeset patch # User blanchet # Date 1473167042 -7200 # Node ID 94336cf98486ad602351018fd5cf774d36a2ca19 # Parent 83841a5c08973401ea25be9882932d5e433a6af6 generalized ML signature diff -r 83841a5c0897 -r 94336cf98486 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Tue Sep 06 11:55:39 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Tue Sep 06 15:04:02 2016 +0200 @@ -807,29 +807,29 @@ val mk_abs = mk_abs_or_rep range_type; val mk_rep = mk_abs_or_rep domain_type; -fun maybe_typedef ctxt force_out_of_line (b, As, mx) set opt_morphs tac = +fun maybe_typedef force_out_of_line (b, As, mx) set opt_morphs tac lthy = let - val threshold = Config.get ctxt typedef_threshold; + val threshold = Config.get lthy typedef_threshold; val repT = HOLogic.dest_setT (fastype_of set); val out_of_line = force_out_of_line orelse (threshold >= 0 andalso Term.size_of_typ repT >= threshold); in if out_of_line then - typedef (b, As, mx) set opt_morphs tac - #>> (fn (T_name, ({Rep_name, Abs_name, ...}, + typedef (b, As, mx) set opt_morphs tac lthy + |>> (fn (T_name, ({Rep_name, Abs_name, ...}, {type_definition, Abs_inverse, Abs_inject, Abs_cases, ...}) : Typedef.info) => (Type (T_name, map TFree As), (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, Abs_cases))) else - pair (repT, + ((repT, (@{const_name id_bnf}, @{const_name id_bnf}, @{thm type_definition_id_bnf_UNIV}, @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV]}, @{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV]}, - @{thm type_definition.Abs_cases[OF type_definition_id_bnf_UNIV]})) + @{thm type_definition.Abs_cases[OF type_definition_id_bnf_UNIV]})), lthy) end; -fun seal_bnf qualify (unfold_set : unfold_set) b has_live_phantoms Ds bnf lthy = +fun seal_bnf qualify (unfold_set : unfold_set) b force_out_of_line Ds bnf lthy = let val live = live_of_bnf bnf; val nwits = nwits_of_bnf bnf; @@ -847,10 +847,10 @@ val T_bind = qualify b; val all_TA_params_in_order = Term.add_tfreesT repTA As'; val TA_params = - (if has_live_phantoms then all_TA_params_in_order + (if force_out_of_line then all_TA_params_in_order else inter (op =) (Term.add_tfreesT repTA []) all_TA_params_in_order); val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) = - maybe_typedef lthy has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE + maybe_typedef force_out_of_line (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; val repTB = mk_T_of_bnf Ds Bs bnf; @@ -882,8 +882,8 @@ val all_deads = map TFree (fold Term.add_tfreesT Ds []); val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) = - maybe_typedef lthy false (bdT_bind, params, NoSyn) - (HOLogic.mk_UNIV bd_repT) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; + maybe_typedef false (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE + (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) = if bdT = bd_repT then (bnf_bd, bd_Card_order_of_bnf bnf RS @{thm ordIso_refl}, @@ -920,7 +920,7 @@ rtac ctxt (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1; fun rel_OO_Grp_tac ctxt = (rtac ctxt (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN' - (if has_live_phantoms then subst_tac ctxt NONE else SELECT_GOAL o unfold_thms_tac ctxt) + (if force_out_of_line then subst_tac ctxt NONE else SELECT_GOAL o unfold_thms_tac ctxt) [type_definition RS @{thm vimage2p_relcompp_converse}] THEN' SELECT_GOAL (unfold_thms_tac ctxt [o_apply, type_definition RS @{thm type_copy_vimage2p_Grp_Rep}, diff -r 83841a5c0897 -r 94336cf98486 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Sep 06 11:55:39 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Sep 06 15:04:02 2016 +0200 @@ -2172,8 +2172,9 @@ xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts, xtor_co_rec_transfers, xtor_co_rec_o_maps, ...}, lthy)) = - fixpoint_bnf I (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs (map dest_TFree As) - (map dest_TFree killed_As) (map dest_TFree Xs) ctrXs_repTs empty_comp_cache no_defs_lthy + fixpoint_bnf false I (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs + (map dest_TFree As) (map dest_TFree killed_As) (map dest_TFree Xs) ctrXs_repTs + empty_comp_cache no_defs_lthy handle BAD_DEAD (X, X_backdrop) => (case X_backdrop of Type (bad_tc, _) => diff -r 83841a5c0897 -r 94336cf98486 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Sep 06 11:55:39 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Sep 06 15:04:02 2016 +0200 @@ -240,7 +240,7 @@ 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)) = - fixpoint_bnf I (construct_mutualized_fp fp mutual_cliques fpTs indexed_fp_ress) + fixpoint_bnf false I (construct_mutualized_fp fp mutual_cliques fpTs indexed_fp_ress) fp_bs As' killed_As' (map dest_TFree Xs) ctrXs_repTs empty_comp_cache no_defs_lthy; val time = time lthy; diff -r 83841a5c0897 -r 94336cf98486 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Sep 06 11:55:39 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Sep 06 15:04:02 2016 +0200 @@ -206,7 +206,7 @@ (term list * (thm list * thm * thm list * thm list)) * local_theory val raw_qualify: (binding -> binding) -> binding -> binding -> binding - val fixpoint_bnf: (binding -> binding) -> + val fixpoint_bnf: bool -> (binding -> binding) -> (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) -> binding list -> (string * sort) list -> (string * sort) list -> (string * sort) list -> @@ -925,7 +925,8 @@ #> extra_qualify #> Binding.concealed end; -fun fixpoint_bnf extra_qualify construct_fp bs resBs Ds0 Xs rhsXs comp_cache0 lthy = +fun fixpoint_bnf force_out_of_line extra_qualify construct_fp bs resBs Ds0 Xs rhsXs comp_cache0 + lthy = let val time = time lthy; val timer = time (Timer.startRealTimer ()); @@ -962,9 +963,9 @@ #> extra_qualify #> not (Config.get lthy'' bnf_internals) ? Binding.concealed; - val ((pre_bnfs, (deadss, absT_infos)), lthy''') = - @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) - bs (not (null live_phantoms) :: replicate (length rhsXs - 1) false) Dss bnfs' lthy'' + val ((pre_bnfs, (deadss, absT_infos)), lthy''') = lthy'' + |> @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) + bs (replicate (length rhsXs) (force_out_of_line orelse not (null live_phantoms))) Dss bnfs' |>> split_list |>> apsnd split_list;