Data.Map

(source)

Finite Maps

Reexports

import public Data.Map.Internal

Definitions

empty : Map k v

  The empty map. O(1)

Totality: total
Visibility: export

foldl : (v -> w -> v) -> v -> Map k w -> v

  Fold the values in the map using the given left-associative binary operator. O(n)

Totality: total
Visibility: export

foldr : (v -> w -> w) -> w -> Map k v -> w

  Fold the values in the map using the given right-associative binary operator. O(n)

Totality: total
Visibility: export

foldlWithKey : (v -> k -> w -> v) -> v -> Map k w -> v

  Fold the keys and values in the map using the given left-associative binary operator. O(n)

Totality: total
Visibility: export

foldrWithKey : (k -> v -> w -> w) -> w -> Map k v -> w

  Fold the keys and values in the map using the given right-associative binary operator. O(n)

Totality: total
Visibility: export

insert : Eq (Map k v) => Eq v => Ord k => k -> v -> Map k v -> Map k v

  Insert a new key and value in the map.
  If the key is already present in the map, the associated value is
  replaced with the supplied value. O(log n)

Totality: total
Visibility: export

insertWith : Ord k => (v -> v -> v) -> k -> v -> Map k v -> Map k v

  Insert with a function, combining new value and old value.
  insertWith f key value mp
  will insert the pair (key, value) into mp if key does
  not exist in the map. If the key does exist, the function will
  insert the pair (key, f new_value old_value). O(log n)

Totality: total
Visibility: export

insertWithKey : Ord k => (k -> v -> v -> v) -> k -> v -> Map k v -> Map k v

  Insert with a function, combining key, new value and old value.
  insertWithKey f key value mp
  will insert the pair (key, value) into map if key does
  not exist in the map. If the key does exist, the function will
  insert the pair (key,f key new_value old_value). O(log n)

Totality: total
Visibility: export

insertLookupWithKey : Ord k => (k -> v -> v -> v) -> k -> v -> Map k v -> (Maybe v, Map k v)

  Combines insert operation with old value retrieval.
  The expression (insertLookupWithKey f k x map)
  is a pair where the first element is equal to (lookup k map)
  and the second element equal to (insertWithKey f k x map). O(log n)

Totality: total
Visibility: export

delete : Eq (Map k v) => Eq k => Ord k => k -> Map k v -> Map k v

  Delete a key and its value from the map. When the key is not
  a member of the map, the original map is returned. O(log n)

Totality: total
Visibility: export

adjustWithKey : Ord k => (k -> v -> v) -> k -> Map k v -> Map k v

  Adjust a value at a specific key. When the key is not
  a member of the map, the original map is returned. O(log n)

Totality: total
Visibility: export

adjust : Ord k => (v -> v) -> k -> Map k v -> Map k v

  Update a value at a specific key with the result of the provided function.
  When the key is not a member of the map, the original map is returned. O(log n)

Totality: total
Visibility: export

updateWithKey : Ord k => (k -> v -> Maybe v) -> k -> Map k v -> Map k v

  The expression (updateWithKey f k map) updates the
  value x at k (if it is in the map). If (f k x) is Nothing,
  the element is deleted. If it is (Just y), the key k is bound
  to the new value y. O(log n)

Totality: total
Visibility: export

update : Ord k => (v -> Maybe v) -> k -> Map k v -> Map k v

  The expression (update f k map) updates the value x
  at k (if it is in the map). If (f x) is Nothing, the element is
  deleted. If it is (Just y), the key k is bound to the new value y. O(log n)

Totality: total
Visibility: export

updateLookupWithKey : Ord k => (k -> v -> Maybe v) -> k -> Map k v -> (Maybe v, Map k v)

  Lookup and update. See also updateWithKey.
  The function returns changed value, if it is updated.
  Returns the original key value if the map entry is deleted. O(log n)

Totality: total
Visibility: export

alter : Ord k => (Maybe v -> Maybe v) -> k -> Map k v -> Map k v

  The expression (alter f k map) alters the value x at k, or absence thereof.
  alter can be used to insert, delete, or update a value in a Map. O(log n)

Totality: total
Visibility: export

lookup : Ord k => k -> Map k v -> Maybe v

  Lookup the value at a key in the map.
  The function will return the corresponding value as (Just value),
  or Nothing if the key isn't in the map. O(log n)

Totality: total
Visibility: export

(!?) : Ord k => Map k v -> k -> Maybe v

  Find the value at a key.
  Returns Nothing when the element can not be found. O(log n)

Totality: total
Visibility: export

member : Ord k => k -> Map k v -> Bool

  Is the key a member of the map? See also notMember. O(log n)

Totality: total
Visibility: export

notMember : Ord k => k -> Map k v -> Bool

  Is the key not a member of the map? See also member. O(log n)

Totality: total
Visibility: export

find : Ord k => k -> Map k v -> v

  Find the value at a key.
  Calls idris_crash when the element can not be found. O(log n)

Totality: total
Visibility: export

(!!) : Ord k => Map k v -> k -> v

  Find the value at a key.
  Calls idris_crash when the element can not be found. O(log n)

Totality: total
Visibility: export

findWithDefault : Ord k => v -> k -> Map k v -> v

  The expression (findWithDefault def k map) returns
  the value at key k or returns default value def
  when the key is not in the map. O(log n)

Totality: total
Visibility: export

lookupLT : Ord k => k -> Map k v -> Maybe (k, v)

  Find largest key smaller than the given one and return the
  corresponding (key, value) pair. O(log n)

Totality: total
Visibility: export

lookupGT : Ord k => k -> Map k v -> Maybe (k, v)

  Find smallest key greater than the given one and return the
  corresponding (key, value) pair. O(log n)

Totality: total
Visibility: export

lookupLE : Ord k => k -> Map k v -> Maybe (k, v)

  Find largest key smaller or equal to the given one and return
  the corresponding (key, value) pair. O(log n)

Totality: total
Visibility: export

lookupGE : Ord k => k -> Map k v -> Maybe (k, v)

  Find smallest key greater or equal to the given one and return
  the corresponding (key, value) pair. O(log n)

Totality: total
Visibility: export

null : Map k v -> Bool

  Is the map empty? O(1)

Totality: total
Visibility: export

splitRoot : Map k v -> List (Map k v)

  Decompose a map into pieces based on the structure of the underlying tree.
  This function is useful for consuming a map in parallel. O(1)

Totality: total
Visibility: export

splitLookup : Ord k => k -> Map k v -> (Map k v, (Maybe v, Map k v))

  The expression (splitLookup k map) splits a map just
  like split but also returns lookup k map. O(log n)

Totality: total
Visibility: export

split : Ord k => k -> Map k v -> (Map k v, Map k v)

  The expression (split k map) is a pair (map1,map2) where
  the keys in map1 are smaller than k and the keys in map2 larger than k.
  Any key equal to k is found in neither map1 nor map2. O(log n)

Totality: total
Visibility: export

filterWithKey : Eq (Map k v) => (k -> v -> Bool) -> Map k v -> Map k v

  Filter all keys/values that satisfy the predicate. O(n)

Totality: total
Visibility: export

filter : Eq (Map k v) => (v -> Bool) -> Map k v -> Map k v

  Filter all values that satisfy the predicate. O(n)

Totality: total
Visibility: export

partitionWithKey : Eq (Map k v) => (k -> v -> Bool) -> Map k v -> (Map k v, Map k v)

  Partition the map according to a predicate. The first
  map contains all elements that satisfy the predicate, the second all
  elements that fail the predicate. See also split. O(n)

Totality: total
Visibility: export

takeWhileAntitone : (k -> Bool) -> Map k v -> Map k v

  Take while a predicate on the keys holds.
  The user is responsible for ensuring that for all keys j and k in the map,
  j < k ==> p j >= p k. See note at spanAntitone. O(log n)

Totality: total
Visibility: export

dropWhileAntitone : (k -> Bool) -> Map k v -> Map k v

  Drop while a predicate on the keys holds.
  The user is responsible for ensuring that for all keys j and k in the map,
  j < k ==> p j >= p k. See note at spanAntitone. O(log n)

Totality: total
Visibility: export

spanAntitone : (k -> Bool) -> Map k v -> (Map k v, Map k v)

  Divide a map at the point where a predicate on the keys stops holding.
  The user is responsible for ensuring that for all keys j and k in the map,
  j < k ==> p j>= p k. O(log n)

Totality: total
Visibility: export

mapMaybeWithKey : (k -> a -> Maybe b) -> Map k a -> Map k b

  Map keys/values and collect the Just results. O(n)

Totality: total
Visibility: export

mapMaybe : (a -> Maybe b) -> Map k a -> Map k b

  Map values and collect the Just results. O(n)

Totality: total
Visibility: export

mapEitherWithKey : (k -> a -> Either b c) -> Map k a -> (Map k b, Map k c)

  Map keys/values and separate the Left and Right results. O(n)

Totality: total
Visibility: export

mapEither : (a -> Either b c) -> Map k a -> (Map k b, Map k c)

  Map values and separate the Left and Right results. O(n)

Totality: total
Visibility: export

isSubmapOfBy : Ord k => (a -> b -> Bool) -> Map k a -> Map k b -> Bool

  The expression (isSubmapOfBy f t1 t2) returns True if
  all keys in t1 are in tree t2, and when f returns True when
  applied to their respective values.

Totality: total
Visibility: export

isSubmapOf : Eq v => Ord k => Map k v -> Map k v -> Bool

  This function is defined as (isSubmapOf = isSubmapOfBy (==)).

Totality: total
Visibility: export

isProperSubmapOfBy : Ord k => (a -> b -> Bool) -> Map k a -> Map k b -> Bool

  Is this a proper submap? (ie. a submap but not equal).
  The expression (isProperSubmapOfBy f m1 m2) returns True when
  keys m1 and keys m2 are not equal,
  all keys in m1 are in m2, and when f returns True when
  applied to their respective values.

Totality: total
Visibility: export

isProperSubmapOf : Eq v => Ord k => Map k v -> Map k v -> Bool

  Is this a proper submap? (ie. a submap but not equal).
  Defined as (isProperSubmapOf = isProperSubmapOfBy (==)).

Totality: total
Visibility: export

lookupIndex : Ord k => k -> Map k v -> Maybe Nat

  Lookup the index of a key, which is its zero-based index in
  the sequence sorted by keys. The index is a number from 0 up to, but not
  including, the size of the map. O(log n)

Totality: total
Visibility: export

findIndex : Ord k => k -> Map k v -> Nat

  Return the index of a key, which is its zero-based index in
  the sequence sorted by keys. The index is a number from 0 up to, but not
  including, the size of the map. Calls idris_crash when the key is not
  a member of the map. O(log n)

Totality: total
Visibility: export

elemAt : Nat -> Map k v -> (k, v)

  Retrieve an element by its index, i.e. by its zero-based
  index in the sequence sorted by keys. If the index is out of range (less
  than zero, greater or equal to size of the map), idris_crash is called. O(log n)

Totality: total
Visibility: export

updateAt : (k -> v -> Maybe v) -> Nat -> Map k v -> Map k v

  Update the element at index, i.e. by its zero-based index in
  the sequence sorted by keys. If the index is out of range (less than zero,
  greater or equal to size of the map), idris_crash is called. O(log n)

Totality: total
Visibility: export

deleteAt : Nat -> Map k v -> Map k v

  Delete the element at index, i.e. by its zero-based index in
  the sequence sorted by keys. If the index is out of range (less than zero,
  greater or equal to size of the map), idris_crash is called. O(log n)

Totality: total
Visibility: export

take : Nat -> Map k v -> Map k v

  Take a given number of entries in key order, beginning
  with the smallest keys. O(log n)

Totality: total
Visibility: export

drop : Nat -> Map k v -> Map k v

  Drop a given number of entries in key order, beginning
  with the smallest keys. O(log n)

Totality: total
Visibility: export

splitAt : Nat -> Map k v -> (Map k v, Map k v)

  Split a map at a particular index. O(log n)

Totality: total
Visibility: export

lookupMin : Map k v -> Maybe (k, v)

  The minimal key of the map. Returns Nothing if the map is empty. O(log n)

Totality: total
Visibility: export

lookupMax : Map k v -> Maybe (k, v)

  The maximal key of the map. Returns Nothing if the map is empty. O(log n)

Totality: total
Visibility: export

findMin : Map k v -> (k, v)

  The minimal key of the map. Calls idris_crash if the map is empty. O(log n)

Totality: total
Visibility: export

findMax : Map k v -> (k, v)

  The maximal key of the map. Calls idris_crash if the map is empty. O(log n)

Totality: total
Visibility: export

deleteMin : Map k v -> Map k v

  Delete the minimal key. Returns an empty map if the map is empty. O(log n)

Totality: total
Visibility: export

deleteMax : Map k v -> Map k v

  Delete the maximal key. Returns an empty map if the map is empty. O(log n)

Totality: total
Visibility: export

minViewWithKey : Map k v -> Maybe ((k, v), Map k v)

  Retrieves the minimal (key,value) pair of the map, and
  the map stripped of that element, or Nothing if passed an empty map. O(log n)

Totality: total
Visibility: export

deleteFindMin : Map k v -> ((k, v), Map k v)

  Delete and find the minimal element. O(log n)

Totality: total
Visibility: export

maxViewWithKey : Map k v -> Maybe ((k, v), Map k v)

  Retrieves the maximal (key,value) pair of the map, and
  the map stripped of that element, or Nothing if passed an empty map. O(log n)

Totality: total
Visibility: export

deleteFindMax : Map k v -> ((k, v), Map k v)

  Delete and find the maximal element. O(log n)

Totality: total
Visibility: export

updateMinWithKey : (k -> v -> Maybe v) -> Map k v -> Map k v

  Update the value at the minimal key. O(log n)

Totality: total
Visibility: export

updateMin : (v -> Maybe v) -> Map k v -> Map k v

  Update the value at the minimal key. O(log n)

Totality: total
Visibility: export

updateMaxWithKey : (k -> v -> Maybe v) -> Map k v -> Map k v

  Update the value at the maximal key. O(log n)

Totality: total
Visibility: export

updateMax : (v -> Maybe v) -> Map k v -> Map k v

  Update the value at the maximal key. O(log n)

Totality: total
Visibility: export

minView : Map k v -> Maybe (v, Map k v)

  Retrieves the value associated with minimal key of the
  map, and the map stripped of that element, or Nothing if passed an empty map. O(log n)

Totality: total
Visibility: export

maxView : Map k v -> Maybe (v, Map k v)

  Retrieves the value associated with maximal key of the
  map, and the map stripped of that element, or Nothing if passed an empty map. O(log n)

Totality: total
Visibility: export

union : Eq (Map k v) => Eq v => Ord k => Map k v -> Map k v -> Map k v

  The expression (union t1 t2) takes the left-biased union of t1 and t2.
  It prefers t1 when duplicate keys are encountered.

Totality: total
Visibility: export

unionWith : Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v

  Union with a combining function.

Totality: total
Visibility: export

unionWithKey : Ord k => (k -> v -> v -> v) -> Map k v -> Map k v -> Map k v

  Union with a combining function.

Totality: total
Visibility: export

unions : Eq (Map k v) => Eq v => Foldable f => Ord k => f (Map k v) -> Map k v

  The union of a list of maps.

Totality: total
Visibility: export

unionsWith : Foldable f => Ord k => (v -> v -> v) -> f (Map k v) -> Map k v

  The union of a list of maps, with a combining operation.

Totality: total
Visibility: export

difference : Ord k => Map k a -> Map k b -> Map k a

  Difference of two maps.
  Return elements of the first map not existing in the second map.

Totality: total
Visibility: export

(\\) : Ord k => Map k a -> Map k b -> Map k a

  Same as difference.

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 7

intersection : Eq (Map k a) => Ord k => Map k a -> Map k b -> Map k a

  Intersection of two maps.
  Return data in the first map for the keys existing in both maps.

Totality: total
Visibility: export

intersectionWith : Ord k => (a -> b -> c) -> Map k a -> Map k b -> Map k c

  Intersection with a combining function.

Totality: total
Visibility: export

intersectionWithKey : Ord k => (k -> a -> b -> c) -> Map k a -> Map k b -> Map k c

  Intersection with a combining function.

Totality: total
Visibility: export

disjoint : Ord k => Map k a -> Map k b -> Bool

  Check whether the key sets of two
  maps are disjoint (i.e., their intersection is empty).

Totality: total
Visibility: export

compose : Ord b => Map b c -> Map a b -> Map a c

  Relate the keys of one map to the values of
  the other, by using the values of the former as keys for lookups in the latter.
  O(n * log(m)), where m is the size of the first argument.

Totality: total
Visibility: export

map : (v -> w) -> Map k v -> Map k w

  Map a function over all values in the map. O(n)

Totality: total
Visibility: export

mapWithKey : (k -> v -> w) -> Map k v -> Map k w

  Map a function over all values in the map. O(n)

Totality: total
Visibility: export

mapAccumL : (v -> k -> w -> (v, c)) -> v -> Map k w -> (v, Map k c)

  The function mapAccumL threads an accumulating
  argument through the map in ascending order of keys. O(n)

Totality: total
Visibility: export

mapAccumRWithKey : (v -> k -> w -> (v, c)) -> v -> Map k w -> (v, Map k c)

  The function mapAccumRWithKey threads an accumulating
  argument through the map in descending order of keys. O(n)

Totality: total
Visibility: export

mapAccumWithKey : (v -> k -> w -> (v, c)) -> v -> Map k w -> (v, Map k c)

  The function mapAccumWithKey threads an accumulating
  argument through the map in ascending order of keys. O(n)

Totality: total
Visibility: export

mapAccum : (v -> w -> (v, c)) -> v -> Map k w -> (v, Map k c)

  The function mapAccum threads an accumulating
  argument through the map in ascending order of keys. O(n)

Totality: total
Visibility: export

toDescList : Map k v -> List (k, v)

  Convert the map to a list of key/value pairs where the keys are in descending order. O(n)

Totality: total
Visibility: export

toAscList : Map k v -> List (k, v)

  Convert the map to a list of key/value pairs where the keys are in ascending order. O(n)

Totality: total
Visibility: export

toList : Map k v -> List (k, v)

  Convert the map to a list of key/value pairs.

Totality: total
Visibility: export

fromList : Ord k => Eq v => Eq (Map k v) => List (k, v) -> Map k v

  Build a map from a list of key/value pairs.
  If the list contains more than one value for the same key, the last value
  for the key is retained.
  If the keys of the list are ordered, a linear-time implementation is used. O(n * log(n))

Totality: total
Visibility: export

keys : Map k v -> List k

  Gets the keys of the map.

Totality: total
Visibility: export

values : Map k v -> List v

  Gets the values of the map.
  Could contain duplicates.

Totality: total
Visibility: export