module Agda.Utils.Map where
import Data.Functor.Compose
import Data.Map (Map)
import qualified Data.Map as Map
import Agda.Utils.Impossible
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
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
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)