1(* Title: Pure/Isar/bundle.ML 2 Author: Makarius 3 4Bundled declarations (notes etc.). 5*) 6 7signature BUNDLE = 8sig 9 val check: Proof.context -> xstring * Position.T -> string 10 val get_bundle: Proof.context -> string -> Attrib.thms 11 val get_bundle_cmd: Proof.context -> xstring * Position.T -> Attrib.thms 12 val print_bundles: bool -> Proof.context -> unit 13 val bundle: binding * Attrib.thms -> 14 (binding * typ option * mixfix) list -> local_theory -> local_theory 15 val bundle_cmd: binding * (Facts.ref * Token.src list) list -> 16 (binding * string option * mixfix) list -> local_theory -> local_theory 17 val init: binding -> theory -> local_theory 18 val unbundle: string list -> local_theory -> local_theory 19 val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory 20 val includes: string list -> Proof.context -> Proof.context 21 val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context 22 val include_: string list -> Proof.state -> Proof.state 23 val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state 24 val including: string list -> Proof.state -> Proof.state 25 val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state 26 val context: string list -> Element.context_i list -> 27 generic_theory -> Binding.scope * local_theory 28 val context_cmd: (xstring * Position.T) list -> Element.context list -> 29 generic_theory -> Binding.scope * local_theory 30end; 31 32structure Bundle: BUNDLE = 33struct 34 35(** context data **) 36 37structure Data = Generic_Data 38( 39 type T = Attrib.thms Name_Space.table * Attrib.thms option; 40 val empty : T = (Name_Space.empty_table "bundle", NONE); 41 val extend = I; 42 fun merge ((tab1, target1), (tab2, target2)) = 43 (Name_Space.merge_tables (tab1, tab2), merge_options (target1, target2)); 44); 45 46 47(* bundles *) 48 49val get_bundles_generic = #1 o Data.get; 50val get_bundles = get_bundles_generic o Context.Proof; 51 52fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt); 53 54val get_bundle_generic = Name_Space.get o get_bundles_generic; 55val get_bundle = get_bundle_generic o Context.Proof; 56fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt; 57 58fun define_bundle (b, bundle) context = 59 let 60 val bundle' = Attrib.trim_context_thms bundle; 61 val (name, bundles') = Name_Space.define context true (b, bundle') (get_bundles_generic context); 62 val context' = (Data.map o apfst o K) bundles' context; 63 in (name, context') end; 64 65 66(* target -- bundle under construction *) 67 68fun the_target thy = 69 (case #2 (Data.get (Context.Theory thy)) of 70 SOME thms => thms 71 | NONE => error "Missing bundle target"); 72 73val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE; 74val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context_thms; 75 76fun augment_target thms = 77 Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy); 78 79 80(* print bundles *) 81 82fun pretty_bundle ctxt (markup_name, bundle) = 83 let 84 val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt; 85 fun prt_thm_attribs atts th = 86 Pretty.block (Pretty.breaks (prt_thm th :: Attrib.pretty_attribs ctxt atts)); 87 fun prt_thms (ths, []) = map prt_thm ths 88 | prt_thms (ths, atts) = map (prt_thm_attribs atts) ths; 89 in 90 Pretty.block ([Pretty.keyword1 "bundle", Pretty.str " ", Pretty.mark_str markup_name] @ 91 (if null bundle then [] else Pretty.fbreaks (Pretty.str " =" :: maps prt_thms bundle))) 92 end; 93 94fun print_bundles verbose ctxt = 95 Pretty.writeln_chunks 96 (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_bundles ctxt))); 97 98 99 100(** define bundle **) 101 102fun transform_bundle phi = 103 map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts)); 104 105 106(* command *) 107 108local 109 110fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy = 111 let 112 val (_, ctxt') = add_fixes raw_fixes lthy; 113 val bundle0 = raw_bundle 114 |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts)); 115 val bundle = 116 Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)] |> map snd |> flat 117 |> transform_bundle (Proof_Context.export_morphism ctxt' lthy); 118 in 119 lthy |> Local_Theory.declaration {syntax = false, pervasive = true} 120 (fn phi => #2 o define_bundle (Morphism.binding phi binding, transform_bundle phi bundle)) 121 end; 122 123in 124 125val bundle = gen_bundle (K I) (K I) Proof_Context.add_fixes; 126val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd; 127 128end; 129 130 131(* target *) 132 133local 134 135fun bad_operation _ = error "Not possible in bundle target"; 136 137fun conclude invisible binding = 138 Local_Theory.background_theory_result (fn thy => 139 thy 140 |> invisible ? Context_Position.set_visible_global false 141 |> Context.Theory 142 |> define_bundle (binding, the_target thy) 143 ||> (Context.the_theory 144 #> invisible ? Context_Position.restore_visible_global thy 145 #> reset_target)); 146 147fun pretty binding lthy = 148 let 149 val bundle = the_target (Proof_Context.theory_of lthy); 150 val (name, lthy') = lthy 151 |> Local_Theory.raw_theory (Context_Position.set_visible_global false) 152 |> conclude true binding; 153 val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy'); 154 val markup_name = 155 Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_bundles thy_ctxt')) name; 156 in [pretty_bundle lthy' (markup_name, bundle)] end; 157 158fun bundle_notes kind facts lthy = 159 let 160 val bundle = facts 161 |> maps (fn ((_, more_atts), thms) => map (fn (ths, atts) => (ths, atts @ more_atts)) thms); 162 in 163 lthy 164 |> augment_target (transform_bundle (Local_Theory.standard_morphism_theory lthy) bundle) 165 |> Generic_Target.standard_notes (op <>) kind facts 166 |> Attrib.local_notes kind facts 167 end; 168 169fun bundle_declaration decl lthy = 170 lthy 171 |> (augment_target o Attrib.internal_declaration) 172 (Morphism.transform (Local_Theory.standard_morphism_theory lthy) decl) 173 |> Generic_Target.standard_declaration (K true) decl; 174 175in 176 177fun init binding thy = 178 thy 179 |> Generic_Target.init 180 {background_naming = Sign.naming_of thy, 181 setup = set_target [] #> Proof_Context.init_global, 182 conclude = conclude false binding #> #2} 183 {define = bad_operation, 184 notes = bundle_notes, 185 abbrev = bad_operation, 186 declaration = K bundle_declaration, 187 theory_registration = bad_operation, 188 locale_dependency = bad_operation, 189 pretty = pretty binding} 190 191end; 192 193 194 195(** activate bundles **) 196 197local 198 199fun gen_activate notes get args ctxt = 200 let val decls = maps (get ctxt) args in 201 ctxt 202 |> Context_Position.set_visible false 203 |> notes [(Binding.empty_atts, decls)] |> #2 204 |> Context_Position.restore_visible ctxt 205 end; 206 207fun gen_includes get = gen_activate (Attrib.local_notes "") get; 208 209fun gen_context get prep_decl raw_incls raw_elems gthy = 210 let 211 val (after_close, lthy) = 212 gthy |> Context.cases (pair Local_Theory.exit o Named_Target.theory_init) 213 (pair I o Local_Theory.assert); 214 val ((_, _, _, lthy'), _) = lthy 215 |> gen_includes get raw_incls 216 |> prep_decl ([], []) I raw_elems; 217 in 218 lthy' |> Local_Theory.init_target 219 {background_naming = Local_Theory.background_naming_of lthy, after_close = after_close} 220 (Local_Theory.operations_of lthy) 221 end; 222 223in 224 225val unbundle = gen_activate Local_Theory.notes get_bundle; 226val unbundle_cmd = gen_activate Local_Theory.notes get_bundle_cmd; 227 228val includes = gen_includes get_bundle; 229val includes_cmd = gen_includes get_bundle_cmd; 230 231fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts; 232fun include_cmd bs = 233 Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts; 234 235fun including bs = Proof.assert_backward #> Proof.map_context (includes bs); 236fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs); 237 238val context = gen_context get_bundle Expression.cert_declaration; 239val context_cmd = gen_context get_bundle_cmd Expression.read_declaration; 240 241end; 242 243end; 244