{-# LANGUAGE CPP #-}
module Agda.Utils.Map where
import Prelude hiding (map, lookup, mapM)
import Data.Map as Map
import Data.Traversable
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
data EitherOrBoth a b = L a | B a b | R b
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)
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
allWithKey :: (k -> a -> Bool) -> Map k a -> Bool
allWithKey f = Map.foldrWithKey (\ k a b -> f k a && b) True
filterKeys :: (k -> Bool) -> Map k a -> Map k a
filterKeys p = filterWithKey (const . p)
unzip :: Map k (a, b) -> (Map k a, Map k b)
unzip m = (Map.map fst m, Map.map snd m)
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)