equal
deleted
inserted
replaced
55 val make_list: (key * 'a) list -> 'a list table |
55 val make_list: (key * 'a) list -> 'a list table |
56 val dest_list: 'a list table -> (key * 'a) list |
56 val dest_list: 'a list table -> (key * 'a) list |
57 val merge_list: ('a * 'a -> bool) -> 'a list table * 'a list table -> 'a list table |
57 val merge_list: ('a * 'a -> bool) -> 'a list table * 'a list table -> 'a list table |
58 type set = unit table |
58 type set = unit table |
59 val insert_set: key -> set -> set |
59 val insert_set: key -> set -> set |
|
60 val remove_set: key -> set -> set |
60 val make_set: key list -> set |
61 val make_set: key list -> set |
61 end; |
62 end; |
62 |
63 |
63 functor Table(Key: KEY): TABLE = |
64 functor Table(Key: KEY): TABLE = |
64 struct |
65 struct |
404 |
405 |
405 (* unit tables *) |
406 (* unit tables *) |
406 |
407 |
407 type set = unit table; |
408 type set = unit table; |
408 |
409 |
409 fun insert_set x = update (x, ()); |
410 fun insert_set x = default (x, ()); |
|
411 fun remove_set x : set -> set = delete_safe x; |
410 fun make_set entries = fold insert_set entries empty; |
412 fun make_set entries = fold insert_set entries empty; |
411 |
413 |
412 |
414 |
413 (* ML pretty-printing *) |
415 (* ML pretty-printing *) |
414 |
416 |