|
1 (* Title: Pure/Tools/plugin.ML |
|
2 Author: Makarius |
|
3 Author: Jasmin Blanchette |
|
4 |
|
5 Named plugins for definitional packages. |
|
6 *) |
|
7 |
|
8 (** plugin name **) |
|
9 |
|
10 signature PLUGIN_NAME = |
|
11 sig |
|
12 val check: Proof.context -> xstring * Position.T -> string |
|
13 val declare: binding -> theory -> string * theory |
|
14 val setup: binding -> string |
|
15 type filter = string -> bool |
|
16 val parse_filter: (Proof.context -> filter) parser |
|
17 val make_filter: Proof.context -> (Proof.context -> filter) -> filter |
|
18 end; |
|
19 |
|
20 structure Plugin_Name: PLUGIN_NAME = |
|
21 struct |
|
22 |
|
23 (* theory data *) |
|
24 |
|
25 structure Data = Theory_Data |
|
26 ( |
|
27 type T = unit Name_Space.table; |
|
28 val empty: T = Name_Space.empty_table "plugin"; |
|
29 val extend = I; |
|
30 val merge = Name_Space.merge_tables; |
|
31 ); |
|
32 |
|
33 |
|
34 (* check *) |
|
35 |
|
36 fun check ctxt = |
|
37 #1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt)); |
|
38 |
|
39 val _ = Theory.setup |
|
40 (ML_Antiquotation.inline @{binding plugin} |
|
41 (Args.context -- Scan.lift (Parse.position Args.name) |
|
42 >> (ML_Syntax.print_string o uncurry check))); |
|
43 |
|
44 |
|
45 (* declare *) |
|
46 |
|
47 fun declare binding thy = |
|
48 let |
|
49 val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.default_naming); |
|
50 val (name, data') = Name_Space.define context true (binding, ()) (Data.get thy); |
|
51 val thy' = Data.put data' thy; |
|
52 in (name, thy') end; |
|
53 |
|
54 fun setup binding = Context.>>> (Context.map_theory_result (declare binding)); |
|
55 |
|
56 |
|
57 (* filter *) |
|
58 |
|
59 type filter = string -> bool; |
|
60 |
|
61 fun make_filter (ctxt: Proof.context) f : filter = f ctxt; |
|
62 |
|
63 val parse_filter = |
|
64 Parse.position (Parse.reserved "plugins") -- |
|
65 Parse.position (Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) -- |
|
66 (@{keyword ":"} |-- Scan.repeat (Parse.position Parse.name)) >> |
|
67 (fn (((_, pos1), (modif, pos2)), args) => fn ctxt => |
|
68 let |
|
69 val _ = Context_Position.reports ctxt (map (rpair Markup.quasi_keyword) [pos1, pos2]); |
|
70 val names = map (check ctxt) args; |
|
71 in modif o member (op =) names end); |
|
72 |
|
73 end; |
|
74 |
|
75 |
|
76 |
|
77 (** plugin content **) |
|
78 |
|
79 signature PLUGIN = |
|
80 sig |
|
81 type T |
|
82 val data: Plugin_Name.filter -> T -> local_theory -> local_theory |
|
83 val interpretation: string -> (T -> local_theory -> local_theory) -> theory -> theory |
|
84 end; |
|
85 |
|
86 functor Plugin(type T): PLUGIN = |
|
87 struct |
|
88 |
|
89 type T = T; |
|
90 |
|
91 |
|
92 (* data with interpretation *) |
|
93 |
|
94 type data = {filter: Plugin_Name.filter, naming: Name_Space.naming, value: T, id: serial}; |
|
95 type interp = {name: string, apply: T -> local_theory -> local_theory, id: serial}; |
|
96 |
|
97 val eq_data: data * data -> bool = op = o pairself #id; |
|
98 val eq_interp: interp * interp -> bool = op = o pairself #id; |
|
99 |
|
100 fun mk_data filter naming x : data = {filter = filter, naming = naming, value = x, id = serial ()}; |
|
101 fun mk_interp name f : interp = {name = name, apply = f, id = serial ()}; |
|
102 |
|
103 |
|
104 (* theory data *) |
|
105 |
|
106 structure Plugin_Data = Theory_Data |
|
107 ( |
|
108 type T = data list * (interp * data list) list; |
|
109 val empty : T = ([], []); |
|
110 val extend = I; |
|
111 val merge_data = merge eq_data; |
|
112 fun merge ((data1, interps1), (data2, interps2)) : T = |
|
113 (merge_data (data1, data2), AList.join eq_interp (K merge_data) (interps1, interps2)); |
|
114 ); |
|
115 |
|
116 |
|
117 (* consolidate data wrt. interpretations *) |
|
118 |
|
119 local |
|
120 |
|
121 fun apply change_naming (interp: interp) (data: data) lthy = |
|
122 lthy |
|
123 |> change_naming ? Local_Theory.map_naming (K (#naming data)) |
|
124 |> #apply interp (#value data) |
|
125 |> Local_Theory.restore_naming lthy; |
|
126 |
|
127 fun unfinished data (interp: interp, data') = |
|
128 (interp, |
|
129 if eq_list eq_data (data, data') then [] |
|
130 else data |> filter (fn d => #filter d (#name interp) andalso not (member eq_data data' d))); |
|
131 |
|
132 fun unfinished_data thy = |
|
133 let |
|
134 val (data, interps) = Plugin_Data.get thy; |
|
135 val finished = map (apsnd (K data)) interps; |
|
136 val thy' = Plugin_Data.put (data, finished) thy; |
|
137 in (map (unfinished data) interps, thy') end; |
|
138 |
|
139 in |
|
140 |
|
141 val consolidate = |
|
142 Local_Theory.raw_theory_result unfinished_data |
|
143 #-> fold_rev (fn (interp, data) => fold_rev (apply false interp) data); |
|
144 |
|
145 val consolidate' = |
|
146 unfinished_data #> (fn (unfinished, thy) => |
|
147 if forall (null o #2) unfinished then NONE |
|
148 else |
|
149 Named_Target.theory_init thy |
|
150 |> fold_rev (fn (interp, data) => fold_rev (apply true interp) data) unfinished |
|
151 |> Local_Theory.exit_global |
|
152 |> SOME); |
|
153 |
|
154 end; |
|
155 |
|
156 val _ = Theory.setup (Theory.at_begin consolidate'); |
|
157 |
|
158 |
|
159 (* add content *) |
|
160 |
|
161 fun data filter x = |
|
162 Local_Theory.background_theory (fn thy => |
|
163 Plugin_Data.map (apfst (cons (mk_data filter (Sign.naming_of thy) x))) thy) |
|
164 #> consolidate; |
|
165 |
|
166 fun interpretation name f = |
|
167 Plugin_Data.map (apsnd (cons (mk_interp name f, []))) |
|
168 #> perhaps consolidate'; |
|
169 |
|
170 end; |
|
171 |