author | wenzelm |
Wed, 08 Apr 2015 11:52:35 +0200 | |
changeset 59952 | 550b74e9b08c |
parent 59917 | 9830c944670f |
child 60379 | 51d9dcd71ad7 |
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 |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56334
diff
changeset
|
9 |
type bundle = (thm list * Token.src list) list |
47057 | 10 |
val check: Proof.context -> xstring * Position.T -> string |
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
11 |
val get_bundle: Proof.context -> string -> bundle |
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
12 |
val get_bundle_cmd: Proof.context -> xstring * Position.T -> bundle |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56334
diff
changeset
|
13 |
val bundle: binding * (thm list * Token.src list) list -> |
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 |
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
17 |
val includes: string list -> Proof.context -> Proof.context |
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
18 |
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
|
19 |
val include_: string list -> Proof.state -> Proof.state |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
20 |
val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
21 |
val including: string list -> Proof.state -> Proof.state |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
22 |
val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state |
59890 | 23 |
val context: string list -> Element.context_i list -> |
24 |
generic_theory -> Binding.scope * local_theory |
|
47253
a00c5c88d8f3
more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents:
47251
diff
changeset
|
25 |
val context_cmd: (xstring * Position.T) list -> Element.context list -> |
59890 | 26 |
generic_theory -> Binding.scope * local_theory |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59890
diff
changeset
|
27 |
val print_bundles: bool -> Proof.context -> unit |
47057 | 28 |
end; |
29 |
||
30 |
structure Bundle: BUNDLE = |
|
31 |
struct |
|
32 |
||
33 |
(* maintain bundles *) |
|
34 |
||
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56334
diff
changeset
|
35 |
type bundle = (thm list * Token.src list) list; |
47057 | 36 |
|
37 |
fun transform_bundle phi : bundle -> bundle = |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56334
diff
changeset
|
38 |
map (fn (fact, atts) => (Morphism.fact phi fact, map (Token.transform_src phi) atts)); |
47057 | 39 |
|
40 |
structure Data = Generic_Data |
|
41 |
( |
|
42 |
type T = bundle Name_Space.table; |
|
43 |
val empty : T = Name_Space.empty_table "bundle"; |
|
44 |
val extend = I; |
|
45 |
val merge = Name_Space.merge_tables; |
|
46 |
); |
|
47 |
||
48 |
val get_bundles = Data.get o Context.Proof; |
|
49 |
||
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
50 |
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt); |
47057 | 51 |
|
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
52 |
val get_bundle = Name_Space.get o get_bundles; |
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
53 |
fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt; |
47057 | 54 |
|
55 |
||
56 |
(* define bundle *) |
|
57 |
||
58 |
local |
|
59 |
||
60 |
fun gen_bundle prep_fact prep_att prep_vars (binding, raw_bundle) fixes lthy = |
|
61 |
let |
|
62 |
val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes; |
|
63 |
val bundle0 = raw_bundle |
|
53111 | 64 |
|> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts)); |
47057 | 65 |
val bundle = |
66 |
Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat |
|
67 |
|> transform_bundle (Proof_Context.export_morphism ctxt' lthy); |
|
68 |
in |
|
69 |
lthy |> Local_Theory.declaration {syntax = false, pervasive = true} |
|
70 |
(fn phi => fn context => |
|
71 |
context |> Data.map |
|
72 |
(#2 o Name_Space.define context true |
|
73 |
(Morphism.binding phi binding, transform_bundle phi bundle))) |
|
74 |
end; |
|
75 |
||
76 |
in |
|
77 |
||
78 |
val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars; |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55763
diff
changeset
|
79 |
val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.read_vars; |
47057 | 80 |
|
81 |
end; |
|
82 |
||
83 |
||
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
84 |
(* include bundles *) |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
85 |
|
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
86 |
local |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
87 |
|
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
88 |
fun gen_includes get args ctxt = |
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
89 |
let val decls = maps (get ctxt) args |
47249
c0481c3c2a6c
added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents:
47070
diff
changeset
|
90 |
in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end; |
47057 | 91 |
|
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
92 |
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
|
93 |
let |
50739
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50301
diff
changeset
|
94 |
val (after_close, lthy) = |
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50301
diff
changeset
|
95 |
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
|
96 |
(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
|
97 |
val ((_, _, _, lthy'), _) = lthy |
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
98 |
|> 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
|
99 |
|> prep_decl ([], []) I raw_elems; |
47253
a00c5c88d8f3
more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents:
47251
diff
changeset
|
100 |
in |
59890 | 101 |
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
|
102 |
(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
|
103 |
end; |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
104 |
|
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
105 |
in |
47057 | 106 |
|
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
107 |
val includes = gen_includes get_bundle; |
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
108 |
val includes_cmd = gen_includes get_bundle_cmd; |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
109 |
|
47068 | 110 |
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
|
111 |
fun include_cmd bs = |
47068 | 112 |
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
|
113 |
|
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
114 |
fun including bs = Proof.assert_backward #> Proof.map_context (includes bs); |
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
115 |
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
|
116 |
|
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
56025
diff
changeset
|
117 |
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
|
118 |
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
|
119 |
|
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
120 |
end; |
47057 | 121 |
|
122 |
||
123 |
(* print_bundles *) |
|
124 |
||
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59890
diff
changeset
|
125 |
fun print_bundles verbose ctxt = |
47057 | 126 |
let |
127 |
val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; |
|
128 |
||
129 |
fun prt_fact (ths, []) = map prt_thm ths |
|
130 |
| prt_fact (ths, atts) = Pretty.enclose "(" ")" |
|
131 |
(Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts; |
|
132 |
||
133 |
fun prt_bundle (name, bundle) = |
|
55763 | 134 |
Pretty.block (Pretty.keyword1 "bundle" :: Pretty.str " " :: Pretty.mark_str name :: |
47057 | 135 |
Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle)); |
136 |
in |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59890
diff
changeset
|
137 |
map prt_bundle (Name_Space.markup_table verbose ctxt (get_bundles ctxt)) |
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56052
diff
changeset
|
138 |
end |> Pretty.writeln_chunks; |
47057 | 139 |
|
140 |
end; |