9 sig |
9 sig |
10 type key |
10 type key |
11 type 'a table |
11 type 'a table |
12 val empty: 'a table |
12 val empty: 'a table |
13 val build: ('a table -> 'a table) -> 'a table |
13 val build: ('a table -> 'a table) -> 'a table |
|
14 val size: 'a table -> int |
14 val is_empty: 'a table -> bool |
15 val is_empty: 'a table -> bool |
15 val map: (key -> 'a -> 'b) -> 'a table -> 'b table |
16 val map: (key -> 'a -> 'b) -> 'a table -> 'b table |
16 val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a |
17 val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a |
17 val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a |
18 val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a |
18 val size: 'a table -> int |
|
19 val dest: 'a table -> (key * 'a) list |
19 val dest: 'a table -> (key * 'a) list |
20 val keys: 'a table -> key list |
20 val keys: 'a table -> key list |
21 val exists: (key * 'a -> bool) -> 'a table -> bool |
21 val exists: (key * 'a -> bool) -> 'a table -> bool |
22 val forall: (key * 'a -> bool) -> 'a table -> bool |
22 val forall: (key * 'a -> bool) -> 'a table -> bool |
23 val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option |
23 val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option |
24 val lookup: 'a table -> key -> 'a option |
24 val lookup: 'a table -> key -> 'a option |
25 val defined: 'a table -> key -> bool |
25 val defined: 'a table -> key -> bool |
26 val add: key * 'a -> 'a table -> 'a table |
26 val add: key * 'a -> 'a table -> 'a table |
27 val make: (key * 'a) list -> 'a table |
27 val make: (key * 'a) list -> 'a table |
28 type set = unit table |
28 type set = int table |
29 val add_set: key -> set -> set |
29 val add_set: key -> set -> set |
30 val make_set: key list -> set |
30 val make_set: key list -> set |
|
31 val list_set: set -> key list |
|
32 val list_set_rev: set -> key list |
31 val subset: set * set -> bool |
33 val subset: set * set -> bool |
32 val eq_set: set * set -> bool |
34 val eq_set: set * set -> bool |
33 end; |
35 end; |
34 |
36 |
35 functor Items(Key: KEY): ITEMS = |
37 functor Items(Key: KEY): ITEMS = |
36 struct |
38 struct |
37 |
39 |
|
40 (* table with length *) |
|
41 |
38 structure Table = Table(Key); |
42 structure Table = Table(Key); |
39 |
43 |
40 type key = Table.key; |
44 type key = Table.key; |
41 type 'a table = 'a Table.table; |
45 datatype 'a table = Items of int * 'a Table.table; |
42 |
46 |
43 val empty = Table.empty; |
47 fun size (Items (n, _)) = n; |
44 val build = Table.build; |
48 fun table (Items (_, tab)) = tab; |
45 val is_empty = Table.is_empty; |
49 |
46 val size = Table.size; |
50 val empty = Items (0, Table.empty); |
47 val dest = Table.dest; |
51 fun build (f: 'a table -> 'a table) = f empty; |
48 val keys = Table.keys; |
52 fun is_empty items = size items = 0; |
49 val exists = Table.exists; |
53 |
50 val forall = Table.forall; |
54 fun dest items = Table.dest (table items); |
51 val get_first = Table.get_first; |
55 fun keys items = Table.keys (table items); |
52 val lookup = Table.lookup; |
56 fun exists pred = Table.exists pred o table; |
53 val defined = Table.defined; |
57 fun forall pred = Table.forall pred o table; |
54 |
58 fun get_first get = Table.get_first get o table; |
55 fun add entry = Table.insert (K true) entry; |
59 fun lookup items = Table.lookup (table items); |
56 fun make entries = Table.build (fold add entries); |
60 fun defined items = Table.defined (table items); |
57 |
61 |
58 type set = unit table; |
62 fun add (key, x) (items as Items (n, tab)) = |
59 |
63 if Table.defined tab key then items |
60 fun add_set x = add (x, ()); |
64 else Items (n + 1, Table.update_new (key, x) tab); |
|
65 |
|
66 fun make entries = build (fold add entries); |
|
67 |
|
68 |
|
69 (* set with order of addition *) |
|
70 |
|
71 type set = int table; |
|
72 |
|
73 fun add_set x (items as Items (n, tab)) = |
|
74 if Table.defined tab x then items |
|
75 else Items (n + 1, Table.update_new (x, n) tab); |
|
76 |
61 fun make_set xs = build (fold add_set xs); |
77 fun make_set xs = build (fold add_set xs); |
62 |
78 |
63 fun subset (A: set, B: set) = forall (defined B o #1) A; |
79 fun subset (A: set, B: set) = forall (defined B o #1) A; |
64 fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B); |
80 fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B); |
65 |
81 |
66 val map = Table.map; |
82 fun list_set_ord ord items = Table.dest (table items) |> sort (ord o apply2 #2) |> map #1 |
67 val fold = Table.fold; |
83 val list_set = list_set_ord int_ord; |
68 val fold_rev = Table.fold_rev; |
84 val list_set_rev = list_set_ord (rev_order o int_ord); |
|
85 |
|
86 fun map f (Items (n, tab)) = Items (n, Table.map f tab); |
|
87 fun fold f = Table.fold f o table; |
|
88 fun fold_rev f = Table.fold_rev f o table; |
69 |
89 |
70 end; |
90 end; |
71 |
91 |
72 signature BASIC_TERM_ORD = |
92 signature BASIC_TERM_ORD = |
73 sig |
93 sig |