equal
deleted
inserted
replaced
18 exception DUP of key |
18 exception DUP of key |
19 exception SAME |
19 exception SAME |
20 exception UNDEF of key |
20 exception UNDEF of key |
21 val empty: 'a table |
21 val empty: 'a table |
22 val is_empty: 'a table -> bool |
22 val is_empty: 'a table -> bool |
|
23 val is_single: 'a table -> bool |
23 val map: (key -> 'a -> 'b) -> 'a table -> 'b table |
24 val map: (key -> 'a -> 'b) -> 'a table -> 'b table |
24 val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a |
25 val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a |
25 val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a |
26 val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a |
26 val dest: 'a table -> (key * 'a) list |
27 val dest: 'a table -> (key * 'a) list |
27 val keys: 'a table -> key list |
28 val keys: 'a table -> key list |
75 Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table; |
76 Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table; |
76 |
77 |
77 exception DUP of key; |
78 exception DUP of key; |
78 |
79 |
79 |
80 |
80 (* empty *) |
81 (* empty and single *) |
81 |
82 |
82 val empty = Empty; |
83 val empty = Empty; |
83 |
84 |
84 fun is_empty Empty = true |
85 fun is_empty Empty = true |
85 | is_empty _ = false; |
86 | is_empty _ = false; |
|
87 |
|
88 fun is_single (Branch2 (Empty, _, Empty)) = true |
|
89 | is_single _ = false; |
86 |
90 |
87 |
91 |
88 (* map and fold combinators *) |
92 (* map and fold combinators *) |
89 |
93 |
90 fun map_table f = |
94 fun map_table f = |