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