58657
|
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 |
|