# HG changeset patch # User blanchet # Date 1409870461 -7200 # Node ID cc71d2be4f0acce777751469fdd4406bf3c0e6f6 # Parent d2ddd401d74dbd014ac5ce686d055ea53dd1f5e5 introduced mechanism to filter interpretations diff -r d2ddd401d74d -r cc71d2be4f0a src/HOL/Ctr_Sugar.thy --- a/src/HOL/Ctr_Sugar.thy Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Ctr_Sugar.thy Fri Sep 05 00:41:01 2014 +0200 @@ -30,12 +30,12 @@ ML_file "Tools/Ctr_Sugar/case_translation.ML" lemma iffI_np: "\x \ \ y; \ x \ y\ \ \ x \ y" -by (erule iffI) (erule contrapos_pn) + by (erule iffI) (erule contrapos_pn) lemma iff_contradict: -"\ P \ P \ Q \ Q \ R" -"\ Q \ P \ Q \ P \ R" -by blast+ + "\ P \ P \ Q \ Q \ R" + "\ Q \ P \ Q \ P \ R" + by blast+ ML_file "Tools/Ctr_Sugar/local_interpretation.ML" ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML" diff -r d2ddd401d74d -r cc71d2be4f0a src/HOL/Library/bnf_axiomatization.ML --- a/src/HOL/Library/bnf_axiomatization.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Library/bnf_axiomatization.ML Fri Sep 05 00:41:01 2014 +0200 @@ -91,7 +91,7 @@ val (bnf, lthy') = after_qed mk_wit_thms thms lthy in - (bnf, BNF_Def.register_bnf key bnf lthy') + (bnf, BNF_Def.register_bnf (K true) key bnf lthy') end; val bnf_axiomatization = prepare_decl (K I) (K I); diff -r d2ddd401d74d -r cc71d2be4f0a src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 05 00:41:01 2014 +0200 @@ -19,9 +19,9 @@ val bnf_of_global: theory -> string -> bnf option val bnf_interpretation: string -> (bnf -> theory -> theory) -> (bnf -> local_theory -> local_theory) -> theory -> theory - val interpret_bnf: bnf -> local_theory -> local_theory + val interpret_bnf: (string -> bool) -> bnf -> local_theory -> local_theory val register_bnf_raw: string -> bnf -> local_theory -> local_theory - val register_bnf: string -> bnf -> local_theory -> local_theory + val register_bnf: (string -> bool) -> string -> bnf -> local_theory -> local_theory val name_of_bnf: bnf -> binding val T_of_bnf: bnf -> typ @@ -1532,8 +1532,8 @@ Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf))); -fun register_bnf key bnf = - register_bnf_raw key bnf #> interpret_bnf bnf; +fun register_bnf keep key bnf = + register_bnf_raw key bnf #> interpret_bnf keep bnf; fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs = (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) => @@ -1572,7 +1572,7 @@ | SOME tac => (mk_triv_wit_thms tac, [])); in Proof.unfolding ([[(defs, [])]]) - (Proof.theorem NONE (uncurry (register_bnf key) oo after_qed mk_wit_thms) + (Proof.theorem NONE (uncurry (register_bnf (K true) key) oo after_qed mk_wit_thms) (map (single o rpair []) goals @ nontriv_wit_goals) lthy) end) oo prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term NONE Binding.empty Binding.empty []; diff -r d2ddd401d74d -r cc71d2be4f0a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 05 00:41:01 2014 +0200 @@ -41,9 +41,9 @@ val fp_sugars_of_global: theory -> fp_sugar list val fp_sugars_interpretation: string -> (fp_sugar list -> theory -> theory) -> (fp_sugar list -> local_theory -> local_theory)-> theory -> theory - val interpret_fp_sugars: fp_sugar list -> local_theory -> local_theory + val interpret_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory - val register_fp_sugars: fp_sugar list -> local_theory -> local_theory + val register_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory val co_induct_of: 'a list -> 'a val strong_co_induct_of: 'a list -> 'a @@ -236,8 +236,8 @@ (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar)))) fp_sugars; -fun register_fp_sugars fp_sugars = - register_fp_sugars_raw fp_sugars #> interpret_fp_sugars fp_sugars; +fun register_fp_sugars keep fp_sugars = + register_fp_sugars_raw fp_sugars #> interpret_fp_sugars keep fp_sugars; fun interpret_bnfs_register_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 @@ -258,8 +258,8 @@ |> morph_fp_sugar (substitute_noted_thm noted)) Ts; in register_fp_sugars_raw fp_sugars - #> fold interpret_bnf (#bnfs fp_res) - #> interpret_fp_sugars fp_sugars + #> fold (interpret_bnf (K true)) (#bnfs fp_res) + #> interpret_fp_sugars (K true) fp_sugars end; (* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A", diff -r d2ddd401d74d -r cc71d2be4f0a src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 05 00:41:01 2014 +0200 @@ -46,10 +46,10 @@ val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option val ctr_sugar_interpretation: string -> (ctr_sugar -> theory -> theory) -> (ctr_sugar -> local_theory -> local_theory) -> theory -> theory - val interpret_ctr_sugar: ctr_sugar -> local_theory -> local_theory + val interpret_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory - val register_ctr_sugar: ctr_sugar -> local_theory -> local_theory - val default_register_ctr_sugar_global: ctr_sugar -> theory -> theory + val register_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory + val default_register_ctr_sugar_global: (string -> bool) -> ctr_sugar -> theory -> theory val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list @@ -193,17 +193,17 @@ Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.update (s, morph_ctr_sugar phi ctr_sugar))); -fun register_ctr_sugar ctr_sugar = - register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar ctr_sugar; +fun register_ctr_sugar keep ctr_sugar = + register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar keep ctr_sugar; -fun default_register_ctr_sugar_global (ctr_sugar as {T = Type (s, _), ...}) thy = +fun default_register_ctr_sugar_global keep (ctr_sugar as {T = Type (s, _), ...}) thy = let val tab = Data.get (Context.Theory thy) in if Symtab.defined tab s then thy else thy |> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab)) - |> Ctr_Sugar_Interpretation.data_global ctr_sugar + |> Ctr_Sugar_Interpretation.data_global keep ctr_sugar end; val isN = "is_"; @@ -1045,7 +1045,7 @@ case_eq_ifs = case_eq_if_thms} |> morph_ctr_sugar (substitute_noted_thm noted); in - (ctr_sugar, lthy' |> register_ctr_sugar ctr_sugar) + (ctr_sugar, lthy' |> register_ctr_sugar (K true) ctr_sugar) end; in (goalss, after_qed, lthy') diff -r d2ddd401d74d -r cc71d2be4f0a src/HOL/Tools/Ctr_Sugar/local_interpretation.ML --- a/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML Fri Sep 05 00:41:01 2014 +0200 @@ -13,8 +13,8 @@ val result: theory -> T list val interpretation: string -> (T -> theory -> theory) -> (T -> local_theory -> local_theory) -> theory -> theory - val data: T -> local_theory -> local_theory - val data_global: T -> theory -> theory + val data: (string -> bool) -> T -> local_theory -> local_theory + val data_global: (string -> bool) -> T -> theory -> theory val init: theory -> theory end; @@ -26,9 +26,9 @@ structure Interp = Theory_Data ( type T = - (Name_Space.naming * T) list + ((Name_Space.naming * (string -> bool)) * T) list * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * (string * stamp)) - * (Name_Space.naming * T) list) list; + * ((Name_Space.naming * (string -> bool)) * T) list) list; val empty = ([], []); val extend = I; fun merge ((data1, interps1), (data2, interps2)) : T = @@ -41,10 +41,17 @@ fun consolidate_common g_or_f lift_lthy thy thy_or_lthy = let val (data, interps) = Interp.get thy; - val unfinished = interps |> map (fn ((gf, _), data') => + + fun unfinished_of ((gf, (name, _)), data') = (g_or_f gf, - if eq_list (eq_snd eq) (data', data) then [] else subtract (eq_snd eq) data' data)); - val finished = interps |> map (apsnd (K data)); + if eq_list (eq_snd eq) (data', data) then + [] + else + subtract (eq_snd eq) data' data + |> map_filter (fn ((naming, keep), x) => if keep name then SOME (naming, x) else NONE)); + + val unfinished = map unfinished_of interps; + val finished = map (apsnd (K data)) interps; in if forall (null o #2) unfinished then NONE @@ -64,12 +71,13 @@ fun interpretation name g f = Interp.map (apsnd (cons (((g, f), (name, stamp ())), []))) #> perhaps consolidate_global; -fun data x = - Local_Theory.background_theory (fn thy => Interp.map (apfst (cons (Sign.naming_of thy, x))) thy) +fun data keep x = + Local_Theory.background_theory + (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy) #> perhaps consolidate; -fun data_global x = - (fn thy => Interp.map (apfst (cons (Sign.naming_of thy, x))) thy) +fun data_global keep x = + (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy) #> perhaps consolidate_global; val init = Theory.at_begin consolidate_global; diff -r d2ddd401d74d -r cc71d2be4f0a src/HOL/Tools/Old_Datatype/old_datatype_data.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Fri Sep 05 00:41:01 2014 +0200 @@ -135,7 +135,7 @@ map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos), cases = cases |> fold Symtab.update (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #> - fold (Ctr_Sugar.default_register_ctr_sugar_global o ctr_sugar_of_info o snd) dt_infos; + fold (Ctr_Sugar.default_register_ctr_sugar_global (K true) o ctr_sugar_of_info o snd) dt_infos; (* complex queries *) diff -r d2ddd401d74d -r cc71d2be4f0a src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Sep 05 00:41:01 2014 +0200 +++ b/src/HOL/Tools/record.ML Fri Sep 05 00:41:01 2014 +0200 @@ -1782,7 +1782,7 @@ else thy; fun add_ctr_sugar ctr sels exhaust inject sel_defs sel_thms = - Ctr_Sugar.default_register_ctr_sugar_global + Ctr_Sugar.default_register_ctr_sugar_global (K true) {T = body_type (fastype_of ctr), ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels], exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject], distincts = [], case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm,