Map.dcl 13.4 KB
Newer Older
1
definition module Data.Map
2

3
/**
Camil Staps's avatar
Camil Staps committed
4 5 6
 * This module provides a dynamic Map type for creating mappings from keys to values
 * Internally it uses an AVL tree to organize the key-value pairs stored in the mapping
 * such that lookup, insert and delete operations can be performed in O(log n).
Camil Staps's avatar
Camil Staps committed
7 8
 *
 * @property-bootstrap
9
 *   import StdBool, StdChar, StdInt, StdTuple
Camil Staps's avatar
Camil Staps committed
10 11
 *   from StdList import all, isMember, removeDup, reverse, instance length []
 *   from Data.Func import on, `on`
12
 *   import Data.GenDefault
Camil Staps's avatar
Camil Staps committed
13 14
 *   from Data.List import nubBy
 *
15 16 17 18 19 20
 *   :: Predicate a = ConstTrue | IsMember [a]
 *
 *   pred :: (Predicate a) a -> Bool | Eq a
 *   pred ConstTrue     _ = True
 *   pred (IsMember cs) c = isMember c cs
 *
Camil Staps's avatar
Camil Staps committed
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
 *   :: GMap k v =
 *     { gma  :: !v
 *     , gmb  :: !v
 *     , gmc  :: !v
 *     , gmd  :: !v
 *     , gme  :: !v
 *     , gmf  :: !v
 *     , rest :: ![(k,v)]
 *     }
 *
 *   class Key k
 *   where keya :: k; keyb :: k; keyc :: k; keyd :: k; keye :: k; keyf :: k
 *
 *   instance Key Char
 *   where keya = 'a'; keyb = 'b'; keyc = 'c'; keyd = 'd'; keye = 'e'; keyf = 'f'
 *
37 38
 *   derive class Gast GMap, Predicate
 *   derive genShow Map, Maybe
39
 *   derive gPrint Map, Maybe
Camil Staps's avatar
Camil Staps committed
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62
 *
 *   kvs :: (GMap k v) -> [(k,v)] | Key k
 *   kvs gm =
 *     [ (keya,gm.gma)
 *     , (keyb,gm.gmb)
 *     , (keyc,gm.gmc)
 *     , (keyd,gm.gmd)
 *     , (keye,gm.gme)
 *     , (keyf,gm.gmf)
 *     : gm.rest
 *     ]
 *
 *   all_present :: [(k,v)] (Map k v) -> Bool | <, == k & == v
 *   all_present kvs m = all (\(k,v) -> get k m == Just v) kvs`
 *   where
 *     kvs` = nubBy ((==) `on` fst) (reverse kvs) // Remove duplicate keys, assuming the last takes precedence
 *
 *   all_from :: (Map k v) [(k,v)] -> Bool | Eq k & Eq v
 *   all_from Tip _ = True
 *   all_from (Bin _ k v l r) kvs = isMember (k,v) kvs && all_from l kvs && all_from r kvs
 *
 * @property-test-with k = Char
 * @property-test-with v = Char
63 64 65
 *
 * @property-test-generator (GMap k v) -> Map k v | Key, <, == k
 *   gen gm = fromList (kvs gm)
Camil Staps's avatar
Camil Staps committed
66
 */
67

68
from Data.Maybe		import :: Maybe (..)
69
from StdOverloaded	import class ==, class <
70 71
from StdBool        import not
from StdFunc        import id
Camil Staps's avatar
Camil Staps committed
72 73
from Data.GenEq import generic gEq
from Data.GenLexOrd import generic gLexOrd, :: LexOrd
74
from Data.Monoid    import class Monoid, class Semigroup
Mart Lubbers's avatar
Mart Lubbers committed
75
import qualified StdList
76
from Data.Functor import class Functor (..)
77
from Data.Set import :: Set
78
from StdOverloaded import class < (..)
79
import StdClass
80 81

/**
Camil Staps's avatar
Camil Staps committed
82 83 84 85 86
 * The abstract Map type provides the mapping.
 * For example "Map Int String" is a mapping "from" integers "to" strings.
 *
 * @var The key type on which the data structure is indexed.
 * @var The type of the values stored in the mapping.
87 88 89 90
 *
 * @invariant integrity: A.m :: Map k v:
 *   log_size m /\
 *   sizes_correct m
91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107
 *
 * @invariant log_size: A.m :: Map k v:
 *   check (<) nelem (2 ^ depth m)
 *   where
 *     nelem = mapSize m
 *
 *     depth :: (Map a b) -> Int
 *     depth Tip = 0
 *     depth (Bin _ _ _ l r) = 1 + (max `on` depth) l r
 *
 * @invariant sizes_correct: A.m :: Map k v:
 *   case m of
 *     Tip                -> prop True
 *     b=:(Bin _ _ _ l r) ->
 *       mapSize b =.= 1 + mapSize l + mapSize r /\
 *       sizes_correct l /\
 *       sizes_correct r
Camil Staps's avatar
Camil Staps committed
108 109 110
 */
:: Map k v
  = Bin !Int !k !v !(Map k v) !(Map k v)
111 112 113
  | Tip

instance Monoid (Map k v) | < k
114
instance Semigroup (Map k v) | < k
115

116 117
instance == (Map k v) | Eq k  & Eq v
instance <  (Map k v) | Ord k & Ord v
Jurriën Stutterheim's avatar
Jurriën Stutterheim committed
118

119 120
//Basic functions

Camil Staps's avatar
Camil Staps committed
121 122 123
/**
 * Check if a Map is empty.
 * @type (Map k a) -> Bool
124 125 126 127
 * @property equivalence with size 0: A.m :: Map k v:
 *   mapSize m == 0 <==> null m
 * @property equivalence with newMap: A.m :: Map k v:
 *   m == newMap <==> null m
128
 * @complexity O(1)
Camil Staps's avatar
Camil Staps committed
129
 */
130 131 132
null mp :== case mp of
              Tip -> True
              _   -> False
Jurriën Stutterheim's avatar
Jurriën Stutterheim committed
133

134
/**
Camil Staps's avatar
Camil Staps committed
135
 * Create an empty Map.
136
 * @result An empty map
137
 * @property is null:
138
 *   null newMap
139
 * @complexity O(1)
Camil Staps's avatar
Camil Staps committed
140
 */
141
newMap      :: w:(Map k u:v), [ w <= u]
142

Camil Staps's avatar
Camil Staps committed
143 144
/**
 * Create a Map with one element.
145
 * @complexity O(1)
Camil Staps's avatar
Camil Staps committed
146 147
 */
singleton   :: !k !v -> Map k v
148

Camil Staps's avatar
Camil Staps committed
149 150
/**
 * The number of elements in a Map.
151
 * @property correctness: A.m :: Map k v:
152
 *   mapSize m =.= length (removeDup (keys m))
Camil Staps's avatar
Camil Staps committed
153
 */
154
mapSize     :: !(Map k v) -> Int
Jurriën Stutterheim's avatar
Jurriën Stutterheim committed
155

156
/**
Camil Staps's avatar
Camil Staps committed
157 158 159 160 161
 * Adds or replaces the value for a given key.
 *
 * @param The key value to add/update
 * @param The value to add/update at the key position
 * @param The original mapping
162
 * @result The modified mapping with the added value
163
 * @property correctness: A.m :: Map k v; k :: k; v :: v:
Camil Staps's avatar
Camil Staps committed
164 165
 *   get k m` =.= Just v /\                                           // Correctly put
 *     check all_present [kv \\ kv=:(k`,_) <- toList m | k <> k`] m` /\ // Other elements untouched
166
 *     integrity m`
Camil Staps's avatar
Camil Staps committed
167 168
 *   where
 *     m` = put k v m
169
 * @complexity O(log n)
Camil Staps's avatar
Camil Staps committed
170
 */
171
put :: !k !a !(Map k a) -> Map k a | < k
172

Camil Staps's avatar
Camil Staps committed
173 174 175 176 177 178 179
/**
 * Searches for a value at a given key position. Works only for non-unique
 * mappings.
 *
 * @type k (Map k v) -> Maybe v | < k
 * @param The key to look for
 * @param The orginal mapping
180
 * @result When found, the value at the key position, if not: Nothing
181
 * @complexity O(log n)
Camil Staps's avatar
Camil Staps committed
182
 */
183 184 185 186 187 188 189 190
get k m :== get` k m
  where
  get` _ Tip              = Nothing
  get` k (Bin _ kx x l r) = if (k < kx)
                              (get` k l)
                              (if (k > kx)
                                 (get` k r)
                                 (Just x))
191

Camil Staps's avatar
Camil Staps committed
192 193 194
/**
 * Searches for a value at a given key position. Works also for unique mappings.
 */
195
getU :: !k !w:(Map k v) -> x:(!Maybe v, !y:(Map k v)) | == k & < k, [ x <= y, w <= y]
Camil Staps's avatar
Camil Staps committed
196

197
/**
Camil Staps's avatar
Camil Staps committed
198 199 200 201
 * Removes the value at a given key position. The mapping itself can be spine unique.
 *
 * @param The key to remove
 * @param The original mapping
202
 * @result The modified mapping with the value/key removed
203
 * @property correctness: A.m :: Map k v; k :: k:
Camil Staps's avatar
Camil Staps committed
204 205
 *   get k m` =.= Nothing /\                                            // Correctly deleted
 *     check all_present [kv \\ kv=:(k`,_) <- toList m | k <> k`] m` /\ // Other elements untouched
206
 *     integrity m`
Camil Staps's avatar
Camil Staps committed
207 208 209
 *   where
 *     m` = del k m
 */
210
del :: !k !(Map k a) -> Map k a | < k
211

Camil Staps's avatar
Camil Staps committed
212 213 214
/**
 * Removes the value at a given key position. The mapping can be unique.
 */
215
delU :: !a !.(Map a b) -> u:(!v:(Maybe b), !Map a b) | == a & < a, [u <= v] // !k !w:(Map k u:v) -> x:(Maybe u:v, !y:(Map k u:v)) | == k & < k, [ w y <= u, x <= y, w <= y]
216

217
foldrWithKey :: !(k v u:a -> u:a) !u:a !(Map k v) -> u:a
218
foldlWithKey :: !(.a -> .(k -> .(v -> .a))) !.a !(Map k v) -> .a
Camil Staps's avatar
Camil Staps committed
219

220
//* @type (v a -> a) a (Map k v) -> a
Camil Staps's avatar
Camil Staps committed
221 222
foldrNoKey f x m :== foldrWithKey (\_ v acc -> f v acc) x m

223
//* @type (a v -> a) a (Map k v) -> a
Camil Staps's avatar
Camil Staps committed
224
foldlNoKey f x m :== foldlWithKey (\acc _ v -> f acc v) x m
225

Camil Staps's avatar
Camil Staps committed
226 227 228 229 230
/**
 * Filter elements in a Map.
 *
 * @param The predicate function.
 * @param The Map.
231
 * @result A new Map that contains exactly those pairs (k,v) from the original Map for which p k v holds.
Camil Staps's avatar
Camil Staps committed
232 233
 */
filterWithKey :: !(k v -> Bool) !(Map k v) -> Map k v
234

Camil Staps's avatar
Camil Staps committed
235 236 237 238
/**
 * A list of the keys in a Map.
 * @type (Map k v) -> [k]
 */
239
keys m :== foldrWithKey (\k _ ks -> [k : ks]) [] m
Camil Staps's avatar
Camil Staps committed
240 241 242 243 244

/**
 * A list of the elements in a Map.
 * @type (Map k v) -> [v]
 */
245
elems m :== foldrNoKey (\x xs -> [x:xs]) [] m
246

247 248 249
//Conversion functions

/**
Camil Staps's avatar
Camil Staps committed
250 251 252 253 254 255
 * Converts a mapping to a list of key value pairs.
 * Because of the internal ordering of the mapping the resulting
 * list is sorted ascending on the key part of the tuple.
 *
 * @type (Map k v) -> [(k,v)]
 * @param The original mapping
256
 * @result A list of key/value tuples in the mapping
Camil Staps's avatar
Camil Staps committed
257
 */
258
toList m :== toAscList m
259 260

/**
Camil Staps's avatar
Camil Staps committed
261 262 263 264
 * Same as toList.
 * @type (Map k v) -> [(k,v)]
 */
toAscList m :== foldrWithKey (\k x xs -> [(k,x):xs]) [] m
265 266

/**
Camil Staps's avatar
Camil Staps committed
267 268 269
 * Converts a list of key/value tuples to a mapping.
 *
 * @param A list of key/value tuples
270
 * @result A mapping containing all the tuples in the list
271
 * @property correctness: A.elems :: [(k,v)]:
272 273
 *   check all_present elems m /\ // All elements put
 *     check all_from m elems /\  // No other elements
274
 *     integrity m
275 276
 *   where
 *     m = fromList elems
277
 * @complexity O(n*log n)
Camil Staps's avatar
Camil Staps committed
278 279
 */
fromList :: !u:[v:(!a, !b)] -> Map a b | == a & < a, [u <= v]
280

281 282 283 284 285 286 287 288 289 290 291 292
/**
 * The keys of all keys of a map.
 * @complexity log(n)
 */
keysSet :: !(Map k a) -> Set k

/**
 * Build a map from a set of keys and a function which for each key computes its value.
 * @complexity log(n)
 */
fromSet :: !(k -> a) !(Set k) -> Map k a

293
derive gEq Map
294
derive gLexOrd Map
295

Camil Staps's avatar
Camil Staps committed
296 297
/**
 * Check if a key exists in a Map.
298
 * @property correctness: A.k :: k; m :: Map k v:
299
 *   member k m <==> isMember k (keys m)
300
 * @complexity O(log n)
Camil Staps's avatar
Camil Staps committed
301
 */
302
member :: !k !(Map k a) -> Bool | < k
303

Camil Staps's avatar
Camil Staps committed
304 305 306
/**
 * Checks if a key is not a member of a Map.
 * @type k (Map k v) -> Bool | < k
307
 * @property correctness: A.k :: k; m :: Map k v:
308
 *   notMember k m <==> not (isMember k (keys m))
Camil Staps's avatar
Camil Staps committed
309
 */
310 311
notMember k m :== not (member k m)

Camil Staps's avatar
Camil Staps committed
312 313 314
/**
 * Find an element in a Map.
 * Aborts when the element is not found.
315
 * @property correctness: A.k :: k; v :: v; m :: Map k v:
316
 *   find k (put k v m) =.= v
317
 * @complexity O(log n)
Camil Staps's avatar
Camil Staps committed
318
 */
319
find :: !k !(Map k a) -> a | < k
320

Camil Staps's avatar
Camil Staps committed
321 322 323 324 325 326
/**
 * Find an element in a Map.
 * When the key does not exist, return a default.
 *
 * @param The default.
 * @param The key to look up.
327
 * @property correctness: A.k :: k; v :: v; m :: Map k v:
328 329 330
 *   findWithDefault default k (put k v m) =.= v /\
 *     findWithDefault default k (del k m) =.= default
 *   where default = gDefault{|*|}
331
 * @complexity O(log n)
Camil Staps's avatar
Camil Staps committed
332
 */
333
findWithDefault :: !a !k !(Map k a) -> a | < k
334

335 336 337 338 339 340

/**
 * Find the (Just key) of an element in a Map.
 * When the element does not exist, return Nothing.
 *
 * @param The element you're looking for.
341
 * @property correctness: A.v :: v; m :: Map k v:
342 343 344
 *   case [k \\ (k,v`) <- toList m | v == v`] of
 *     []    -> findKey v m =.= Nothing
 *     [k:_] -> findKey v m =.= Just k
345
 * @complexity O(n)
346 347 348 349
 */
findKey :: !a !(Map k a) -> Maybe k | == a

/**
Peter Achten's avatar
Peter Achten committed
350
 * Find a (Just key) of an element in a Map, for which the function yields True.
351 352
 * When the element does not exist, return Nothing.
 *
Peter Achten's avatar
Peter Achten committed
353
 * @param The search function for checking values in the Map.
354
 * @property correctness: A.p :: Predicate v; m :: Map k v:
355 356 357
 *   case [k \\ (k,v) <- toList m | pred p v] of
 *     []    -> findKeyWith (pred p) m =.= Nothing
 *     [k:_] -> findKeyWith (pred p) m =.= Just k
358
 * @complexity O(n)
359
 */
Peter Achten's avatar
Peter Achten committed
360
findKeyWith :: !(a -> Bool) !(Map k a) -> Maybe k
361 362 363 364 365 366 367

/**
 * Find the key of an element in a Map.
 * If the element is not a member, return the first parameter.
 *
 * @param The result if the second parameter does not occur as a value in the Map.
 * @param The element you're looking for.
368
 * @property correctness: A.v :: v; m :: Map k v:
369 370 371 372
 *   case findKey v m of
 *     Nothing -> findKeyWithDefault default v m =.= default
 *     Just k  -> findKeyWithDefault default v m =.= k
 *   where default = gDefault{|*|}
373
 * @complexity O(n)
374 375 376 377
 */
findKeyWithDefault :: !k !a !(Map k a) -> k | == a

/**
Peter Achten's avatar
Peter Achten committed
378
 * Find the key of an element in a Map, for which the function yields True.
379 380
 * If the element is not a member, return the second parameter.
 *
Peter Achten's avatar
Peter Achten committed
381 382
 * @param The search function for checking values in the Map.
 * @param The result when all values in the Map check as False.
383
 * @property correctness: A.p :: Predicate v; m :: Map k v:
384 385 386 387
 *   case findKeyWith (pred p) m of
 *     Nothing -> findKeyWithDefaultWith (pred p) default m =.= default
 *     Just k  -> findKeyWithDefaultWith (pred p) default m =.= k
 *   where default = gDefault{|*|}
388
 * @complexity O(n)
389
 */
Peter Achten's avatar
Peter Achten committed
390
findKeyWithDefaultWith :: !(a -> Bool) !k !(Map k a) -> k
391 392


393
alter :: !((Maybe a) -> Maybe a) !k !(Map k a) -> Map k a | < k
394

Camil Staps's avatar
Camil Staps committed
395
/**
396
 * Get the index of a key in a Map so that it can be retrieved with
397
 * {{`elemAt`}}.
398 399
 */
getIndex :: !k !(Map k a) -> Maybe Int | < k
Camil Staps's avatar
Camil Staps committed
400 401

/**
402
 * Get the entry at a certain index. To get an index for a certain key, see
403
 * {{`getIndex`}}.
Camil Staps's avatar
Camil Staps committed
404
 */
405
elemAt :: !Int !(Map k a) -> Maybe (!k, !a)
406

407 408 409 410 411 412 413 414 415 416 417
/**
 * Update an entry at a certain index. To get an index for a certain key, see
 * {{`getIndex`}}.
 *
 * @param The update function
 * @param The index
 * @param The map
 * @result The new map, or Maybe in case of an index out of range
 */
updateAt :: !(k a -> Maybe a) !Int !(Map k a) -> Maybe (Map k a)

418
findMin :: !(Map k a) -> (!k, !a)
419

420
findMax :: !(Map k a) -> (!k, !a)
421

422
unions :: ![Map k a] -> Map k a | < k
423

424
unionsWith :: !(a a -> a) ![Map k a] -> Map k a | < k
425

426
unionWith :: !(a a -> a) !(Map k a) !(Map k a) -> Map k a | < k
427

428
unionWithKey :: !(k a a -> a) !(Map k a) !(Map k a) -> Map k a | < k
429

430 431 432 433 434 435
intersection :: !(Map k a) !(Map k b) -> Map k a | < k

intersectionWith :: !(a b -> c) !(Map k a) !(Map k b) -> Map k c | < k

intersectionWithKey :: !(k a b -> c) !(Map k a) !(Map k b) -> Map k c | < k

436
union :: !(Map k a) !(Map k a) -> Map k a | < k
437 438 439 440

mergeWithKey :: !(k a b -> Maybe c) !((Map k a) -> Map k c) !((Map k b) -> Map k c)
             !(Map k a) !(Map k b) -> Map k c | < k

Camil Staps's avatar
Camil Staps committed
441 442 443 444 445 446
/**
 * Removes the values at given key positions. The mapping itself can be spine unique.
 *
 * @type [a] (Map a b) -> Map a b | <, == a
 * @param The list of keys to remove
 * @param The original mapping
447
 * @result The modified mapping with the values/keys removed
Camil Staps's avatar
Camil Staps committed
448
 */
Mart Lubbers's avatar
Mart Lubbers committed
449
delList xs m :== 'StdList'.foldr (\k m -> del k m) m xs
450

Camil Staps's avatar
Camil Staps committed
451 452 453 454 455 456
/**
 * Adds or replaces a list of key/value pairs.
 *
 * @type [(a, b)] (Map a b) -> Map a b | ==, < a
 * @param A list of key/value tuples
 * @param The original mapping
457
 * @result The modified mapping with the added values
Camil Staps's avatar
Camil Staps committed
458
 */
459 460
putList xs m :== union (fromList xs) m

461
instance Functor (Map k)
462 463
where
	fmap :: !(a -> b) !(Map k a) -> Map k b
464 465

difference :: !(Map k a) !(Map k b) -> Map k a | < k
466 467 468
mapWithKey :: !(k a -> b) !(Map k a) -> Map k b
isSubmapOf :: !(Map k a) !(Map k a) -> Bool | < k & Eq a
isSubmapOfBy :: !(a b -> Bool) !(Map k a) !(Map k b) -> Bool | < k