Data.DMap

A module describing the dependent map (`DMap`).
Copied from haskell's "dependent-map" package.

Reexports

Definitions

ShowS : Type

  A copy of Haskells `ShowS` type

Visibility: public export

data DMap : (a -> Type) -> (a -> Type) -> Type

  Dependent maps: 'k' is a GADT-like thing with a facility for
  rediscovering its type parameter, elements of which function as identifiers
  tagged with the type of the thing they identify.  Real GADTs are one
  useful instantiation of `k`, as are 'Tag's from "Data.Unique.Tag" in the
  'prim-uniq' package.
  
  Semantically, `'DMap' k f` is equivalent to a set of `'DSum' k f` where no two
  elements have the same tag.
  
  More informally, 'DMap' is to dependent products as 'M.Map' is to `(->)`.
  Thus it could also be thought of as a partial (in the sense of \"partial
  function\") dependent product.

Totality: total
Visibility: export
Constructors:

Tip : DMap k f

Bin : Int -> k v -> f v -> DMap k f -> DMap k f -> DMap k f

Hints:

DFoldable (DMap k)

DFunctor (DMap k)

DEq k => DEq f => Eq (DMap k f)

DOrd k => Monoid (DMap k f)

DOrd k => DOrd f => Ord (DMap k f)

DOrd k => Semigroup (DMap k f)

DShow k => DShow f => Show (DMap k f)

empty : DMap k f

  *O(1)*. The empty map.
  
  ```
  empty      == fromList []
  size empty == 0
  ```

Visibility: export

singleton : k v -> f v -> DMap k f

  *O(1)*. A map with a single element.
  
  ```
  singleton k v        == fromList [k :=> v]
  size (singleton k v) == 1
  ```

Visibility: export

null : DMap k f -> Bool

  *O(1)*. Is the map empty?

Visibility: export

size : DMap k f -> Int

  *O(1)*. The number of elements in the map.

Visibility: export

lookup : DOrd k => k v -> DMap k f -> Maybe (f v)

  *O(log n)*. 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.

Visibility: export

minViewWithKey : DMap k f -> Maybe (DSum k f, DMap k f)

  *O(log n)*. Retrieves the minimal (key :=> value) entry of the map, and
  the map stripped of that element, or 'Nothing' if passed an empty map.

Visibility: export

maxViewWithKey : DMap k f -> Maybe (DSum k f, DMap k f)

  *O(log n)*. Retrieves the maximal (key :=> value) entry of the map, and
  the map stripped of that element, or 'Nothing' if passed an empty map.

Visibility: export

deleteFindMax : DMap k f -> (DSum k f, DMap k f)

  *O(log n)*. Delete and find the maximal element.
  
  Given `k1, k2 < k3`
  ```
  deleteFindMax (fromList [k1 :=> v1, k2 :=> v2, k3 :=> v3]) == (k3 :=> v3, fromList [k1 :=> v1, k2 :=> v2])
  deleteFindMax empty                                            Error: can not return the maximal element of an empty map
  ```

Visibility: export

deleteFindMin : DMap k f -> (DSum k f, DMap k f)

  *O(log n)*. Delete and find the minimal element.
  
  Given `k2 > k1, k3`
  ```
  deleteFindMin (fromList [k1 :=> v1, k2 :=> v2, k3 :=> v3]) == (k2 :=> v2, fromList [k1 :=> v1, k3 :=> v3])
  deleteFindMin                                                  Error: can not return the minimal element of an empty map
  ```

Visibility: export

member : DOrd k => k a -> DMap k f -> Bool

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

Visibility: export

notMember : DOrd k => k v -> DMap k f -> Bool

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

Visibility: export

findWithDefault : DOrd k => f v -> k v -> DMap k f -> f v

  *O(log n)*. 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.

Visibility: export

insert : DOrd k => k v -> f v -> DMap k f -> DMap k f

  *O(log n)*. 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. 'insert' is equivalent to
  `'insertWith' 'const'`.

Visibility: export

insertWithKey : DOrd k => (k v -> f v -> f v -> f v) -> k v -> f v -> DMap k f -> DMap k f

  *O(log n)*. Insert with a function, combining key, new value and old value.
  `'insertWithKey' f key value mp`
  will insert the entry `key :=> value` into `mp` if key does
  not exist in the map. If the key does exist, the function will
  insert the entry `key :=> f key new_value old_value`.
  Note that the key passed to f is the same key passed to 'insertWithKey'.

Visibility: export

insertWith : DOrd k => (f v -> f v -> f v) -> k v -> f v -> DMap k f -> DMap k f

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

Visibility: export

insertLookupWithKey : DOrd k => (k v -> f v -> f v -> f v) -> k v -> f v -> DMap k f -> (Maybe (f v), DMap k f)

  *O(log n)*. 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`)

Visibility: export

delete : DOrd k => k v -> DMap k f -> DMap k f

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

Visibility: export

updateWithKey : DOrd k => (k v -> f v -> Maybe (f v)) -> k v -> DMap k f -> DMap k f

  *O(log n)*. 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`.

Visibility: export

update : DOrd k => (f v -> Maybe (f v)) -> k v -> DMap k f -> DMap k f

  *O(log n)*. 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`.

Visibility: export

updateLookupWithKey : DOrd k => (k v -> f v -> Maybe (f v)) -> k v -> DMap k f -> (Maybe (f v), DMap k f)

  *O(log n)*. 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.

Visibility: export

alter : DOrd k => (Maybe (f v) -> Maybe (f v)) -> k v -> DMap k f -> DMap k f

  *O(log n)*. 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'.
  In short : `'lookup' k ('alter' f k m) = f ('lookup' k m)`.

Visibility: export

alterF : DOrd k => Functor f => k v -> (Maybe (g v) -> f (Maybe (g v))) -> DMap k g -> f (DMap k g)

  Works the same as 'alter' except the new value is returned in some 'Functor' `f`.
  In short : `(\v' -> alter (const v') k dm) <$> f (lookup k dm)`

Visibility: export

lookupIndex : DOrd k => k v -> DMap k f -> Maybe Int

  *O(log n)*. Lookup the *index* of a key. The index is a number from
  *0* up to, but not including, the 'size' of the map.

Visibility: export

findIndex : DOrd k => k v -> DMap k f -> Int

  *O(log n)*. Return the *index* of a key. The index is a number from
  *0* up to, but not including, the 'size' of the map. Calls 'error' when
  the key is not a 'member' of the map.

Visibility: export

elemAt : Int -> DMap k f -> DSum k f

  *O(log n)*. Retrieve an element by *index*. Calls 'error' when an
  invalid index is used.

Visibility: export

updateAt : (k v -> f v -> Maybe (f v)) -> Int -> DMap k f -> DMap k f

  *O(log n)*. Update the element at *index*. Does nothing when an
  invalid index is used.

Visibility: export

deleteAt : Int -> DMap k f -> DMap k f

  *O(log n)*. Delete the element at *index*.
  Defined as (`'deleteAt' i map = 'updateAt' (\k x -> 'Nothing') i map`).

Visibility: export

lookupMin : DMap k f -> Maybe (DSum k f)

Visibility: export

findMin : DMap k f -> DSum k f

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

Visibility: export

lookupMax : DMap k f -> Maybe (DSum k f)

Visibility: export

findMax : DMap k f -> DSum k f

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

Visibility: export

deleteMin : DMap k f -> DMap k f

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

Visibility: export

deleteMax : DMap k f -> DMap k f

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

Visibility: export

updateMinWithKey : (k v -> f v -> Maybe (f v)) -> DMap k f -> DMap k f

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

Visibility: export

updateMaxWithKey : (k v -> f v -> Maybe (f v)) -> DMap k f -> DMap k f

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

Visibility: export

split : DOrd k => k v -> DMap k f -> (DMap k f, DMap k f)

  *O(log n)*. 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`.

Visibility: export

splitLookup : DOrd k => k v -> DMap k f -> (DMap k f, (Maybe (f v), DMap k f))

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

Visibility: export

union : DOrd k => DMap k f -> DMap k f -> DMap k f

  *O(m*log(n/m + 1)), m <= n*.
  The expression (`'union' t1 t2`) takes the left-biased union of `t1` and `t2`.
  It prefers `t1` when duplicate keys are encountered,
  i.e. (`'union' == 'unionWith' 'const'`).

Visibility: export

unions : DOrd k => List (DMap k f) -> DMap k f

  The union of a list of maps:
    (`'unions' == 'Prelude.foldl' 'union' 'empty'`).

Visibility: export

unionWithKey : DOrd k => (k v -> f v -> f v -> f v) -> DMap k f -> DMap k f -> DMap k f

  *O(n+m)*.
  Union with a combining function.

Visibility: export

unionsWithKey : DOrd k => (k v -> f v -> f v -> f v) -> List (DMap k f) -> DMap k f

  The union of a list of maps, with a combining operation:
    (`'unionsWithKey' f == 'Prelude.foldl' ('unionWithKey' f) 'empty'`).

Visibility: export

difference : DOrd k => DMap k f -> DMap k g -> DMap k f

  *O(m * log (n/m + 1)), m <= n*. Difference of two maps.
  Return elements of the first map not existing in the second map.

Visibility: export

differenceWithKey : DOrd k => (k v -> f v -> g v -> Maybe (f v)) -> DMap k f -> DMap k g -> DMap k f

  *O(n+m)*. Difference with a combining function. When two equal keys are
  encountered, the combining function is applied to the key and both values.
  If it returns 'Nothing', the element is discarded (proper set difference). If
  it returns (`'Just' y`), the element is updated with a new value `y`.

Visibility: export

intersection : DOrd k => DMap k f -> DMap k f -> DMap k f

  *O(m * log (n/m + 1), m <= n*. Intersection of two maps.
  Return data in the first map for the keys existing in both maps.
  (`'intersection' m1 m2 == 'intersectionWith' 'const' m1 m2`).

Visibility: export

intersectionWithKey : DOrd k => (k v -> f v -> g v -> h v) -> DMap k f -> DMap k g -> DMap k h

  *O(m * log (n/m + 1), m <= n*. Intersection with a combining function.

Visibility: export

isSubmapOfBy : DOrd k => (k v -> k v -> f v -> g v -> Bool) -> DMap k f -> DMap k g -> Bool

  *O(n+m)*.
  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 keys and values.

Visibility: export

isProperSubmapOfBy : DOrd k => (k v -> k v -> f v -> g v -> Bool) -> DMap k f -> DMap k g -> Bool

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

Visibility: export

filterWithKey : DOrd k => (k v -> f v -> Bool) -> DMap k f -> DMap k f

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

Visibility: export

partitionWithKey : DOrd k => (k v -> f v -> Bool) -> DMap k f -> (DMap k f, DMap k f)

  *O(n)*. 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'.

Visibility: export

mapMaybe : DOrd k => (f v -> Maybe (g v)) -> DMap k f -> DMap k g

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

Visibility: export

mapEitherWithKey : DOrd k => (k v -> f v -> Either (g v) (h v)) -> DMap k f -> (DMap k g, DMap k h)

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

Visibility: export

foldrWithKey : (k v -> f v -> b -> b) -> b -> DMap k f -> b

  *O(n)*. Post-order fold.  The function will be applied from the lowest
  value to the highest.

Visibility: export

foldlWithKey : (b -> k v -> f v -> b) -> b -> DMap k f -> b

  *O(n)*. Pre-order fold.  The function will be applied from the highest
  value to the lowest.

Visibility: export

fromList : DOrd k => List (DSum k f) -> DMap k f

  *O(n*log n)*. Build a map from a list of key/value pairs. See also 'fromAscList'.
  If the list contains more than one value for the same key, the last value
  for the key is retained.

Visibility: export

fromListWithKey : DOrd k => (k v -> f v -> f v -> f v) -> List (DSum k f) -> DMap k f

  *O(n*log n)*. Build a map from a list of key/value pairs with a combining function. See also 'fromAscListWithKey'.

Visibility: export

toAscList : DMap k f -> List (DSum k f)

  *O(n)*. Convert to an ascending list.

Visibility: export

toList : DMap k f -> List (DSum k f)

  *O(n)*. Convert to a list of key/value pairs.

Visibility: export

toDescList : DMap k f -> List (DSum k f)

  *O(n)*. Convert to a descending list.

Visibility: export

fromDistinctAscList : List (DSum k f) -> DMap k f

  *O(n)*. Build a map from an ascending list of distinct elements in linear time.
  *The precondition is not checked.*

Visibility: export

fromAscListWithKey : DEq k => (k v -> f v -> f v -> f v) -> List (DSum k f) -> DMap k f

  *O(n)*. Build a map from an ascending list in linear time with a
  combining function for equal keys.
  *The precondition (input list is ascending) is not checked.*

Visibility: export

fromAscList : DEq k => List (DSum k f) -> DMap k f

  *O(n)*. Build a map from an ascending list in linear time.
  *The precondition (input list is ascending) is not checked.*

Visibility: export

assocs : DMap k f -> List (DSum k f)

  *O(n)*. Return all key/value pairs in the map in ascending key order.

Visibility: export

keys : DMap k f -> List (Some k)

  *O(n)*. Return all keys of the map in ascending order.
  
  ```
  keys (fromList [k1 :=> v1, k2 :=> v2]) == [k1, k2]
  keys empty == []
  ```

Visibility: export

map : (f v -> g v) -> DMap k f -> DMap k g

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

Visibility: export

ffor : DMap k f -> (f v -> g v) -> DMap k g

  *O(n)*.
  `'ffor' == 'flip' 'map'` except we cannot actually use
  'flip' because of the lack of impredicative types.

Visibility: export

mapWithKey : (k v -> f v -> g v) -> DMap k f -> DMap k g

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

Visibility: export

fforWithKey : DMap k f -> (k v -> f v -> g v) -> DMap k g

  *O(n)*.
  `'fforWithKey' == 'flip' 'mapWithKey'` except we cannot actually use
  'flip' because of the lack of impredicative types.

Visibility: export

traverseWithKey_ : Applicative t => (k v -> f v -> t ()) -> DMap k f -> t ()

  *O(n)*.
  `'traverseWithKey' f m == 'fromList' <$> 'traverse' (\(k, v) -> (,) k <$> f k v) ('toList' m)`
  That is, behaves exactly like a regular 'traverse' except that the traversing
  function also has access to the key associated with a value.

Visibility: export

forWithKey_ : Applicative t => DMap k f -> (k v -> f v -> t ()) -> t ()

  *O(n)*.
  `'forWithKey' == 'flip' 'traverseWithKey'` except we cannot actually use
  'flip' because of the lack of impredicative types.

Visibility: export

traverseWithKey : Applicative t => (k v -> f v -> t (g v)) -> DMap k f -> t (DMap k g)

  *O(n)*.
  `'traverseWithKey' f m == 'fromList' <$> 'traverse' (\(k, v) -> (,) k <$> f k v) ('toList' m)`
  That is, behaves exactly like a regular 'traverse' except that the traversing
  function also has access to the key associated with a value.

Visibility: export

forWithKey : Applicative t => DMap k f -> (k v -> f v -> t (g v)) -> t (DMap k g)

  *O(n)*.
  `'forWithKey' == 'flip' 'traverseWithKey'` except we cannot actually use
  'flip' because of the lack of impredicative types.

Visibility: export

mapAccumLWithKey : (a -> k v -> f v -> (a, g v)) -> a -> DMap k f -> (a, DMap k g)

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

Visibility: export

mapAccumRWithKey : (a -> k v -> f v -> (a, g v)) -> a -> DMap k f -> (a, DMap k g)

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

Visibility: export

mapKeysWith : DOrd k2 => (k2 v -> f v -> f v -> f v) -> (k1 v -> k2 v) -> DMap k1 f -> DMap k2 f

  *O(n*log n)*.
  `'mapKeysWith' c f s` is the map obtained by applying `f` to each key of `s`.
  
  The size of the result may be smaller if `f` maps two or more distinct
  keys to the same new key.  In this case the associated values will be
  combined using `c`.

Visibility: export

mapKeysMonotonic : (k1 v -> k2 v) -> DMap k1 f -> DMap k2 f

  *O(n)*.
  `'mapKeysMonotonic' f s == 'mapKeys' f s`, but works only when `f`
  is strictly monotonic.
  That is, for any values `x` and `y`, if `x` < `y` then `f x` < `f y`.
  *The precondition is not checked.*
  Semi-formally, we have:
  
  ```
  and [x < y ==> f x < f y | x <- ls, y <- ls]
                      ==> mapKeysMonotonic f s == mapKeys f s
      where ls = keys s
  ```
  
  This means that `f` maps distinct original keys to distinct resulting keys.
  This function has better performance than 'mapKeys'.

Visibility: export

showTreeWith : (k v -> f v -> String) -> Bool -> Bool -> DMap k f -> String

  *O(n)*. The expression (`'showTreeWith' showelem hang wide map`) shows
  the tree that implements the map. Elements are shown using the `showElem` function. If `hang` is
  'True', a *hanging* tree is shown otherwise a rotated tree is shown. If
  `wide` is 'True', an extra wide version is shown.

Visibility: export

showTree : DShow k => DShow f => DMap k f -> String

  *O(n)*. Show the tree that implements the map. The tree is shown
  in a compressed, hanging format. See 'showTreeWith'.

Visibility: export

valid : DOrd k => DMap k f -> Bool

  *O(n)*. Test if the internal map structure is valid.

Visibility: export

genDMap : DOrd k => Range Nat -> Gen (DSum k v) -> Gen (DMap k v)

  Generates a map using a 'Range' to determine the size.

Visibility: export