|
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 |
|
16 val include_: string -> Proof.state -> Proof.state |
|
17 val include_cmd: xstring * Position.T -> Proof.state -> Proof.state |
|
18 val including: string -> Proof.state -> Proof.state |
|
19 val including_cmd: xstring * Position.T -> Proof.state -> Proof.state |
|
20 val print_bundles: Proof.context -> unit |
|
21 end; |
|
22 |
|
23 structure Bundle: BUNDLE = |
|
24 struct |
|
25 |
|
26 (* maintain bundles *) |
|
27 |
|
28 type bundle = (thm list * Args.src list) list; |
|
29 |
|
30 fun transform_bundle phi : bundle -> bundle = |
|
31 map (fn (fact, atts) => (Morphism.fact phi fact, map (Args.transform_values phi) atts)); |
|
32 |
|
33 structure Data = Generic_Data |
|
34 ( |
|
35 type T = bundle Name_Space.table; |
|
36 val empty : T = Name_Space.empty_table "bundle"; |
|
37 val extend = I; |
|
38 val merge = Name_Space.merge_tables; |
|
39 ); |
|
40 |
|
41 val get_bundles = Data.get o Context.Proof; |
|
42 |
|
43 fun the_bundle ctxt name = |
|
44 (case Symtab.lookup (#2 (get_bundles ctxt)) name of |
|
45 SOME bundle => bundle |
|
46 | NONE => error ("Unknown bundle " ^ quote name)); |
|
47 |
|
48 fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt); |
|
49 |
|
50 |
|
51 (* define bundle *) |
|
52 |
|
53 local |
|
54 |
|
55 fun gen_bundle prep_fact prep_att prep_vars (binding, raw_bundle) fixes lthy = |
|
56 let |
|
57 val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes; |
|
58 val bundle0 = raw_bundle |
|
59 |> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts)); |
|
60 val bundle = |
|
61 Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat |
|
62 |> transform_bundle (Proof_Context.export_morphism ctxt' lthy); |
|
63 in |
|
64 lthy |> Local_Theory.declaration {syntax = false, pervasive = true} |
|
65 (fn phi => fn context => |
|
66 context |> Data.map |
|
67 (#2 o Name_Space.define context true |
|
68 (Morphism.binding phi binding, transform_bundle phi bundle))) |
|
69 end; |
|
70 |
|
71 in |
|
72 |
|
73 val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars; |
|
74 val bundle_cmd = |
|
75 gen_bundle Proof_Context.get_fact (Attrib.intern_src o Proof_Context.theory_of) |
|
76 Proof_Context.read_vars; |
|
77 |
|
78 end; |
|
79 |
|
80 |
|
81 (* include bundle *) |
|
82 |
|
83 fun gen_include prep raw_name = |
|
84 Proof.map_context (fn ctxt => |
|
85 let |
|
86 val bundle = the_bundle ctxt (prep ctxt raw_name); |
|
87 val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt); |
|
88 val note = ((Binding.empty, []), map (apsnd (map attrib)) bundle); |
|
89 in #2 (Proof_Context.note_thmss "" [note] ctxt) end); |
|
90 |
|
91 fun include_ name = Proof.assert_forward #> gen_include (K I) name #> Proof.put_facts NONE; |
|
92 fun include_cmd name = Proof.assert_forward #> gen_include check name #> Proof.put_facts NONE; |
|
93 fun including name = Proof.assert_backward #> gen_include (K I) name; |
|
94 fun including_cmd name = Proof.assert_backward #> gen_include check name; |
|
95 |
|
96 |
|
97 (* print_bundles *) |
|
98 |
|
99 fun print_bundles ctxt = |
|
100 let |
|
101 val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; |
|
102 |
|
103 fun prt_fact (ths, []) = map prt_thm ths |
|
104 | prt_fact (ths, atts) = Pretty.enclose "(" ")" |
|
105 (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts; |
|
106 |
|
107 fun prt_bundle (name, bundle) = |
|
108 Pretty.block (Pretty.command "bundle" :: Pretty.str " " :: Pretty.str name :: |
|
109 Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle)); |
|
110 in |
|
111 map prt_bundle (Name_Space.extern_table ctxt (get_bundles ctxt)) |
|
112 end |> Pretty.chunks |> Pretty.writeln; |
|
113 |
|
114 end; |
|
115 |