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
|
4850
|
20 |
val none: 'a -> 'a * 'b attribute list
|
|
21 |
val no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list
|
|
22 |
val no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list
|
4790
|
23 |
val fail: string -> string -> 'a
|
4780
|
24 |
val apply: ('a * tthm) * 'a attribute list -> ('a * tthm)
|
4850
|
25 |
val applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list)
|
4780
|
26 |
val pretty_tthm: tthm -> Pretty.T
|
|
27 |
val tag: tag -> 'a attribute
|
4790
|
28 |
val untag: tag -> 'a attribute
|
4780
|
29 |
val lemma: tag
|
|
30 |
val assumption: tag
|
|
31 |
val tag_lemma: 'a attribute
|
|
32 |
val tag_assumption: 'a attribute
|
|
33 |
end;
|
|
34 |
|
|
35 |
structure Attribute: ATTRIBUTE =
|
|
36 |
struct
|
|
37 |
|
|
38 |
|
|
39 |
(** tags and attributes **)
|
|
40 |
|
|
41 |
type tag = string * string list;
|
|
42 |
type tthm = thm * tag list;
|
|
43 |
type 'a attribute = 'a * tthm -> 'a * tthm;
|
|
44 |
|
|
45 |
fun thm_of (thm, _) = thm;
|
|
46 |
fun tthm_of thm = (thm, []);
|
|
47 |
|
4850
|
48 |
fun none x = (x, []);
|
|
49 |
fun no_attrs (x, y) = ((x, (y, [])), []);
|
|
50 |
fun no_attrss (x, ys) = ((x, map (rpair []) ys), []);
|
|
51 |
|
4790
|
52 |
|
|
53 |
(* apply attributes *)
|
|
54 |
|
|
55 |
exception FAIL of string * string;
|
|
56 |
|
|
57 |
fun fail name msg = raise FAIL (name, msg);
|
|
58 |
|
5023
|
59 |
(* FIXME error (!!?), push up the warning (??) *)
|
4790
|
60 |
fun warn_failed (name, msg) =
|
4797
|
61 |
warning ("Failed invocation of " ^ quote name ^ " attribute: " ^ msg);
|
4790
|
62 |
|
4850
|
63 |
fun apply (x_th, []) = x_th
|
|
64 |
| apply (x_th, f :: fs) = apply (f x_th handle FAIL info => (warn_failed info; x_th), fs);
|
|
65 |
|
|
66 |
fun applys ((x, []), _) = (x, [])
|
|
67 |
| applys ((x, th :: ths), atts) =
|
|
68 |
let
|
|
69 |
val (x', th') = apply ((x, th), atts);
|
|
70 |
val (x'', ths') = applys ((x', ths), atts);
|
|
71 |
in (x'', th' :: ths') end;
|
4780
|
72 |
|
|
73 |
|
|
74 |
(* display tagged theorems *)
|
|
75 |
|
|
76 |
fun pretty_tag (name, []) = Pretty.str name
|
|
77 |
| pretty_tag (name, args) = Pretty.block
|
|
78 |
[Pretty.str name, Pretty.list "(" ")" (map Pretty.str args)];
|
|
79 |
|
|
80 |
val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
|
|
81 |
|
|
82 |
fun pretty_tthm (thm, []) = Pretty.quote (Display.pretty_thm thm)
|
|
83 |
| pretty_tthm (thm, tags) = Pretty.block
|
|
84 |
[Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
|
|
85 |
|
|
86 |
|
|
87 |
(* basic attributes *)
|
|
88 |
|
4790
|
89 |
fun tag tg (x, (thm, tags)) = (x, (thm, tg ins tags));
|
|
90 |
fun untag tg (x, (thm, tags)) = (x, (thm, tags \ tg));
|
4780
|
91 |
|
|
92 |
val lemma = ("lemma", []);
|
|
93 |
val assumption = ("assumption", []);
|
|
94 |
fun tag_lemma x = tag lemma x;
|
|
95 |
fun tag_assumption x = tag assumption x;
|
|
96 |
|
|
97 |
|
|
98 |
end;
|
|
99 |
|
|
100 |
|
|
101 |
structure BasicAttribute: BASIC_ATTRIBUTE = Attribute;
|
|
102 |
open BasicAttribute;
|