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