37 val update: (key * 'a) -> 'a table -> 'a table |
36 val update: (key * 'a) -> 'a table -> 'a table |
38 val update_new: (key * 'a) -> 'a table -> 'a table (*exception DUP*) |
37 val update_new: (key * 'a) -> 'a table -> 'a table (*exception DUP*) |
39 val default: key * 'a -> 'a table -> 'a table |
38 val default: key * 'a -> 'a table -> 'a table |
40 val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table |
39 val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table |
41 val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table |
40 val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table |
42 val make: (key * 'a) list -> 'a table (*exception DUPS*) |
41 val make: (key * 'a) list -> 'a table (*exception DUP*) |
43 val extend: 'a table * (key * 'a) list -> 'a table (*exception DUPS*) |
42 val extend: 'a table * (key * 'a) list -> 'a table (*exception DUP*) |
44 val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) -> |
43 val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) -> |
45 'a table * 'a table -> 'a table (*exception DUPS*) |
44 'a table * 'a table -> 'a table (*exception DUP*) |
46 val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUPS*) |
45 val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUP*) |
47 val delete: key -> 'a table -> 'a table (*exception UNDEF*) |
46 val delete: key -> 'a table -> 'a table (*exception UNDEF*) |
48 val delete_safe: key -> 'a table -> 'a table |
47 val delete_safe: key -> 'a table -> 'a table |
49 val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool |
48 val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool |
50 val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table (*exception DUP*) |
49 val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table (*exception DUP*) |
51 val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table |
50 val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table |
54 val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table |
53 val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table |
55 val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table |
54 val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table |
56 val make_list: (key * 'a) list -> 'a list table |
55 val make_list: (key * 'a) list -> 'a list table |
57 val dest_list: 'a list table -> (key * 'a) list |
56 val dest_list: 'a list table -> (key * 'a) list |
58 val merge_list: ('a * 'a -> bool) -> |
57 val merge_list: ('a * 'a -> bool) -> |
59 'a list table * 'a list table -> 'a list table (*exception DUPS*) |
58 'a list table * 'a list table -> 'a list table (*exception DUP*) |
60 end; |
59 end; |
61 |
60 |
62 functor TableFun(Key: KEY): TABLE = |
61 functor TableFun(Key: KEY): TABLE = |
63 struct |
62 struct |
64 |
63 |
348 | SOME y => if eq (x, y) then delete key tab else tab); |
346 | SOME y => if eq (x, y) then delete key tab else tab); |
349 |
347 |
350 |
348 |
351 (* simultaneous modifications *) |
349 (* simultaneous modifications *) |
352 |
350 |
353 fun reject_dups (tab, []) = tab |
351 fun extend (table, args) = fold update_new args table; |
354 | reject_dups (_, dups) = raise DUPS (rev dups); |
|
355 |
|
356 fun extend (table, args) = |
|
357 let |
|
358 fun add (key, x) (tab, dups) = |
|
359 (update_new (key, x) tab, dups) handle DUP dup => (tab, dup :: dups); |
|
360 in reject_dups (fold add args (table, [])) end; |
|
361 |
352 |
362 fun make entries = extend (empty, entries); |
353 fun make entries = extend (empty, entries); |
363 |
354 |
364 fun join f (table1, table2) = |
355 fun join f (table1, table2) = |
365 let |
356 let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab; |
366 fun add (key, y) (tab, dups) = |
357 in fold_table add table2 table1 end; |
367 let val tab' = modify key (fn NONE => y | SOME x => f key (x, y)) tab |
|
368 in (tab', dups) end handle DUP dup => (tab, dup :: dups); |
|
369 in reject_dups (fold_table add table2 (table1, [])) end; |
|
370 |
358 |
371 fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key); |
359 fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key); |
372 |
360 |
373 |
361 |
374 (* list tables *) |
362 (* list tables *) |