    module Agda.Utils.Map where

    import Data.Functor.Compose
    import Data.Map (Map)
    import qualified Data.Map as Map
    -- import Data.Maybe (mapMaybe) -- UNUSED

    import Agda.Utils.Impossible

    -- * Monadic map operations
    ---------------------------------------------------------------------------

    -- | Update monadically the value at one position (must exist!).
    adjustM :: (Functor f, Ord k) => (v -> f v) -> k -> Map k v -> f (Map k v)
    adjustM :: forall (f :: * -> *) k v.
    (Functor f, Ord k) =>
    (v -> f v) -> k -> Map k v -> f (Map k v)
    adjustM v -> f v
    f = (Maybe v -> f (Maybe v)) -> k -> Map k v -> f (Map k v)
    forall (f :: * -> *) k a.
    (Functor f, Ord k) =>
    (Maybe a -> f (Maybe a)) -> k -> Map k a -> f (Map k a)
    Map.alterF ((Maybe v -> f (Maybe v)) -> k -> Map k v -> f (Map k v))
    -> (Maybe v -> f (Maybe v)) -> k -> Map k v -> f (Map k v)
    forall a b. (a -> b) -> a -> b
    $ \case
      Maybe v
    Nothing -> f (Maybe v)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      Just v
    v  -> v -> Maybe v
    forall a. a -> Maybe a
    Just (v -> Maybe v) -> f v -> f (Maybe v)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> v -> f v
    f v
    v

    -- | Wrapper for 'adjustM' for convenience.
    adjustM' :: (Functor f, Ord k) => (v -> f (a, v)) -> k -> Map k v -> f (a, Map k v)
    adjustM' :: forall (f :: * -> *) k v a.
    (Functor f, Ord k) =>
    (v -> f (a, v)) -> k -> Map k v -> f (a, Map k v)
    adjustM' v -> f (a, v)
    f k
    k = Compose f ((,) a) (Map k v) -> f (a, Map k v)
    forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
    Compose f g a -> f (g a)
    getCompose (Compose f ((,) a) (Map k v) -> f (a, Map k v))
    -> (Map k v -> Compose f ((,) a) (Map k v))
    -> Map k v
    -> f (a, Map k v)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (v -> Compose f ((,) a) v)
    -> k -> Map k v -> Compose f ((,) a) (Map k v)
    forall (f :: * -> *) k v.
    (Functor f, Ord k) =>
    (v -> f v) -> k -> Map k v -> f (Map k v)
    adjustM (f (a, v) -> Compose f ((,) a) v
    forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose (f (a, v) -> Compose f ((,) a) v)
    -> (v -> f (a, v)) -> v -> Compose f ((,) a) v
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . v -> f (a, v)
    f) k
    k

    -- UNUSED Liang-Ting Chen (05-07-2019)
    -- data EitherOrBoth a b = L a | B a b | R b
    --
    -- -- | Not very efficient (goes via a list), but it'll do.
    -- unionWithM :: (Ord k, Monad m) => (a -> a -> m a) -> Map k a -> Map k a -> m (Map k a)
    -- unionWithM f m1 m2 = fromList <$> mapM combine (toList m)
    --     where
    --         m = unionWith both (map L m1) (map R m2)
    --
    --         both (L a) (R b) = B a b
    --         both _     _     = __IMPOSSIBLE__
    --
    --         combine (k, B a b) = (,) k <$> f a b
    --         combine (k, L a)   = return (k, a)
    --         combine (k, R b)   = return (k, b)
    --
    -- UNUSED Liang-Ting Chen (05-07-2019)
    -- insertWithKeyM :: (Ord k, Monad m) => (k -> a -> a -> m a) -> k -> a -> Map k a -> m (Map k a)
    -- insertWithKeyM clash k x m =
    --     case lookup k m of
    --         Just y  -> do
    --             z <- clash k x y
    --             return $ insert k z m
    --         Nothing -> return $ insert k x m

    -- * Non-monadic map operations
    ---------------------------------------------------------------------------

    -- UNUSED Liang-Ting Chen (05-07-2019)
    -- -- | Big conjunction over a map.
    -- allWithKey :: (k -> a -> Bool) -> Map k a -> Bool
    -- allWithKey f = Map.foldrWithKey (\ k a b -> f k a && b) True

    -- | Filter a map based on the keys.
    filterKeys :: (k -> Bool) -> Map k a -> Map k a
    filterKeys :: forall k a. (k -> Bool) -> Map k a -> Map k a
    filterKeys k -> Bool
    p = (k -> a -> Bool) -> Map k a -> Map k a
    forall k a. (k -> a -> Bool) -> Map k a -> Map k a
    Map.filterWithKey (Bool -> a -> Bool
    forall a b. a -> b -> a
    const (Bool -> a -> Bool) -> (k -> Bool) -> k -> a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . k -> Bool
    p)

    -- UNUSED Andreas (2021-08-19)
    -- -- | O(n log n).  Rebuilds the map from scratch.
    -- --   Not worse than 'Map.mapKeys'.
    -- mapMaybeKeys :: (Ord k1, Ord k2) => (k1 -> Maybe k2) -> Map k1 a -> Map k2 a
    -- mapMaybeKeys f = Map.fromList . mapMaybe (\ (k,a) -> (,a) <$> f k) . Map.toList

    -- UNUSED Liang-Ting Chen (05-07-2019)
    -- -- | Unzip a map.
    -- unzip :: Map k (a, b) -> (Map k a, Map k b)
    -- unzip m = (Map.map fst m, Map.map snd m)
    --
    -- UNUSED Liang-Ting Chen (05-07-2019)
    -- unzip3 :: Map k (a, b, c) -> (Map k a, Map k b, Map k c)
    -- unzip3 m = (Map.map fst3 m, Map.map snd3 m, Map.map thd3 m)
    --