13 val ord: T ord |
13 val ord: T ord |
14 structure Set: SET |
14 structure Set: SET |
15 structure Table: TABLE |
15 structure Table: TABLE |
16 val empty: T |
16 val empty: T |
17 val is_empty: T -> bool |
17 val is_empty: T -> bool |
18 val print: T -> string |
18 |
19 val short: T -> string |
|
20 type P = T * Position.T |
19 type P = T * Position.T |
21 val none: P |
20 val none: P |
22 val list: string * Position.T -> 'a list -> (P * 'a) list |
21 val list: string * Position.T -> 'a list -> (P * 'a) list |
23 val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list |
22 val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list |
|
23 |
|
24 val print: T -> string |
|
25 val short: T -> string |
24 end; |
26 end; |
25 |
27 |
26 structure Thm_Name: THM_NAME = |
28 structure Thm_Name: THM_NAME = |
27 struct |
29 struct |
|
30 |
|
31 (* type T *) |
28 |
32 |
29 type T = string * int; |
33 type T = string * int; |
30 val ord = prod_ord string_ord int_ord; |
34 val ord = prod_ord string_ord int_ord; |
31 |
35 |
32 structure Set = Set(type key = T val ord = ord); |
36 structure Set = Set(type key = T val ord = ord); |
33 structure Table = Table(Set.Key); |
37 structure Table = Table(Set.Key); |
34 |
38 |
35 val empty: T = ("", 0); |
39 val empty: T = ("", 0); |
36 fun is_empty ((a, _): T) = a = ""; |
40 fun is_empty ((a, _): T) = a = ""; |
37 |
41 |
38 fun print (name, index) = |
|
39 if name = "" orelse index = 0 then name |
|
40 else name ^ enclose "(" ")" (string_of_int index); |
|
41 |
42 |
42 fun short (name, index) = |
43 (* type P *) |
43 if name = "" orelse index = 0 then name |
|
44 else name ^ "_" ^ string_of_int index; |
|
45 |
|
46 |
44 |
47 type P = T * Position.T; |
45 type P = T * Position.T; |
48 |
46 |
49 val none: P = (empty, Position.none); |
47 val none: P = (empty, Position.none); |
50 |
48 |
52 | list ("", pos) xs = map (fn thm => ((empty, pos), thm)) xs |
50 | list ("", pos) xs = map (fn thm => ((empty, pos), thm)) xs |
53 | list (name, pos) xs = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) xs; |
51 | list (name, pos) xs = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) xs; |
54 |
52 |
55 fun expr name = burrow_fst (burrow (list name)); |
53 fun expr name = burrow_fst (burrow (list name)); |
56 |
54 |
|
55 |
|
56 (* output *) |
|
57 |
|
58 fun print (name, index) = |
|
59 if name = "" orelse index = 0 then name |
|
60 else name ^ enclose "(" ")" (string_of_int index); |
|
61 |
|
62 fun short (name, index) = |
|
63 if name = "" orelse index = 0 then name |
|
64 else name ^ "_" ^ string_of_int index; |
|
65 |
57 end; |
66 end; |