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