4780
|
1 |
(* Title: Pure/attribute.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
|
|
5 |
Theorem tags and attributes.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature BASIC_ATTRIBUTE =
|
|
9 |
sig
|
|
10 |
type tag
|
|
11 |
type tthm
|
|
12 |
type 'a attribute
|
|
13 |
end;
|
|
14 |
|
|
15 |
signature ATTRIBUTE =
|
|
16 |
sig
|
|
17 |
include BASIC_ATTRIBUTE
|
|
18 |
val thm_of: tthm -> thm
|
|
19 |
val tthm_of: thm -> tthm
|
5872
|
20 |
val thms_of: tthm list -> thm list
|
|
21 |
val tthms_of: thm list -> tthm list
|
|
22 |
val rule: ('a -> thm -> thm) -> 'a attribute
|
4850
|
23 |
val none: 'a -> 'a * 'b attribute list
|
|
24 |
val no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list
|
|
25 |
val no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list
|
4780
|
26 |
val apply: ('a * tthm) * 'a attribute list -> ('a * tthm)
|
4850
|
27 |
val applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list)
|
4780
|
28 |
val pretty_tthm: tthm -> Pretty.T
|
5901
|
29 |
val pretty_tthms: tthm list -> Pretty.T
|
5872
|
30 |
val print_tthm: tthm -> unit
|
5901
|
31 |
val print_tthms: tthm list -> unit
|
4780
|
32 |
val tag: tag -> 'a attribute
|
4790
|
33 |
val untag: tag -> 'a attribute
|
4780
|
34 |
val lemma: tag
|
|
35 |
val assumption: tag
|
5194
|
36 |
val internal: tag
|
4780
|
37 |
val tag_lemma: 'a attribute
|
|
38 |
val tag_assumption: 'a attribute
|
5194
|
39 |
val tag_internal: 'a attribute
|
4780
|
40 |
end;
|
|
41 |
|
|
42 |
structure Attribute: ATTRIBUTE =
|
|
43 |
struct
|
|
44 |
|
|
45 |
|
|
46 |
(** tags and attributes **)
|
|
47 |
|
|
48 |
type tag = string * string list;
|
|
49 |
type tthm = thm * tag list;
|
|
50 |
type 'a attribute = 'a * tthm -> 'a * tthm;
|
|
51 |
|
|
52 |
fun thm_of (thm, _) = thm;
|
|
53 |
fun tthm_of thm = (thm, []);
|
|
54 |
|
5872
|
55 |
fun thms_of ths = map thm_of ths;
|
|
56 |
fun tthms_of ths = map tthm_of ths;
|
5835
|
57 |
|
5872
|
58 |
fun rule f (x, (thm, _)) = (x, (f x thm, []));
|
5835
|
59 |
|
4850
|
60 |
fun none x = (x, []);
|
|
61 |
fun no_attrs (x, y) = ((x, (y, [])), []);
|
|
62 |
fun no_attrss (x, ys) = ((x, map (rpair []) ys), []);
|
|
63 |
|
4790
|
64 |
|
|
65 |
(* apply attributes *)
|
|
66 |
|
5901
|
67 |
fun apply (x_th, atts) = Library.apply atts x_th;
|
|
68 |
fun applys (x_ths, atts) = foldl_map (Library.apply atts) x_ths;
|
4780
|
69 |
|
|
70 |
|
|
71 |
(* display tagged theorems *)
|
|
72 |
|
5559
|
73 |
fun pretty_tag (name, args) = Pretty.strs (name :: args);
|
4780
|
74 |
val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
|
|
75 |
|
|
76 |
fun pretty_tthm (thm, []) = Pretty.quote (Display.pretty_thm thm)
|
|
77 |
| pretty_tthm (thm, tags) = Pretty.block
|
|
78 |
[Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
|
|
79 |
|
5901
|
80 |
fun pretty_tthms [th] = pretty_tthm th
|
|
81 |
| pretty_tthms ths = Pretty.block (Pretty.fbreaks (map pretty_tthm ths));
|
|
82 |
|
5872
|
83 |
val print_tthm = Pretty.writeln o pretty_tthm;
|
5901
|
84 |
val print_tthms = Pretty.writeln o pretty_tthms;
|
5872
|
85 |
|
4780
|
86 |
|
|
87 |
(* basic attributes *)
|
|
88 |
|
5559
|
89 |
fun tag tg (x, (thm, tags)) = (x, (thm, if tg mem tags then tags else tags @ [tg]));
|
4790
|
90 |
fun untag tg (x, (thm, tags)) = (x, (thm, tags \ tg));
|
4780
|
91 |
|
|
92 |
val lemma = ("lemma", []);
|
|
93 |
val assumption = ("assumption", []);
|
5194
|
94 |
val internal = ("internal", []);
|
4780
|
95 |
fun tag_lemma x = tag lemma x;
|
|
96 |
fun tag_assumption x = tag assumption x;
|
5194
|
97 |
fun tag_internal x = tag internal x;
|
4780
|
98 |
|
|
99 |
|
|
100 |
end;
|
|
101 |
|
|
102 |
|
|
103 |
structure BasicAttribute: BASIC_ATTRIBUTE = Attribute;
|
|
104 |
open BasicAttribute;
|