# HG changeset patch # User blanchet # Date 1409777345 -7200 # Node ID 1661312763808467a9165dd8c12ccce09e0c17b0 # Parent 710710a66173446fe9fecf1e3033a9160ac5dc5c introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales diff -r 710710a66173 -r 166131276380 src/HOL/Ctr_Sugar.thy --- a/src/HOL/Ctr_Sugar.thy Wed Sep 03 22:47:48 2014 +0200 +++ b/src/HOL/Ctr_Sugar.thy Wed Sep 03 22:49:05 2014 +0200 @@ -37,6 +37,7 @@ "\ Q \ P \ Q \ P \ R" by blast+ +ML_file "Tools/Ctr_Sugar/local_interpretation.ML" ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML" ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML" ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML" diff -r 710710a66173 -r 166131276380 src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Wed Sep 03 22:47:48 2014 +0200 +++ b/src/HOL/Lifting.thy Wed Sep 03 22:49:05 2014 +0200 @@ -556,11 +556,8 @@ lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2 ML_file "Tools/Lifting/lifting_bnf.ML" - ML_file "Tools/Lifting/lifting_term.ML" - ML_file "Tools/Lifting/lifting_def.ML" - ML_file "Tools/Lifting/lifting_setup.ML" hide_const (open) POS NEG diff -r 710710a66173 -r 166131276380 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Wed Sep 03 22:47:48 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Sep 03 22:49:05 2014 +0200 @@ -17,7 +17,10 @@ val transfer_bnf: theory -> bnf -> bnf val bnf_of: Proof.context -> string -> bnf option val bnf_of_global: theory -> string -> bnf option - val bnf_interpretation: (bnf -> theory -> theory) -> theory -> theory + val bnf_interpretation: (bnf -> theory -> theory) -> (bnf -> local_theory -> local_theory) -> + theory -> theory + val interpret_bnf: 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 name_of_bnf: bnf -> binding @@ -1512,7 +1515,7 @@ (key, goals, wit_goalss, after_qed, lthy, one_step_defs) end; -structure BNF_Interpretation = Interpretation +structure BNF_Interpretation = Local_Interpretation ( type T = bnf; val eq: T * T -> bool = op = o pairself T_of_bnf; @@ -1533,13 +1536,14 @@ |> Sign.restore_naming thy end; -fun bnf_interpretation f = BNF_Interpretation.interpretation (with_repaired_path f); +val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path; +val interpret_bnf = BNF_Interpretation.data; -fun register_bnf key bnf = +fun register_bnf_raw key bnf = Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf))) - #> Local_Theory.background_theory - (fn thy => BNF_Interpretation.data (the (bnf_of_global thy key)) thy); + (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 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) => diff -r 710710a66173 -r 166131276380 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Sep 03 22:47:48 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Sep 03 22:49:05 2014 +0200 @@ -12,7 +12,8 @@ val fp_sugar_of_global: theory -> string -> BNF_FP_Util.fp_sugar option val fp_sugars_of: Proof.context -> BNF_FP_Util.fp_sugar list val fp_sugars_of_global: theory -> BNF_FP_Util.fp_sugar list - val fp_sugar_interpretation: (BNF_FP_Util.fp_sugar list -> theory -> theory) -> theory -> theory + val fp_sugar_interpretation: (BNF_FP_Util.fp_sugar list -> theory -> theory) -> + (BNF_FP_Util.fp_sugar list -> local_theory -> local_theory)-> theory -> theory val register_fp_sugars: BNF_FP_Util.fp_sugar list -> local_theory -> local_theory val co_induct_of: 'a list -> 'a @@ -158,7 +159,7 @@ fun co_induct_of (i :: _) = i; fun strong_co_induct_of [_, s] = s; -structure FP_Sugar_Interpretation = Interpretation +structure FP_Sugar_Interpretation = Local_Interpretation ( type T = fp_sugar list; val eq: T * T -> bool = op = o pairself (map #T); @@ -171,7 +172,7 @@ |> f (map (transfer_fp_sugar thy) fp_sugars) |> Sign.restore_naming thy; -fun fp_sugar_interpretation f = FP_Sugar_Interpretation.interpretation (with_repaired_path f); +val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path; fun register_fp_sugars (fp_sugars as {fp, ...} :: _) = fold (fn fp_sugar as {T = Type (s, _), ...} => @@ -179,12 +180,12 @@ (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar)))) fp_sugars #> fp = Least_FP ? generate_lfp_size fp_sugars - #> Local_Theory.background_theory (fn thy => FP_Sugar_Interpretation.data - (map (the o fp_sugar_of_global thy o fst o dest_Type o #T) fp_sugars) thy); + #> FP_Sugar_Interpretation.data fp_sugars; -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 co_rec_discss co_rec_selsss rel_injectss rel_distinctss noted = +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 + common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss + rel_distinctss noted = let val fp_sugars = map_index (fn (kk, T) => @@ -199,7 +200,8 @@ rel_distincts = nth rel_distinctss kk} |> morph_fp_sugar (substitute_noted_thm noted)) Ts; in - register_fp_sugars fp_sugars + fold interpret_bnf (#bnfs fp_res) + #> register_fp_sugars fp_sugars end; (* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A", @@ -1972,10 +1974,10 @@ (* for "datatype_realizer.ML": *) |>> name_noted_thms (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN - |-> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs - live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm] - (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss - rel_distinctss + |-> interpret_bnfs_register_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos + fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs + mapss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) + rel_injectss rel_distinctss end; fun derive_note_coinduct_corecs_thms_for_types @@ -2064,13 +2066,15 @@ |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs) [flat corec_sel_thmss, flat corec_thmss] |> Local_Theory.notes (common_notes @ notes) - |-> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs - live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss - [coinduct_thm, coinduct_strong_thm] (transpose [coinduct_thms, coinduct_strong_thms]) - corec_thmss corec_disc_thmss corec_sel_thmsss rel_injectss rel_distinctss + |-> interpret_bnfs_register_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos + fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs + mapss [coinduct_thm, coinduct_strong_thm] + (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss + corec_sel_thmsss rel_injectss rel_distinctss end; val lthy'' = lthy' + |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~ xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~ diff -r 710710a66173 -r 166131276380 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Sep 03 22:47:48 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Wed Sep 03 22:49:05 2014 +0200 @@ -2435,8 +2435,7 @@ fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms => fn consts => bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms) - (SOME deads) map_b rel_b set_bs consts - #> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy))) + (SOME deads) map_b rel_b set_bs consts) bs tacss map_bs rel_bs set_bss wit_thmss ((((((replicate n Binding.empty ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ all_witss) ~~ map SOME Jrels) diff -r 710710a66173 -r 166131276380 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Wed Sep 03 22:47:48 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Wed Sep 03 22:49:05 2014 +0200 @@ -1722,8 +1722,7 @@ val (Ibnfs, lthy) = fold_map6 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads) - map_b rel_b set_bs consts - #> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy))) + map_b rel_b set_bs consts) bs tacss map_bs rel_bs set_bss ((((((replicate n Binding.empty ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels) lthy; diff -r 710710a66173 -r 166131276380 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Sep 03 22:47:48 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Sep 03 22:49:05 2014 +0200 @@ -281,8 +281,10 @@ end; fun interpretation nesting_pref f = - Old_Datatype_Data.interpretation (old_interpretation_of nesting_pref f) - #> fp_sugar_interpretation (new_interpretation_of nesting_pref f); + let val new_f = new_interpretation_of nesting_pref f in + Old_Datatype_Data.interpretation (old_interpretation_of nesting_pref f) + #> fp_sugar_interpretation new_f (Local_Theory.background_theory o new_f) + end; val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]}; diff -r 710710a66173 -r 166131276380 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Sep 03 22:47:48 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Sep 03 22:49:05 2014 +0200 @@ -43,7 +43,8 @@ val ctr_sugars_of_global: theory -> ctr_sugar list val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option - val ctr_sugar_interpretation: (ctr_sugar -> theory -> theory) -> theory -> theory + val ctr_sugar_interpretation: (ctr_sugar -> theory -> theory) -> + (ctr_sugar -> local_theory -> local_theory) -> theory -> theory val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory val default_register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory @@ -170,26 +171,25 @@ val ctr_sugar_of_case = ctr_sugar_of_case_generic o Context.Proof; val ctr_sugar_of_case_global = ctr_sugar_of_case_generic o Context.Theory; -structure Ctr_Sugar_Interpretation = Interpretation +structure Ctr_Sugar_Interpretation = Local_Interpretation ( type T = ctr_sugar; val eq: T * T -> bool = op = o pairself #ctrs; ); -fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy = +fun with_repaired_path g (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy = thy |> Sign.root_path |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1))))) - |> (fn thy => f (transfer_ctr_sugar thy ctr_sugar) thy) + |> (fn thy => g (transfer_ctr_sugar thy ctr_sugar) thy) |> Sign.restore_naming thy; -fun ctr_sugar_interpretation f = Ctr_Sugar_Interpretation.interpretation (with_repaired_path f); +val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path; fun register_ctr_sugar key ctr_sugar = Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar))) - #> Local_Theory.background_theory - (fn thy => Ctr_Sugar_Interpretation.data (the (ctr_sugar_of_global thy key)) thy); + #> Ctr_Sugar_Interpretation.data ctr_sugar; fun default_register_ctr_sugar_global key ctr_sugar thy = let val tab = Data.get (Context.Theory thy) in @@ -198,7 +198,7 @@ else thy |> Context.theory_map (Data.put (Symtab.update_new (key, ctr_sugar) tab)) - |> Ctr_Sugar_Interpretation.data ctr_sugar + |> Ctr_Sugar_Interpretation.data_global ctr_sugar end; val isN = "is_"; diff -r 710710a66173 -r 166131276380 src/HOL/Tools/Ctr_Sugar/local_interpretation.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML Wed Sep 03 22:49:05 2014 +0200 @@ -0,0 +1,72 @@ +(* Title: HOL/Tools/Ctr_Sugar/local_interpretation.ML + Author: Jasmin Blanchette, TU Muenchen + +Generic interpretation of local theory data -- ad hoc. Based on + + Title: Pure/interpretation.ML + Author: Florian Haftmann and Makarius +*) + +signature LOCAL_INTERPRETATION = +sig + type T + val result: theory -> T list + val interpretation: (T -> theory -> theory) -> (T -> local_theory -> local_theory) -> theory -> + theory + val data: T -> local_theory -> local_theory + val data_global: T -> theory -> theory + val init: theory -> theory +end; + +functor Local_Interpretation(type T val eq: T * T -> bool): LOCAL_INTERPRETATION = +struct + +type T = T; + +structure Interp = Theory_Data +( + type T = + T list + * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * stamp) * T list) list; + val empty = ([], []); + val extend = I; + fun merge ((data1, interps1), (data2, interps2)) : T = + (Library.merge eq (data1, data2), + AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2)); +); + +val result = #1 o Interp.get; + +fun consolidate lthy = + let + val thy = Proof_Context.theory_of lthy; + val (data, interps) = Interp.get thy; + val unfinished = interps |> map (fn (((_, f), _), xs) => + (f, if eq_list eq (xs, data) then [] else subtract eq xs data)); + val finished = interps |> map (fn (interp, _) => (interp, data)); + in + if forall (null o #2) unfinished then NONE + else SOME (lthy |> fold_rev (uncurry fold_rev) unfinished + |> Local_Theory.background_theory (Interp.put (data, finished))) + end; + +fun consolidate_global thy = + let + val (data, interps) = Interp.get thy; + val unfinished = interps |> map (fn (((g, _), _), xs) => + (g, if eq_list eq (xs, data) then [] else subtract eq xs data)); + val finished = interps |> map (fn (interp, _) => (interp, data)); + in + if forall (null o #2) unfinished then NONE + else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished)) + end; + +fun interpretation g f = + Interp.map (apsnd (cons (((g, f), stamp ()), []))) #> perhaps consolidate_global; + +fun data x = Local_Theory.background_theory (Interp.map (apfst (cons x))) #> perhaps consolidate; +fun data_global x = Interp.map (apfst (cons x)) #> perhaps consolidate_global; + +val init = Theory.at_begin consolidate_global; + +end; diff -r 710710a66173 -r 166131276380 src/HOL/Tools/Lifting/lifting_bnf.ML --- a/src/HOL/Tools/Lifting/lifting_bnf.ML Wed Sep 03 22:47:48 2014 +0200 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Wed Sep 03 22:49:05 2014 +0200 @@ -116,6 +116,7 @@ end val _ = Context.>> (Context.map_theory (bnf_interpretation - (bnf_only_type_ctr (fn bnf => map_local_theory (lifting_bnf_interpretation bnf))))) + (bnf_only_type_ctr (map_local_theory o lifting_bnf_interpretation)) + (bnf_only_type_ctr lifting_bnf_interpretation))) end diff -r 710710a66173 -r 166131276380 src/HOL/Tools/Transfer/transfer_bnf.ML --- a/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Sep 03 22:47:48 2014 +0200 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Sep 03 22:49:05 2014 +0200 @@ -291,7 +291,8 @@ end val _ = Context.>> (Context.map_theory (bnf_interpretation - (bnf_only_type_ctr (fn bnf => map_local_theory (transfer_bnf_interpretation bnf))))) + (bnf_only_type_ctr (map_local_theory o transfer_bnf_interpretation)) + (bnf_only_type_ctr (transfer_bnf_interpretation)))) (* simplification rules for the predicator *) @@ -360,7 +361,8 @@ snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy) end -val _ = Context.>> (Context.map_theory (fp_sugar_interpretation (fp_sugar_only_type_ctr - (fn fp_sugars => map_local_theory (fold transfer_fp_sugar_interpretation fp_sugars))))) +val _ = Context.>> (Context.map_theory (fp_sugar_interpretation + (fp_sugar_only_type_ctr (map_local_theory o fold transfer_fp_sugar_interpretation)) + (fp_sugar_only_type_ctr (fold transfer_fp_sugar_interpretation)))) end diff -r 710710a66173 -r 166131276380 src/Pure/interpretation.ML --- a/src/Pure/interpretation.ML Wed Sep 03 22:47:48 2014 +0200 +++ b/src/Pure/interpretation.ML Wed Sep 03 22:49:05 2014 +0200 @@ -47,4 +47,3 @@ val init = Theory.at_begin consolidate; end; -