Idris2Doc : Data.AssocList

Data.AssocList

(source)
Definitions
0 Key : Type
  Totality: total
  Visibility: public export
0 (<) : Maybe Key -> Maybe Key -> Type
  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 6
0 (<=) : Maybe Key -> Maybe Key -> Type
  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 6
data AL : Maybe Key -> Type -> Type
  A provably sorted assoc list with `Bits64` as the key type.
  
  This is mainly useful for short sequences of key / value pairs.
  It comes with O(n) runtime complexity for `insert`, `update`,
  `lookup` and `delete`, but also with fast O(n) complexity for
  `union` and `intersection`.

  Totality: total
  Visibility: public export
  Constructors:
  
Nil : AL Nothing a
  
(::) : (p : (Key, a)) -> AL ix a -> {auto 0 _ : Just (fst p) < ix} -> AL (Just (fst p)) a

  Hints:
  
Eq a => Eq (AL m a)
  
Foldable (AL ix)
  
Functor (AL ix)
  
Show a => Show (AL m a)
  
Traversable (AL ix)
foldlKV_ : (acc -> (Key, el) -> acc) -> acc -> AL m el -> acc
  Totality: total
  Visibility: public export
traverseKV_ : Applicative f => ((Key, a) -> f b) -> AL m a -> f (AL m b)
  Totality: total
  Visibility: public export
lookup_ : Key -> AL ix a -> Maybe a
  Lookup a key in an assoc list.

  Totality: total
  Visibility: public export
nonEmpty_ : AL m a -> Bool
  Totality: total
  Visibility: public export
isEmpty_ : AL m a -> Bool
  Totality: total
  Visibility: public export
pairs_ : AL ix a -> List (Key, a)
  Extracts the key / value pairs from the assoc list.

  Totality: total
  Visibility: public export
keys_ : AL ix a -> List Key
  Extracts the keys from the assoc list.

  Totality: total
  Visibility: public export
values_ : AL ix a -> List a
  Extracts the values from the assoc list.

  Totality: total
  Visibility: public export
length_ : AL ix a -> Nat
  Totality: total
  Visibility: public export
heq : Eq a => AL m a -> AL n a -> Bool
  Heterogeneous equality check.

  Totality: total
  Visibility: public export
record InsertRes : Key -> Maybe Key -> Type -> Type
  Inserting a new key / value pair leads to a new assoc list where the
  key at the head is either equal to the new key or the one previously
  at the head.
  
  @ k  New key that was inserted
  @ mk Key index of the original assoc list

  Totality: total
  Visibility: public export
  Constructor: 
IR : AL (Just firstKey) a -> (0 _ : Either (firstKey = k) (Just firstKey = mk)) -> InsertRes k mk a

  Projections:
  
0 .firstKey : InsertRes k mk a -> Key
  
.pairs : ({rec:0} : InsertRes k mk a) -> AL (Just (firstKey {rec:0})) a
  
0 .prf : ({rec:0} : InsertRes k mk a) -> Either (firstKey {rec:0} = k) (Just (firstKey {rec:0}) = mk)
0 .firstKey : InsertRes k mk a -> Key
  Totality: total
  Visibility: public export
0 firstKey : InsertRes k mk a -> Key
  Totality: total
  Visibility: public export
.pairs : ({rec:0} : InsertRes k mk a) -> AL (Just (firstKey {rec:0})) a
  Totality: total
  Visibility: public export
pairs : ({rec:0} : InsertRes k mk a) -> AL (Just (firstKey {rec:0})) a
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : InsertRes k mk a) -> Either (firstKey {rec:0} = k) (Just (firstKey {rec:0}) = mk)
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : InsertRes k mk a) -> Either (firstKey {rec:0} = k) (Just (firstKey {rec:0}) = mk)
  Totality: total
  Visibility: public export
insert_ : (k : Key) -> a -> AL ix a -> InsertRes k ix a
  Inserts a new key / value pair into an assoc list.
  The result type reflects the possibilities with regard
  to the head pair of the new assoc list.
  
  Note: If the given key `k` is already present in the assoc list,
  its associated value will be replaced with `v`.

  Totality: total
  Visibility: public export
insertWith_ : (a -> a -> a) -> (k : Key) -> a -> AL ix a -> InsertRes k ix a
  Like `insert` but in case `k` is already present in the assoc
  list, the `v` will be cobine with the old value via function `f`.

  Totality: total
  Visibility: public export
record DeleteRes : Maybe Key -> Type -> Type
  Deleting an entry from an assoc list results in a new assoc list
  the index of which is equal to or smaller than the one from
  the original list.
  
  @ m1 : Key index of the original assoc list.

  Totality: total
  Visibility: public export
  Constructor: 
DR : AL mx a -> (0 _ : m1 <= mx) -> DeleteRes m1 a

  Projections:
  
0 .mx : DeleteRes m1 a -> Maybe Key
  
.pairs : ({rec:0} : DeleteRes m1 a) -> AL (mx {rec:0}) a
  
0 .prf : ({rec:0} : DeleteRes m1 a) -> m1 <= mx {rec:0}
0 .mx : DeleteRes m1 a -> Maybe Key
  Totality: total
  Visibility: public export
0 mx : DeleteRes m1 a -> Maybe Key
  Totality: total
  Visibility: public export
.pairs : ({rec:0} : DeleteRes m1 a) -> AL (mx {rec:0}) a
  Totality: total
  Visibility: public export
pairs : ({rec:0} : DeleteRes m1 a) -> AL (mx {rec:0}) a
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : DeleteRes m1 a) -> m1 <= mx {rec:0}
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : DeleteRes m1 a) -> m1 <= mx {rec:0}
  Totality: total
  Visibility: public export
prependDR : (p : (Key, a)) -> DeleteRes m a -> {auto 0 _ : Just (fst p) < m} -> DeleteRes (Just (fst p)) a
  Totality: total
  Visibility: export
delete_ : Key -> AL m a -> DeleteRes m a
  Tries to remove the entry with the given key from the
  assoc list. The key index of the result will be equal to
  or greater than `m`.

  Totality: total
  Visibility: export
mapMaybe_ : (a -> Maybe b) -> AL m a -> DeleteRes m b
  Applies the given function to all values, keeping only the
  `Just` results.

  Totality: total
  Visibility: export
mapMaybeK_ : (Key -> a -> Maybe b) -> AL m a -> DeleteRes m b
  Applies the given function to all key / value pairs, keeping only the
  `Just` results.

  Totality: total
  Visibility: export
update_ : Key -> (a -> a) -> AL m a -> AL m a
  Updates the value at the given position by applying the given function.

  Totality: total
  Visibility: export
updateA_ : Applicative f => Key -> (a -> f a) -> AL m a -> f (AL m a)
  Updates the value at the given position by applying the given effectful
  computation.

  Totality: total
  Visibility: export
record UnionRes : Maybe Key -> Maybe Key -> Type -> Type
  Result of computing the union of two assoc lists with
  key indices `m1` and `m2`. The result's key index is equal to either
  `m1` or `m2`

  Totality: total
  Visibility: public export
  Constructor: 
UR : AL mx a -> (0 _ : Either (m1 = mx) (m2 = mx)) -> UnionRes m1 m2 a

  Projections:
  
0 .mx : UnionRes m1 m2 a -> Maybe Key
  
.pairs : ({rec:0} : UnionRes m1 m2 a) -> AL (mx {rec:0}) a
  
0 .prf : ({rec:0} : UnionRes m1 m2 a) -> Either (m1 = mx {rec:0}) (m2 = mx {rec:0})
0 .mx : UnionRes m1 m2 a -> Maybe Key
  Totality: total
  Visibility: public export
0 mx : UnionRes m1 m2 a -> Maybe Key
  Totality: total
  Visibility: public export
.pairs : ({rec:0} : UnionRes m1 m2 a) -> AL (mx {rec:0}) a
  Totality: total
  Visibility: public export
pairs : ({rec:0} : UnionRes m1 m2 a) -> AL (mx {rec:0}) a
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : UnionRes m1 m2 a) -> Either (m1 = mx {rec:0}) (m2 = mx {rec:0})
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : UnionRes m1 m2 a) -> Either (m1 = mx {rec:0}) (m2 = mx {rec:0})
  Totality: total
  Visibility: public export
prepLT : (p : (Key, a)) -> UnionRes m1 (Just k2) a -> {auto 0 _ : Just (fst p) < m1} -> {auto 0 _ : Just (fst p) < Just k2} -> UnionRes (Just (fst p)) (Just k2) a
  Totality: total
  Visibility: public export
prepGT : (p : (Key, a)) -> UnionRes (Just k1) m2 a -> {auto 0 _ : Just (fst p) < m2} -> {auto 0 _ : Just (fst p) < Just k1} -> UnionRes (Just k1) (Just (fst p)) a
  Totality: total
  Visibility: public export
prepEQ : (p : (Key, a)) -> (0 _ : fst p = k) -> UnionRes m1 m2 a -> {auto 0 _ : Just (fst p) < m1} -> {auto 0 _ : Just k < m2} -> UnionRes (Just (fst p)) x a
  Totality: total
  Visibility: public export
union_ : AL m1 a -> AL m2 a -> UnionRes m1 m2 a
  Computes the union of two assoc lists.
  
  In case of identical keys, the value of the second list
  is dropped. Use `unionWith` for better control over handling
  duplicate entries.

  Totality: total
  Visibility: public export
unionMap_ : (a -> a -> b) -> (a -> b) -> AL m1 a -> AL m2 a -> UnionRes m1 m2 b
  Like `union` but in case of identical keys appearing in
  both lists, the associated values are combined using
  function `f`. Otherwise, values are converted with `g`.

  Totality: total
  Visibility: public export
unionWith_ : (a -> a -> a) -> AL m1 a -> AL m2 a -> UnionRes m1 m2 a
  Like `union` but in case of identical keys appearing in
  both lists, the associated values are combined using
  function `f`.

  Totality: total
  Visibility: public export
record IntersectRes : Maybe Key -> Maybe Key -> Type -> Type
  The result of building the intersection of two assoc lists may
  contain an arbitrary new key index, which is not smaller than
  the head indices of the original lists.

  Totality: total
  Visibility: public export
  Constructor: 
IS : AL mx a -> (0 _ : m1 <= mx) -> (0 _ : m2 <= mx) -> IntersectRes m1 m2 a

  Projections:
  
0 .mx : IntersectRes m1 m2 a -> Maybe Key
  
.pairs : ({rec:0} : IntersectRes m1 m2 a) -> AL (mx {rec:0}) a
  
0 .prf1 : ({rec:0} : IntersectRes m1 m2 a) -> m1 <= mx {rec:0}
  
0 .prf2 : ({rec:0} : IntersectRes m1 m2 a) -> m2 <= mx {rec:0}
0 .mx : IntersectRes m1 m2 a -> Maybe Key
  Totality: total
  Visibility: public export
0 mx : IntersectRes m1 m2 a -> Maybe Key
  Totality: total
  Visibility: public export
.pairs : ({rec:0} : IntersectRes m1 m2 a) -> AL (mx {rec:0}) a
  Totality: total
  Visibility: public export
pairs : ({rec:0} : IntersectRes m1 m2 a) -> AL (mx {rec:0}) a
  Totality: total
  Visibility: public export
0 .prf1 : ({rec:0} : IntersectRes m1 m2 a) -> m1 <= mx {rec:0}
  Totality: total
  Visibility: public export
0 prf1 : ({rec:0} : IntersectRes m1 m2 a) -> m1 <= mx {rec:0}
  Totality: total
  Visibility: public export
0 .prf2 : ({rec:0} : IntersectRes m1 m2 a) -> m2 <= mx {rec:0}
  Totality: total
  Visibility: public export
0 prf2 : ({rec:0} : IntersectRes m1 m2 a) -> m2 <= mx {rec:0}
  Totality: total
  Visibility: public export
prependIS : (p : (Key, a)) -> (0 _ : fst p = k) -> IntersectRes m1 m2 a -> {auto 0 _ : Just (fst p) < m1} -> IntersectRes (Just (fst p)) (Just k) a
  Totality: total
  Visibility: public export
intersect_ : AL m1 a -> AL m2 a -> IntersectRes m1 m2 a
  Computes the intersection of two assoc lists, keeping
  only entries appearing in both lists. Only the values of
  the first list are being kept.

  Totality: total
  Visibility: public export
intersectWith_ : (a -> a -> b) -> AL m1 a -> AL m2 a -> IntersectRes m1 m2 b
  Computes the intersection of two assoc lists, keeping
  only entries appearing in both lists. Values of the two
  lists are combine using function `f`.

  Totality: total
  Visibility: public export
record AssocList : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkAL : AL firstKey a -> AssocList a

  Projections:
  
0 .firstKey : AssocList a -> Maybe Key
  
.repr : ({rec:0} : AssocList a) -> AL (firstKey {rec:0}) a

  Hints:
  
Eq a => Eq (AssocList a)
  
Foldable AssocList
  
Functor AssocList
  
Show a => Show (AssocList a)
  
Traversable AssocList
0 .firstKey : AssocList a -> Maybe Key
  Totality: total
  Visibility: public export
0 firstKey : AssocList a -> Maybe Key
  Totality: total
  Visibility: public export
.repr : ({rec:0} : AssocList a) -> AL (firstKey {rec:0}) a
  Totality: total
  Visibility: public export
repr : ({rec:0} : AssocList a) -> AL (firstKey {rec:0}) a
  Totality: total
  Visibility: public export
foldlKV : (acc -> (Key, el) -> acc) -> acc -> AssocList el -> acc
  Totality: total
  Visibility: public export
traverseKV : Applicative f => ((Key, a) -> f b) -> AssocList a -> f (AssocList b)
  Totality: total
  Visibility: public export
lookup : Key -> AssocList a -> Maybe a
  Lookup a key in an assoc list.

  Totality: total
  Visibility: public export
nonEmpty : AssocList a -> Bool
  Totality: total
  Visibility: public export
isEmpty : AssocList a -> Bool
  Totality: total
  Visibility: public export
pairs : AssocList a -> List (Key, a)
  Extracts the key / value pairs from the assoc list.

  Totality: total
  Visibility: public export
keys : AssocList a -> List Key
  Extracts the keys from the assoc list.

  Totality: total
  Visibility: public export
values : AssocList a -> List a
  Extracts the values from the assoc list.

  Totality: total
  Visibility: public export
length : AssocList a -> Nat
  Totality: total
  Visibility: public export
insert : Key -> a -> AssocList a -> AssocList a
  Inserts a new key / value pair into an assoc list.
  The result type reflects the possibilities with regard
  to the head pair of the new assoc list.
  
  Note: If the given key `k` is already present in the assoc list,
  its associated value will be replaced with `v`.

  Totality: total
  Visibility: public export
insertWith : (a -> a -> a) -> Key -> a -> AssocList a -> AssocList a
  Like `insert` but in case `k` is already present in the assoc
  list, the `v` will be cobine with the old value via function `f`.

  Totality: total
  Visibility: public export
fromList : List (Key, a) -> AssocList a
  Totality: total
  Visibility: public export
delete : Key -> AssocList a -> AssocList a
  Tries to remove the entry with the given key from the
  assoc list. The key index of the result will be equal to
  or greater than `m`.

  Totality: total
  Visibility: public export
mapMaybe : (a -> Maybe b) -> AssocList a -> AssocList b
  Applies the given function to all values, keeping only the
  `Just` results.

  Totality: total
  Visibility: public export
mapMaybeK : (Key -> a -> Maybe b) -> AssocList a -> AssocList b
  Applies the given function to all key / value pairs, keeping only the
  `Just` results.

  Totality: total
  Visibility: public export
update : Key -> (a -> a) -> AssocList a -> AssocList a
  Updates the value at the given position by applying the given function.

  Totality: total
  Visibility: public export
updateA : Applicative f => Key -> (a -> f a) -> AssocList a -> f (AssocList a)
  Updates the value at the given position by applying the given effectful
  computation.

  Totality: total
  Visibility: public export
union : AssocList a -> AssocList a -> AssocList a
  Computes the union of two assoc lists.
  
  In case of identical keys, the value of the second list
  is dropped. Use `unionWith` for better control over handling
  duplicate entries.

  Totality: total
  Visibility: public export
unionMap : (a -> a -> b) -> (a -> b) -> AssocList a -> AssocList a -> AssocList b
  Like `union` but in case of identical keys appearing in
  both lists, the associated values are combined using
  function `f`. Otherwise, values are converted with `g`.

  Totality: total
  Visibility: public export
unionWith : (a -> a -> a) -> AssocList a -> AssocList a -> AssocList a
  Like `union` but in case of identical keys appearing in
  both lists, the associated values are combined using
  function `f`.

  Totality: total
  Visibility: public export
intersect : AssocList a -> AssocList a -> AssocList a
  Computes the intersection of two assoc lists, keeping
  only entries appearing in both lists. Only the values of
  the first list are being kept.

  Totality: total
  Visibility: public export
intersectWith : (a -> a -> b) -> AssocList a -> AssocList a -> AssocList b
  Computes the intersection of two assoc lists, keeping
  only entries appearing in both lists. Values of the two
  lists are combine using function `f`.

  Totality: total
  Visibility: public export