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