author | wenzelm |
Wed, 21 Mar 2012 23:26:35 +0100 | |
changeset 47069 | 451fc10a81f3 |
parent 47068 | 2027ff3136cc |
child 47070 | 15cd66da537f |
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 |
type bundle = (thm list * Args.src list) list |
|
10 |
val the_bundle: Proof.context -> string -> bundle |
|
11 |
val check: Proof.context -> xstring * Position.T -> string |
|
12 |
val bundle: binding * (thm list * Args.src list) list -> |
|
13 |
(binding * typ option * mixfix) list -> local_theory -> local_theory |
|
14 |
val bundle_cmd: binding * (Facts.ref * Args.src list) list -> |
|
15 |
(binding * string option * mixfix) list -> local_theory -> local_theory |
|
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
16 |
val includes: string list -> Proof.context -> Proof.context |
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
17 |
val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context |
47069 | 18 |
val context_includes: string list -> generic_theory -> local_theory |
19 |
val context_includes_cmd: (xstring * Position.T) list -> generic_theory -> local_theory |
|
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
20 |
val include_: string list -> Proof.state -> Proof.state |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
21 |
val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
22 |
val including: string list -> Proof.state -> Proof.state |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
23 |
val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state |
47057 | 24 |
val print_bundles: Proof.context -> unit |
25 |
end; |
|
26 |
||
27 |
structure Bundle: BUNDLE = |
|
28 |
struct |
|
29 |
||
30 |
(* maintain bundles *) |
|
31 |
||
32 |
type bundle = (thm list * Args.src list) list; |
|
33 |
||
34 |
fun transform_bundle phi : bundle -> bundle = |
|
35 |
map (fn (fact, atts) => (Morphism.fact phi fact, map (Args.transform_values phi) atts)); |
|
36 |
||
37 |
structure Data = Generic_Data |
|
38 |
( |
|
39 |
type T = bundle Name_Space.table; |
|
40 |
val empty : T = Name_Space.empty_table "bundle"; |
|
41 |
val extend = I; |
|
42 |
val merge = Name_Space.merge_tables; |
|
43 |
); |
|
44 |
||
45 |
val get_bundles = Data.get o Context.Proof; |
|
46 |
||
47 |
fun the_bundle ctxt name = |
|
48 |
(case Symtab.lookup (#2 (get_bundles ctxt)) name of |
|
49 |
SOME bundle => bundle |
|
50 |
| NONE => error ("Unknown bundle " ^ quote name)); |
|
51 |
||
52 |
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt); |
|
53 |
||
54 |
||
55 |
(* define bundle *) |
|
56 |
||
57 |
local |
|
58 |
||
59 |
fun gen_bundle prep_fact prep_att prep_vars (binding, raw_bundle) fixes lthy = |
|
60 |
let |
|
61 |
val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes; |
|
62 |
val bundle0 = raw_bundle |
|
63 |
|> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts)); |
|
64 |
val bundle = |
|
65 |
Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat |
|
66 |
|> transform_bundle (Proof_Context.export_morphism ctxt' lthy); |
|
67 |
in |
|
68 |
lthy |> Local_Theory.declaration {syntax = false, pervasive = true} |
|
69 |
(fn phi => fn context => |
|
70 |
context |> Data.map |
|
71 |
(#2 o Name_Space.define context true |
|
72 |
(Morphism.binding phi binding, transform_bundle phi bundle))) |
|
73 |
end; |
|
74 |
||
75 |
in |
|
76 |
||
77 |
val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars; |
|
78 |
val bundle_cmd = |
|
79 |
gen_bundle Proof_Context.get_fact (Attrib.intern_src o Proof_Context.theory_of) |
|
80 |
Proof_Context.read_vars; |
|
81 |
||
82 |
end; |
|
83 |
||
84 |
||
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
85 |
(* include bundles *) |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
86 |
|
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
87 |
local |
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
88 |
|
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
89 |
fun gen_includes prep args ctxt = |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
90 |
let |
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
91 |
val decls = maps (the_bundle ctxt o prep ctxt) args; |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
92 |
val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt); |
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
93 |
val note = ((Binding.empty, []), map (apsnd (map attrib)) decls); |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
94 |
in #2 (Proof_Context.note_thmss "" [note] ctxt) end; |
47057 | 95 |
|
47069 | 96 |
fun gen_context prep args (Context.Theory thy) = |
97 |
Named_Target.theory_init thy |
|
98 |
|> Local_Theory.target (gen_includes prep args) |
|
99 |
| gen_context prep args (Context.Proof lthy) = |
|
100 |
Named_Target.assert lthy |
|
101 |
|> gen_includes prep args |
|
102 |
|> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy); |
|
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
103 |
|
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
104 |
in |
47057 | 105 |
|
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
106 |
val includes = gen_includes (K I); |
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
107 |
val includes_cmd = gen_includes check; |
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
108 |
|
47069 | 109 |
val context_includes = gen_context (K I); |
110 |
val context_includes_cmd = gen_context check; |
|
111 |
||
47068 | 112 |
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
|
113 |
fun include_cmd bs = |
47068 | 114 |
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
|
115 |
|
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
116 |
fun including bs = Proof.assert_backward #> Proof.map_context (includes bs); |
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
47066
diff
changeset
|
117 |
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
|
118 |
|
47066
8a6124d09ff5
basic support for nested contexts including bundles;
wenzelm
parents:
47057
diff
changeset
|
119 |
end; |
47057 | 120 |
|
121 |
||
122 |
(* print_bundles *) |
|
123 |
||
124 |
fun print_bundles ctxt = |
|
125 |
let |
|
126 |
val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; |
|
127 |
||
128 |
fun prt_fact (ths, []) = map prt_thm ths |
|
129 |
| prt_fact (ths, atts) = Pretty.enclose "(" ")" |
|
130 |
(Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts; |
|
131 |
||
132 |
fun prt_bundle (name, bundle) = |
|
133 |
Pretty.block (Pretty.command "bundle" :: Pretty.str " " :: Pretty.str name :: |
|
134 |
Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle)); |
|
135 |
in |
|
136 |
map prt_bundle (Name_Space.extern_table ctxt (get_bundles ctxt)) |
|
137 |
end |> Pretty.chunks |> Pretty.writeln; |
|
138 |
||
139 |
end; |
|
140 |