Data.SortedMap.Dependent

Definitions

data SortedDMap : (k : Type) -> (k -> Type) -> Type

Totality: total
Visibility: export
Constructors:

Empty : Ord k => SortedDMap k v

M : {auto o : Ord k} -> (n : Nat) -> Tree n k v o -> SortedDMap k v

Hints:

Cast (SortedDMap k (const v)) (SortedMap k v)

Cast (SortedMap k v) (SortedDMap k (const v))

(DecEq k, Eq (v x)) => Eq (SortedDMap k v)

DecEq k => Ord k => Semigroup (v x) => Monoid (SortedDMap k v)

DecEq k => Semigroup (v x) => Semigroup (SortedDMap k v)

(Show k, Show (v x)) => Show (SortedDMap k v)

empty : Ord k => SortedDMap k v

Visibility: export

lookup : k -> SortedDMap k v -> Maybe (y : k ** v y)

Visibility: export

lookupPrecise : DecEq k => (x : k) -> SortedDMap k v -> Maybe (v x)

Visibility: export

insert : (x : k) -> v x -> SortedDMap k v -> SortedDMap k v

Visibility: export

singleton : Ord k => (x : k) -> v x -> SortedDMap k v

Visibility: export

insertFrom : Foldable f => f (x : k ** v x) -> SortedDMap k v -> SortedDMap k v

Visibility: export

delete : k -> SortedDMap k v -> SortedDMap k v

Visibility: export

update : DecEq k => (x : k) -> (Maybe (v x) -> Maybe (v x)) -> SortedDMap k v -> SortedDMap k v

  Updates or deletes a value based on the decision function
  
  The decision function takes information about the presence of the value,
  and the value itself, if it is present.
  It returns a new value or the fact that there should be no value as the result.
  
  The current implementation performs up to two traversals of the original map

Visibility: export

updateExisting : DecEq k => (x : k) -> (v x -> v x) -> SortedDMap k v -> SortedDMap k v

  Updates existing value, if it is present, and does nothing otherwise
  
  The current implementation performs up to two traversals of the original map

Visibility: export

fromList : Ord k => List (x : k ** v x) -> SortedDMap k v

Visibility: export

toList : SortedDMap k v -> List (x : k ** v x)

Visibility: export

keys : SortedDMap k v -> List k

  Gets the keys of the map.

Visibility: export

values : SortedDMap k v -> List (x : k ** v x)

Visibility: export

map : (v x -> w x) -> SortedDMap k v -> SortedDMap k w

Visibility: export

foldl : (acc -> (x : k ** v x) -> acc) -> acc -> SortedDMap k v -> acc

Visibility: export

foldr : ((x : k ** v x) -> acc -> acc) -> acc -> SortedDMap k v -> acc

Visibility: export

foldlM : Monad m => (acc -> (x : k ** v x) -> m acc) -> acc -> SortedDMap k v -> m acc

Visibility: export

foldMap : Monoid m => ((x : k) -> v x -> m) -> SortedDMap k v -> m

Visibility: export

null : SortedDMap k v -> Bool

Visibility: export

traverse : Applicative f => (v x -> f (w x)) -> SortedDMap k v -> f (SortedDMap k w)

Visibility: export

mergeWith : DecEq k => (v x -> v x -> v x) -> SortedDMap k v -> SortedDMap k v -> SortedDMap k v

  Merge two maps. When encountering duplicate keys, using a function to combine the values.
  Uses the ordering of the first map given.

Visibility: export

merge : DecEq k => Semigroup (v x) => SortedDMap k v -> SortedDMap k v -> SortedDMap k v

  Merge two maps using the Semigroup (and by extension, Monoid) operation.
  Uses mergeWith internally, so the ordering of the left map is kept.

Visibility: export

mergeLeft : DecEq k => SortedDMap k v -> SortedDMap k v -> SortedDMap k v

  Left-biased merge, also keeps the ordering specified  by the left map.

Visibility: export

lookupBetween : k -> SortedDMap k v -> (Maybe (x : k ** v x), Maybe (x : k ** v x))

  looks up a key in map, returning the left and right closest values, so that
   k1 <= k < k2. If at the end of the beginning and/or end of the sorted map, returns
  nothing appropriately

Visibility: export

leftMost : SortedDMap k v -> Maybe (x : k ** v x)

  Returns the leftmost (least) key and value

Visibility: export

rightMost : SortedDMap k v -> Maybe (x : k ** v x)

  Returns the rightmost (greatest) key and value

Visibility: export

strictSubmap : DecEq k => Eq (v x) => SortedDMap k v -> SortedDMap k v -> Bool

Visibility: export