1 (* ========================================================================= *) |
1 (* ========================================================================= *) |
2 (* FINITE MAPS *) |
2 (* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *) |
3 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *) |
3 (* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *) |
4 (* ========================================================================= *) |
4 (* ========================================================================= *) |
5 |
5 |
6 signature Map = |
6 signature Map = |
7 sig |
7 sig |
8 |
8 |
9 (* ------------------------------------------------------------------------- *) |
9 (* ------------------------------------------------------------------------- *) |
10 (* Finite maps *) |
10 (* A type of finite maps. *) |
11 (* ------------------------------------------------------------------------- *) |
11 (* ------------------------------------------------------------------------- *) |
12 |
12 |
13 type ('key,'a) map |
13 type ('key,'a) map |
14 |
14 |
|
15 (* ------------------------------------------------------------------------- *) |
|
16 (* Constructors. *) |
|
17 (* ------------------------------------------------------------------------- *) |
|
18 |
15 val new : ('key * 'key -> order) -> ('key,'a) map |
19 val new : ('key * 'key -> order) -> ('key,'a) map |
|
20 |
|
21 val singleton : ('key * 'key -> order) -> 'key * 'a -> ('key,'a) map |
|
22 |
|
23 (* ------------------------------------------------------------------------- *) |
|
24 (* Map size. *) |
|
25 (* ------------------------------------------------------------------------- *) |
16 |
26 |
17 val null : ('key,'a) map -> bool |
27 val null : ('key,'a) map -> bool |
18 |
28 |
19 val size : ('key,'a) map -> int |
29 val size : ('key,'a) map -> int |
20 |
30 |
21 val singleton : ('key * 'key -> order) -> 'key * 'a -> ('key,'a) map |
31 (* ------------------------------------------------------------------------- *) |
|
32 (* Querying. *) |
|
33 (* ------------------------------------------------------------------------- *) |
22 |
34 |
23 val inDomain : 'key -> ('key,'a) map -> bool |
35 val peekKey : ('key,'a) map -> 'key -> ('key * 'a) option |
24 |
36 |
25 val peek : ('key,'a) map -> 'key -> 'a option |
37 val peek : ('key,'a) map -> 'key -> 'a option |
|
38 |
|
39 val get : ('key,'a) map -> 'key -> 'a (* raises Error *) |
|
40 |
|
41 val pick : ('key,'a) map -> 'key * 'a (* an arbitrary key/value pair *) |
|
42 |
|
43 val nth : ('key,'a) map -> int -> 'key * 'a (* in the range [0,size-1] *) |
|
44 |
|
45 val random : ('key,'a) map -> 'key * 'a |
|
46 |
|
47 (* ------------------------------------------------------------------------- *) |
|
48 (* Adding. *) |
|
49 (* ------------------------------------------------------------------------- *) |
26 |
50 |
27 val insert : ('key,'a) map -> 'key * 'a -> ('key,'a) map |
51 val insert : ('key,'a) map -> 'key * 'a -> ('key,'a) map |
28 |
52 |
29 val insertList : ('key,'a) map -> ('key * 'a) list -> ('key,'a) map |
53 val insertList : ('key,'a) map -> ('key * 'a) list -> ('key,'a) map |
30 |
54 |
31 val get : ('key,'a) map -> 'key -> 'a (* raises Error *) |
55 (* ------------------------------------------------------------------------- *) |
|
56 (* Removing. *) |
|
57 (* ------------------------------------------------------------------------- *) |
32 |
58 |
33 (* Union and intersect prefer keys in the second map *) |
59 val delete : ('key,'a) map -> 'key -> ('key,'a) map (* must be present *) |
|
60 |
|
61 val remove : ('key,'a) map -> 'key -> ('key,'a) map |
|
62 |
|
63 val deletePick : ('key,'a) map -> ('key * 'a) * ('key,'a) map |
|
64 |
|
65 val deleteNth : ('key,'a) map -> int -> ('key * 'a) * ('key,'a) map |
|
66 |
|
67 val deleteRandom : ('key,'a) map -> ('key * 'a) * ('key,'a) map |
|
68 |
|
69 (* ------------------------------------------------------------------------- *) |
|
70 (* Joining (all join operations prefer keys in the second map). *) |
|
71 (* ------------------------------------------------------------------------- *) |
|
72 |
|
73 val merge : |
|
74 {first : 'key * 'a -> 'c option, |
|
75 second : 'key * 'b -> 'c option, |
|
76 both : ('key * 'a) * ('key * 'b) -> 'c option} -> |
|
77 ('key,'a) map -> ('key,'b) map -> ('key,'c) map |
34 |
78 |
35 val union : |
79 val union : |
36 ('a * 'a -> 'a option) -> ('key,'a) map -> ('key,'a) map -> ('key,'a) map |
80 (('key * 'a) * ('key * 'a) -> 'a option) -> |
|
81 ('key,'a) map -> ('key,'a) map -> ('key,'a) map |
37 |
82 |
38 val intersect : |
83 val intersect : |
39 ('a * 'a -> 'a option) -> ('key,'a) map -> ('key,'a) map -> ('key,'a) map |
84 (('key * 'a) * ('key * 'b) -> 'c option) -> |
|
85 ('key,'a) map -> ('key,'b) map -> ('key,'c) map |
40 |
86 |
41 val delete : ('key,'a) map -> 'key -> ('key,'a) map (* raises Error *) |
87 (* ------------------------------------------------------------------------- *) |
|
88 (* Set operations on the domain. *) |
|
89 (* ------------------------------------------------------------------------- *) |
42 |
90 |
43 val difference : ('key,'a) map -> ('key,'b) map -> ('key,'a) map |
91 val inDomain : 'key -> ('key,'a) map -> bool |
|
92 |
|
93 val unionDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map |
|
94 |
|
95 val unionListDomain : ('key,'a) map list -> ('key,'a) map |
|
96 |
|
97 val intersectDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map |
|
98 |
|
99 val intersectListDomain : ('key,'a) map list -> ('key,'a) map |
|
100 |
|
101 val differenceDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map |
|
102 |
|
103 val symmetricDifferenceDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map |
|
104 |
|
105 val equalDomain : ('key,'a) map -> ('key,'a) map -> bool |
44 |
106 |
45 val subsetDomain : ('key,'a) map -> ('key,'a) map -> bool |
107 val subsetDomain : ('key,'a) map -> ('key,'a) map -> bool |
46 |
108 |
47 val equalDomain : ('key,'a) map -> ('key,'a) map -> bool |
109 val disjointDomain : ('key,'a) map -> ('key,'a) map -> bool |
|
110 |
|
111 (* ------------------------------------------------------------------------- *) |
|
112 (* Mapping and folding. *) |
|
113 (* ------------------------------------------------------------------------- *) |
48 |
114 |
49 val mapPartial : ('key * 'a -> 'b option) -> ('key,'a) map -> ('key,'b) map |
115 val mapPartial : ('key * 'a -> 'b option) -> ('key,'a) map -> ('key,'b) map |
50 |
|
51 val filter : ('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) map |
|
52 |
116 |
53 val map : ('key * 'a -> 'b) -> ('key,'a) map -> ('key,'b) map |
117 val map : ('key * 'a -> 'b) -> ('key,'a) map -> ('key,'b) map |
54 |
118 |
55 val app : ('key * 'a -> unit) -> ('key,'a) map -> unit |
119 val app : ('key * 'a -> unit) -> ('key,'a) map -> unit |
56 |
120 |
57 val transform : ('a -> 'b) -> ('key,'a) map -> ('key,'b) map |
121 val transform : ('a -> 'b) -> ('key,'a) map -> ('key,'b) map |
58 |
122 |
|
123 val filter : ('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) map |
|
124 |
|
125 val partition : |
|
126 ('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) map * ('key,'a) map |
|
127 |
59 val foldl : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's |
128 val foldl : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's |
60 |
129 |
61 val foldr : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's |
130 val foldr : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's |
|
131 |
|
132 (* ------------------------------------------------------------------------- *) |
|
133 (* Searching. *) |
|
134 (* ------------------------------------------------------------------------- *) |
62 |
135 |
63 val findl : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option |
136 val findl : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option |
64 |
137 |
65 val findr : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option |
138 val findr : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option |
66 |
139 |
70 |
143 |
71 val exists : ('key * 'a -> bool) -> ('key,'a) map -> bool |
144 val exists : ('key * 'a -> bool) -> ('key,'a) map -> bool |
72 |
145 |
73 val all : ('key * 'a -> bool) -> ('key,'a) map -> bool |
146 val all : ('key * 'a -> bool) -> ('key,'a) map -> bool |
74 |
147 |
75 val domain : ('key,'a) map -> 'key list |
148 val count : ('key * 'a -> bool) -> ('key,'a) map -> int |
|
149 |
|
150 (* ------------------------------------------------------------------------- *) |
|
151 (* Comparing. *) |
|
152 (* ------------------------------------------------------------------------- *) |
|
153 |
|
154 val compare : ('a * 'a -> order) -> ('key,'a) map * ('key,'a) map -> order |
|
155 |
|
156 val equal : ('a -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map -> bool |
|
157 |
|
158 (* ------------------------------------------------------------------------- *) |
|
159 (* Converting to and from lists. *) |
|
160 (* ------------------------------------------------------------------------- *) |
|
161 |
|
162 val keys : ('key,'a) map -> 'key list |
|
163 |
|
164 val values : ('key,'a) map -> 'a list |
76 |
165 |
77 val toList : ('key,'a) map -> ('key * 'a) list |
166 val toList : ('key,'a) map -> ('key * 'a) list |
78 |
167 |
79 val fromList : ('key * 'key -> order) -> ('key * 'a) list -> ('key,'a) map |
168 val fromList : ('key * 'key -> order) -> ('key * 'a) list -> ('key,'a) map |
80 |
169 |
81 val random : ('key,'a) map -> 'key * 'a (* raises Empty *) |
170 (* ------------------------------------------------------------------------- *) |
82 |
171 (* Pretty-printing. *) |
83 val compare : ('a * 'a -> order) -> ('key,'a) map * ('key,'a) map -> order |
172 (* ------------------------------------------------------------------------- *) |
84 |
|
85 val equal : ('a -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map -> bool |
|
86 |
173 |
87 val toString : ('key,'a) map -> string |
174 val toString : ('key,'a) map -> string |
88 |
175 |
89 (* ------------------------------------------------------------------------- *) |
176 (* ------------------------------------------------------------------------- *) |
90 (* Iterators over maps *) |
177 (* Iterators over maps. *) |
91 (* ------------------------------------------------------------------------- *) |
178 (* ------------------------------------------------------------------------- *) |
92 |
179 |
93 type ('key,'a) iterator |
180 type ('key,'a) iterator |
94 |
181 |
95 val mkIterator : ('key,'a) map -> ('key,'a) iterator option |
182 val mkIterator : ('key,'a) map -> ('key,'a) iterator option |