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