author | wenzelm |
Thu, 06 Jun 2024 12:42:42 +0200 | |
changeset 80267 | ea908185a597 |
parent 78095 | bc42c074e58f |
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 |
|
72605 | 9 |
type name = string |
74261
d28a51dd9da6
export other entities, e.g. relevant for formal document output;
wenzelm
parents:
74122
diff
changeset
|
10 |
val bundle_space: Context.generic -> Name_Space.T |
47057 | 11 |
val check: Proof.context -> xstring * Position.T -> string |
72605 | 12 |
val get: Proof.context -> name -> Attrib.thms |
72452
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
13 |
val read: Proof.context -> xstring * Position.T -> Attrib.thms |
74122 | 14 |
val extern: Proof.context -> string -> xstring |
63270 | 15 |
val print_bundles: bool -> Proof.context -> unit |
63267 | 16 |
val bundle: binding * Attrib.thms -> |
47057 | 17 |
(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
|
18 |
val bundle_cmd: binding * (Facts.ref * Token.src list) list -> |
47057 | 19 |
(binding * string option * mixfix) list -> local_theory -> local_theory |
63270 | 20 |
val init: binding -> theory -> local_theory |
72605 | 21 |
val unbundle: name list -> local_theory -> local_theory |
63282 | 22 |
val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory |
72605 | 23 |
val includes: name list -> Proof.context -> Proof.context |
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
24 |
val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context |
72605 | 25 |
val include_: name list -> Proof.state -> Proof.state |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
26 |
val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state |
72605 | 27 |
val including: name list -> Proof.state -> Proof.state |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
28 |
val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state |
47057 | 29 |
end; |
30 |
||
31 |
structure Bundle: BUNDLE = |
|
32 |
struct |
|
33 |
||
63270 | 34 |
(** context data **) |
35 |
||
36 |
structure Data = Generic_Data |
|
37 |
( |
|
38 |
type T = Attrib.thms Name_Space.table * Attrib.thms option; |
|
74261
d28a51dd9da6
export other entities, e.g. relevant for formal document output;
wenzelm
parents:
74122
diff
changeset
|
39 |
val empty : T = (Name_Space.empty_table Markup.bundleN, NONE); |
63270 | 40 |
fun merge ((tab1, target1), (tab2, target2)) = |
41 |
(Name_Space.merge_tables (tab1, tab2), merge_options (target1, target2)); |
|
42 |
); |
|
43 |
||
44 |
||
45 |
(* bundles *) |
|
46 |
||
72605 | 47 |
type name = string |
48 |
||
72452
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
49 |
val get_all_generic = #1 o Data.get; |
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
50 |
val get_all = get_all_generic o Context.Proof; |
63270 | 51 |
|
74261
d28a51dd9da6
export other entities, e.g. relevant for formal document output;
wenzelm
parents:
74122
diff
changeset
|
52 |
val bundle_space = Name_Space.space_of_table o #1 o Data.get; |
d28a51dd9da6
export other entities, e.g. relevant for formal document output;
wenzelm
parents:
74122
diff
changeset
|
53 |
|
72452
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
54 |
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_all ctxt); |
63270 | 55 |
|
72452
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
56 |
val get = Name_Space.get o get_all_generic o Context.Proof; |
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
57 |
|
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
58 |
fun read ctxt = get ctxt o check ctxt; |
63270 | 59 |
|
74122 | 60 |
fun extern ctxt = Name_Space.extern ctxt (Name_Space.space_of_table (get_all ctxt)); |
61 |
||
63270 | 62 |
|
63 |
(* target -- bundle under construction *) |
|
64 |
||
65 |
fun the_target thy = |
|
77908
a6bd716a6124
tuned: concise combinators instead of bulky case-expressions;
wenzelm
parents:
74561
diff
changeset
|
66 |
#2 (Data.get (Context.Theory thy)) |
a6bd716a6124
tuned: concise combinators instead of bulky case-expressions;
wenzelm
parents:
74561
diff
changeset
|
67 |
|> \<^if_none>\<open>error "Missing bundle target"\<close>; |
63270 | 68 |
|
69 |
val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE; |
|
67652 | 70 |
val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context_thms; |
63270 | 71 |
|
72 |
fun augment_target thms = |
|
73 |
Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy); |
|
74 |
||
75 |
||
76 |
(* print bundles *) |
|
77 |
||
78 |
fun pretty_bundle ctxt (markup_name, bundle) = |
|
79 |
let |
|
80 |
val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt; |
|
63275 | 81 |
fun prt_thm_attribs atts th = |
82 |
Pretty.block (Pretty.breaks (prt_thm th :: Attrib.pretty_attribs ctxt atts)); |
|
63270 | 83 |
fun prt_thms (ths, []) = map prt_thm ths |
63275 | 84 |
| prt_thms (ths, atts) = map (prt_thm_attribs atts) ths; |
63270 | 85 |
in |
86 |
Pretty.block ([Pretty.keyword1 "bundle", Pretty.str " ", Pretty.mark_str markup_name] @ |
|
63275 | 87 |
(if null bundle then [] else Pretty.fbreaks (Pretty.str " =" :: maps prt_thms bundle))) |
63270 | 88 |
end; |
89 |
||
90 |
fun print_bundles verbose ctxt = |
|
91 |
Pretty.writeln_chunks |
|
72452
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
92 |
(map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_all ctxt))); |
63270 | 93 |
|
94 |
||
95 |
||
96 |
(** define bundle **) |
|
47057 | 97 |
|
78064
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
98 |
(* context and morphisms *) |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
99 |
|
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
100 |
val trim_context_bundle = |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
101 |
map (fn (fact, atts) => (map Thm.trim_context fact, (map o map) Token.trim_context atts)); |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
102 |
|
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
103 |
fun transfer_bundle thy = |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
104 |
map (fn (fact, atts) => (map (Thm.transfer thy) fact, (map o map) (Token.transfer thy) atts)); |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
105 |
|
63267 | 106 |
fun transform_bundle phi = |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61268
diff
changeset
|
107 |
map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts)); |
47057 | 108 |
|
78064
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
109 |
fun define_bundle (b, bundle) context = |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
110 |
let |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
111 |
val (name, bundles') = get_all_generic context |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
112 |
|> Name_Space.define context true (b, trim_context_bundle bundle); |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
113 |
val context' = (Data.map o apfst o K) bundles' context; |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
114 |
in (name, context') end; |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
115 |
|
47057 | 116 |
|
63270 | 117 |
(* command *) |
47057 | 118 |
|
119 |
local |
|
120 |
||
60469 | 121 |
fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy = |
47057 | 122 |
let |
60469 | 123 |
val (_, ctxt') = add_fixes raw_fixes lthy; |
47057 | 124 |
val bundle0 = raw_bundle |
53111 | 125 |
|> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts)); |
47057 | 126 |
val bundle = |
78066 | 127 |
Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)] |
128 |
|> maps #2 |
|
78069 | 129 |
|> transform_bundle (Proof_Context.export_morphism ctxt' lthy) |
130 |
|> trim_context_bundle; |
|
47057 | 131 |
in |
78095 | 132 |
lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = Binding.pos_of binding} |
78069 | 133 |
(fn phi => fn context => |
134 |
let val psi = Morphism.set_trim_context'' context phi |
|
135 |
in #2 (define_bundle (Morphism.binding psi binding, transform_bundle psi bundle) context) end) |
|
47057 | 136 |
end; |
137 |
||
138 |
in |
|
139 |
||
60469 | 140 |
val bundle = gen_bundle (K I) (K I) Proof_Context.add_fixes; |
141 |
val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd; |
|
47057 | 142 |
|
143 |
end; |
|
144 |
||
145 |
||
63270 | 146 |
(* target *) |
147 |
||
148 |
local |
|
149 |
||
150 |
fun bad_operation _ = error "Not possible in bundle target"; |
|
151 |
||
63275 | 152 |
fun conclude invisible binding = |
63270 | 153 |
Local_Theory.background_theory_result (fn thy => |
63275 | 154 |
thy |
155 |
|> invisible ? Context_Position.set_visible_global false |
|
156 |
|> Context.Theory |
|
157 |
|> define_bundle (binding, the_target thy) |
|
63277 | 158 |
||> (Context.the_theory |
159 |
#> invisible ? Context_Position.restore_visible_global thy |
|
160 |
#> reset_target)); |
|
63270 | 161 |
|
162 |
fun pretty binding lthy = |
|
163 |
let |
|
164 |
val bundle = the_target (Proof_Context.theory_of lthy); |
|
63275 | 165 |
val (name, lthy') = lthy |
166 |
|> Local_Theory.raw_theory (Context_Position.set_visible_global false) |
|
167 |
|> conclude true binding; |
|
63270 | 168 |
val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy'); |
169 |
val markup_name = |
|
72452
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
170 |
Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_all thy_ctxt')) name; |
63270 | 171 |
in [pretty_bundle lthy' (markup_name, bundle)] end; |
172 |
||
173 |
fun bundle_notes kind facts lthy = |
|
174 |
let |
|
175 |
val bundle = facts |
|
176 |
|> maps (fn ((_, more_atts), thms) => map (fn (ths, atts) => (ths, atts @ more_atts)) thms); |
|
177 |
in |
|
178 |
lthy |
|
179 |
|> 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
|
180 |
|> Generic_Target.standard_notes (op <>) kind facts |
63270 | 181 |
|> Attrib.local_notes kind facts |
182 |
end; |
|
183 |
||
78095 | 184 |
fun bundle_declaration pos decl lthy = |
63270 | 185 |
lthy |
78095 | 186 |
|> (augment_target o Attrib.internal_declaration pos) |
63270 | 187 |
(Morphism.transform (Local_Theory.standard_morphism_theory lthy) decl) |
188 |
|> Generic_Target.standard_declaration (K true) decl; |
|
189 |
||
190 |
in |
|
191 |
||
192 |
fun init binding thy = |
|
193 |
thy |
|
72516
17dc99589a91
unified Local_Theory.init with Generic_Target.init
haftmann
parents:
72504
diff
changeset
|
194 |
|> Local_Theory.init |
66335
a849ce33923d
treat exit separate from regular local theory operations
haftmann
parents:
63352
diff
changeset
|
195 |
{background_naming = Sign.naming_of thy, |
66337
5caea089dd17
more structural sharing between common target Generic_Target.init
haftmann
parents:
66336
diff
changeset
|
196 |
setup = set_target [] #> Proof_Context.init_global, |
5caea089dd17
more structural sharing between common target Generic_Target.init
haftmann
parents:
66336
diff
changeset
|
197 |
conclude = conclude false binding #> #2} |
63270 | 198 |
{define = bad_operation, |
199 |
notes = bundle_notes, |
|
200 |
abbrev = bad_operation, |
|
78095 | 201 |
declaration = fn {pos, ...} => bundle_declaration pos, |
63270 | 202 |
theory_registration = bad_operation, |
203 |
locale_dependency = bad_operation, |
|
78095 | 204 |
pretty = pretty binding}; |
63270 | 205 |
|
206 |
end; |
|
207 |
||
208 |
||
209 |
||
63282 | 210 |
(** activate bundles **) |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
211 |
|
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
212 |
local |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
213 |
|
72452
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
214 |
fun gen_activate notes prep_bundle args ctxt = |
78064
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
215 |
let |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
216 |
val thy = Proof_Context.theory_of ctxt; |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
217 |
val decls = maps (prep_bundle ctxt) args |> transfer_bundle thy; |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
218 |
in |
63031 | 219 |
ctxt |
220 |
|> Context_Position.set_visible false |
|
78064
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78061
diff
changeset
|
221 |
|> notes [(Binding.empty_atts, decls)] |> #2 |
63031 | 222 |
|> Context_Position.restore_visible ctxt |
223 |
end; |
|
47057 | 224 |
|
72504 | 225 |
fun gen_unbundle prep_bundle = gen_activate Local_Theory.notes prep_bundle; |
226 |
||
72452
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
227 |
fun gen_includes prep_bundle = gen_activate (Attrib.local_notes "") prep_bundle; |
63282 | 228 |
|
72504 | 229 |
fun gen_include prep_bundle bs = |
230 |
Proof.assert_forward #> Proof.map_context (gen_includes prep_bundle bs) #> Proof.reset_facts; |
|
231 |
||
232 |
fun gen_including prep_bundle bs = |
|
233 |
Proof.assert_backward #> Proof.map_context (gen_includes prep_bundle bs) |
|
234 |
||
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
235 |
in |
47057 | 236 |
|
72504 | 237 |
val unbundle = gen_unbundle get; |
238 |
val unbundle_cmd = gen_unbundle read; |
|
63282 | 239 |
|
72452
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
240 |
val includes = gen_includes get; |
9017dfa56367
avoid _cmd suffix where no Isar command is involved
haftmann
parents:
72450
diff
changeset
|
241 |
val includes_cmd = gen_includes read; |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
242 |
|
72504 | 243 |
val include_ = gen_include get; |
244 |
val include_cmd = gen_include read; |
|
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
245 |
|
72504 | 246 |
val including = gen_including get; |
247 |
val including_cmd = gen_including read; |
|
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
248 |
|
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
249 |
end; |
47057 | 250 |
|
251 |
end; |