author | wenzelm |
Wed, 23 Jan 2019 23:12:40 +0100 | |
changeset 69729 | 4591221824f6 |
parent 67652 | 11716a084cae |
child 72433 | 7e0e497dacbc |
permissions | -rw-r--r-- |
47057 | 1 |
(* Title: Pure/Isar/bundle.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Bundled declarations (notes etc.). |
|
5 |
*) |
|
6 |
||
7 |
signature BUNDLE = |
|
8 |
sig |
|
9 |
val check: Proof.context -> xstring * Position.T -> string |
|
63267 | 10 |
val get_bundle: Proof.context -> string -> Attrib.thms |
11 |
val get_bundle_cmd: Proof.context -> xstring * Position.T -> Attrib.thms |
|
63270 | 12 |
val print_bundles: bool -> Proof.context -> unit |
63267 | 13 |
val bundle: binding * Attrib.thms -> |
47057 | 14 |
(binding * typ option * mixfix) list -> local_theory -> local_theory |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56334
diff
changeset
|
15 |
val bundle_cmd: binding * (Facts.ref * Token.src list) list -> |
47057 | 16 |
(binding * string option * mixfix) list -> local_theory -> local_theory |
63270 | 17 |
val init: binding -> theory -> local_theory |
63282 | 18 |
val unbundle: string list -> local_theory -> local_theory |
19 |
val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory |
|
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
20 |
val includes: string list -> Proof.context -> Proof.context |
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
21 |
val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
22 |
val include_: string list -> Proof.state -> Proof.state |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
23 |
val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
24 |
val including: string list -> Proof.state -> Proof.state |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
25 |
val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state |
59890 | 26 |
val context: string list -> Element.context_i list -> |
27 |
generic_theory -> Binding.scope * local_theory |
|
47253
a00c5c88d8f3
more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents:
47251
diff
changeset
|
28 |
val context_cmd: (xstring * Position.T) list -> Element.context list -> |
59890 | 29 |
generic_theory -> Binding.scope * local_theory |
47057 | 30 |
end; |
31 |
||
32 |
structure Bundle: BUNDLE = |
|
33 |
struct |
|
34 |
||
63270 | 35 |
(** context data **) |
36 |
||
37 |
structure 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 |
||
49 |
val get_bundles_generic = #1 o Data.get; |
|
50 |
val get_bundles = get_bundles_generic o Context.Proof; |
|
51 |
||
52 |
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt); |
|
53 |
||
54 |
val get_bundle_generic = Name_Space.get o get_bundles_generic; |
|
55 |
val get_bundle = get_bundle_generic o Context.Proof; |
|
56 |
fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt; |
|
57 |
||
67627 | 58 |
fun define_bundle (b, bundle) context = |
63270 | 59 |
let |
67652 | 60 |
val bundle' = Attrib.trim_context_thms bundle; |
67627 | 61 |
val (name, bundles') = Name_Space.define context true (b, bundle') (get_bundles_generic context); |
63270 | 62 |
val context' = (Data.map o apfst o K) bundles' context; |
63 |
in (name, context') end; |
|
64 |
||
65 |
||
66 |
(* target -- bundle under construction *) |
|
67 |
||
68 |
fun the_target thy = |
|
69 |
(case #2 (Data.get (Context.Theory thy)) of |
|
70 |
SOME thms => thms |
|
71 |
| NONE => error "Missing bundle target"); |
|
72 |
||
73 |
val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE; |
|
67652 | 74 |
val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context_thms; |
63270 | 75 |
|
76 |
fun augment_target thms = |
|
77 |
Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy); |
|
78 |
||
79 |
||
80 |
(* print bundles *) |
|
81 |
||
82 |
fun pretty_bundle ctxt (markup_name, bundle) = |
|
83 |
let |
|
84 |
val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt; |
|
63275 | 85 |
fun prt_thm_attribs atts th = |
86 |
Pretty.block (Pretty.breaks (prt_thm th :: Attrib.pretty_attribs ctxt atts)); |
|
63270 | 87 |
fun prt_thms (ths, []) = map prt_thm ths |
63275 | 88 |
| prt_thms (ths, atts) = map (prt_thm_attribs atts) ths; |
63270 | 89 |
in |
90 |
Pretty.block ([Pretty.keyword1 "bundle", Pretty.str " ", Pretty.mark_str markup_name] @ |
|
63275 | 91 |
(if null bundle then [] else Pretty.fbreaks (Pretty.str " =" :: maps prt_thms bundle))) |
63270 | 92 |
end; |
93 |
||
94 |
fun 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 **) |
|
47057 | 101 |
|
63267 | 102 |
fun transform_bundle phi = |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61268
diff
changeset
|
103 |
map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts)); |
47057 | 104 |
|
105 |
||
63270 | 106 |
(* command *) |
47057 | 107 |
|
108 |
local |
|
109 |
||
60469 | 110 |
fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy = |
47057 | 111 |
let |
60469 | 112 |
val (_, ctxt') = add_fixes raw_fixes lthy; |
47057 | 113 |
val bundle0 = raw_bundle |
53111 | 114 |
|> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts)); |
47057 | 115 |
val bundle = |
63352 | 116 |
Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)] |> map snd |> flat |
47057 | 117 |
|> transform_bundle (Proof_Context.export_morphism ctxt' lthy); |
118 |
in |
|
119 |
lthy |> Local_Theory.declaration {syntax = false, pervasive = true} |
|
63270 | 120 |
(fn phi => #2 o define_bundle (Morphism.binding phi binding, transform_bundle phi bundle)) |
47057 | 121 |
end; |
122 |
||
123 |
in |
|
124 |
||
60469 | 125 |
val bundle = gen_bundle (K I) (K I) Proof_Context.add_fixes; |
126 |
val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd; |
|
47057 | 127 |
|
128 |
end; |
|
129 |
||
130 |
||
63270 | 131 |
(* target *) |
132 |
||
133 |
local |
|
134 |
||
135 |
fun bad_operation _ = error "Not possible in bundle target"; |
|
136 |
||
63275 | 137 |
fun conclude invisible binding = |
63270 | 138 |
Local_Theory.background_theory_result (fn thy => |
63275 | 139 |
thy |
140 |
|> invisible ? Context_Position.set_visible_global false |
|
141 |
|> Context.Theory |
|
142 |
|> define_bundle (binding, the_target thy) |
|
63277 | 143 |
||> (Context.the_theory |
144 |
#> invisible ? Context_Position.restore_visible_global thy |
|
145 |
#> reset_target)); |
|
63270 | 146 |
|
147 |
fun pretty binding lthy = |
|
148 |
let |
|
149 |
val bundle = the_target (Proof_Context.theory_of lthy); |
|
63275 | 150 |
val (name, lthy') = lthy |
151 |
|> Local_Theory.raw_theory (Context_Position.set_visible_global false) |
|
152 |
|> conclude true binding; |
|
63270 | 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 |
||
158 |
fun 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) |
|
63278
6c963f1fc388
avoid duplicate Attrib.local_notes in aux. context;
wenzelm
parents:
63277
diff
changeset
|
165 |
|> Generic_Target.standard_notes (op <>) kind facts |
63270 | 166 |
|> Attrib.local_notes kind facts |
167 |
end; |
|
168 |
||
169 |
fun 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 |
||
175 |
in |
|
176 |
||
177 |
fun init binding thy = |
|
178 |
thy |
|
66337
5caea089dd17
more structural sharing between common target Generic_Target.init
haftmann
parents:
66336
diff
changeset
|
179 |
|> Generic_Target.init |
66335
a849ce33923d
treat exit separate from regular local theory operations
haftmann
parents:
63352
diff
changeset
|
180 |
{background_naming = Sign.naming_of thy, |
66337
5caea089dd17
more structural sharing between common target Generic_Target.init
haftmann
parents:
66336
diff
changeset
|
181 |
setup = set_target [] #> Proof_Context.init_global, |
5caea089dd17
more structural sharing between common target Generic_Target.init
haftmann
parents:
66336
diff
changeset
|
182 |
conclude = conclude false binding #> #2} |
63270 | 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, |
|
66335
a849ce33923d
treat exit separate from regular local theory operations
haftmann
parents:
63352
diff
changeset
|
189 |
pretty = pretty binding} |
63270 | 190 |
|
191 |
end; |
|
192 |
||
193 |
||
194 |
||
63282 | 195 |
(** activate bundles **) |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
196 |
|
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
197 |
local |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
198 |
|
63282 | 199 |
fun gen_activate notes get args ctxt = |
63031 | 200 |
let val decls = maps (get ctxt) args in |
201 |
ctxt |
|
202 |
|> Context_Position.set_visible false |
|
63352 | 203 |
|> notes [(Binding.empty_atts, decls)] |> #2 |
63031 | 204 |
|> Context_Position.restore_visible ctxt |
205 |
end; |
|
47057 | 206 |
|
63282 | 207 |
fun gen_includes get = gen_activate (Attrib.local_notes "") get; |
208 |
||
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
209 |
fun gen_context get prep_decl raw_incls raw_elems gthy = |
47253
a00c5c88d8f3
more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents:
47251
diff
changeset
|
210 |
let |
50739
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50301
diff
changeset
|
211 |
val (after_close, lthy) = |
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50301
diff
changeset
|
212 |
gthy |> Context.cases (pair Local_Theory.exit o Named_Target.theory_init) |
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50301
diff
changeset
|
213 |
(pair I o Local_Theory.assert); |
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50301
diff
changeset
|
214 |
val ((_, _, _, lthy'), _) = lthy |
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
215 |
|> gen_includes get raw_incls |
50739
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50301
diff
changeset
|
216 |
|> prep_decl ([], []) I raw_elems; |
47253
a00c5c88d8f3
more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents:
47251
diff
changeset
|
217 |
in |
59890 | 218 |
lthy' |> Local_Theory.init_target |
66336
13e7dc5f7c3d
exit always refers to the bottom of a nested local theory stack, after_close always to all non-bottom elements
haftmann
parents:
66335
diff
changeset
|
219 |
{background_naming = Local_Theory.background_naming_of lthy, after_close = after_close} |
13e7dc5f7c3d
exit always refers to the bottom of a nested local theory stack, after_close always to all non-bottom elements
haftmann
parents:
66335
diff
changeset
|
220 |
(Local_Theory.operations_of lthy) |
47253
a00c5c88d8f3
more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents:
47251
diff
changeset
|
221 |
end; |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
222 |
|
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
223 |
in |
47057 | 224 |
|
63282 | 225 |
val unbundle = gen_activate Local_Theory.notes get_bundle; |
226 |
val unbundle_cmd = gen_activate Local_Theory.notes get_bundle_cmd; |
|
227 |
||
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
228 |
val includes = gen_includes get_bundle; |
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
229 |
val includes_cmd = gen_includes get_bundle_cmd; |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
230 |
|
47068 | 231 |
fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts; |
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
232 |
fun include_cmd bs = |
47068 | 233 |
Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts; |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
234 |
|
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
235 |
fun including bs = Proof.assert_backward #> Proof.map_context (includes bs); |
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
236 |
fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs); |
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
237 |
|
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
238 |
val context = gen_context get_bundle Expression.cert_declaration; |
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
239 |
val context_cmd = gen_context get_bundle_cmd Expression.read_declaration; |
47253
a00c5c88d8f3
more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents:
47251
diff
changeset
|
240 |
|
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
241 |
end; |
47057 | 242 |
|
243 |
end; |