author | wenzelm |
Mon, 10 Apr 2017 11:29:47 +0200 | |
changeset 65452 | 9e9750a7932c |
parent 63352 | 4eaf35781b23 |
child 66335 | a849ce33923d |
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 |
||
58 |
fun define_bundle def context = |
|
59 |
let |
|
60 |
val (name, bundles') = Name_Space.define context true def (get_bundles_generic context); |
|
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; |
|
73 |
val set_target = Context.theory_map o Data.map o apsnd o K o SOME; |
|
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 |
|
95 |
(map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_bundles ctxt))); |
|
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 = |
|
154 |
Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_bundles thy_ctxt')) name; |
|
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 |
|
178 |
|> Sign.change_begin |
|
179 |
|> set_target [] |
|
180 |
|> Proof_Context.init_global |
|
181 |
|> Local_Theory.init (Sign.naming_of thy) |
|
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, |
|
188 |
pretty = pretty binding, |
|
63275 | 189 |
exit = conclude false binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local} |
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 |
59880
30687c3f2b10
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
wenzelm
parents:
58011
diff
changeset
|
219 |
(Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close |
47253
a00c5c88d8f3
more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents:
47251
diff
changeset
|
220 |
end; |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
221 |
|
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
222 |
in |
47057 | 223 |
|
63282 | 224 |
val unbundle = gen_activate Local_Theory.notes get_bundle; |
225 |
val unbundle_cmd = gen_activate Local_Theory.notes get_bundle_cmd; |
|
226 |
||
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
227 |
val includes = gen_includes get_bundle; |
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
228 |
val includes_cmd = gen_includes get_bundle_cmd; |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
229 |
|
47068 | 230 |
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
|
231 |
fun include_cmd bs = |
47068 | 232 |
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
|
233 |
|
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
234 |
fun including bs = Proof.assert_backward #> Proof.map_context (includes bs); |
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
235 |
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
|
236 |
|
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
237 |
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
|
238 |
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
|
239 |
|
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
240 |
end; |
47057 | 241 |
|
242 |
end; |