{-# LANGUAGE CPP #-}
module Agda.Utils.AssocList where
import Prelude hiding (lookup)
import qualified Data.List as List
import Data.Function
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
type AssocList k v = [(k,v)]
lookup :: Eq k => k -> AssocList k v -> Maybe v
lookup = List.lookup
keys :: AssocList k v -> [k]
keys = map fst
insert :: k -> v -> AssocList k v -> AssocList k v
insert k v = ((k,v) :)
update :: Eq k => k -> v -> AssocList k v -> AssocList k v
update k v = updateAt k $ const v
delete :: Eq k => k -> AssocList k v -> AssocList k v
delete k = List.deleteBy ((==) `on` fst) (k, __IMPOSSIBLE__)
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
mapWithKey :: (k -> v -> v) -> AssocList k v -> AssocList k v
mapWithKey f = map $ \ (k,v) -> (k, f k v)
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 g [] = pure []
mapM g (x : xs) = (:) <$> g x <*> mapM g xs
mapKeysMonotonic :: (k -> k') -> AssocList k v -> AssocList k' v
mapKeysMonotonic f = map $ mapFst f