6118
|
1 |
(* Title: Pure/General/table.ML
|
5015
|
2 |
ID: $Id$
|
15014
|
3 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
|
5015
|
4 |
|
8806
|
5 |
Generic tables and tables indexed by strings. Efficient purely
|
15014
|
6 |
functional implementation using balanced 2-3 trees.
|
5015
|
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
|
15014
|
21 |
exception UNDEF of key
|
5015
|
22 |
val empty: 'a table
|
|
23 |
val is_empty: 'a table -> bool
|
5681
|
24 |
val map: ('a -> 'b) -> 'a table -> 'b table
|
|
25 |
val foldl: ('a * (key * 'b) -> 'a) -> 'a * 'b table -> 'a
|
5015
|
26 |
val dest: 'a table -> (key * 'a) list
|
5681
|
27 |
val keys: 'a table -> key list
|
8409
|
28 |
val min_key: 'a table -> key option
|
15160
|
29 |
val max_key: 'a table -> key option
|
7061
|
30 |
val exists: (key * 'a -> bool) -> 'a table -> bool
|
16192
|
31 |
val forall: (key * 'a -> bool) -> 'a table -> bool
|
5015
|
32 |
val lookup: 'a table * key -> 'a option
|
|
33 |
val update: (key * 'a) * 'a table -> 'a table
|
12287
|
34 |
val update_new: (key * 'a) * 'a table -> 'a table (*exception DUP*)
|
15665
|
35 |
val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
|
12287
|
36 |
val make: (key * 'a) list -> 'a table (*exception DUPS*)
|
|
37 |
val extend: 'a table * (key * 'a) list -> 'a table (*exception DUPS*)
|
|
38 |
val join: ('a * 'a -> 'a option) -> 'a table * 'a table -> 'a table (*exception DUPS*)
|
|
39 |
val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUPS*)
|
15665
|
40 |
val delete: key -> 'a table -> 'a table (*exception UNDEF*)
|
15761
|
41 |
val delete_safe: key -> 'a table -> 'a table
|
|
42 |
val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table (*exception DUP*)
|
16139
|
43 |
val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table
|
5015
|
44 |
val lookup_multi: 'a list table * key -> 'a list
|
8606
|
45 |
val update_multi: (key * 'a) * 'a list table -> 'a list table
|
16139
|
46 |
val remove_multi: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table
|
5015
|
47 |
val make_multi: (key * 'a) list -> 'a list table
|
|
48 |
val dest_multi: 'a list table -> (key * 'a) list
|
12287
|
49 |
val merge_multi: ('a * 'a -> bool) ->
|
15761
|
50 |
'a list table * 'a list table -> 'a list table (*exception DUPS*)
|
12287
|
51 |
val merge_multi': ('a * 'a -> bool) ->
|
15761
|
52 |
'a list table * 'a list table -> 'a list table (*exception DUPS*)
|
5015
|
53 |
end;
|
|
54 |
|
|
55 |
functor TableFun(Key: KEY): TABLE =
|
|
56 |
struct
|
|
57 |
|
|
58 |
|
|
59 |
(* datatype table *)
|
|
60 |
|
|
61 |
type key = Key.key;
|
|
62 |
|
|
63 |
datatype 'a table =
|
|
64 |
Empty |
|
|
65 |
Branch2 of 'a table * (key * 'a) * 'a table |
|
|
66 |
Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
|
|
67 |
|
|
68 |
exception DUP of key;
|
|
69 |
exception DUPS of key list;
|
|
70 |
|
|
71 |
|
5681
|
72 |
(* empty *)
|
|
73 |
|
5015
|
74 |
val empty = Empty;
|
|
75 |
|
|
76 |
fun is_empty Empty = true
|
|
77 |
| is_empty _ = false;
|
|
78 |
|
5681
|
79 |
|
|
80 |
(* map and fold combinators *)
|
|
81 |
|
|
82 |
fun map_table _ Empty = Empty
|
|
83 |
| map_table f (Branch2 (left, (k, x), right)) =
|
|
84 |
Branch2 (map_table f left, (k, f x), map_table f right)
|
|
85 |
| map_table f (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
|
|
86 |
Branch3 (map_table f left, (k1, f x1), map_table f mid, (k2, f x2), map_table f right);
|
|
87 |
|
|
88 |
fun foldl_table _ (x, Empty) = x
|
|
89 |
| foldl_table f (x, Branch2 (left, p, right)) =
|
|
90 |
foldl_table f (f (foldl_table f (x, left), p), right)
|
|
91 |
| foldl_table f (x, Branch3 (left, p1, mid, p2, right)) =
|
|
92 |
foldl_table f (f (foldl_table f (f (foldl_table f (x, left), p1), mid), p2), right);
|
|
93 |
|
|
94 |
fun dest tab = rev (foldl_table (fn (rev_ps, p) => p :: rev_ps) ([], tab));
|
|
95 |
fun keys tab = rev (foldl_table (fn (rev_ks, (k, _)) => k :: rev_ks) ([], tab));
|
16192
|
96 |
|
|
97 |
local exception TRUE in
|
|
98 |
|
|
99 |
fun exists pred tab =
|
|
100 |
(foldl_table (fn ((), e) => if pred e then raise TRUE else ()) ((), tab); false)
|
|
101 |
handle TRUE => true;
|
|
102 |
|
|
103 |
fun forall pred = not o exists (not o pred);
|
|
104 |
|
|
105 |
end;
|
5015
|
106 |
|
15531
|
107 |
fun min_key Empty = NONE
|
16002
|
108 |
| min_key (Branch2 (left, (k, _), _)) = SOME (if_none (min_key left) k)
|
|
109 |
| min_key (Branch3 (left, (k, _), _, _, _)) = SOME (if_none (min_key left) k);
|
8409
|
110 |
|
15531
|
111 |
fun max_key Empty = NONE
|
16002
|
112 |
| max_key (Branch2 (_, (k, _), right)) = SOME (if_none (max_key right) k)
|
|
113 |
| max_key (Branch3 (_, _, _, (k,_), right)) = SOME (if_none (max_key right) k);
|
15665
|
114 |
|
5015
|
115 |
|
|
116 |
(* lookup *)
|
|
117 |
|
15531
|
118 |
fun lookup (Empty, _) = NONE
|
5015
|
119 |
| lookup (Branch2 (left, (k, x), right), key) =
|
|
120 |
(case Key.ord (key, k) of
|
|
121 |
LESS => lookup (left, key)
|
15531
|
122 |
| EQUAL => SOME x
|
5015
|
123 |
| GREATER => lookup (right, key))
|
|
124 |
| lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right), key) =
|
|
125 |
(case Key.ord (key, k1) of
|
|
126 |
LESS => lookup (left, key)
|
15531
|
127 |
| EQUAL => SOME x1
|
5015
|
128 |
| GREATER =>
|
|
129 |
(case Key.ord (key, k2) of
|
|
130 |
LESS => lookup (mid, key)
|
15531
|
131 |
| EQUAL => SOME x2
|
5015
|
132 |
| GREATER => lookup (right, key)));
|
|
133 |
|
|
134 |
|
15665
|
135 |
(* updates *)
|
5015
|
136 |
|
|
137 |
datatype 'a growth =
|
|
138 |
Stay of 'a table |
|
|
139 |
Sprout of 'a table * (key * 'a) * 'a table;
|
|
140 |
|
15761
|
141 |
exception SAME;
|
|
142 |
|
15665
|
143 |
fun modify key f tab =
|
|
144 |
let
|
|
145 |
fun modfy Empty = Sprout (Empty, (key, f NONE), Empty)
|
|
146 |
| modfy (Branch2 (left, p as (k, x), right)) =
|
|
147 |
(case Key.ord (key, k) of
|
|
148 |
LESS =>
|
|
149 |
(case modfy left of
|
|
150 |
Stay left' => Stay (Branch2 (left', p, right))
|
|
151 |
| Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right)))
|
|
152 |
| EQUAL => Stay (Branch2 (left, (k, f (SOME x)), right))
|
|
153 |
| GREATER =>
|
|
154 |
(case modfy right of
|
|
155 |
Stay right' => Stay (Branch2 (left, p, right'))
|
|
156 |
| Sprout (right1, q, right2) =>
|
|
157 |
Stay (Branch3 (left, p, right1, q, right2))))
|
|
158 |
| modfy (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) =
|
|
159 |
(case Key.ord (key, k1) of
|
5015
|
160 |
LESS =>
|
15665
|
161 |
(case modfy left of
|
|
162 |
Stay left' => Stay (Branch3 (left', p1, mid, p2, right))
|
|
163 |
| Sprout (left1, q, left2) =>
|
|
164 |
Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right)))
|
|
165 |
| EQUAL => Stay (Branch3 (left, (k1, f (SOME x1)), mid, p2, right))
|
5015
|
166 |
| GREATER =>
|
15665
|
167 |
(case Key.ord (key, k2) of
|
|
168 |
LESS =>
|
|
169 |
(case modfy mid of
|
|
170 |
Stay mid' => Stay (Branch3 (left, p1, mid', p2, right))
|
|
171 |
| Sprout (mid1, q, mid2) =>
|
|
172 |
Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right)))
|
|
173 |
| EQUAL => Stay (Branch3 (left, p1, mid, (k2, f (SOME x2)), right))
|
|
174 |
| GREATER =>
|
|
175 |
(case modfy right of
|
|
176 |
Stay right' => Stay (Branch3 (left, p1, mid, p2, right'))
|
|
177 |
| Sprout (right1, q, right2) =>
|
|
178 |
Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2)))));
|
5015
|
179 |
|
15665
|
180 |
in
|
|
181 |
(case modfy tab of
|
|
182 |
Stay tab' => tab'
|
|
183 |
| Sprout br => Branch2 br)
|
|
184 |
handle SAME => tab
|
|
185 |
end;
|
5015
|
186 |
|
15761
|
187 |
fun update ((key, x), tab) = modify key (fn _ => x) tab;
|
|
188 |
fun update_new ((key, x), tab) = modify key (fn NONE => x | SOME _ => raise DUP key) tab;
|
|
189 |
fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x);
|
5015
|
190 |
|
|
191 |
|
12287
|
192 |
(* extend and make *)
|
5015
|
193 |
|
15761
|
194 |
fun extend (table, args) =
|
12287
|
195 |
let
|
15761
|
196 |
fun add (key, x) (tab, dups) =
|
16002
|
197 |
if is_some (lookup (tab, key)) then (tab, key :: dups)
|
15761
|
198 |
else (update ((key, x), tab), dups);
|
12287
|
199 |
in
|
15761
|
200 |
(case fold add args (table, []) of
|
12287
|
201 |
(table', []) => table'
|
|
202 |
| (_, dups) => raise DUPS (rev dups))
|
|
203 |
end;
|
|
204 |
|
|
205 |
fun make pairs = extend (empty, pairs);
|
|
206 |
|
5015
|
207 |
|
15014
|
208 |
(* delete *)
|
|
209 |
|
15665
|
210 |
exception UNDEF of key;
|
|
211 |
|
|
212 |
local
|
|
213 |
|
|
214 |
fun compare NONE (k2, _) = LESS
|
|
215 |
| compare (SOME k1) (k2, _) = Key.ord (k1, k2);
|
15014
|
216 |
|
|
217 |
fun if_eq EQUAL x y = x
|
|
218 |
| if_eq _ x y = y;
|
|
219 |
|
15531
|
220 |
fun del (SOME k) Empty = raise UNDEF k
|
|
221 |
| del NONE (Branch2 (Empty, p, Empty)) = (p, (true, Empty))
|
|
222 |
| del NONE (Branch3 (Empty, p, Empty, q, Empty)) =
|
15014
|
223 |
(p, (false, Branch2 (Empty, q, Empty)))
|
15665
|
224 |
| del k (Branch2 (Empty, p, Empty)) = (case compare k p of
|
16002
|
225 |
EQUAL => (p, (true, Empty)) | _ => raise UNDEF (the k))
|
15665
|
226 |
| del k (Branch3 (Empty, p, Empty, q, Empty)) = (case compare k p of
|
15014
|
227 |
EQUAL => (p, (false, Branch2 (Empty, q, Empty)))
|
15665
|
228 |
| _ => (case compare k q of
|
15014
|
229 |
EQUAL => (q, (false, Branch2 (Empty, p, Empty)))
|
16002
|
230 |
| _ => raise UNDEF (the k)))
|
15665
|
231 |
| del k (Branch2 (l, p, r)) = (case compare k p of
|
15014
|
232 |
LESS => (case del k l of
|
|
233 |
(p', (false, l')) => (p', (false, Branch2 (l', p, r)))
|
|
234 |
| (p', (true, l')) => (p', case r of
|
|
235 |
Branch2 (rl, rp, rr) =>
|
|
236 |
(true, Branch3 (l', p, rl, rp, rr))
|
|
237 |
| Branch3 (rl, rp, rm, rq, rr) => (false, Branch2
|
|
238 |
(Branch2 (l', p, rl), rp, Branch2 (rm, rq, rr)))))
|
15531
|
239 |
| ord => (case del (if_eq ord NONE k) r of
|
15014
|
240 |
(p', (false, r')) => (p', (false, Branch2 (l, if_eq ord p' p, r')))
|
|
241 |
| (p', (true, r')) => (p', case l of
|
|
242 |
Branch2 (ll, lp, lr) =>
|
|
243 |
(true, Branch3 (ll, lp, lr, if_eq ord p' p, r'))
|
|
244 |
| Branch3 (ll, lp, lm, lq, lr) => (false, Branch2
|
|
245 |
(Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r'))))))
|
15665
|
246 |
| del k (Branch3 (l, p, m, q, r)) = (case compare k q of
|
|
247 |
LESS => (case compare k p of
|
15014
|
248 |
LESS => (case del k l of
|
|
249 |
(p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r)))
|
|
250 |
| (p', (true, l')) => (p', (false, case (m, r) of
|
|
251 |
(Branch2 (ml, mp, mr), Branch2 _) =>
|
|
252 |
Branch2 (Branch3 (l', p, ml, mp, mr), q, r)
|
|
253 |
| (Branch3 (ml, mp, mm, mq, mr), _) =>
|
|
254 |
Branch3 (Branch2 (l', p, ml), mp, Branch2 (mm, mq, mr), q, r)
|
|
255 |
| (Branch2 (ml, mp, mr), Branch3 (rl, rp, rm, rq, rr)) =>
|
|
256 |
Branch3 (Branch2 (l', p, ml), mp, Branch2 (mr, q, rl), rp,
|
|
257 |
Branch2 (rm, rq, rr)))))
|
15531
|
258 |
| ord => (case del (if_eq ord NONE k) m of
|
15014
|
259 |
(p', (false, m')) =>
|
|
260 |
(p', (false, Branch3 (l, if_eq ord p' p, m', q, r)))
|
|
261 |
| (p', (true, m')) => (p', (false, case (l, r) of
|
|
262 |
(Branch2 (ll, lp, lr), Branch2 _) =>
|
|
263 |
Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r)
|
|
264 |
| (Branch3 (ll, lp, lm, lq, lr), _) =>
|
|
265 |
Branch3 (Branch2 (ll, lp, lm), lq,
|
|
266 |
Branch2 (lr, if_eq ord p' p, m'), q, r)
|
|
267 |
| (_, Branch3 (rl, rp, rm, rq, rr)) =>
|
|
268 |
Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp,
|
|
269 |
Branch2 (rm, rq, rr))))))
|
15531
|
270 |
| ord => (case del (if_eq ord NONE k) r of
|
15014
|
271 |
(q', (false, r')) =>
|
|
272 |
(q', (false, Branch3 (l, p, m, if_eq ord q' q, r')))
|
|
273 |
| (q', (true, r')) => (q', (false, case (l, m) of
|
|
274 |
(Branch2 _, Branch2 (ml, mp, mr)) =>
|
|
275 |
Branch2 (l, p, Branch3 (ml, mp, mr, if_eq ord q' q, r'))
|
|
276 |
| (_, Branch3 (ml, mp, mm, mq, mr)) =>
|
|
277 |
Branch3 (l, p, Branch2 (ml, mp, mm), mq,
|
|
278 |
Branch2 (mr, if_eq ord q' q, r'))
|
|
279 |
| (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) =>
|
|
280 |
Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp,
|
|
281 |
Branch2 (mr, if_eq ord q' q, r'))))));
|
|
282 |
|
15665
|
283 |
in
|
|
284 |
|
15761
|
285 |
fun delete key tab = snd (snd (del (SOME key) tab));
|
|
286 |
fun delete_safe key tab = delete key tab handle UNDEF _ => tab;
|
15014
|
287 |
|
15665
|
288 |
end;
|
|
289 |
|
15014
|
290 |
|
15761
|
291 |
(* insert and remove *)
|
|
292 |
|
|
293 |
fun insert eq (key, x) =
|
|
294 |
modify key (fn NONE => x | SOME y => if eq (x, y) then raise SAME else raise DUP key);
|
|
295 |
|
|
296 |
fun remove eq (key, x) tab =
|
|
297 |
(case lookup (tab, key) of
|
|
298 |
NONE => tab
|
|
299 |
| SOME y => if eq (x, y) then delete key tab else tab);
|
|
300 |
|
|
301 |
|
12287
|
302 |
(* join and merge *)
|
5015
|
303 |
|
12287
|
304 |
fun join f (table1, table2) =
|
|
305 |
let
|
|
306 |
fun add ((tab, dups), (key, x)) =
|
|
307 |
(case lookup (tab, key) of
|
15531
|
308 |
NONE => (update ((key, x), tab), dups)
|
|
309 |
| SOME y =>
|
12287
|
310 |
(case f (y, x) of
|
15531
|
311 |
SOME z => (update ((key, z), tab), dups)
|
|
312 |
| NONE => (tab, key :: dups)));
|
12287
|
313 |
in
|
|
314 |
(case foldl_table add ((table1, []), table2) of
|
|
315 |
(table', []) => table'
|
|
316 |
| (_, dups) => raise DUPS (rev dups))
|
|
317 |
end;
|
|
318 |
|
15531
|
319 |
fun merge eq tabs = join (fn (y, x) => if eq (y, x) then SOME y else NONE) tabs;
|
5015
|
320 |
|
|
321 |
|
15761
|
322 |
(* tables with multiple entries per key *)
|
|
323 |
|
16002
|
324 |
fun lookup_multi arg = if_none (lookup arg) [];
|
15761
|
325 |
|
|
326 |
fun update_multi ((key, x), tab) = modify key (fn NONE => [x] | SOME xs => x :: xs) tab;
|
5015
|
327 |
|
15761
|
328 |
fun remove_multi eq (key, x) tab =
|
|
329 |
map_entry key (fn xs => (case Library.remove eq x xs of [] => raise UNDEF key | ys => ys)) tab
|
|
330 |
handle UNDEF _ => delete key tab;
|
5015
|
331 |
|
15761
|
332 |
fun make_multi args = foldr update_multi empty args;
|
|
333 |
fun dest_multi tab = List.concat (map (fn (key, xs) => map (pair key) xs) (dest tab));
|
15531
|
334 |
fun merge_multi eq tabs = join (fn (xs, xs') => SOME (gen_merge_lists eq xs xs')) tabs;
|
|
335 |
fun merge_multi' eq tabs = join (fn (xs, xs') => SOME (gen_merge_lists' eq xs xs')) tabs;
|
5015
|
336 |
|
|
337 |
|
5681
|
338 |
(*final declarations of this structure!*)
|
|
339 |
val map = map_table;
|
|
340 |
val foldl = foldl_table;
|
5015
|
341 |
|
|
342 |
end;
|
|
343 |
|
|
344 |
|
|
345 |
(*tables indexed by strings*)
|
|
346 |
structure Symtab = TableFun(type key = string val ord = string_ord);
|