|
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 val print_attributes: theory -> unit |
|
14 end; |
|
15 |
|
16 signature ATTRIBUTE = |
|
17 sig |
|
18 include BASIC_ATTRIBUTE |
|
19 val thm_of: tthm -> thm |
|
20 val tthm_of: thm -> tthm |
|
21 val apply: ('a * tthm) * 'a attribute list -> ('a * tthm) |
|
22 val pretty_tthm: tthm -> Pretty.T |
|
23 val tag: tag -> 'a attribute |
|
24 val simple: string -> 'a attribute |
|
25 val lemma: tag |
|
26 val assumption: tag |
|
27 val tag_lemma: 'a attribute |
|
28 val tag_assumption: 'a attribute |
|
29 val setup: theory -> theory |
|
30 val global_attr: theory -> xstring -> string list -> theory attribute |
|
31 val local_attr: theory -> xstring -> string list -> object Symtab.table attribute |
|
32 val add_attrs: (bstring * ((string list -> theory attribute) * |
|
33 (string list -> object Symtab.table attribute))) list -> theory -> theory |
|
34 end; |
|
35 |
|
36 structure Attribute: ATTRIBUTE = |
|
37 struct |
|
38 |
|
39 |
|
40 (** tags and attributes **) |
|
41 |
|
42 type tag = string * string list; |
|
43 type tthm = thm * tag list; |
|
44 type 'a attribute = 'a * tthm -> 'a * tthm; |
|
45 |
|
46 fun thm_of (thm, _) = thm; |
|
47 fun tthm_of thm = (thm, []); |
|
48 |
|
49 fun apply x_attrs = foldl (op |>) x_attrs; |
|
50 |
|
51 |
|
52 (* display tagged theorems *) |
|
53 |
|
54 fun pretty_tag (name, []) = Pretty.str name |
|
55 | pretty_tag (name, args) = Pretty.block |
|
56 [Pretty.str name, Pretty.list "(" ")" (map Pretty.str args)]; |
|
57 |
|
58 val pretty_tags = Pretty.list "[" "]" o map pretty_tag; |
|
59 |
|
60 fun pretty_tthm (thm, []) = Pretty.quote (Display.pretty_thm thm) |
|
61 | pretty_tthm (thm, tags) = Pretty.block |
|
62 [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags]; |
|
63 |
|
64 |
|
65 (* basic attributes *) |
|
66 |
|
67 fun tag name_args (x, (thm, tags)) = (x, (thm, name_args ins tags)); |
|
68 fun simple name = tag (name, []); |
|
69 |
|
70 val lemma = ("lemma", []); |
|
71 val assumption = ("assumption", []); |
|
72 fun tag_lemma x = tag lemma x; |
|
73 fun tag_assumption x = tag assumption x; |
|
74 |
|
75 |
|
76 |
|
77 (** theory data **) |
|
78 |
|
79 (* data kind 'attributes' *) |
|
80 |
|
81 val attributesK = "Pure/attributes"; |
|
82 |
|
83 exception Attributes of |
|
84 {space: NameSpace.T, |
|
85 attrs: |
|
86 ((string list -> theory attribute) * |
|
87 (string list -> object Symtab.table attribute)) Symtab.table}; |
|
88 |
|
89 fun print_attributes thy = Display.print_data thy attributesK; |
|
90 |
|
91 |
|
92 (* setup *) |
|
93 |
|
94 local |
|
95 val empty = Attributes {space = NameSpace.empty, attrs = Symtab.empty}; |
|
96 |
|
97 fun prep_ext (x as Attributes _) = x; |
|
98 |
|
99 fun merge (Attributes {space = space1, attrs = attrs1}, |
|
100 Attributes {space = space2, attrs = attrs2}) = |
|
101 Attributes { |
|
102 space = NameSpace.merge (space1, space2), |
|
103 attrs = Symtab.merge (K true) (attrs1, attrs2)}; |
|
104 |
|
105 fun print _ (Attributes {space, attrs}) = |
|
106 (Pretty.writeln (Display.pretty_name_space ("attribute name space", space)); |
|
107 Pretty.writeln (Pretty.strs ("attributes:" :: map fst (Symtab.dest attrs)))); |
|
108 in |
|
109 val setup = Theory.init_data [(attributesK, (empty, prep_ext, merge, print))]; |
|
110 end; |
|
111 |
|
112 |
|
113 (* get data record *) |
|
114 |
|
115 fun get_attributes_sg sg = |
|
116 (case Sign.get_data sg attributesK of |
|
117 Attributes x => x |
|
118 | _ => sys_error "get_attributes_sg"); |
|
119 |
|
120 val get_attributes = get_attributes_sg o Theory.sign_of; |
|
121 |
|
122 |
|
123 (* get global / local attributes *) |
|
124 |
|
125 fun attrs which thy raw_name args = |
|
126 let |
|
127 val {space, attrs} = get_attributes thy; |
|
128 val name = NameSpace.intern space raw_name; |
|
129 in |
|
130 (case Symtab.lookup (attrs, name) of |
|
131 None => error ("Unknown attribute: " ^ quote name) |
|
132 | Some p => which p args) |
|
133 end; |
|
134 |
|
135 val global_attr = attrs fst; |
|
136 val local_attr = attrs snd; |
|
137 |
|
138 |
|
139 (* add_attrs *) |
|
140 |
|
141 fun add_attrs raw_attrs thy = |
|
142 let |
|
143 val full = Sign.full_name (Theory.sign_of thy); |
|
144 val new_attrs = map (apfst full) raw_attrs; |
|
145 |
|
146 val {space, attrs} = get_attributes thy; |
|
147 val space' = NameSpace.extend (space, map fst new_attrs); |
|
148 val attrs' = Symtab.extend (attrs, new_attrs) |
|
149 handle Symtab.DUPS dups => |
|
150 error ("Duplicate declaration of attributes(s) " ^ commas_quote dups); |
|
151 in |
|
152 Theory.put_data (attributesK, Attributes {space = space', attrs = attrs'}) thy |
|
153 end; |
|
154 |
|
155 |
|
156 end; |
|
157 |
|
158 |
|
159 structure BasicAttribute: BASIC_ATTRIBUTE = Attribute; |
|
160 open BasicAttribute; |