content: {-# OPTIONS_GHC -Wunused-imports #-}
  
  -- | Additional functions for association lists.
  
  module Agda.Utils.AssocList
    ( module Agda.Utils.AssocList
    , lookup
    ) where
  
  import Prelude hiding (lookup)
  
  import Data.Function (on)
  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 m = (`Map.lookup` Map.fromListWith (\ _new old -> old) m)
  
  -- | O(n).
  --   Get the domain (list of keys) of the finite map.
  keys :: AssocList k v -> [k]
  keys = map 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 k v = ((k,v) :)
  
  -- | 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 k v = updateAt k $ const 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 k = List.deleteBy ((==) `on` fst) (k, __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 k f = loop where
    loop []       = __IMPOSSIBLE__
    loop (p@(k',v) : ps)
      | k == k'   = (k, f v) : ps
      | otherwise = p : loop ps
  
  -- | O(n).
  --   Map over an association list, preserving the order.
  mapWithKey :: (k -> v -> v) -> AssocList k v -> AssocList k v
  mapWithKey f = map $ \ (k,v) -> (k, f k 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 f = mapM $ \ (k,v) -> (k,) <$> f k v
    where
      -- mapM is applicative!
      mapM g [] = pure []
      mapM g (x : xs) = (:) <$> g x <*> mapM g 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 f = map $ mapFst f
  