wenzelm@5823
|
1 |
(* Title: Pure/Isar/attrib.ML
|
wenzelm@5823
|
2 |
Author: Markus Wenzel, TU Muenchen
|
wenzelm@5823
|
3 |
|
wenzelm@18734
|
4 |
Symbolic representation of attributes -- with name and syntax.
|
wenzelm@5823
|
5 |
*)
|
wenzelm@5823
|
6 |
|
wenzelm@5823
|
7 |
signature ATTRIB =
|
wenzelm@5823
|
8 |
sig
|
wenzelm@27729
|
9 |
type src = Args.src
|
haftmann@29581
|
10 |
type binding = binding * src list
|
haftmann@28965
|
11 |
val empty_binding: binding
|
wenzelm@27729
|
12 |
val print_attributes: theory -> unit
|
wenzelm@16458
|
13 |
val intern: theory -> xstring -> string
|
wenzelm@16458
|
14 |
val intern_src: theory -> src -> src
|
wenzelm@21031
|
15 |
val pretty_attribs: Proof.context -> src list -> Pretty.T list
|
wenzelm@26891
|
16 |
val defined: theory -> string -> bool
|
wenzelm@18734
|
17 |
val attribute: theory -> src -> attribute
|
wenzelm@18734
|
18 |
val attribute_i: theory -> src -> attribute
|
wenzelm@26336
|
19 |
val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
|
wenzelm@18905
|
20 |
val map_specs: ('a -> 'att) ->
|
wenzelm@30766
|
21 |
(('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
|
wenzelm@18905
|
22 |
val map_facts: ('a -> 'att) ->
|
wenzelm@17105
|
23 |
(('c * 'a list) * ('d * 'a list) list) list ->
|
wenzelm@18905
|
24 |
(('c * 'att list) * ('d * 'att list) list) list
|
wenzelm@30766
|
25 |
val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
|
wenzelm@30766
|
26 |
(('c * 'a list) * ('b * 'a list) list) list ->
|
wenzelm@30766
|
27 |
(('c * 'att list) * ('fact * 'att list) list) list
|
wenzelm@20289
|
28 |
val crude_closure: Proof.context -> src -> src
|
wenzelm@18734
|
29 |
val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
|
wenzelm@30518
|
30 |
val syntax: attribute context_parser -> src -> attribute
|
wenzelm@30527
|
31 |
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
|
wenzelm@30578
|
32 |
val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
|
wenzelm@30578
|
33 |
theory -> theory
|
wenzelm@25983
|
34 |
val no_args: attribute -> src -> attribute
|
wenzelm@30527
|
35 |
val add_del: attribute -> attribute -> attribute context_parser
|
wenzelm@25983
|
36 |
val add_del_args: attribute -> attribute -> src -> attribute
|
wenzelm@30518
|
37 |
val thm_sel: Facts.interval list parser
|
wenzelm@30518
|
38 |
val thm: thm context_parser
|
wenzelm@30518
|
39 |
val thms: thm list context_parser
|
wenzelm@30518
|
40 |
val multi_thm: thm list context_parser
|
wenzelm@24110
|
41 |
val print_configs: Proof.context -> unit
|
wenzelm@25983
|
42 |
val internal: (morphism -> attribute) -> src
|
wenzelm@24126
|
43 |
val register_config: Config.value Config.T -> theory -> theory
|
wenzelm@24110
|
44 |
val config_bool: bstring -> bool -> bool Config.T * (theory -> theory)
|
wenzelm@24110
|
45 |
val config_int: bstring -> int -> int Config.T * (theory -> theory)
|
wenzelm@24110
|
46 |
val config_string: bstring -> string -> string Config.T * (theory -> theory)
|
wenzelm@24110
|
47 |
val config_bool_global: bstring -> bool -> bool Config.T * (theory -> theory)
|
wenzelm@24110
|
48 |
val config_int_global: bstring -> int -> int Config.T * (theory -> theory)
|
wenzelm@24110
|
49 |
val config_string_global: bstring -> string -> string Config.T * (theory -> theory)
|
wenzelm@5823
|
50 |
end;
|
wenzelm@5823
|
51 |
|
wenzelm@5823
|
52 |
structure Attrib: ATTRIB =
|
wenzelm@5823
|
53 |
struct
|
wenzelm@5823
|
54 |
|
wenzelm@27812
|
55 |
structure T = OuterLex;
|
wenzelm@27812
|
56 |
structure P = OuterParse;
|
wenzelm@27812
|
57 |
|
wenzelm@28084
|
58 |
|
wenzelm@28084
|
59 |
(* source and bindings *)
|
wenzelm@28084
|
60 |
|
wenzelm@15703
|
61 |
type src = Args.src;
|
wenzelm@15703
|
62 |
|
haftmann@29581
|
63 |
type binding = binding * src list;
|
haftmann@28965
|
64 |
val empty_binding: binding = (Binding.empty, []);
|
wenzelm@28084
|
65 |
|
wenzelm@28084
|
66 |
|
wenzelm@27729
|
67 |
|
wenzelm@18734
|
68 |
(** named attributes **)
|
wenzelm@18636
|
69 |
|
wenzelm@18734
|
70 |
(* theory data *)
|
wenzelm@5823
|
71 |
|
wenzelm@24110
|
72 |
structure Attributes = TheoryDataFun
|
wenzelm@22846
|
73 |
(
|
wenzelm@18734
|
74 |
type T = (((src -> attribute) * string) * stamp) NameSpace.table;
|
wenzelm@16344
|
75 |
val empty = NameSpace.empty_table;
|
wenzelm@6546
|
76 |
val copy = I;
|
wenzelm@16458
|
77 |
val extend = I;
|
wenzelm@23655
|
78 |
fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
|
wenzelm@23655
|
79 |
error ("Attempt to merge different versions of attribute " ^ quote dup);
|
wenzelm@22846
|
80 |
);
|
wenzelm@5823
|
81 |
|
wenzelm@22846
|
82 |
fun print_attributes thy =
|
wenzelm@22846
|
83 |
let
|
wenzelm@24110
|
84 |
val attribs = Attributes.get thy;
|
wenzelm@22846
|
85 |
fun prt_attr (name, ((_, comment), _)) = Pretty.block
|
wenzelm@22846
|
86 |
[Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
|
wenzelm@22846
|
87 |
in
|
wenzelm@22846
|
88 |
[Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
|
wenzelm@22846
|
89 |
|> Pretty.chunks |> Pretty.writeln
|
wenzelm@22846
|
90 |
end;
|
wenzelm@7611
|
91 |
|
wenzelm@5823
|
92 |
|
wenzelm@21031
|
93 |
(* name space *)
|
wenzelm@15703
|
94 |
|
wenzelm@24110
|
95 |
val intern = NameSpace.intern o #1 o Attributes.get;
|
wenzelm@15703
|
96 |
val intern_src = Args.map_name o intern;
|
wenzelm@15703
|
97 |
|
wenzelm@24110
|
98 |
val extern = NameSpace.extern o #1 o Attributes.get o ProofContext.theory_of;
|
wenzelm@21031
|
99 |
|
wenzelm@21031
|
100 |
|
wenzelm@21031
|
101 |
(* pretty printing *)
|
wenzelm@21031
|
102 |
|
wenzelm@21031
|
103 |
fun pretty_attribs _ [] = []
|
wenzelm@21031
|
104 |
| pretty_attribs ctxt srcs =
|
wenzelm@21031
|
105 |
[Pretty.enclose "[" "]"
|
wenzelm@21031
|
106 |
(Pretty.commas (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs))];
|
wenzelm@21031
|
107 |
|
wenzelm@15703
|
108 |
|
wenzelm@18734
|
109 |
(* get attributes *)
|
wenzelm@5823
|
110 |
|
wenzelm@26891
|
111 |
val defined = Symtab.defined o #2 o Attributes.get;
|
wenzelm@26891
|
112 |
|
wenzelm@18734
|
113 |
fun attribute_i thy =
|
wenzelm@5823
|
114 |
let
|
wenzelm@24110
|
115 |
val attrs = #2 (Attributes.get thy);
|
wenzelm@5879
|
116 |
fun attr src =
|
wenzelm@16344
|
117 |
let val ((name, _), pos) = Args.dest_src src in
|
wenzelm@17412
|
118 |
(case Symtab.lookup attrs name of
|
skalberg@15531
|
119 |
NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
|
wenzelm@27751
|
120 |
| SOME ((att, _), _) => (Position.report (Markup.attribute name) pos; att src))
|
wenzelm@5823
|
121 |
end;
|
wenzelm@5823
|
122 |
in attr end;
|
wenzelm@5823
|
123 |
|
wenzelm@18734
|
124 |
fun attribute thy = attribute_i thy o intern_src thy;
|
wenzelm@18636
|
125 |
|
haftmann@31177
|
126 |
fun eval_thms ctxt args = ProofContext.note_thmss Thm.generatedK
|
wenzelm@30766
|
127 |
[(Thm.empty_binding, args |> map (fn (a, atts) =>
|
wenzelm@30766
|
128 |
(ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
|
wenzelm@26685
|
129 |
|> fst |> maps snd;
|
wenzelm@24723
|
130 |
|
wenzelm@5823
|
131 |
|
wenzelm@17105
|
132 |
(* attributed declarations *)
|
wenzelm@17105
|
133 |
|
wenzelm@17105
|
134 |
fun map_specs f = map (apfst (apsnd (map f)));
|
wenzelm@30766
|
135 |
|
wenzelm@17105
|
136 |
fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f))));
|
wenzelm@30766
|
137 |
fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
|
wenzelm@17105
|
138 |
|
wenzelm@17105
|
139 |
|
wenzelm@15703
|
140 |
(* crude_closure *)
|
wenzelm@15703
|
141 |
|
wenzelm@15703
|
142 |
(*Produce closure without knowing facts in advance! The following
|
wenzelm@18734
|
143 |
works reasonably well for attribute parsers that do not peek at the
|
wenzelm@18734
|
144 |
thm structure.*)
|
wenzelm@15703
|
145 |
|
wenzelm@15703
|
146 |
fun crude_closure ctxt src =
|
wenzelm@18734
|
147 |
(try (fn () => attribute_i (ProofContext.theory_of ctxt) src
|
wenzelm@18734
|
148 |
(Context.Proof ctxt, Drule.asm_rl)) ();
|
wenzelm@15703
|
149 |
Args.closure src);
|
wenzelm@15703
|
150 |
|
wenzelm@15703
|
151 |
|
wenzelm@5823
|
152 |
(* add_attributes *)
|
wenzelm@5823
|
153 |
|
wenzelm@5823
|
154 |
fun add_attributes raw_attrs thy =
|
wenzelm@5823
|
155 |
let
|
wenzelm@18734
|
156 |
val new_attrs =
|
haftmann@28997
|
157 |
raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
|
wenzelm@30466
|
158 |
fun add attrs = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_attrs attrs
|
wenzelm@23655
|
159 |
handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
|
wenzelm@24110
|
160 |
in Attributes.map add thy end;
|
wenzelm@5823
|
161 |
|
wenzelm@5823
|
162 |
|
wenzelm@30527
|
163 |
(* attribute setup *)
|
wenzelm@5823
|
164 |
|
wenzelm@30527
|
165 |
fun syntax scan src (context, th) =
|
wenzelm@30527
|
166 |
let val (f: attribute, context') = Args.syntax "attribute" scan src context
|
wenzelm@30527
|
167 |
in f (context', th) end;
|
wenzelm@30527
|
168 |
|
wenzelm@30527
|
169 |
fun setup name scan comment = add_attributes [(Binding.name_of name, syntax scan, comment)];
|
wenzelm@30527
|
170 |
|
wenzelm@30527
|
171 |
fun attribute_setup name (txt, pos) cmt =
|
wenzelm@30527
|
172 |
Context.theory_map (ML_Context.expression pos
|
wenzelm@30527
|
173 |
"val (name, scan, comment): binding * attribute context_parser * string"
|
wenzelm@30527
|
174 |
"Context.map_theory (Attrib.setup name scan comment)"
|
wenzelm@30527
|
175 |
("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));
|
wenzelm@30527
|
176 |
|
wenzelm@30527
|
177 |
|
wenzelm@30527
|
178 |
(* basic syntax *)
|
wenzelm@5823
|
179 |
|
wenzelm@25983
|
180 |
fun no_args x = syntax (Scan.succeed x);
|
wenzelm@5823
|
181 |
|
wenzelm@30527
|
182 |
fun add_del add del = (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add));
|
wenzelm@30527
|
183 |
fun add_del_args add del = syntax (add_del add del);
|
wenzelm@5879
|
184 |
|
wenzelm@5879
|
185 |
|
wenzelm@25983
|
186 |
|
wenzelm@25983
|
187 |
(** parsing attributed theorems **)
|
wenzelm@5879
|
188 |
|
wenzelm@27812
|
189 |
val thm_sel = P.$$$ "(" |-- P.list1
|
wenzelm@27812
|
190 |
(P.nat --| P.minus -- P.nat >> Facts.FromTo ||
|
wenzelm@27812
|
191 |
P.nat --| P.minus >> Facts.From ||
|
wenzelm@27812
|
192 |
P.nat >> Facts.Single) --| P.$$$ ")";
|
wenzelm@27812
|
193 |
|
wenzelm@18636
|
194 |
local
|
wenzelm@18636
|
195 |
|
wenzelm@21698
|
196 |
val fact_name = Args.internal_fact >> K "<fact>" || Args.name;
|
wenzelm@21698
|
197 |
|
wenzelm@26336
|
198 |
fun gen_thm pick = Scan.depend (fn context =>
|
wenzelm@26336
|
199 |
let
|
wenzelm@26336
|
200 |
val thy = Context.theory_of context;
|
wenzelm@26685
|
201 |
val get = Context.cases (PureThy.get_fact context) ProofContext.get_fact context;
|
wenzelm@26361
|
202 |
val get_fact = get o Facts.Fact;
|
wenzelm@27820
|
203 |
fun get_named pos name = get (Facts.Named ((name, pos), NONE));
|
wenzelm@26336
|
204 |
in
|
wenzelm@27820
|
205 |
P.$$$ "[" |-- Args.attribs (intern thy) --| P.$$$ "]" >> (fn srcs =>
|
wenzelm@24008
|
206 |
let
|
wenzelm@26336
|
207 |
val atts = map (attribute_i thy) srcs;
|
wenzelm@26336
|
208 |
val (context', th') = Library.apply atts (context, Drule.dummy_thm);
|
wenzelm@26336
|
209 |
in (context', pick "" [th']) end)
|
wenzelm@26336
|
210 |
||
|
wenzelm@26336
|
211 |
(Scan.ahead Args.alt_name -- Args.named_fact get_fact
|
wenzelm@27820
|
212 |
>> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
|
wenzelm@27820
|
213 |
Scan.ahead (P.position fact_name) :|-- (fn (name, pos) =>
|
wenzelm@27820
|
214 |
Args.named_fact (get_named pos) -- Scan.option thm_sel
|
wenzelm@27820
|
215 |
>> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
|
wenzelm@26336
|
216 |
-- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
|
wenzelm@26336
|
217 |
let
|
wenzelm@26336
|
218 |
val ths = Facts.select thmref fact;
|
wenzelm@26336
|
219 |
val atts = map (attribute_i thy) srcs;
|
wenzelm@30193
|
220 |
val (context', ths') = Library.foldl_map (Library.apply atts) (context, ths);
|
wenzelm@26336
|
221 |
in (context', pick name ths') end)
|
wenzelm@26336
|
222 |
end);
|
berghofe@15456
|
223 |
|
wenzelm@18636
|
224 |
in
|
wenzelm@18636
|
225 |
|
wenzelm@26336
|
226 |
val thm = gen_thm Facts.the_single;
|
wenzelm@18998
|
227 |
val multi_thm = gen_thm (K I);
|
wenzelm@19482
|
228 |
val thms = Scan.repeat multi_thm >> flat;
|
wenzelm@18636
|
229 |
|
wenzelm@18636
|
230 |
end;
|
wenzelm@18636
|
231 |
|
wenzelm@5879
|
232 |
|
wenzelm@5879
|
233 |
|
wenzelm@25983
|
234 |
(** basic attributes **)
|
wenzelm@5879
|
235 |
|
wenzelm@25983
|
236 |
(* internal *)
|
wenzelm@5879
|
237 |
|
wenzelm@27812
|
238 |
fun internal att = Args.src (("Pure.attribute", [T.mk_attribute att]), Position.none);
|
wenzelm@5823
|
239 |
|
wenzelm@25983
|
240 |
val internal_att =
|
wenzelm@25983
|
241 |
syntax (Scan.lift Args.internal_attribute >> Morphism.form);
|
wenzelm@25983
|
242 |
|
wenzelm@25983
|
243 |
|
wenzelm@25983
|
244 |
(* tags *)
|
wenzelm@25983
|
245 |
|
wenzelm@27865
|
246 |
val tagged = syntax (Scan.lift (Args.name -- Args.name) >> Thm.tag);
|
wenzelm@27865
|
247 |
val untagged = syntax (Scan.lift Args.name >> Thm.untag);
|
wenzelm@25983
|
248 |
|
wenzelm@27865
|
249 |
val kind = syntax (Scan.lift Args.name >> Thm.kind);
|
wenzelm@25983
|
250 |
|
wenzelm@25983
|
251 |
|
wenzelm@25983
|
252 |
(* rule composition *)
|
wenzelm@25983
|
253 |
|
wenzelm@25983
|
254 |
val COMP_att =
|
wenzelm@27812
|
255 |
syntax (Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
|
wenzelm@25983
|
256 |
>> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B))));
|
wenzelm@25983
|
257 |
|
wenzelm@25983
|
258 |
val THEN_att =
|
wenzelm@27812
|
259 |
syntax (Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
|
wenzelm@25983
|
260 |
>> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B))));
|
wenzelm@25983
|
261 |
|
wenzelm@25983
|
262 |
val OF_att =
|
wenzelm@25983
|
263 |
syntax (thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A)));
|
wenzelm@25983
|
264 |
|
wenzelm@25983
|
265 |
|
wenzelm@25983
|
266 |
(* rename_abs *)
|
wenzelm@25983
|
267 |
|
wenzelm@25983
|
268 |
val rename_abs = syntax
|
wenzelm@25983
|
269 |
(Scan.lift (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars')));
|
wenzelm@25983
|
270 |
|
wenzelm@25983
|
271 |
|
wenzelm@25983
|
272 |
(* unfold / fold definitions *)
|
wenzelm@25983
|
273 |
|
wenzelm@25983
|
274 |
fun unfolded_syntax rule =
|
wenzelm@25983
|
275 |
syntax (thms >>
|
wenzelm@25983
|
276 |
(fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths)));
|
wenzelm@25983
|
277 |
|
wenzelm@25983
|
278 |
val unfolded = unfolded_syntax LocalDefs.unfold;
|
wenzelm@25983
|
279 |
val folded = unfolded_syntax LocalDefs.fold;
|
wenzelm@25983
|
280 |
|
wenzelm@25983
|
281 |
|
wenzelm@25983
|
282 |
(* rule cases *)
|
wenzelm@25983
|
283 |
|
wenzelm@27812
|
284 |
val consumes = syntax (Scan.lift (Scan.optional P.nat 1) >> RuleCases.consumes);
|
wenzelm@25983
|
285 |
val case_names = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names);
|
wenzelm@25983
|
286 |
val case_conclusion =
|
wenzelm@25983
|
287 |
syntax (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion);
|
wenzelm@27812
|
288 |
val params = syntax (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> RuleCases.params);
|
wenzelm@25983
|
289 |
|
wenzelm@25983
|
290 |
|
wenzelm@25983
|
291 |
(* rule format *)
|
wenzelm@25983
|
292 |
|
wenzelm@25983
|
293 |
val rule_format = syntax (Args.mode "no_asm"
|
wenzelm@25983
|
294 |
>> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format));
|
wenzelm@25983
|
295 |
|
wenzelm@25983
|
296 |
val elim_format = no_args (Thm.rule_attribute (K Tactic.make_elim));
|
wenzelm@25983
|
297 |
|
wenzelm@25983
|
298 |
|
wenzelm@25983
|
299 |
(* misc rules *)
|
wenzelm@25983
|
300 |
|
wenzelm@25983
|
301 |
val standard = no_args (Thm.rule_attribute (K Drule.standard));
|
wenzelm@25983
|
302 |
|
wenzelm@26715
|
303 |
val no_vars = no_args (Thm.rule_attribute (fn context => fn th =>
|
wenzelm@26715
|
304 |
let
|
wenzelm@26715
|
305 |
val ctxt = Variable.set_body false (Context.proof_of context);
|
wenzelm@26715
|
306 |
val ((_, [th']), _) = Variable.import_thms true [th] ctxt;
|
wenzelm@25983
|
307 |
in th' end));
|
wenzelm@25983
|
308 |
|
wenzelm@25983
|
309 |
val eta_long =
|
wenzelm@25983
|
310 |
no_args (Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion)));
|
wenzelm@25983
|
311 |
|
wenzelm@25983
|
312 |
val rotated = syntax
|
wenzelm@27812
|
313 |
(Scan.lift (Scan.optional P.int 1) >> (fn n => Thm.rule_attribute (K (rotate_prems n))));
|
wenzelm@25983
|
314 |
|
berghofe@29690
|
315 |
val abs_def = no_args (Thm.rule_attribute (K Drule.abs_def));
|
berghofe@29690
|
316 |
|
wenzelm@25983
|
317 |
|
wenzelm@25983
|
318 |
(* theory setup *)
|
wenzelm@25983
|
319 |
|
wenzelm@26463
|
320 |
val _ = Context.>> (Context.map_theory
|
wenzelm@25983
|
321 |
(add_attributes
|
wenzelm@25983
|
322 |
[("attribute", internal_att, "internal attribute"),
|
wenzelm@25983
|
323 |
("tagged", tagged, "tagged theorem"),
|
wenzelm@25983
|
324 |
("untagged", untagged, "untagged theorem"),
|
wenzelm@25983
|
325 |
("kind", kind, "theorem kind"),
|
wenzelm@25983
|
326 |
("COMP", COMP_att, "direct composition with rules (no lifting)"),
|
wenzelm@25983
|
327 |
("THEN", THEN_att, "resolution with rule"),
|
wenzelm@25983
|
328 |
("OF", OF_att, "rule applied to facts"),
|
wenzelm@25983
|
329 |
("rename_abs", rename_abs, "rename bound variables in abstractions"),
|
wenzelm@25983
|
330 |
("unfolded", unfolded, "unfolded definitions"),
|
wenzelm@25983
|
331 |
("folded", folded, "folded definitions"),
|
wenzelm@25983
|
332 |
("standard", standard, "result put into standard form"),
|
wenzelm@25983
|
333 |
("elim_format", elim_format, "destruct rule turned into elimination rule format"),
|
wenzelm@25983
|
334 |
("no_vars", no_vars, "frozen schematic vars"),
|
wenzelm@25983
|
335 |
("eta_long", eta_long, "put theorem into eta long beta normal form"),
|
wenzelm@25983
|
336 |
("consumes", consumes, "number of consumed facts"),
|
wenzelm@25983
|
337 |
("case_names", case_names, "named rule cases"),
|
wenzelm@25983
|
338 |
("case_conclusion", case_conclusion, "named conclusion of rule cases"),
|
wenzelm@25983
|
339 |
("params", params, "named rule parameters"),
|
wenzelm@25983
|
340 |
("atomize", no_args ObjectLogic.declare_atomize, "declaration of atomize rule"),
|
wenzelm@25983
|
341 |
("rulify", no_args ObjectLogic.declare_rulify, "declaration of rulify rule"),
|
wenzelm@25983
|
342 |
("rule_format", rule_format, "result put into standard rule format"),
|
wenzelm@25983
|
343 |
("rotated", rotated, "rotated theorem premises"),
|
wenzelm@25983
|
344 |
("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
|
berghofe@29690
|
345 |
"declaration of definitional transformations"),
|
berghofe@29690
|
346 |
("abs_def", abs_def, "abstract over free variables of a definition")]));
|
wenzelm@8633
|
347 |
|
wenzelm@5823
|
348 |
|
wenzelm@5823
|
349 |
|
wenzelm@24110
|
350 |
(** configuration options **)
|
wenzelm@5823
|
351 |
|
wenzelm@24110
|
352 |
(* naming *)
|
wenzelm@24110
|
353 |
|
wenzelm@24110
|
354 |
structure Configs = TheoryDataFun
|
wenzelm@24713
|
355 |
(
|
wenzelm@24110
|
356 |
type T = Config.value Config.T Symtab.table;
|
wenzelm@24110
|
357 |
val empty = Symtab.empty;
|
wenzelm@24110
|
358 |
val copy = I;
|
wenzelm@24110
|
359 |
val extend = I;
|
wenzelm@24110
|
360 |
fun merge _ = Symtab.merge (K true);
|
wenzelm@24713
|
361 |
);
|
wenzelm@24110
|
362 |
|
wenzelm@24110
|
363 |
fun print_configs ctxt =
|
wenzelm@24110
|
364 |
let
|
wenzelm@24110
|
365 |
val thy = ProofContext.theory_of ctxt;
|
wenzelm@24110
|
366 |
fun prt (name, config) =
|
wenzelm@24110
|
367 |
let val value = Config.get ctxt config in
|
wenzelm@24110
|
368 |
Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
|
wenzelm@24110
|
369 |
Pretty.str (Config.print_value value)]
|
wenzelm@24110
|
370 |
end;
|
wenzelm@24110
|
371 |
val configs = NameSpace.extern_table (#1 (Attributes.get thy), Configs.get thy);
|
wenzelm@24110
|
372 |
in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
|
wenzelm@24110
|
373 |
|
wenzelm@24110
|
374 |
|
wenzelm@24110
|
375 |
(* concrete syntax *)
|
wenzelm@23988
|
376 |
|
wenzelm@24003
|
377 |
local
|
wenzelm@24003
|
378 |
|
wenzelm@27820
|
379 |
val equals = P.$$$ "=";
|
wenzelm@24003
|
380 |
|
wenzelm@24110
|
381 |
fun scan_value (Config.Bool _) =
|
wenzelm@24110
|
382 |
equals -- Args.$$$ "false" >> K (Config.Bool false) ||
|
wenzelm@24110
|
383 |
equals -- Args.$$$ "true" >> K (Config.Bool true) ||
|
wenzelm@24110
|
384 |
Scan.succeed (Config.Bool true)
|
wenzelm@27812
|
385 |
| scan_value (Config.Int _) = equals |-- P.int >> Config.Int
|
wenzelm@24110
|
386 |
| scan_value (Config.String _) = equals |-- Args.name >> Config.String;
|
wenzelm@24003
|
387 |
|
wenzelm@24110
|
388 |
fun scan_config thy config =
|
wenzelm@24110
|
389 |
let val config_type = Config.get_thy thy config
|
wenzelm@24110
|
390 |
in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end;
|
wenzelm@24003
|
391 |
|
wenzelm@24003
|
392 |
in
|
wenzelm@24003
|
393 |
|
wenzelm@24126
|
394 |
fun register_config config thy =
|
wenzelm@24126
|
395 |
let
|
wenzelm@24126
|
396 |
val bname = Config.name_of config;
|
haftmann@28965
|
397 |
val name = Sign.full_bname thy bname;
|
wenzelm@24126
|
398 |
in
|
wenzelm@24126
|
399 |
thy
|
wenzelm@24126
|
400 |
|> add_attributes [(bname, syntax (Scan.lift (scan_config thy config) >> Morphism.form),
|
wenzelm@24126
|
401 |
"configuration option")]
|
wenzelm@24126
|
402 |
|> Configs.map (Symtab.update (name, config))
|
wenzelm@24126
|
403 |
end;
|
wenzelm@24110
|
404 |
|
wenzelm@24110
|
405 |
fun declare_config make coerce global name default =
|
wenzelm@24110
|
406 |
let
|
wenzelm@24110
|
407 |
val config_value = Config.declare global name (make default);
|
wenzelm@24110
|
408 |
val config = coerce config_value;
|
wenzelm@24126
|
409 |
in (config, register_config config_value) end;
|
wenzelm@24110
|
410 |
|
wenzelm@24110
|
411 |
val config_bool = declare_config Config.Bool Config.bool false;
|
wenzelm@24110
|
412 |
val config_int = declare_config Config.Int Config.int false;
|
wenzelm@24110
|
413 |
val config_string = declare_config Config.String Config.string false;
|
wenzelm@24110
|
414 |
|
wenzelm@24110
|
415 |
val config_bool_global = declare_config Config.Bool Config.bool true;
|
wenzelm@24110
|
416 |
val config_int_global = declare_config Config.Int Config.int true;
|
wenzelm@24110
|
417 |
val config_string_global = declare_config Config.String Config.string true;
|
wenzelm@24003
|
418 |
|
wenzelm@24003
|
419 |
end;
|
wenzelm@23988
|
420 |
|
wenzelm@23988
|
421 |
|
wenzelm@18636
|
422 |
(* theory setup *)
|
wenzelm@15703
|
423 |
|
wenzelm@26463
|
424 |
val _ = Context.>> (Context.map_theory
|
wenzelm@24178
|
425 |
(register_config Unify.trace_bound_value #>
|
wenzelm@24178
|
426 |
register_config Unify.search_bound_value #>
|
wenzelm@24178
|
427 |
register_config Unify.trace_simp_value #>
|
wenzelm@24178
|
428 |
register_config Unify.trace_types_value #>
|
wenzelm@26463
|
429 |
register_config MetaSimplifier.simp_depth_limit_value));
|
wenzelm@5823
|
430 |
|
wenzelm@5823
|
431 |
end;
|