Map.dcl 13 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
from Text.GenJSON      import generic JSONEncode, generic JSONDecode, :: JSONNode
Camil Staps's avatar
Camil Staps committed
73 74
from Data.GenEq import generic gEq
from Data.GenLexOrd import generic gLexOrd, :: LexOrd
75
from Data.Monoid    import class Monoid, class Semigroup
Mart Lubbers's avatar
Mart Lubbers committed
76
import qualified StdList
77
from Data.List import foldr
78
from Data.Functor import class Functor (..)
79
from StdOverloaded import class < (..)
80
import StdClass
81 82

/**
Camil Staps's avatar
Camil Staps committed
83 84 85 86 87
 * 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.
88 89 90 91
 *
 * @invariant integrity: A.m :: Map k v:
 *   log_size m /\
 *   sizes_correct m
92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
 *
 * @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
109 110 111
 */
:: Map k v
  = Bin !Int !k !v !(Map k v) !(Map k v)
112 113 114
  | Tip

instance Monoid (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
Camil Staps's avatar
Camil Staps committed
128
 */
129 130 131
null mp :== case mp of
              Tip -> True
              _   -> False
Jurriën Stutterheim's avatar
Jurriën Stutterheim committed
132

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

Camil Staps's avatar
Camil Staps committed
141 142 143 144
/**
 * Create a Map with one element.
 */
singleton   :: !k !v -> Map k v
145

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

153
/**
Camil Staps's avatar
Camil Staps committed
154 155 156 157 158
 * 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
159
 * @result The modified mapping with the added value
160
 * @property correctness: A.m :: Map k v; k :: k; v :: v:
Camil Staps's avatar
Camil Staps committed
161 162
 *   get k m` =.= Just v /\                                           // Correctly put
 *     check all_present [kv \\ kv=:(k`,_) <- toList m | k <> k`] m` /\ // Other elements untouched
163
 *     integrity m`
Camil Staps's avatar
Camil Staps committed
164 165
 *   where
 *     m` = put k v m
Camil Staps's avatar
Camil Staps committed
166
 */
167
put :: !k !a !(Map k a) -> Map k a | < k
168

Camil Staps's avatar
Camil Staps committed
169 170 171 172 173 174 175
/**
 * 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
176
 * @result When found, the value at the key position, if not: Nothing
Camil Staps's avatar
Camil Staps committed
177
 */
178 179 180 181 182 183 184 185
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))
186

Camil Staps's avatar
Camil Staps committed
187 188 189
/**
 * Searches for a value at a given key position. Works also for unique mappings.
 */
190
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
191

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

Camil Staps's avatar
Camil Staps committed
207 208 209
/**
 * Removes the value at a given key position. The mapping can be unique.
 */
210
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]
211

212
foldrWithKey :: !(k v u:a -> u:a) !u:a !(Map k v) -> u:a
213
foldlWithKey :: !(.a -> .(k -> .(v -> .a))) !.a !(Map k v) -> .a
Camil Staps's avatar
Camil Staps committed
214

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

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

Camil Staps's avatar
Camil Staps committed
221 222 223 224 225
/**
 * Filter elements in a Map.
 *
 * @param The predicate function.
 * @param The Map.
226
 * @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
227 228
 */
filterWithKey :: !(k v -> Bool) !(Map k v) -> Map k v
229

Camil Staps's avatar
Camil Staps committed
230 231 232 233
/**
 * A list of the keys in a Map.
 * @type (Map k v) -> [k]
 */
234
keys m :== foldrWithKey (\k _ ks -> [k : ks]) [] m
Camil Staps's avatar
Camil Staps committed
235 236 237 238 239

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

242 243 244
//Conversion functions

/**
Camil Staps's avatar
Camil Staps committed
245 246 247 248 249 250
 * 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
251
 * @result A list of key/value tuples in the mapping
Camil Staps's avatar
Camil Staps committed
252
 */
253
toList m :== toAscList m
254 255

/**
Camil Staps's avatar
Camil Staps committed
256 257 258 259
 * Same as toList.
 * @type (Map k v) -> [(k,v)]
 */
toAscList m :== foldrWithKey (\k x xs -> [(k,x):xs]) [] m
260 261

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

derive JSONEncode Map
derive JSONDecode Map
derive gEq Map
278
derive gLexOrd Map
279

Camil Staps's avatar
Camil Staps committed
280 281
/**
 * Check if a key exists in a Map.
282
 * @property correctness: A.k :: k; m :: Map k v:
283
 *   member k m <==> isMember k (keys m)
Camil Staps's avatar
Camil Staps committed
284
 */
285
member :: !k !(Map k a) -> Bool | < k
286

Camil Staps's avatar
Camil Staps committed
287 288 289
/**
 * Checks if a key is not a member of a Map.
 * @type k (Map k v) -> Bool | < k
290
 * @property correctness: A.k :: k; m :: Map k v:
291
 *   notMember k m <==> not (isMember k (keys m))
Camil Staps's avatar
Camil Staps committed
292
 */
293 294
notMember k m :== not (member k m)

Camil Staps's avatar
Camil Staps committed
295 296 297
/**
 * Find an element in a Map.
 * Aborts when the element is not found.
298
 * @property correctness: A.k :: k; v :: v; m :: Map k v:
299
 *   find k (put k v m) =.= v
Camil Staps's avatar
Camil Staps committed
300
 */
301
find :: !k !(Map k a) -> a | < k
302

Camil Staps's avatar
Camil Staps committed
303 304 305 306 307 308
/**
 * Find an element in a Map.
 * When the key does not exist, return a default.
 *
 * @param The default.
 * @param The key to look up.
309
 * @property correctness: A.k :: k; v :: v; m :: Map k v:
310 311 312
 *   findWithDefault default k (put k v m) =.= v /\
 *     findWithDefault default k (del k m) =.= default
 *   where default = gDefault{|*|}
Camil Staps's avatar
Camil Staps committed
313
 */
314
findWithDefault :: !a !k !(Map k a) -> a | < k
315

316 317 318 319 320 321

/**
 * 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.
322
 * @property correctness: A.v :: v; m :: Map k v:
323 324 325
 *   case [k \\ (k,v`) <- toList m | v == v`] of
 *     []    -> findKey v m =.= Nothing
 *     [k:_] -> findKey v m =.= Just k
326 327 328 329
 */
findKey :: !a !(Map k a) -> Maybe k | == a

/**
Peter Achten's avatar
Peter Achten committed
330
 * Find a (Just key) of an element in a Map, for which the function yields True.
331 332
 * When the element does not exist, return Nothing.
 *
Peter Achten's avatar
Peter Achten committed
333
 * @param The search function for checking values in the Map.
334
 * @property correctness: A.p :: Predicate v; m :: Map k v:
335 336 337
 *   case [k \\ (k,v) <- toList m | pred p v] of
 *     []    -> findKeyWith (pred p) m =.= Nothing
 *     [k:_] -> findKeyWith (pred p) m =.= Just k
338
 */
Peter Achten's avatar
Peter Achten committed
339
findKeyWith :: !(a -> Bool) !(Map k a) -> Maybe k
340 341 342 343 344 345 346

/**
 * 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.
347
 * @property correctness: A.v :: v; m :: Map k v:
348 349 350 351
 *   case findKey v m of
 *     Nothing -> findKeyWithDefault default v m =.= default
 *     Just k  -> findKeyWithDefault default v m =.= k
 *   where default = gDefault{|*|}
352 353 354 355
 */
findKeyWithDefault :: !k !a !(Map k a) -> k | == a

/**
Peter Achten's avatar
Peter Achten committed
356
 * Find the key of an element in a Map, for which the function yields True.
357 358
 * If the element is not a member, return the second parameter.
 *
Peter Achten's avatar
Peter Achten committed
359 360
 * @param The search function for checking values in the Map.
 * @param The result when all values in the Map check as False.
361
 * @property correctness: A.p :: Predicate v; m :: Map k v:
362 363 364 365
 *   case findKeyWith (pred p) m of
 *     Nothing -> findKeyWithDefaultWith (pred p) default m =.= default
 *     Just k  -> findKeyWithDefaultWith (pred p) default m =.= k
 *   where default = gDefault{|*|}
366
 */
Peter Achten's avatar
Peter Achten committed
367
findKeyWithDefaultWith :: !(a -> Bool) !k !(Map k a) -> k
368 369


370
alter :: !((Maybe a) -> Maybe a) !k !(Map k a) -> Map k a | < k
371

Camil Staps's avatar
Camil Staps committed
372
/**
373
 * Get the index of a key in a Map so that it can be retrieved with
374
 * {{`elemAt`}}.
375 376
 */
getIndex :: !k !(Map k a) -> Maybe Int | < k
Camil Staps's avatar
Camil Staps committed
377 378

/**
379
 * Get the entry at a certain index. To get an index for a certain key, see
380
 * {{`getIndex`}}.
Camil Staps's avatar
Camil Staps committed
381
 */
382
elemAt :: !Int !(Map k a) -> Maybe (!k, !a)
383

384 385 386 387 388 389 390 391 392 393 394
/**
 * 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)

395
findMin :: !(Map k a) -> (!k, !a)
396

397
findMax :: !(Map k a) -> (!k, !a)
398

399
unions :: ![Map k a] -> Map k a | < k
400

401
unionsWith :: !(a a -> a) ![Map k a] -> Map k a | < k
402

403
unionWith :: !(a a -> a) !(Map k a) !(Map k a) -> Map k a | < k
404

405
unionWithKey :: !(k a a -> a) !(Map k a) !(Map k a) -> Map k a | < k
406

407 408 409 410 411 412
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

413
union :: !(Map k a) !(Map k a) -> Map k a | < k
414 415 416 417 418 419

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

foldlStrict :: !(a b -> a) !a ![b] -> a

Camil Staps's avatar
Camil Staps committed
420 421 422 423 424 425
/**
 * 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
426
 * @result The modified mapping with the values/keys removed
Camil Staps's avatar
Camil Staps committed
427
 */
Mart Lubbers's avatar
Mart Lubbers committed
428
delList xs m :== 'StdList'.foldr (\k m -> del k m) m xs
429

Camil Staps's avatar
Camil Staps committed
430 431 432 433 434 435
/**
 * 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
436
 * @result The modified mapping with the added values
Camil Staps's avatar
Camil Staps committed
437
 */
438 439
putList xs m :== union (fromList xs) m

440
instance Functor (Map k)
441 442

difference :: !(Map k a) !(Map k b) -> Map k a | < k
443 444 445
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