    -- | Additional functions for association lists.

    module Agda.Utils.AssocList
      ( module Agda.Utils.AssocList
      , lookup
      ) where

    import Prelude hiding (lookup)

    import Data.Function
    import Data.List (lookup)
    import qualified Data.List as List
    import qualified Data.Map  as Map

    import Agda.Utils.Tuple

    import Agda.Utils.Impossible

    -- | A finite map, represented as a set of pairs.
    --
    --   Invariant: at most one value per key.
    type AssocList k v = [(k,v)]

    -- Lookup, reexported from Data.List.
    -- O(n).
    -- lookup :: Eq k => k -> AssocList k v -> Maybe v

    -- | 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)@.
    apply :: Ord k => AssocList k v -> k -> Maybe v
    apply :: forall k v. Ord k => AssocList k v -> k -> Maybe v
    apply AssocList k v
    m = (k -> Map k v -> Maybe v
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` (v -> v -> v) -> AssocList k v -> Map k v
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith (\ v
    _new v
    old -> v
    old) AssocList k v
    m)

    -- | O(n).
    --   Get the domain (list of keys) of the finite map.
    keys :: AssocList k v -> [k]
    keys :: forall k v. AssocList k v -> [k]
    keys = ((k, v) -> k) -> [(k, v)] -> [k]
    forall a b. (a -> b) -> [a] -> [b]
    map (k, v) -> k
    forall a b. (a, b) -> a
    fst

    -- | O(1).
    --   Add a new binding.
    --   Assumes the binding is not yet in the list.
    insert :: k -> v -> AssocList k v -> AssocList k v
    insert :: forall k v. k -> v -> AssocList k v -> AssocList k v
    insert k
    k v
    v = ((k
    k,v
    v) (k, v) -> [(k, v)] -> [(k, v)]
    forall a. a -> [a] -> [a]
    :)

    -- | 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.
    update :: Eq k => k -> v -> AssocList k v -> AssocList k v
    update :: forall k v. Eq k => k -> v -> AssocList k v -> AssocList k v
    update k
    k v
    v = k -> (v -> v) -> AssocList k v -> AssocList k v
    forall k v. Eq k => k -> (v -> v) -> AssocList k v -> AssocList k v
    updateAt k
    k ((v -> v) -> AssocList k v -> AssocList k v)
    -> (v -> v) -> AssocList k v -> AssocList k v
    forall a b. (a -> b) -> a -> b
    $ v -> v -> v
    forall a b. a -> b -> a
    const v
    v

    -- | O(n).
    --   Delete a binding.
    --   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
    delete :: forall k v. Eq k => k -> AssocList k v -> AssocList k v
    delete k
    k = ((k, v) -> (k, v) -> Bool) -> (k, v) -> [(k, v)] -> [(k, v)]
    forall a. (a -> a -> Bool) -> a -> [a] -> [a]
    List.deleteBy (k -> k -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (k -> k -> Bool) -> ((k, v) -> k) -> (k, v) -> (k, v) -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (k, v) -> k
    forall a b. (a, b) -> a
    fst) (k
    k, v
    forall a. HasCallStack => a
    __IMPOSSIBLE__)

    -- | 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.
    updateAt :: Eq k => k -> (v -> v) -> AssocList k v -> AssocList k v
    updateAt :: forall k v. Eq k => k -> (v -> v) -> AssocList k v -> AssocList k v
    updateAt k
    k v -> v
    f = [(k, v)] -> [(k, v)]
    loop where
      loop :: [(k, v)] -> [(k, v)]
    loop []       = [(k, v)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      loop (p :: (k, v)
    p@(k
    k',v
    v) : [(k, v)]
    ps)
        | k
    k k -> k -> Bool
    forall a. Eq a => a -> a -> Bool
    == k
    k'   = (k
    k, v -> v
    f v
    v) (k, v) -> [(k, v)] -> [(k, v)]
    forall a. a -> [a] -> [a]
    : [(k, v)]
    ps
        | Bool
    otherwise = (k, v)
    p (k, v) -> [(k, v)] -> [(k, v)]
    forall a. a -> [a] -> [a]
    : [(k, v)] -> [(k, v)]
    loop [(k, v)]
    ps

    -- | O(n).
    --   Map over an association list, preserving the order.
    mapWithKey :: (k -> v -> v) -> AssocList k v -> AssocList k v
    mapWithKey :: forall k v. (k -> v -> v) -> AssocList k v -> AssocList k v
    mapWithKey k -> v -> v
    f = ((k, v) -> (k, v)) -> [(k, v)] -> [(k, v)]
    forall a b. (a -> b) -> [a] -> [b]
    map (((k, v) -> (k, v)) -> [(k, v)] -> [(k, v)])
    -> ((k, v) -> (k, v)) -> [(k, v)] -> [(k, v)]
    forall a b. (a -> b) -> a -> b
    $ \ (k
    k,v
    v) -> (k
    k, k -> v -> v
    f k
    k v
    v)

    -- | O(n).
    --   If called with a effect-producing function, violation of the invariant
    --   could matter here (duplicating effects).
    mapWithKeyM :: Applicative m => (k -> v -> m v) -> AssocList k v -> m (AssocList k v)
    mapWithKeyM :: forall (m :: * -> *) k v.
    Applicative m =>
    (k -> v -> m v) -> AssocList k v -> m (AssocList k v)
    mapWithKeyM k -> v -> m v
    f = ((k, v) -> m (k, v)) -> [(k, v)] -> m [(k, v)]
    forall {f :: * -> *} {t} {a}.
    Applicative f =>
    (t -> f a) -> [t] -> f [a]
    mapM (((k, v) -> m (k, v)) -> [(k, v)] -> m [(k, v)])
    -> ((k, v) -> m (k, v)) -> [(k, v)] -> m [(k, v)]
    forall a b. (a -> b) -> a -> b
    $ \ (k
    k,v
    v) -> (k
    k,) (v -> (k, v)) -> m v -> m (k, v)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> k -> v -> m v
    f k
    k v
    v
      where
        -- mapM is applicative!
        mapM :: (t -> f a) -> [t] -> f [a]
    mapM t -> f a
    g [] = [a] -> f [a]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
        mapM t -> f a
    g (t
    x : [t]
    xs) = (:) (a -> [a] -> [a]) -> f a -> f ([a] -> [a])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t -> f a
    g t
    x f ([a] -> [a]) -> f [a] -> f [a]
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (t -> f a) -> [t] -> f [a]
    mapM t -> f a
    g [t]
    xs

    -- | O(n).
    --   Named in analogy to 'Data.Map.mapKeysMonotonic'.
    --   To preserve the invariant, it is sufficient that the key
    --   transformation is injective (rather than monotonic).
    mapKeysMonotonic :: (k -> k') -> AssocList k v -> AssocList k' v
    mapKeysMonotonic :: forall k k' v. (k -> k') -> AssocList k v -> AssocList k' v
    mapKeysMonotonic k -> k'
    f = ((k, v) -> (k', v)) -> [(k, v)] -> [(k', v)]
    forall a b. (a -> b) -> [a] -> [b]
    map (((k, v) -> (k', v)) -> [(k, v)] -> [(k', v)])
    -> ((k, v) -> (k', v)) -> [(k, v)] -> [(k', v)]
    forall a b. (a -> b) -> a -> b
    $ (k -> k') -> (k, v) -> (k', v)
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst k -> k'
    f