1{-# LANGUAGE CPP #-} 2 3module Agda.Utils.Map where 4 5import Data.Functor.Compose 6import Data.Map (Map) 7import qualified Data.Map as Map 8import Data.Maybe (mapMaybe) 9 10import Agda.Utils.Functor 11import Agda.Utils.Impossible 12 13-- * Monadic map operations 14--------------------------------------------------------------------------- 15 16-- | Update monadically the value at one position (must exist!). 17adjustM :: (Functor f, Ord k) => (v -> f v) -> k -> Map k v -> f (Map k v) 18#if MIN_VERSION_containers(0,5,8) 19adjustM f = Map.alterF $ \case 20 Nothing -> __IMPOSSIBLE__ 21 Just v -> Just <$> f v 22#else 23adjustM f k m = 24 f (Map.findWithDefault __IMPOSSIBLE__ k m) <&> \ v -> Map.insert k v m 25#endif 26 27-- | Wrapper for 'adjustM' for convenience. 28adjustM' :: (Functor f, Ord k) => (v -> f (a, v)) -> k -> Map k v -> f (a, Map k v) 29adjustM' f k = getCompose . adjustM (Compose . f) k 30 31-- UNUSED Liang-Ting Chen (05-07-2019) 32-- data EitherOrBoth a b = L a | B a b | R b 33-- 34-- -- | Not very efficient (goes via a list), but it'll do. 35-- unionWithM :: (Ord k, Monad m) => (a -> a -> m a) -> Map k a -> Map k a -> m (Map k a) 36-- unionWithM f m1 m2 = fromList <$> mapM combine (toList m) 37-- where 38-- m = unionWith both (map L m1) (map R m2) 39-- 40-- both (L a) (R b) = B a b 41-- both _ _ = __IMPOSSIBLE__ 42-- 43-- combine (k, B a b) = (,) k <$> f a b 44-- combine (k, L a) = return (k, a) 45-- combine (k, R b) = return (k, b) 46-- 47-- UNUSED Liang-Ting Chen (05-07-2019) 48-- insertWithKeyM :: (Ord k, Monad m) => (k -> a -> a -> m a) -> k -> a -> Map k a -> m (Map k a) 49-- insertWithKeyM clash k x m = 50-- case lookup k m of 51-- Just y -> do 52-- z <- clash k x y 53-- return $ insert k z m 54-- Nothing -> return $ insert k x m 55 56-- * Non-monadic map operations 57--------------------------------------------------------------------------- 58 59-- UNUSED Liang-Ting Chen (05-07-2019) 60-- -- | Big conjunction over a map. 61-- allWithKey :: (k -> a -> Bool) -> Map k a -> Bool 62-- allWithKey f = Map.foldrWithKey (\ k a b -> f k a && b) True 63 64-- | Filter a map based on the keys. 65filterKeys :: (k -> Bool) -> Map k a -> Map k a 66filterKeys p = Map.filterWithKey (const . p) 67 68-- | O(n log n). Rebuilds the map from scratch. 69-- Not worse than 'Map.mapKeys'. 70mapMaybeKeys :: (Ord k1, Ord k2) => (k1 -> Maybe k2) -> Map k1 a -> Map k2 a 71mapMaybeKeys f = Map.fromList . mapMaybe (\ (k,a) -> (,a) <$> f k) . Map.toList 72 73-- UNUSED Liang-Ting Chen (05-07-2019) 74-- -- | Unzip a map. 75-- unzip :: Map k (a, b) -> (Map k a, Map k b) 76-- unzip m = (Map.map fst m, Map.map snd m) 77-- 78-- UNUSED Liang-Ting Chen (05-07-2019) 79-- unzip3 :: Map k (a, b, c) -> (Map k a, Map k b, Map k c) 80-- unzip3 m = (Map.map fst3 m, Map.map snd3 m, Map.map thd3 m) 81-- 82