|
1 (* Title: Pure/table.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 Generic tables and tables indexed by strings. No delete operation. |
|
6 Implemented as balanced 2-3 trees. |
|
7 *) |
|
8 |
|
9 signature KEY = |
|
10 sig |
|
11 type key |
|
12 val ord: key * key -> order |
|
13 end; |
|
14 |
|
15 signature TABLE = |
|
16 sig |
|
17 type key |
|
18 type 'a table |
|
19 exception DUP of key |
|
20 exception DUPS of key list |
|
21 val empty: 'a table |
|
22 val is_empty: 'a table -> bool |
|
23 val dest: 'a table -> (key * 'a) list |
|
24 val lookup: 'a table * key -> 'a option |
|
25 val update: (key * 'a) * 'a table -> 'a table |
|
26 val update_new: (key * 'a) * 'a table -> 'a table (*exception DUP*) |
|
27 val make: (key * 'a) list -> 'a table (*exception DUPS*) |
|
28 val extend: 'a table * (key * 'a) list -> 'a table (*exception DUPS*) |
|
29 val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUPS*) |
|
30 val lookup_multi: 'a list table * key -> 'a list |
|
31 val make_multi: (key * 'a) list -> 'a list table |
|
32 val dest_multi: 'a list table -> (key * 'a) list |
|
33 val map: ('a -> 'b) -> 'a table -> 'b table |
|
34 end; |
|
35 |
|
36 functor TableFun(Key: KEY): TABLE = |
|
37 struct |
|
38 |
|
39 |
|
40 (* datatype table *) |
|
41 |
|
42 type key = Key.key; |
|
43 |
|
44 datatype 'a table = |
|
45 Empty | |
|
46 Branch2 of 'a table * (key * 'a) * 'a table | |
|
47 Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table; |
|
48 |
|
49 exception DUP of key; |
|
50 exception DUPS of key list; |
|
51 |
|
52 |
|
53 val empty = Empty; |
|
54 |
|
55 fun is_empty Empty = true |
|
56 | is_empty _ = false; |
|
57 |
|
58 fun dest Empty = [] |
|
59 | dest (Branch2 (left, p, right)) = dest left @ [p] @ dest right |
|
60 | dest (Branch3 (left, p1, mid, p2, right)) = |
|
61 dest left @ [p1] @ dest mid @ [p2] @ dest right; |
|
62 |
|
63 |
|
64 (* lookup *) |
|
65 |
|
66 fun lookup (Empty, _) = None |
|
67 | lookup (Branch2 (left, (k, x), right), key) = |
|
68 (case Key.ord (key, k) of |
|
69 LESS => lookup (left, key) |
|
70 | EQUAL => Some x |
|
71 | GREATER => lookup (right, key)) |
|
72 | lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right), key) = |
|
73 (case Key.ord (key, k1) of |
|
74 LESS => lookup (left, key) |
|
75 | EQUAL => Some x1 |
|
76 | GREATER => |
|
77 (case Key.ord (key, k2) of |
|
78 LESS => lookup (mid, key) |
|
79 | EQUAL => Some x2 |
|
80 | GREATER => lookup (right, key))); |
|
81 |
|
82 |
|
83 (* update *) |
|
84 |
|
85 fun compare (k1, _) (k2, _) = Key.ord (k1, k2); |
|
86 |
|
87 datatype 'a growth = |
|
88 Stay of 'a table | |
|
89 Sprout of 'a table * (key * 'a) * 'a table; |
|
90 |
|
91 fun insert pair Empty = Sprout (Empty, pair, Empty) |
|
92 | insert pair (Branch2 (left, p, right)) = |
|
93 (case compare pair p of |
|
94 LESS => |
|
95 (case insert pair left of |
|
96 Stay left' => Stay (Branch2 (left', p, right)) |
|
97 | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right))) |
|
98 | EQUAL => Stay (Branch2 (left, pair, right)) |
|
99 | GREATER => |
|
100 (case insert pair right of |
|
101 Stay right' => Stay (Branch2 (left, p, right')) |
|
102 | Sprout (right1, q, right2) => |
|
103 Stay (Branch3 (left, p, right1, q, right2)))) |
|
104 | insert pair (Branch3 (left, p1, mid, p2, right)) = |
|
105 (case compare pair p1 of |
|
106 LESS => |
|
107 (case insert pair left of |
|
108 Stay left' => Stay (Branch3 (left', p1, mid, p2, right)) |
|
109 | Sprout (left1, q, left2) => |
|
110 Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right))) |
|
111 | EQUAL => Stay (Branch3 (left, pair, mid, p2, right)) |
|
112 | GREATER => |
|
113 (case compare pair p2 of |
|
114 LESS => |
|
115 (case insert pair mid of |
|
116 Stay mid' => Stay (Branch3 (left, p1, mid', p2, right)) |
|
117 | Sprout (mid1, q, mid2) => |
|
118 Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right))) |
|
119 | EQUAL => Stay (Branch3 (left, p1, mid, pair, right)) |
|
120 | GREATER => |
|
121 (case insert pair right of |
|
122 Stay right' => Stay (Branch3 (left, p1, mid, p2, right')) |
|
123 | Sprout (right1, q, right2) => |
|
124 Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2))))); |
|
125 |
|
126 fun update (pair, tab) = |
|
127 (case insert pair tab of |
|
128 Stay tab => tab |
|
129 | Sprout br => Branch2 br); |
|
130 |
|
131 fun update_new (pair as (key, _), tab) = |
|
132 if is_none (lookup (tab, key)) then update (pair, tab) |
|
133 else raise DUP key; |
|
134 |
|
135 |
|
136 (* make, extend, merge tables *) |
|
137 |
|
138 fun add eq ((tab, dups), (key, x)) = |
|
139 (case lookup (tab, key) of |
|
140 None => (update ((key, x), tab), dups) |
|
141 | Some x' => |
|
142 if eq (x, x') then (tab, dups) |
|
143 else (tab, dups @ [key])); |
|
144 |
|
145 fun enter eq (tab, pairs) = |
|
146 (case foldl (add eq) ((tab, []), pairs) of |
|
147 (tab', []) => tab' |
|
148 | (_, dups) => raise DUPS dups); |
|
149 |
|
150 fun extend tab_pairs = enter (K false) tab_pairs; |
|
151 fun make pairs = extend (empty, pairs); |
|
152 fun merge eq (tab1, tab2) = enter eq (tab1, dest tab2); |
|
153 |
|
154 |
|
155 (* tables with multiple entries per key (preserving order) *) |
|
156 |
|
157 fun lookup_multi tab_key = if_none (lookup tab_key) []; |
|
158 |
|
159 fun cons_entry ((key, x), tab) = |
|
160 update ((key, x :: lookup_multi (tab, key)), tab); |
|
161 |
|
162 fun make_multi pairs = foldr cons_entry (pairs, empty); |
|
163 |
|
164 fun dest_multi tab = |
|
165 flat (map (fn (key, xs) => map (Library.pair key) xs) (dest tab)); |
|
166 |
|
167 |
|
168 (* map *) |
|
169 |
|
170 fun map _ Empty = Empty |
|
171 | map f (Branch2 (left, (k, x), right)) = |
|
172 Branch2 (map f left, (k, f x), map f right) |
|
173 | map f (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = |
|
174 Branch3 (map f left, (k1, f x1), map f mid, (k2, f x2), map f right); |
|
175 |
|
176 |
|
177 end; |
|
178 |
|
179 |
|
180 (*tables indexed by strings*) |
|
181 structure Symtab = TableFun(type key = string val ord = string_ord); |