Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.AssocList

Description

Additional functions for association lists.

Synopsis

- type AssocList k v = [(k, v)]
- apply :: Ord k => AssocList k v -> k -> Maybe v
- keys :: AssocList k v -> [k]
- insert :: k -> v -> AssocList k v -> AssocList k v
- update :: Eq k => k -> v -> AssocList k v -> AssocList k v
- delete :: Eq k => k -> AssocList k v -> AssocList k v
- updateAt :: Eq k => k -> (v -> v) -> AssocList k v -> AssocList k v
- mapWithKey :: (k -> v -> v) -> AssocList k v -> AssocList k v
- mapWithKeyM :: Applicative m => (k -> v -> m v) -> AssocList k v -> m (AssocList k v)
- mapKeysMonotonic :: (k -> k') -> AssocList k v -> AssocList k' v
- lookup :: Eq a => a -> [(a, b)] -> Maybe b

# Documentation

type AssocList k v = [(k, v)] Source #

A finite map, represented as a set of pairs.

Invariant: at most one value per key.

apply :: Ord k => AssocList k v -> k -> Maybe v Source #

Lookup keys in the same association list often. Use partially applied to create partial function `apply m :: k -> Maybe v`.

- First time: `O(n log n)` in the worst case.
- Subsequently: `O(log n)`.

Specification: `apply m == (`lookup` m)`.

keys :: AssocList k v -> [k] Source #

O(n). Get the domain (list of keys) of the finite map.

insert :: k -> v -> AssocList k v -> AssocList k v Source #

O(1). Add a new binding. Assumes the binding is not yet in the list.

update :: Eq k => k -> v -> AssocList k v -> AssocList k v Source #

O(n). Update the value at a key. The key must be in the domain of the finite map. Otherwise, an internal error is raised.

delete :: Eq k => k -> AssocList k v -> AssocList k v Source #

O(n). Delete a binding. The key must be in the domain of the finite map. Otherwise, an internal error is raised.

updateAt :: Eq k => k -> (v -> v) -> AssocList k v -> AssocList k v Source #

O(n). Update the value at a key with a certain function. The key must be in the domain of the finite map. Otherwise, an internal error is raised.

mapWithKey :: (k -> v -> v) -> AssocList k v -> AssocList k v Source #

O(n). Map over an association list, preserving the order.

mapWithKeyM :: Applicative m => (k -> v -> m v) -> AssocList k v -> m (AssocList k v) Source #

O(n). If called with a effect-producing function, violation of the invariant could matter here (duplicating effects).

mapKeysMonotonic :: (k -> k') -> AssocList k v -> AssocList k' v Source #

O(n). Named in analogy to `mapKeysMonotonic`. To preserve the invariant, it is sufficient that the key transformation is injective (rather than monotonic).

lookup :: Eq a => a -> [(a, b)] -> Maybe b Source #

\(\mathcal{O}(n)\). `lookup` `key assocs` looks up a key in an association list.

    >>> lookup 2 []
    Nothing
    >>> lookup 2 [(1, "first")]
    Nothing
    >>> lookup 2 [(1, "first"), (2, "second"), (3, "third")]
    Just "second"