refined-containers 0.1.0.2 → 0.1.1.0

raw patch · 13 files changed

+1696/−99 lines, 13 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• refined-containers.cabal +3/−2
• src/Data/HashMap/Common/Refined.hs +106/−14
• src/Data/HashMap/Refined.hs +225/−9
• src/Data/HashMap/Strict/Refined.hs +220/−11
• src/Data/HashSet/Refined.hs +1/−1
• src/Data/IntMap/Common/Refined.hs +134/−15
• src/Data/IntMap/Refined.hs +224/−7
• src/Data/IntMap/Strict/Refined.hs +208/−10
• src/Data/IntSet/Refined.hs +1/−1
• src/Data/Map/Common/Refined.hs +141/−15
• src/Data/Map/Refined.hs +225/−7
• src/Data/Map/Strict/Refined.hs +207/−6
• src/Data/Set/Refined.hs +1/−1

@@ -23,10 +23,11 @@ license-file: LICENSE author: mniip@typeable.io maintainer: mniip@typeable.io-version: 0.1.0.2+version: 0.1.1.0 build-type: Simple  tested-with:+    , GHC == 9.12.1     , GHC == 9.10.1     , GHC == 9.8.2     , GHC == 9.6.6@@ -42,7 +43,7 @@  library     build-depends:-        , base >= 4.12 && < 4.21+        , base >= 4.12 && < 4.22         , adjunctions >= 4.4 && < 4.5         , constraints >= 0.11 && < 0.15         , containers >= 0.5.7 && < 0.8

@@ -4,6 +4,7 @@  import           Control.Monad.Reader import           Control.DeepSeq+import           Data.Bifoldable import           Data.Coerce import           Data.Constraint (Dict(..)) import           Data.Container.Refined.Hashable@@ -11,6 +12,7 @@ import           Data.Container.Refined.Unsafe import           Data.Distributive import           Data.Foldable.WithIndex+import           Data.Functor.Classes import           Data.Functor.Rep import           Data.Functor.WithIndex import qualified Data.Hashable as Hashable@@ -22,6 +24,7 @@ import           Data.Traversable.WithIndex import           Data.Type.Coercion import           Data.Type.Equality ((:~:)(..))+import           Prelude hiding (zipWith) import           Refined import           Refined.Unsafe import           Unsafe.Coerce@@ -44,7 +47,10 @@ -- always derive @'KnownHashSet' s k@ by pattern matching on the 'Dict' returned -- by 'keysSet'. newtype HashMap s k a = HashMap (HashMap.HashMap k a)-  deriving newtype (Eq, Ord, Show, Functor, Foldable, Hashable.Hashable, NFData)+  deriving newtype+    ( Eq, Eq1, Eq2, Ord, Ord1, Ord2, Show, Show1, Show2+    , Functor, Foldable, Bifoldable, Hashable.Hashable, NFData+    )   deriving stock (Traversable) type role HashMap nominal nominal representational @@ -90,7 +96,7 @@ -- -- @ -- 'withHashMap' ('fromHashMap' ...---   $ \(m :: 'HashMap' s k a) -> doSomethingWith \@s+--   $ \\(m :: 'HashMap' s k a) -> doSomethingWith \@s -- @ withHashMap   :: forall k a r. SomeHashMap k a -> (forall s. HashMap s k a -> r) -> r@@ -100,6 +106,26 @@ fromHashMap :: forall k a. HashMap.HashMap k a -> SomeHashMap k a fromHashMap m = SomeHashMap (HashMap m) +-- | Given a set of keys @s@ known ahead of time, verify whether a regular+-- 'Data.HashMap.Lazy.HashMap' has exactly that set of keys.+verifyHashMap+  :: forall s k a. (Hashable k, KnownHashSet s k)+  => HashMap.HashMap k a -> Maybe (HashMap s k a)+verifyHashMap m+#if MIN_VERSION_unordered_containers(0, 2, 12)+  | HashMap.isSubmapOfBy (\_ _ -> True) m (HashSet.toMap keys)+  , HashMap.isSubmapOfBy (\_ _ -> True) (HashSet.toMap keys) m+#else+  | All True <- flip HashMap.foldMapWithKey m \k _+    -> All $ k `HashSet.member` keys+  , All True <- flip foldMap keys \k+    -> All $ k `HashMap.member` m+#endif+  = Just (HashMap m)+  | otherwise = Nothing+  where+    keys = reflect $ Proxy @s+ -- | An existential wrapper for a 'HashMap' with an as-yet-unknown set of keys, -- together with a proof of some fact @p@ about the set. Pattern matching on it -- gives you a way to refer to the set (the parameter @s@). Functions that@@ -214,12 +240,26 @@  -- | Given two maps proven to have the same keys, for each key apply the -- function to the associated values, to obtain a new map with the same keys.-zipWithKey+zipWith   :: forall s k a b c. Hashable k-  => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c-zipWithKey f (HashMap m1) (HashMap m2) = HashMap-  $ HashMap.intersectionWithKey (f . unsafeKey) m1 m2+  => (a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c+zipWith f (HashMap m1) (HashMap m2) = HashMap $ HashMap.intersectionWith f m1 m2 +-- | Return the union of two maps. For keys that exist in both maps, the value+-- is taken from the first map.+--+-- @+-- 'union' = unionWith 'const'+-- @+union+  :: forall s t k a. Hashable k+  => HashMap s k a+  -> HashMap t k a+  -> SomeHashMapWith (UnionProof 'Hashed s t) k a+union (HashMap m1) (HashMap m2) = SomeHashMapWith+  (HashMap $ HashMap.union m1 m2)+  $ UnionProof unsafeSubset unsafeSubsetWith2+ -- | Remove the keys that appear in the second map from the first map. difference   :: forall s t k a b. Hashable k@@ -230,6 +270,20 @@   = SomeHashMapWith (HashMap $ HashMap.difference m1 m2)     $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset +-- | Return the intersection of two maps, taking values from the first map.+--+-- @+-- 'intersection' = intersectionWith 'const'+-- @+intersection+  :: forall s t k a b. Hashable k+  => HashMap s k a+  -> HashMap t k b+  -> SomeHashMapWith (IntersectionProof 'Hashed s t) k a+intersection (HashMap m1) (HashMap m2) = SomeHashMapWith+  (HashMap $ HashMap.intersection m1 m2)+  $ IntersectionProof unsafeSubset unsafeSubsetWith2+ -- | Apply a function to all values in a map, together with their corresponding -- keys, that are proven to be in the map. The set of keys remains the same. mapWithKey@@ -288,6 +342,25 @@ toList :: forall s k a. HashMap s k a -> [(Key s k, a)] toList = gcoerceWith (unsafeCastKey @s @k) $ coerce $ HashMap.toList @k @a +-- | Retain only the values that satisfy the predicate, returning a potentially+-- smaller map.+filter+  :: forall s k a. (a -> Bool)+  -> HashMap s k a+  -> SomeHashMapWith (SupersetProof 'Hashed s) k a+filter p (HashMap m) = SomeHashMapWith (HashMap $ HashMap.filter p m)+  $ SupersetProof unsafeSubset++-- | Retain only the keys that satisfy the predicate, returning a potentially+-- smaller map.+filterKeys+  :: forall s k a. (Key s k -> Bool)+  -> HashMap s k a+  -> SomeHashMapWith (SupersetProof 'Hashed s) k a+filterKeys p (HashMap m) = SomeHashMapWith+  (HashMap $ HashMap.filterWithKey (\k _ -> p (unsafeKey k)) m)+  $ SupersetProof unsafeSubset+ -- | Retain only the key-value pairs that satisfy the predicate, returning a -- potentially smaller map. filterWithKey@@ -317,6 +390,25 @@  -- | Partition a map into two disjoint submaps: those whose key-value pairs -- satisfy the predicate, and those whose don't.+partition+  :: forall s k a. Hashable k -- TODO: this is only used in the proof+  => (a -> Bool)+  -> HashMap s k a+  -> Some2HashMapWith (PartitionProof 'Hashed s k) k a a+partition p (HashMap m) = Some2HashMapWith+  (HashMap $ HashMap.filter p m)+  (HashMap $ HashMap.filter (not . p) m)+  $ PartitionProof+    do \k -> case HashMap.lookup (unrefine k) m of+        Nothing -> error+          "partition: bug: Data.HashMap.Refined has been subverted"+        Just x -> if p x+          then Left $ unsafeKey $ unrefine k+          else Right $ unsafeKey $ unrefine k+    unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g++-- | Partition a map into two disjoint submaps: those whose key-value pairs+-- satisfy the predicate, and those whose don't. partitionWithKey   :: forall s k a. Hashable k -- TODO: this is only used in the proof   => (Key s k -> a -> Bool)@@ -349,15 +441,15 @@ castKey = castRefined  -- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps--- can be interconverted too. For example, 'zipWithKey' can be implemented via--- 'Data.HashMap.Refined.intersectionWithKey' by proving that the set of keys--- remains unchanged:+-- can be interconverted too. For example, 'Data.HashMap.Refined.zipWithKey' can+-- be implemented via 'Data.HashMap.Refined.intersectionWithKey' by proving that+-- the set of keys remains unchanged: -- -- @--- 'zipWithKey'+-- 'Data.HashMap.Refined.zipWithKey' --   :: forall s k a b c. 'Hashable' k --   => ('Key' s k -> a -> b -> c) -> 'HashMap' s k a -> 'HashMap' s k b -> 'HashMap' s k c--- 'zipWithKey' f m1 m2+-- 'Data.HashMap.Refined.zipWithKey' f m1 m2 --   | v'SomeHashMapWith' @r m proof <- 'Data.HashMap.Refined.intersectionWithKey' (f . 'andLeft') m1 m2 --   , v'IntersectionProof' p1 p2 <- proof --   , ( v'Coercion' :: t'Coercion' ('HashMap' r k c) ('HashMap' s k c))@@ -382,10 +474,10 @@   itraverse = traverseWithKey  -- | Similar to the instance for functions -- zip corresponding keys. To use--- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWithKey'.+-- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWith'. instance (Hashable k, KnownHashSet s k) => Applicative (HashMap s k) where   pure x = fromSet \_ -> x-  (<*>) = zipWithKey (const id)+  (<*>) = zipWith id  -- | @'bind' m f@ is a map that for each key @k :: 'Key' s k@, contains the -- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.@@ -408,7 +500,7 @@  -- | Append the values at the corresponding keys instance (Hashable k, Semigroup a) => Semigroup (HashMap s k a) where-  (<>) = zipWithKey (const (<>))+  (<>) = zipWith (<>)  instance (Hashable k, KnownHashSet s k, Monoid a)   => Monoid (HashMap s k a) where

@@ -43,18 +43,26 @@   , SingletonProof(..)   , fromSet   , Common.fromHashMap+  , Common.verifyHashMap+  , fromTraversable+  , fromTraversableWith   , fromTraversableWithKey   , FromTraversableProof(..)   -- * Insertion   , insert+  , insertWith+  , insertWithKey   , InsertProof(..)   , reinsert   , insertLookupWithKey   -- * Deletion/Update   , Common.delete+  , adjust'   , adjust   , adjustWithKey+  , update'   , update+  , updateWithKey   , updateLookupWithKey   -- * Query   , Common.lookup@@ -66,21 +74,29 @@   , Common.disjoint   , DisjointProof(..)   -- * Combine+  , zipWith   , zipWithKey   , bind+  , Common.union+  , unionWith   , unionWithKey   , UnionProof(..)   , Common.difference   , DifferenceProof(..)+  , differenceWith   , differenceWithKey   , PartialDifferenceProof(..)+  , Common.intersection+  , intersectionWith   , intersectionWithKey   , IntersectionProof(..)   -- * Traversal+  , map   , mapWithKey   , traverseWithKey   , mapAccumLWithKey   , mapAccumRWithKey+  , mapKeys   , mapKeysWith   , MapProof(..)   , backpermuteKeys@@ -97,10 +113,15 @@   -- * Filter   , Common.restrictKeys   , Common.withoutKeys+  , Common.filter+  , Common.filterKeys   , Common.filterWithKey+  , Common.partition   , Common.partitionWithKey   , PartitionProof(..)+  , mapMaybe   , mapMaybeWithKey+  , mapEither   , mapEitherWithKey   -- * Casts   , Common.castKey@@ -115,7 +136,7 @@ import           Data.Functor import           Data.HashMap.Common.Refined   ( HashMap(..), Key, unsafeCastKey, unsafeKey, SomeHashMapWith(..)-  , Some2HashMapWith(..), fromSet, (!), zipWithKey, mapWithKey, traverseWithKey+  , Some2HashMapWith(..), fromSet, (!), zipWith, mapWithKey, traverseWithKey   , bind   ) import qualified Data.HashMap.Common.Refined as Common@@ -123,7 +144,7 @@ import           Data.Traversable import           Data.Traversable.WithIndex import           Data.Type.Coercion-import           Prelude hiding (lookup, null)+import           Prelude hiding (lookup, map, null, zipWith) import           Refined import           Refined.Unsafe @@ -136,7 +157,42 @@ singleton k v = SomeHashMapWith (HashMap $ HashMap.singleton k v)   $ SingletonProof (unsafeKey k) --- | Create a map from an arbitrary traversable of key-value pairs.+-- | Create a map from an arbitrary traversable of key-value pairs. If a key is+-- repeated, the retained value is the last one in traversal order. If you're+-- looking for @fromList@, this is the function you want.+fromTraversable+  :: forall t k a. (Traversable t, Hashable k)+  => t (k, a) -> SomeHashMapWith (FromTraversableProof 'Hashed t k) k a+fromTraversable xs = SomeHashMapWith (HashMap m) $ FromTraversableProof proof+  where+    (m, proof) = mapAccumL+      (\s (k, v) -> let !s' = HashMap.insert k v s in (s', unsafeKey k))+      HashMap.empty+      xs++-- | Create a map from an arbitrary traversable of key-value pairs, with a+-- function for combining values for repeated keys. The function is called as if+-- by 'foldl1', but flipped:+--+-- @+-- 'fromTraversableWith' f [(k, x1), (k, x2), (k, x3)]+--   = 'singleton' k (f x3 (f x2 x1))+-- @+fromTraversableWith+  :: forall t k a. (Traversable t, Hashable k)+  => (a -> a -> a)+  -> t (k, a)+  -> SomeHashMapWith (FromTraversableProof 'Hashed t k) k a+fromTraversableWith f xs+  = SomeHashMapWith (HashMap m) $ FromTraversableProof proof+  where+    (m, proof) = mapAccumL+      (\s (k, v) -> let !s' = HashMap.insertWith f k v s in (s', unsafeKey k))+      HashMap.empty+      xs++-- | Create a map from an arbitrary traversable of key-value pairs. Like+-- 'fromTraversableWith', but the combining function has access to the key. fromTraversableWithKey   :: forall t k a. (Traversable t, Hashable k)   => (k -> a -> a -> a)@@ -160,6 +216,35 @@ insert k v (HashMap m) = SomeHashMapWith (HashMap $ HashMap.insert k v m)   $ InsertProof (unsafeKey k) unsafeSubset +-- | Insert a key-value pair into the map to obtain a potentially larger map,+-- guaranteed to contain the given key. If the key was already present, the+-- supplied function is used to combine the new value with the old (in that+-- order).+insertWith+  :: forall s k a. Hashable k+  => (a -> a -> a)+  -> k+  -> a+  -> HashMap s k a+  -> SomeHashMapWith (InsertProof 'Hashed k s) k a+insertWith f k v (HashMap m) = SomeHashMapWith+  (HashMap $ HashMap.insertWith f k v m)+  $ InsertProof (unsafeKey k) unsafeSubset++-- | Insert a key-value pair into the map to obtain a potentially larger map,+-- guaranteed to contain the given key. Like 'insertWith', but the combining+-- function has access to the key, which is guaranteed to be in the old map.+insertWithKey+  :: forall s k a. Hashable k+  => (Key s k -> a -> a -> a)+  -> k+  -> a+  -> HashMap s k a+  -> SomeHashMapWith (InsertProof 'Hashed k s) k a+insertWithKey f k v (HashMap m) = SomeHashMapWith+  (HashMap $ HashMap.insertWith (f $ unsafeKey k) k v m)+  $ InsertProof (unsafeKey k) unsafeSubset+ -- | Overwrite a key-value pair that is known to already be in the map. The set -- of keys remains the same. reinsert@@ -183,12 +268,22 @@     $ InsertProof (unsafeKey k) unsafeSubset   ) +-- | If the given key is in the map, update the value at that key using the+-- given function. In any case, the set of keys remains the same.+adjust'+  :: forall s k a. Hashable k => (a -> a) -> k -> HashMap s k a -> HashMap s k a+adjust' = coerce $ HashMap.adjust @k @a+ -- | Update the value at a specific key known the be in the map using the given -- function. The set of keys remains the same.+--+-- @+-- 'reinsert' k v = 'adjust (const v) k'+-- @ adjust   :: forall s k a. Hashable k   => (a -> a) -> Key s k -> HashMap s k a -> HashMap s k a-adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ HashMap.adjust @k @a+adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ adjust' @s @k @a  -- | If the given key is in the map, update the associated value using the given -- function with a proof that the key was in the map; otherwise return the map@@ -198,6 +293,17 @@   => (Key s k -> a -> a) -> k -> HashMap s k a -> HashMap s k a adjustWithKey f k (HashMap m) = HashMap $ HashMap.adjust (f $ unsafeKey k) k m +-- | If a key is present in the map, update its value or delete it using the+-- given function, returning a potentially smaller map.+update'+  :: forall s k a. Hashable k+  => (a -> Maybe a)+  -> k+  -> HashMap s k a+  -> SomeHashMapWith (SupersetProof 'Hashed s) k a+update' f k (HashMap m) = SomeHashMapWith (HashMap $ HashMap.update f k m)+  $ SupersetProof unsafeSubset+ -- | Update or delete a key known to be in the map using the given function, -- returning a potentially smaller map. update@@ -206,10 +312,21 @@   -> Key s k   -> HashMap s k a   -> SomeHashMapWith (SupersetProof 'Hashed s) k a-update f k (HashMap m)-  = SomeHashMapWith (HashMap $ HashMap.update f (unrefine k) m)-    $ SupersetProof unsafeSubset+update = gcoerceWith (unsafeCastKey @s @k) $ coerce $ update' @s @k @a +-- | If a key is present in the map, update its value or delete it using the+-- given function with a proof that the key was in the map, returning a+-- potentially smaller map.+updateWithKey+  :: forall s k a. Hashable k+  => (Key s k -> a -> Maybe a)+  -> k+  -> HashMap s k a+  -> SomeHashMapWith (SupersetProof 'Hashed s) k a+updateWithKey f k (HashMap m) = SomeHashMapWith+  (HashMap $ HashMap.update (f $ unsafeKey k) k m)+  $ SupersetProof unsafeSubset+ -- | If the given key is in the map, update or delete it using the given -- function with a proof that the key was in the map; otherwise the map is -- unchanged. Alongside return the new value if it was updated, or the old value@@ -226,8 +343,28 @@     $ SupersetProof unsafeSubset   ) +-- | Given two maps proven to have the same keys, for each key apply the+-- function to the associated values, to obtain a new map with the same keys.+zipWithKey+  :: forall s k a b c. Hashable k+  => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c+zipWithKey f (HashMap m1) (HashMap m2) = HashMap+  $ HashMap.intersectionWithKey (f . unsafeKey) m1 m2+ -- | Return the union of two maps, with a given combining function for keys that -- exist in both maps simultaneously.+unionWith+  :: forall s t k a. Hashable k+  => (a -> a -> a)+  -> HashMap s k a+  -> HashMap t k a+  -> SomeHashMapWith (UnionProof 'Hashed s t) k a+unionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith+  (HashMap $ HashMap.unionWith f m1 m2)+  $ UnionProof unsafeSubset unsafeSubsetWith2++-- | Return the union of two maps, with a given combining function for keys that+-- exist in both maps simultaneously. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@ -- respectively.@@ -241,8 +378,20 @@   (HashMap $ HashMap.unionWithKey (f . reallyUnsafeRefine) m1 m2)   $ UnionProof unsafeSubset unsafeSubsetWith2 --- | For keys that appear in both maps, the given function decides whether the--- key is removed from the first map.+-- | Return the first map, but for keys that appear in both maps, the given+-- function decides whether the key is removed.+differenceWith+  :: forall s t k a b. Hashable k+  => (a -> b -> Maybe a)+  -> HashMap s k a+  -> HashMap t k b+  -> SomeHashMapWith (PartialDifferenceProof 'Hashed s t) k a+differenceWith f (HashMap m1) (HashMap m2) = SomeHashMapWith+  (HashMap $ HashMap.differenceWith f m1 m2)+  $ PartialDifferenceProof unsafeSubset unsafeSubset++-- | Return the first map, but for keys that appear in both maps, the given+-- function decides whether the key is removed. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@ -- respectively.@@ -260,6 +409,17 @@   $ PartialDifferenceProof unsafeSubset unsafeSubset  -- | Return the intersection of two maps with the given combining function.+intersectionWith+  :: forall s t k a b c. Hashable k+  => (a -> b -> c)+  -> HashMap s k a+  -> HashMap t k b+  -> SomeHashMapWith (IntersectionProof 'Hashed s t) k c+intersectionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith+  (HashMap $ HashMap.intersectionWith f m1 m2)+  $ IntersectionProof unsafeSubset unsafeSubsetWith2++-- | Return the intersection of two maps with the given combining function. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@ -- respectively.@@ -273,6 +433,10 @@   (HashMap $ HashMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)   $ IntersectionProof unsafeSubset unsafeSubsetWith2 +-- | Apply a function to all values in a map. The set of keys remains the same.+map :: forall s k a b. (a -> b) -> HashMap s k a -> HashMap s k b+map = coerce $ HashMap.map @a @b @k+ -- | Thread an accumularing argument through the map in ascending order of -- hashes. mapAccumLWithKey@@ -291,6 +455,28 @@   -> (a, HashMap s k c) mapAccumRWithKey f = imapAccumR (flip f) +-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results+-- into a new map. For keys that were mapped to the same new key, the value is+-- picked in an unspecified way.+mapKeys+  :: forall s k1 k2 a. Hashable k2+  => (Key s k1 -> k2)+  -> HashMap s k1 a+  -> SomeHashMapWith (MapProof 'Hashed s k1 k2) k2 a+mapKeys g (HashMap m) = SomeHashMapWith+  (HashMap $ HashMap.fromList+    $ HashMap.foldrWithKey (\k x xs -> (g $ unsafeKey k, x) : xs) [] m)+  $ MapProof (unsafeKey . g) \k2 ->+    case HashMap.lookup (unrefine k2) backMap of+      Nothing -> error "mapKeys: bug: Data.HashMap.Refined has been subverted"+      Just k1 -> k1+  where+    ~backMap = HashMap.fromList+      [ (k2, unsafeKey k1)+      | k1 <- HashMap.keys m+      , let !k2 = g $ unsafeKey k1+      ]+ -- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the -- results into a new map. For keys that were mapped to the same new key, @c@ -- acts as the combining function for corresponding values.@@ -315,6 +501,15 @@       , let !k2 = g $ unsafeKey k1       ] +-- | Apply a function to all values in a map and collect only the 'Just'+-- results, returning a potentially smaller map.+mapMaybe+  :: forall s k a b. (a -> Maybe b)+  -> HashMap s k a+  -> SomeHashMapWith (SupersetProof 'Hashed s) k b+mapMaybe f (HashMap m) = SomeHashMapWith (HashMap $ HashMap.mapMaybe f m)+  $ SupersetProof unsafeSubset+ -- | Apply a function to all values in a map, together with their corresponding -- keys, and collect only the 'Just' results, returning a potentially smaller -- map.@@ -325,6 +520,27 @@ mapMaybeWithKey f (HashMap m)   = SomeHashMapWith (HashMap $ HashMap.mapMaybeWithKey (f . unsafeKey) m)     $ SupersetProof unsafeSubset++-- | Apply a function to all values in a map and collect the 'Left' and 'Right'+-- results into separate (disjoint) maps.+mapEither+  :: forall s k a b c. Hashable k -- TODO: this is only used in the proof+  => (a -> Either b c)+  -> HashMap s k a+  -> Some2HashMapWith (PartitionProof 'Hashed s k) k b c+mapEither p (HashMap m)+  | m' <- HashMap.map p m+  = Some2HashMapWith+    (HashMap $ HashMap.mapMaybe (either Just (const Nothing)) m')+    (HashMap $ HashMap.mapMaybe (either (const Nothing) Just) m')+    $ PartitionProof+      do \k -> case HashMap.lookup (unrefine k) m of+          Nothing -> error+            "mapEither: bug: Data.HashMap.Refined has been subverted"+          Just x -> case p x of+            Left _ -> Left $ unsafeKey $ unrefine k+            Right _ -> Right $ unsafeKey $ unrefine k+      unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g  -- | Apply a function to all values in a map, together with their corresponding -- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

@@ -43,18 +43,26 @@   , SingletonProof(..)   , fromSet   , Common.fromHashMap+  , Common.verifyHashMap+  , fromTraversable+  , fromTraversableWith   , fromTraversableWithKey   , FromTraversableProof(..)   -- * Insertion   , insert+  , insertWith+  , insertWithKey   , InsertProof(..)   , reinsert   , insertLookupWithKey   -- * Deletion/Update   , Common.delete+  , adjust'   , adjust   , adjustWithKey+  , update'   , update+  , updateWithKey   , updateLookupWithKey   -- * Query   , Common.lookup@@ -66,21 +74,29 @@   , Common.disjoint   , DisjointProof(..)   -- * Combine+  , zipWith   , zipWithKey   , bind+  , Common.union+  , unionWith   , unionWithKey   , UnionProof(..)   , Common.difference   , DifferenceProof(..)+  , differenceWith   , differenceWithKey   , PartialDifferenceProof(..)+  , Common.intersection+  , intersectionWith   , intersectionWithKey   , IntersectionProof(..)   -- * Traversal+  , map   , mapWithKey   , traverseWithKey   , mapAccumLWithKey   , mapAccumRWithKey+  , mapKeys   , mapKeysWith   , MapProof(..)   , backpermuteKeys@@ -97,10 +113,15 @@   -- * Filter   , Common.restrictKeys   , Common.withoutKeys+  , Common.filter+  , Common.filterKeys   , Common.filterWithKey+  , Common.partition   , Common.partitionWithKey   , PartitionProof(..)+  , mapMaybe   , mapMaybeWithKey+  , mapEither   , mapEitherWithKey   -- * Casts   , Common.castKey@@ -116,7 +137,7 @@ import qualified Data.HashMap.Strict as HashMap import           Data.HashMap.Common.Refined   ( HashMap(..), Key, unsafeCastKey, unsafeKey, SomeHashMapWith(..)-  , Some2HashMapWith(..), (!)+  , Some2HashMapWith(..), (!), zipWith   ) import qualified Data.HashMap.Common.Refined as Common import qualified Data.HashSet as HashSet@@ -125,7 +146,7 @@ import           Data.Traversable import           Data.Traversable.WithIndex import           Data.Type.Coercion-import           Prelude hiding (lookup, null)+import           Prelude hiding (lookup, map, null, zipWith) import           Refined import           Refined.Unsafe @@ -144,14 +165,49 @@ fromSet f = HashMap $ HashMap.mapWithKey (\k _ -> f $ unsafeKey k)   $ HashSet.toMap (reflect $ Proxy @s) --- | Create a map from an arbitrary traversable of key-value pairs.+-- | Create a map from an arbitrary traversable of key-value pairs. If a key is+-- repeated, the retained value is the last one in traversal order. If you're+-- looking for @fromList@, this is the function you want.+fromTraversable+  :: forall t k a. (Traversable t, Hashable k)+  => t (k, a) -> SomeHashMapWith (FromTraversableProof 'Hashed t k) k a+fromTraversable xs = SomeHashMapWith (HashMap m) $ FromTraversableProof proof+  where+    (m, proof) = mapAccumL+      (\s (k, v) -> let !s' = HashMap.insert k v s in (s', unsafeKey k))+      HashMap.empty+      xs++-- | Create a map from an arbitrary traversable of key-value pairs, with a+-- function for combining values for repeated keys. The function is called as if+-- by 'foldl1', but flipped:+--+-- @+-- 'fromTraversableWith' f [(k, x1), (k, x2), (k, x3)]+--   = 'singleton' k (f x3 (f x2 x1))+-- @+fromTraversableWith+  :: forall t k a. (Traversable t, Hashable k)+  => (a -> a -> a)+  -> t (k, a)+  -> SomeHashMapWith (FromTraversableProof 'Hashed t k) k a+fromTraversableWith f xs+  = SomeHashMapWith (HashMap m) $ FromTraversableProof proof+  where+    (m, proof) = mapAccumL+      (\s (k, v) -> let !s' = HashMap.insertWith f k v s in (s', unsafeKey k))+      HashMap.empty+      xs++-- | Create a map from an arbitrary traversable of key-value pairs. Like+-- 'fromTraversableWith', but the combining function has access to the key. fromTraversableWithKey   :: forall t k a. (Traversable t, Hashable k)   => (k -> a -> a -> a)   -> t (k, a)   -> SomeHashMapWith (FromTraversableProof 'Hashed t k) k a-fromTraversableWithKey f xs = SomeHashMapWith (HashMap m)-  $ FromTraversableProof proof+fromTraversableWithKey f xs+  = SomeHashMapWith (HashMap m) $ FromTraversableProof proof   where     (m, proof) = mapAccumL       (\s (k, v)@@ -168,8 +224,41 @@ insert k v (HashMap m) = SomeHashMapWith (HashMap $ HashMap.insert k v m)   $ InsertProof (unsafeKey k) unsafeSubset +-- | Insert a key-value pair into the map to obtain a potentially larger map,+-- guaranteed to contain the given key. If the key was already present, the+-- supplied function is used to combine the new value with the old (in that+-- order).+insertWith+  :: forall s k a. Hashable k+  => (a -> a -> a)+  -> k+  -> a+  -> HashMap s k a+  -> SomeHashMapWith (InsertProof 'Hashed k s) k a+insertWith f k v (HashMap m) = SomeHashMapWith+  (HashMap $ HashMap.insertWith f k v m)+  $ InsertProof (unsafeKey k) unsafeSubset++-- | Insert a key-value pair into the map to obtain a potentially larger map,+-- guaranteed to contain the given key. Like 'insertWith', but the combining+-- function has access to the key, which is guaranteed to be in the old map.+insertWithKey+  :: forall s k a. Hashable k+  => (Key s k -> a -> a -> a)+  -> k+  -> a+  -> HashMap s k a+  -> SomeHashMapWith (InsertProof 'Hashed k s) k a+insertWithKey f k v (HashMap m) = SomeHashMapWith+  (HashMap $ HashMap.insertWith (f $ unsafeKey k) k v m)+  $ InsertProof (unsafeKey k) unsafeSubset+ -- | Overwrite a key-value pair that is known to already be in the map. The set -- of keys remains the same.+--+-- @+-- 'reinsert' k v = 'adjust (const v) k'+-- @ reinsert   :: forall s k a. Hashable k   => Key s k -> a -> HashMap s k a -> HashMap s k a@@ -191,12 +280,18 @@     $ InsertProof (unsafeKey k) unsafeSubset   ) +-- | If the given key is in the map, update the value at that key using the+-- given function. In any case, the set of keys remains the same.+adjust'+  :: forall s k a. Hashable k => (a -> a) -> k -> HashMap s k a -> HashMap s k a+adjust' = coerce $ HashMap.adjust @k @a+ -- | Update the value at a specific key known the be in the map using the given -- function. The set of keys remains the same. adjust   :: forall s k a. Hashable k   => (a -> a) -> Key s k -> HashMap s k a -> HashMap s k a-adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ HashMap.adjust @k @a+adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ adjust' @s @k @a  -- | If the given key is in the map, update the associated value using the given -- function with a proof that the key was in the map; otherwise return the map@@ -206,6 +301,17 @@   => (Key s k -> a -> a) -> k -> HashMap s k a -> HashMap s k a adjustWithKey f k (HashMap m) = HashMap $ HashMap.adjust (f $ unsafeKey k) k m +-- | If a key is present in the map, update its value or delete it using the+-- given function, returning a potentially smaller map.+update'+  :: forall s k a. Hashable k+  => (a -> Maybe a)+  -> k+  -> HashMap s k a+  -> SomeHashMapWith (SupersetProof 'Hashed s) k a+update' f k (HashMap m) = SomeHashMapWith (HashMap $ HashMap.update f k m)+  $ SupersetProof unsafeSubset+ -- | Update or delete a key known to be in the map using the given function, -- returning a potentially smaller map. update@@ -214,10 +320,21 @@   -> Key s k   -> HashMap s k a   -> SomeHashMapWith (SupersetProof 'Hashed s) k a-update f k (HashMap m)-  = SomeHashMapWith (HashMap $ HashMap.update f (unrefine k) m)-    $ SupersetProof unsafeSubset+update = gcoerceWith (unsafeCastKey @s @k) $ coerce $ update' @s @k @a +-- | If a key is present in the map, update its value or delete it using the+-- given function with a proof that the key was in the map, returning a+-- potentially smaller map.+updateWithKey+  :: forall s k a. Hashable k+  => (Key s k -> a -> Maybe a)+  -> k+  -> HashMap s k a+  -> SomeHashMapWith (SupersetProof 'Hashed s) k a+updateWithKey f k (HashMap m) = SomeHashMapWith+  (HashMap $ HashMap.update (f $ unsafeKey k) k m)+  $ SupersetProof unsafeSubset+ -- | If the given key is in the map, update or delete it using the given -- function with a proof that the key was in the map; otherwise the map is -- unchanged. Alongside return the new value if it was updated, or the old value@@ -244,6 +361,18 @@  -- | Return the union of two maps, with a given combining function for keys that -- exist in both maps simultaneously.+unionWith+  :: forall s t k a. Hashable k+  => (a -> a -> a)+  -> HashMap s k a+  -> HashMap t k a+  -> SomeHashMapWith (UnionProof 'Hashed s t) k a+unionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith+  (HashMap $ HashMap.unionWith f m1 m2)+  $ UnionProof unsafeSubset unsafeSubsetWith2++-- | Return the union of two maps, with a given combining function for keys that+-- exist in both maps simultaneously. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@ -- respectively.@@ -257,8 +386,20 @@   (HashMap $ HashMap.unionWithKey (f . reallyUnsafeRefine) m1 m2)   $ UnionProof unsafeSubset unsafeSubsetWith2 --- | For keys that appear in both maps, the given function decides whether the--- key is removed from the first map.+-- | Return the first map, but for keys that appear in both maps, the given+-- function decides whether the key is removed.+differenceWith+  :: forall s t k a b. Hashable k+  => (a -> b -> Maybe a)+  -> HashMap s k a+  -> HashMap t k b+  -> SomeHashMapWith (PartialDifferenceProof 'Hashed s t) k a+differenceWith f (HashMap m1) (HashMap m2) = SomeHashMapWith+  (HashMap $ HashMap.differenceWith f m1 m2)+  $ PartialDifferenceProof unsafeSubset unsafeSubset++-- | Return the first map, but for keys that appear in both maps, the given+-- function decides whether the key is removed. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@ -- respectively.@@ -276,6 +417,17 @@   $ PartialDifferenceProof unsafeSubset unsafeSubset  -- | Return the intersection of two maps with the given combining function.+intersectionWith+  :: forall s t k a b c. Hashable k+  => (a -> b -> c)+  -> HashMap s k a+  -> HashMap t k b+  -> SomeHashMapWith (IntersectionProof 'Hashed s t) k c+intersectionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith+  (HashMap $ HashMap.intersectionWith f m1 m2)+  $ IntersectionProof unsafeSubset unsafeSubsetWith2++-- | Return the intersection of two maps with the given combining function. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@ -- respectively.@@ -289,6 +441,10 @@   (HashMap $ HashMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)   $ IntersectionProof unsafeSubset unsafeSubsetWith2 +-- | Apply a function to all values in a map. The set of keys remains the same.+map :: forall s k a b. (a -> b) -> HashMap s k a -> HashMap s k b+map = coerce $ HashMap.map @a @b @k+ -- | Apply a function to all values in a map, together with their corresponding -- keys, that are proven to be in the map. The set of keys remains the same. mapWithKey@@ -323,6 +479,29 @@   -> (a, HashMap s k c) mapAccumRWithKey f = imapAccumR (flip f) +-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results+-- into a new map. For keys that were mapped to the same new key, the value is+-- picked in an unspecified way.+mapKeys+  :: forall s k1 k2 a. Hashable k2+  => (Key s k1 -> k2)+  -> HashMap s k1 a+  -> SomeHashMapWith (MapProof 'Hashed s k1 k2) k2 a+mapKeys g (HashMap m) = SomeHashMapWith+  (HashMap $ HashMap.fromList+    $ HashMap.foldrWithKey (\k x xs -> (g $ unsafeKey k, x) : xs) [] m)+  $ MapProof (unsafeKey . g) \k2 ->+    case HashMap.lookup (unrefine k2) backMap of+      Nothing -> error+        "mapKeys: bug: Data.HashMap.Strict.Refined has been subverted"+      Just k1 -> k1+  where+    ~backMap = HashMap.fromList+      [ (k2, unsafeKey k1)+      | k1 <- HashMap.keys m+      , let !k2 = g $ unsafeKey k1+      ]+ -- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the -- results into a new map. For keys that were mapped to the same new key, @c@ -- acts as the combining function for corresponding values.@@ -347,6 +526,15 @@       , let !k2 = g $ unsafeKey k1       ] +-- | Apply a function to all values in a map and collect only the 'Just'+-- results, returning a potentially smaller map.+mapMaybe+  :: forall s k a b. (a -> Maybe b)+  -> HashMap s k a+  -> SomeHashMapWith (SupersetProof 'Hashed s) k b+mapMaybe f (HashMap m) = SomeHashMapWith (HashMap $ HashMap.mapMaybe f m)+  $ SupersetProof unsafeSubset+ -- | Apply a function to all values in a map, together with their corresponding -- keys, and collect only the 'Just' results, returning a potentially smaller -- map.@@ -357,6 +545,27 @@ mapMaybeWithKey f (HashMap m)   = SomeHashMapWith (HashMap $ HashMap.mapMaybeWithKey (f . unsafeKey) m)     $ SupersetProof unsafeSubset++-- | Apply a function to all values in a map and collect the 'Left' and 'Right'+-- results into separate (disjoint) maps.+mapEither+  :: forall s k a b c. Hashable k -- TODO: this is only used in the proof+  => (a -> Either b c)+  -> HashMap s k a+  -> Some2HashMapWith (PartitionProof 'Hashed s k) k b c+mapEither p (HashMap m)+  | m' <- HashMap.map p m+  = Some2HashMapWith+    (HashMap $ HashMap.mapMaybe (either Just (const Nothing)) m')+    (HashMap $ HashMap.mapMaybe (either (const Nothing) Just) m')+    $ PartitionProof+      do \k -> case HashMap.lookup (unrefine k) m of+          Nothing -> error+            "mapEither: bug: Data.HashMap.Refined has been subverted"+          Just x -> case p x of+            Left _ -> Left $ unsafeKey $ unrefine k+            Right _ -> Right $ unsafeKey $ unrefine k+      unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g  -- | Apply a function to all values in a map, together with their corresponding -- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

@@ -165,7 +165,7 @@ -- you a way to refer to the set (the parameter @s@), e.g.: -- -- @--- 'withHashSet' ('fromHashSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s+-- 'withHashSet' ('fromHashSet' ...) $ \\(_ :: 'Proxy' s) -> doSomethingWith \@s -- @ withHashSet   :: forall a r. SomeHashSet a

@@ -14,11 +14,13 @@ import           Data.Functor.WithIndex import qualified Data.Hashable as Hashable import qualified Data.IntMap as IntMap+import qualified Data.IntSet as IntSet import           Data.Proxy import           Data.Reflection import           Data.Traversable.WithIndex import           Data.Type.Coercion import           Data.Type.Equality ((:~:)(..))+import           Prelude hiding (zipWith) import           Refined import           Refined.Unsafe import           Unsafe.Coerce@@ -36,6 +38,9 @@ import qualified Data.List as List #endif +#if MIN_VERSION_containers(0, 5, 9) || MIN_VERSION_hashable(1, 4, 0)+import           Data.Functor.Classes+#endif  -- | A wrapper around a regular 'Data.IntMap.IntMap' with a type parameter @s@ -- identifying the set of keys present in the map.@@ -52,6 +57,9 @@ #if MIN_VERSION_hashable(1, 3, 4)   deriving newtype (Hashable.Hashable) #endif+#if MIN_VERSION_containers(0, 5, 9) || MIN_VERSION_hashable(1, 4, 0)+  deriving newtype (Eq1, Ord1, Show1)+#endif   deriving stock (Traversable) type role IntMap nominal representational @@ -96,7 +104,8 @@ -- parameter @s@), e.g.: -- -- @--- 'withIntMap' ('fromIntMap' ...) $ \(m :: 'IntMap' s a) -> doSomethingWith \@s+-- 'withIntMap' ('fromIntMap' ...)+--   $ \\(m :: 'IntMap' s a) -> doSomethingWith \@s -- @ withIntMap :: forall a r. SomeIntMap a -> (forall s. IntMap s a -> r) -> r withIntMap (SomeIntMap m) k = k m@@ -105,6 +114,14 @@ fromIntMap :: forall a. IntMap.IntMap a -> SomeIntMap a fromIntMap m = SomeIntMap (IntMap m) +-- | Given a set of keys @s@ known ahead of time, verify whether a regular+-- 'Data.IntMap.IntMap' has exactly that set of keys.+verifyIntMap+  :: forall s a. KnownIntSet s => IntMap.IntMap a -> Maybe (IntMap s a)+verifyIntMap m+  | IntMap.keys m == IntSet.toList (reflect $ Proxy @s) = Just (IntMap m)+  | otherwise = Nothing+ -- | An existential wrapper for an 'IntMap' with an as-yet-unknown set of keys, -- together with a proof of some fact @p@ about the set. Pattern matching on it -- gives you a way to refer to the set (the parameter @s@). Functions that@@ -234,23 +251,36 @@  -- | Given two maps proven to have the same keys, for each key apply the -- function to the associated values, to obtain a new map with the same keys.-zipWithKey-  :: forall s a b c. (Key s -> a -> b -> c)+zipWith+  :: forall s a b c. (a -> b -> c)   -> IntMap s a   -> IntMap s b   -> IntMap s c-zipWithKey f (IntMap m1) (IntMap m2) = IntMap-  $ IntMap.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)+zipWith f (IntMap m1) (IntMap m2) = IntMap+  $ IntMap.mergeWithKey (\_ x y -> Just $ f x y)     (\m -> if IntMap.null m       then IntMap.empty-      else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")+      else error "zipWith: bug: Data.IntMap.Refined has been subverted")     (\m -> if IntMap.null m       then IntMap.empty-      else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")+      else error "zipWith: bug: Data.IntMap.Refined has been subverted")     --  ^ Work around https://github.com/haskell/containers/issues/979     m1     m2 +-- | Return the union of two maps. For keys that exist in both maps, the value+-- is taken from the first map.+--+-- @+-- 'union' = unionWith 'const'+-- @+union+  :: forall s t a. IntMap s a+  -> IntMap t a+  -> SomeIntMapWith (UnionProof 'Int s t) a+union (IntMap m1) (IntMap m2) = SomeIntMapWith (IntMap $ IntMap.union m1 m2)+  $ UnionProof unsafeSubset unsafeSubsetWith2+ -- | Remove the keys that appear in the second map from the first map. difference   :: forall s t a b. IntMap s a@@ -260,6 +290,19 @@   (IntMap $ IntMap.difference m1 m2)   $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset +-- | Return the intersection of two maps, taking values from the first map.+--+-- @+-- 'intersection' = intersectionWith 'const'+-- @+intersection+  :: forall s t a b. IntMap s a+  -> IntMap t b+  -> SomeIntMapWith (IntersectionProof 'Int s t) a+intersection (IntMap m1) (IntMap m2) = SomeIntMapWith+  (IntMap $ IntMap.intersection m1 m2)+  $ IntersectionProof unsafeSubset unsafeSubsetWith2+ -- | Apply a function to all values in a map, together with their corresponding -- keys, that are proven to be in the map. The set of keys remains the same. mapWithKey :: forall s a b. (Key s -> a -> b) -> IntMap s a -> IntMap s b@@ -318,6 +361,29 @@  -- | Retain only the key-value pairs that satisfy the predicate, returning a -- potentially smaller map.+filter+  :: forall s a. (a -> Bool)+  -> IntMap s a+  -> SomeIntMapWith (SupersetProof 'Int s) a+filter p (IntMap m) = SomeIntMapWith (IntMap $ IntMap.filter p m)+  $ SupersetProof unsafeSubset++-- | Retain only the key-value pairs that satisfy the predicate, returning a+-- potentially smaller map.+filterKeys+  :: forall s a. (Key s -> Bool)+  -> IntMap s a+  -> SomeIntMapWith (SupersetProof 'Int s) a+filterKeys p (IntMap m) = SomeIntMapWith+#if MIN_VERSION_containers(0, 8, 0)+  (IntMap $ IntMap.filterKeys (p . unsafeKey) m)+#else+  (IntMap $ IntMap.filterWithKey (\k _ -> p (unsafeKey k)) m)+#endif+  $ SupersetProof unsafeSubset++-- | Retain only the key-value pairs that satisfy the predicate, returning a+-- potentially smaller map. filterWithKey   :: forall s a. (Key s -> a -> Bool)   -> IntMap s a@@ -351,6 +417,22 @@ #endif   $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset +-- | Partition a map into two disjoint submaps: those whose values satisfy the+-- predicate, and those whose don't.+partition+  :: forall s a. (a -> Bool)+  -> IntMap s a+  -> Some2IntMapWith (PartitionProof 'Int s Int) a a+partition p (IntMap m) = case IntMap.partition p m of+  (m1, m2) -> Some2IntMapWith (IntMap m1) (IntMap m2) $ PartitionProof+    do \k -> case IntMap.lookup (unrefine k) m of+        Nothing -> error+          "partition: bug: Data.IntMap.Refined has been subverted"+        Just x -> if p x+          then Left $ unsafeKey $ unrefine k+          else Right $ unsafeKey $ unrefine k+    unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g+ -- | Partition a map into two disjoint submaps: those whose key-value pairs -- satisfy the predicate, and those whose don't. partitionWithKey@@ -368,6 +450,43 @@             else Right $ unsafeKey $ unrefine k       unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g +-- | Take the a submap of keys up to a point where the predicate stops holding.+--+-- If @p@ is antitone ( \(\forall x y, x < y \implies p(x) \ge p(y)\) ), then+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is+-- chosen in an unspecified way.+takeWhileAntitone+  :: forall s a. (Key s -> Bool)+  -> IntMap s a+  -> SomeIntMapWith (SupersetProof 'Int s) a+takeWhileAntitone p (IntMap m) = SomeIntMapWith+#if MIN_VERSION_containers(0, 6, 7)+  (IntMap $ IntMap.takeWhileAntitone (p . unsafeKey) m)+#else+  (IntMap $ IntMap.fromDistinctAscList+    $ List.takeWhile (p . unsafeKey . fst) $ IntMap.toAscList m)+#endif+  $ SupersetProof unsafeSubset++-- | Take the a submap of keys starting from a point where the predicate stops+-- holding.+--+-- If @p@ is antitone ( \(\forall x y, x < y \implies p(x) \ge p(y)\) ), then+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is+-- chosen in an unspecified way.+dropWhileAntitone+  :: forall s a. (Key s -> Bool)+  -> IntMap s a+  -> SomeIntMapWith (SupersetProof 'Int s) a+dropWhileAntitone p (IntMap m) = SomeIntMapWith+#if MIN_VERSION_containers(0, 6, 7)+  (IntMap $ IntMap.dropWhileAntitone (p . unsafeKey) m)+#else+  (IntMap $ IntMap.fromDistinctAscList+    $ List.dropWhile (p . unsafeKey . fst) $ IntMap.toAscList m)+#endif+  $ SupersetProof unsafeSubset+ -- | Divide a map into two disjoint submaps at a point where the predicate on -- the keys stops holding. --@@ -442,17 +561,17 @@ castKey = castRefined  -- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps--- can be interconverted too. For example, 'zipWithKey' can be implemented via--- 'Data.IntMap.Refined.intersectionWithKey' by proving that the set of keys--- remains unchanged:+-- can be interconverted too. For example, 'Data.IntMap.Refined.zipWithKey' can+-- be implemented via 'Data.IntMap.Refined.intersectionWithKey' by proving that+-- the set of keys remains unchanged: -- -- @--- 'zipWithKey'+-- 'Data.IntMap.Refined.zipWithKey' --   :: forall s a b c. ('Key' s -> a -> b -> c) --   -> 'IntMap' s a --   -> 'IntMap' s b --   -> 'IntMap' s c--- 'zipWithKey' f m1 m2+-- 'Data.IntMap.Refined.zipWithKey' f m1 m2 --   | v'SomeIntMapWith' @r m proof <- 'Data.IntMap.Refined.intersectionWithKey' (f . 'andLeft') m1 m2 --   , v'IntersectionProof' p1 p2 <- proof --   , ( v'Coercion' :: t'Coercion' ('IntMap' r c) ('IntMap' s c))@@ -479,10 +598,10 @@   itraverse = traverseWithKey  -- | Similar to the instance for functions -- zip corresponding keys. To use--- '<*>'/'Control.Applicative.liftA2' without 'KnownIntSet' see 'zipWithKey'.+-- '<*>'/'Control.Applicative.liftA2' without 'KnownIntSet' see 'zipWith'. instance  KnownIntSet s => Applicative (IntMap s) where   pure x = fromSet \_ -> x-  (<*>) = zipWithKey (const id)+  (<*>) = zipWith id  -- | @'bind' m f@ is a map that for each key @k :: 'Key' s@, contains the -- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.@@ -502,7 +621,7 @@  -- | Append the values at the corresponding keys instance Semigroup a => Semigroup (IntMap s a) where-  (<>) = zipWithKey (const (<>))+  (<>) = zipWith (<>)  instance (KnownIntSet s, Monoid a) => Monoid (IntMap s a) where   mempty = fromSet \_ -> mempty

@@ -34,18 +34,26 @@   , SingletonProof(..)   , fromSet   , Common.fromIntMap+  , Common.verifyIntMap+  , fromTraversable+  , fromTraversableWith   , fromTraversableWithKey   , FromTraversableProof(..)   -- * Insertion   , insert+  , insertWith+  , insertWithKey   , InsertProof(..)   , reinsert   , insertLookupWithKey   -- * Deletion/Update   , Common.delete+  , adjust'   , adjust   , adjustWithKey+  , update'   , update+  , updateWithKey   , updateLookupWithKey   -- * Query   , Common.lookup@@ -61,21 +69,29 @@   , Common.disjoint   , DisjointProof(..)   -- * Combine+  , zipWith   , zipWithKey   , bind+  , Common.union+  , unionWith   , unionWithKey   , UnionProof(..)   , Common.difference   , DifferenceProof(..)+  , differenceWith   , differenceWithKey   , PartialDifferenceProof(..)+  , Common.intersection+  , intersectionWith   , intersectionWithKey   , IntersectionProof(..)   -- * Traversal+  , map   , mapWithKey   , traverseWithKey   , mapAccumLWithKey   , mapAccumRWithKey+  , mapKeys   , mapKeysWith   , MapProof(..)   , backpermuteKeys@@ -93,12 +109,19 @@   -- * Filter   , Common.restrictKeys   , Common.withoutKeys+  , Common.filter+  , Common.filterKeys   , Common.filterWithKey+  , Common.partition   , Common.partitionWithKey   , PartitionProof(..)+  , Common.takeWhileAntitone+  , Common.dropWhileAntitone   , Common.spanAntitone   , PartialPartitionProof(..)+  , mapMaybe   , mapMaybeWithKey+  , mapEither   , mapEitherWithKey   , Common.splitLookup   , SplitProof(..)@@ -122,13 +145,13 @@ import qualified Data.IntMap as IntMap import           Data.IntMap.Common.Refined   ( IntMap(..), Key, unsafeCastKey, unsafeKey, SomeIntMapWith(..)-  , Some2IntMapWith(..), fromSet, (!), zipWithKey, mapWithKey, traverseWithKey+  , Some2IntMapWith(..), fromSet, (!), zipWith, mapWithKey, traverseWithKey   , bind   ) import qualified Data.IntMap.Common.Refined as Common import           Data.Traversable import           Data.Type.Coercion-import           Prelude hiding (lookup, null)+import           Prelude hiding (lookup, map, null, zipWith) import           Refined import           Refined.Unsafe @@ -139,7 +162,42 @@ singleton k v = SomeIntMapWith (IntMap $ IntMap.singleton k v)   $ SingletonProof (unsafeKey k) --- | Create a map from an arbitrary traversable of key-value pairs.+-- | Create a map from an arbitrary traversable of key-value pairs. If a key is+-- repeated, the retained value is the last one in traversal order. If you're+-- looking for @fromList@, this is the function you want.+fromTraversable+  :: forall t a. Traversable t+  => t (Int, a) -> SomeIntMapWith (FromTraversableProof 'Int t Int) a+fromTraversable xs = SomeIntMapWith (IntMap m) $ FromTraversableProof proof+  where+    (m, proof) = mapAccumL+      (\s (k, v) -> let !s' = IntMap.insert k v s in (s', unsafeKey k))+      IntMap.empty+      xs++-- | Create a map from an arbitrary traversable of key-value pairs, with a+-- function for combining values for repeated keys. The function is called as if+-- by 'foldl1', but flipped:+--+-- @+-- 'fromTraversableWith' f [(k, x1), (k, x2), (k, x3)]+--   = 'singleton' k (f x3 (f x2 x1))+-- @+fromTraversableWith+  :: forall t a. Traversable t+  => (a -> a -> a)+  -> t (Int, a)+  -> SomeIntMapWith (FromTraversableProof 'Int t Int) a+fromTraversableWith f xs+  = SomeIntMapWith (IntMap m) $ FromTraversableProof proof+  where+    (m, proof) = mapAccumL+      (\s (k, v) -> let !s' = IntMap.insertWith f k v s in (s', unsafeKey k))+      IntMap.empty+      xs++-- | Create a map from an arbitrary traversable of key-value pairs. Like+-- 'fromTraversableWith', but the combining function has access to the key. fromTraversableWithKey   :: forall t a. Traversable t   => (Int -> a -> a -> a)@@ -164,6 +222,33 @@ insert k v (IntMap m) = SomeIntMapWith (IntMap $ IntMap.insert k v m)   $ InsertProof (unsafeKey k) unsafeSubset +-- | Insert a key-value pair into the map to obtain a potentially larger map,+-- guaranteed to contain the given key. If the key was already present, the+-- supplied function is used to combine the new value with the old (in that+-- order).+insertWith+  :: forall s a. (a -> a -> a)+  -> Int+  -> a+  -> IntMap s a+  -> SomeIntMapWith (InsertProof 'Int Int s) a+insertWith f k v (IntMap m) = SomeIntMapWith+  (IntMap $ IntMap.insertWith f k v m)+  $ InsertProof (unsafeKey k) unsafeSubset++-- | Insert a key-value pair into the map to obtain a potentially larger map,+-- guaranteed to contain the given key. Like 'insertWith', but the combining+-- function has access to the key, which is guaranteed to be in the old map.+insertWithKey+  :: forall s a. (Key s -> a -> a -> a)+  -> Int+  -> a+  -> IntMap s a+  -> SomeIntMapWith (InsertProof 'Int Int s) a+insertWithKey f k v (IntMap m) = SomeIntMapWith+  (IntMap $ IntMap.insertWithKey (f . unsafeKey) k v m)+  $ InsertProof (unsafeKey k) unsafeSubset+ -- | Overwrite a key-value pair that is known to already be in the map. The set -- of keys remains the same. reinsert@@ -184,10 +269,19 @@     (v', !m') -> ((unsafeKey k,) <$> v',)       $ SomeIntMapWith (IntMap m') $ InsertProof (unsafeKey k) unsafeSubset +-- | If the given key is in the map, update the value at that key using the+-- given function. In any case, the set of keys remains the same.+adjust' :: forall s a. (a -> a) -> Int -> IntMap s a -> IntMap s a+adjust' = coerce $ IntMap.adjust @a+ -- | Update the value at a specific key known the be in the map using the given -- function. The set of keys remains the same.+--+-- @+-- 'reinsert' k v = 'adjust (const v) k'+-- @ adjust :: forall s a. (a -> a) -> Key s -> IntMap s a -> IntMap s a-adjust = gcoerceWith (unsafeCastKey @s) $ coerce $ IntMap.adjust @a+adjust = gcoerceWith (unsafeCastKey @s) $ coerce $ adjust' @s @a  -- | If the given key is in the map, update the associated value using the given -- function with a proof that the key was in the map; otherwise return the map@@ -197,6 +291,16 @@ adjustWithKey = gcoerceWith (unsafeCastKey @s) $ coerce   $ IntMap.adjustWithKey @a +-- | If a key is present in the map, update its value or delete it using the+-- given function, returning a potentially smaller map.+update'+  :: forall s a. (a -> Maybe a)+  -> Int+  -> IntMap s a+  -> SomeIntMapWith (SupersetProof 'Int s) a+update' f k (IntMap m) = SomeIntMapWith (IntMap $ IntMap.update f k m)+  $ SupersetProof unsafeSubset+ -- | Update or delete a key known to be in the map using the given function, -- returning a potentially smaller map. update@@ -204,7 +308,18 @@   -> Key s   -> IntMap s a   -> SomeIntMapWith (SupersetProof 'Int s) a-update f k (IntMap m) = SomeIntMapWith (IntMap $ IntMap.update f (unrefine k) m)+update = gcoerceWith (unsafeCastKey @s) $ coerce $ update' @s @a++-- | If a key is present in the map, update its value or delete it using the+-- given function with a proof that the key was in the map, returning a+-- potentially smaller map.+updateWithKey+  :: forall s a. (Key s -> a -> Maybe a)+  -> Int+  -> IntMap s a+  -> SomeIntMapWith (SupersetProof 'Int s) a+updateWithKey f k (IntMap m) = SomeIntMapWith+  (IntMap $ IntMap.updateWithKey (f . unsafeKey) k m)   $ SupersetProof unsafeSubset  -- | If the given key is in the map, update or delete it using the given@@ -221,8 +336,38 @@     (v', !m') -> ((unsafeKey k,) <$> v',)       $ SomeIntMapWith (IntMap m') $ SupersetProof unsafeSubset +-- | Given two maps proven to have the same keys, for each key apply the+-- function to the associated values, to obtain a new map with the same keys.+zipWithKey+  :: forall s a b c. (Key s -> a -> b -> c)+  -> IntMap s a+  -> IntMap s b+  -> IntMap s c+zipWithKey f (IntMap m1) (IntMap m2) = IntMap+  $ IntMap.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)+    (\m -> if IntMap.null m+      then IntMap.empty+      else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")+    (\m -> if IntMap.null m+      then IntMap.empty+      else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")+    --  ^ Work around https://github.com/haskell/containers/issues/979+    m1+    m2+ -- | Return the union of two maps, with a given combining function for keys that -- exist in both maps simultaneously.+unionWith+  :: forall s t a. (a -> a -> a)+  -> IntMap s a+  -> IntMap t a+  -> SomeIntMapWith (UnionProof 'Int s t) a+unionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith+  (IntMap $ IntMap.unionWith f m1 m2)+  $ UnionProof unsafeSubset unsafeSubsetWith2++-- | Return the union of two maps, with a given combining function for keys that+-- exist in both maps simultaneously. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@ -- respectively.@@ -235,8 +380,19 @@   = SomeIntMapWith (IntMap $ IntMap.unionWithKey (f . reallyUnsafeRefine) m1 m2)     $ UnionProof unsafeSubset unsafeSubsetWith2 --- | For keys that appear in both maps, the given function decides whether the--- key is removed from the first map.+-- | Return the first map, but for keys that appear in both maps, the given+-- function decides whether the key is removed.+differenceWith+  :: forall s t a b. (a -> b -> Maybe a)+  -> IntMap s a+  -> IntMap t b+  -> SomeIntMapWith (PartialDifferenceProof 'Int s t) a+differenceWith f (IntMap m1) (IntMap m2) = SomeIntMapWith+  (IntMap $ IntMap.differenceWith f m1 m2)+  $ PartialDifferenceProof unsafeSubset unsafeSubset++-- | Return the first map, but for keys that appear in both maps, the given+-- function decides whether the key is removed. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@ -- respectively.@@ -253,6 +409,16 @@   $ PartialDifferenceProof unsafeSubset unsafeSubset  -- | Return the intersection of two maps with the given combining function.+intersectionWith+  :: forall s t a b c. (a -> b -> c)+  -> IntMap s a+  -> IntMap t b+  -> SomeIntMapWith (IntersectionProof 'Int s t) c+intersectionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith+  (IntMap $ IntMap.intersectionWith f m1 m2)+  $ IntersectionProof unsafeSubset unsafeSubsetWith2++-- | Return the intersection of two maps with the given combining function. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@ -- respectively.@@ -268,6 +434,10 @@   (IntMap $ IntMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)   $ IntersectionProof unsafeSubset unsafeSubsetWith2 +-- | Apply a function to all values in a map. The set of keys remains the same.+map :: forall s a b. (a -> b) -> IntMap s a -> IntMap s b+map = coerce $ IntMap.map @a @b+ -- | Thread an accumularing argument through the map in ascending order of keys. mapAccumLWithKey   :: forall s a b c. (a -> Key s -> b -> (a, c))@@ -287,6 +457,27 @@ mapAccumRWithKey = gcoerceWith (unsafeCastKey @s) $ coerce   $ IntMap.mapAccumRWithKey @a @b @c +-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results+-- into a new map. For keys that were mapped to the same new key, the value+-- corresponding to the greatest of the original keys is retained.+mapKeys+  :: forall s a. (Key s -> Int)+  -> IntMap s a+  -> SomeIntMapWith (MapProof 'Int s Int Int) a+mapKeys g (IntMap m)+  = SomeIntMapWith (IntMap $ IntMap.mapKeys (g . unsafeKey) m)+    $ MapProof (unsafeKey . g) \k2 ->+      case IntMap.lookup (unrefine k2) backMap of+        Nothing -> error+          "mapKeys: bug: Data.IntMap.Refined has been subverted"+        Just k1 -> k1+  where+    ~backMap = IntMap.fromList+      [ (k2, unsafeKey k1)+      | k1 <- IntMap.keys m+      , let !k2 = g $ unsafeKey k1+      ]+ -- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the -- results into a new map. For keys that were mapped to the same new key, @c@ -- acts as the combining function for corresponding values.@@ -309,6 +500,15 @@       , let !k2 = g $ unsafeKey k1       ] +-- | Apply a function to all values in a map and collect only the 'Just'+-- results, returning a potentially smaller map.+mapMaybe+  :: forall s a b. (a -> Maybe b)+  -> IntMap s a+  -> SomeIntMapWith (SupersetProof 'Int s) b+mapMaybe f (IntMap m) = SomeIntMapWith (IntMap $ IntMap.mapMaybe f m)+  $ SupersetProof unsafeSubset+ -- | Apply a function to all values in a map, together with their corresponding -- keys, and collect only the 'Just' results, returning a potentially smaller -- map.@@ -319,6 +519,23 @@ mapMaybeWithKey f (IntMap m)   = SomeIntMapWith (IntMap $ IntMap.mapMaybeWithKey (f . unsafeKey) m)     $ SupersetProof unsafeSubset++-- | Apply a function to all values in a map and collect the 'Left' and 'Right'+-- results into separate (disjoint) maps.+mapEither+  :: forall s a b c. (a -> Either b c)+  -> IntMap s a+  -> Some2IntMapWith (PartitionProof 'Int s Int) b c+mapEither p (IntMap m)+  = case IntMap.mapEither p m of+    (m1, m2) -> Some2IntMapWith (IntMap m1) (IntMap m2) $ PartitionProof+      do \k -> case IntMap.lookup (unrefine k) m of+          Nothing -> error+            "mapEither: bug: Data.IntMap.Refined has been subverted"+          Just x -> case p x of+            Left _ -> Left $ unsafeKey $ unrefine k+            Right _ -> Right $ unsafeKey $ unrefine k+      unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g  -- | Apply a function to all values in a map, together with their corresponding -- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

@@ -34,18 +34,26 @@   , SingletonProof(..)   , fromSet   , Common.fromIntMap+  , Common.verifyIntMap+  , fromTraversable+  , fromTraversableWith   , fromTraversableWithKey   , FromTraversableProof(..)   -- * Insertion   , insert+  , insertWith+  , insertWithKey   , InsertProof(..)   , reinsert   , insertLookupWithKey   -- * Deletion/Update   , Common.delete+  , adjust'   , adjust   , adjustWithKey+  , update'   , update+  , updateWithKey   , updateLookupWithKey   -- * Query   , Common.lookup@@ -61,21 +69,29 @@   , Common.disjoint   , DisjointProof(..)   -- * Combine+  , zipWith   , zipWithKey   , bind+  , Common.union+  , unionWith   , unionWithKey   , UnionProof(..)   , Common.difference   , DifferenceProof(..)+  , differenceWith   , differenceWithKey   , PartialDifferenceProof(..)+  , Common.intersection+  , intersectionWith   , intersectionWithKey   , IntersectionProof(..)   -- * Traversal+  , map   , mapWithKey   , traverseWithKey   , mapAccumLWithKey   , mapAccumRWithKey+  , mapKeys   , mapKeysWith   , MapProof(..)   , backpermuteKeys@@ -93,12 +109,19 @@   -- * Filter   , Common.restrictKeys   , Common.withoutKeys+  , Common.filter+  , Common.filterKeys   , Common.filterWithKey+  , Common.partition   , Common.partitionWithKey   , PartitionProof(..)+  , Common.takeWhileAntitone+  , Common.dropWhileAntitone   , Common.spanAntitone   , PartialPartitionProof(..)+  , mapMaybe   , mapMaybeWithKey+  , mapEither   , mapEitherWithKey   , Common.splitLookup   , SplitProof(..)@@ -122,14 +145,14 @@ import qualified Data.IntMap.Strict as IntMap import           Data.IntMap.Common.Refined   ( IntMap(..), Key, unsafeCastKey, unsafeKey, SomeIntMapWith(..)-  , Some2IntMapWith(..), (!)+  , Some2IntMapWith(..), (!), zipWith   ) import qualified Data.IntMap.Common.Refined as Common import           Data.Proxy import           Data.Reflection import           Data.Traversable import           Data.Type.Coercion-import           Prelude hiding (lookup, null)+import           Prelude hiding (lookup, map, null, zipWith) import           Refined import           Refined.Unsafe @@ -145,17 +168,52 @@ fromSet :: forall s a. KnownIntSet s => (Key s -> a) -> IntMap s a fromSet f = IntMap $ IntMap.fromSet (f . unsafeKey) (reflect $ Proxy @s) --- | Create a map from an arbitrary traversable of key-value pairs.+-- | Create a map from an arbitrary traversable of key-value pairs. If a key is+-- repeated, the retained value is the last one in traversal order. If you're+-- looking for @fromList@, this is the function you want.+fromTraversable+  :: forall t a. Traversable t+  => t (Int, a) -> SomeIntMapWith (FromTraversableProof 'Int t Int) a+fromTraversable xs = SomeIntMapWith (IntMap m) $ FromTraversableProof proof+  where+    (m, proof) = mapAccumL+      (\s (k, v) -> let !s' = IntMap.insert k v s in (s', unsafeKey k))+      IntMap.empty+      xs++-- | Create a map from an arbitrary traversable of key-value pairs, with a+-- function for combining values for repeated keys. The function is called as if+-- by 'foldl1', but flipped:+--+-- @+-- 'fromTraversableWith' f [(k, x1), (k, x2), (k, x3)]+--   = 'singleton' k (f x3 (f x2 x1))+-- @+fromTraversableWith+  :: forall t a. Traversable t+  => (a -> a -> a)+  -> t (Int, a)+  -> SomeIntMapWith (FromTraversableProof 'Int t Int) a+fromTraversableWith f xs+  = SomeIntMapWith (IntMap m) $ FromTraversableProof proof+  where+    (m, proof) = mapAccumL+      (\s (k, v) -> let !s' = IntMap.insertWith f k v s in (s', unsafeKey k))+      IntMap.empty+      xs++-- | Create a map from an arbitrary traversable of key-value pairs. Like+-- 'fromTraversableWith', but the combining function has access to the key. fromTraversableWithKey   :: forall t a. Traversable t   => (Int -> a -> a -> a)   -> t (Int, a)   -> SomeIntMapWith (FromTraversableProof 'Int t Int) a-fromTraversableWithKey f xs = SomeIntMapWith (IntMap m)-  $ FromTraversableProof proof+fromTraversableWithKey f xs+  = SomeIntMapWith (IntMap m) $ FromTraversableProof proof   where     (m, proof) = mapAccumL-      (\s (k, v) -> (IntMap.insertWithKey f k v s, unsafeKey k))+      (\s (k, v) -> let !s' = IntMap.insertWithKey f k v s in (s', unsafeKey k))       IntMap.empty       xs @@ -170,8 +228,39 @@ insert k v (IntMap m) = SomeIntMapWith (IntMap $ IntMap.insert k v m)   $ InsertProof (unsafeKey k) unsafeSubset +-- | Insert a key-value pair into the map to obtain a potentially larger map,+-- guaranteed to contain the given key. If the key was already present, the+-- supplied function is used to combine the new value with the old (in that+-- order).+insertWith+  :: forall s a. (a -> a -> a)+  -> Int+  -> a+  -> IntMap s a+  -> SomeIntMapWith (InsertProof 'Int Int s) a+insertWith f k v (IntMap m) = SomeIntMapWith+  (IntMap $ IntMap.insertWith f k v m)+  $ InsertProof (unsafeKey k) unsafeSubset++-- | Insert a key-value pair into the map to obtain a potentially larger map,+-- guaranteed to contain the given key. Like 'insertWith', but the combining+-- function has access to the key, which is guaranteed to be in the old map.+insertWithKey+  :: forall s a. (Key s -> a -> a -> a)+  -> Int+  -> a+  -> IntMap s a+  -> SomeIntMapWith (InsertProof 'Int Int s) a+insertWithKey f k v (IntMap m) = SomeIntMapWith+  (IntMap $ IntMap.insertWithKey (f . unsafeKey) k v m)+  $ InsertProof (unsafeKey k) unsafeSubset+ -- | Overwrite a key-value pair that is known to already be in the map. The set -- of keys remains the same.+--+-- @+-- 'reinsert' k v = 'adjust (const v) k'+-- @ reinsert   :: forall s a. Key s -> a -> IntMap s a -> IntMap s a reinsert = gcoerceWith (unsafeCastKey @s) $ coerce $ IntMap.insert @a@@ -190,10 +279,15 @@     (v', !m') -> ((unsafeKey k,) <$> v',)       $ SomeIntMapWith (IntMap m') $ InsertProof (unsafeKey k) unsafeSubset +-- | If the given key is in the map, update the value at that key using the+-- given function. In any case, the set of keys remains the same.+adjust' :: forall s a. (a -> a) -> Int -> IntMap s a -> IntMap s a+adjust' = coerce $ IntMap.adjust @a+ -- | Update the value at a specific key known the be in the map using the given -- function. The set of keys remains the same. adjust :: forall s a. (a -> a) -> Key s -> IntMap s a -> IntMap s a-adjust = gcoerceWith (unsafeCastKey @s) $ coerce $ IntMap.adjust @a+adjust = gcoerceWith (unsafeCastKey @s) $ coerce $ adjust' @s @a  -- | If the given key is in the map, update the associated value using the given -- function with a proof that the key was in the map; otherwise return the map@@ -203,6 +297,16 @@ adjustWithKey = gcoerceWith (unsafeCastKey @s) $ coerce   $ IntMap.adjustWithKey @a +-- | If a key is present in the map, update its value or delete it using the+-- given function, returning a potentially smaller map.+update'+  :: forall s a. (a -> Maybe a)+  -> Int+  -> IntMap s a+  -> SomeIntMapWith (SupersetProof 'Int s) a+update' f k (IntMap m) = SomeIntMapWith (IntMap $ IntMap.update f k m)+  $ SupersetProof unsafeSubset+ -- | Update or delete a key known to be in the map using the given function, -- returning a potentially smaller map. update@@ -210,7 +314,18 @@   -> Key s   -> IntMap s a   -> SomeIntMapWith (SupersetProof 'Int s) a-update f k (IntMap m) = SomeIntMapWith (IntMap $ IntMap.update f (unrefine k) m)+update = gcoerceWith (unsafeCastKey @s) $ coerce $ update' @s @a++-- | If a key is present in the map, update its value or delete it using the+-- given function with a proof that the key was in the map, returning a+-- potentially smaller map.+updateWithKey+  :: forall s a. (Key s -> a -> Maybe a)+  -> Int+  -> IntMap s a+  -> SomeIntMapWith (SupersetProof 'Int s) a+updateWithKey f k (IntMap m) = SomeIntMapWith+  (IntMap $ IntMap.updateWithKey (f . unsafeKey) k m)   $ SupersetProof unsafeSubset  -- | If the given key is in the map, update or delete it using the given@@ -250,6 +365,17 @@  -- | Return the union of two maps, with a given combining function for keys that -- exist in both maps simultaneously.+unionWith+  :: forall s t a. (a -> a -> a)+  -> IntMap s a+  -> IntMap t a+  -> SomeIntMapWith (UnionProof 'Int s t) a+unionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith+  (IntMap $ IntMap.unionWith f m1 m2)+  $ UnionProof unsafeSubset unsafeSubsetWith2++-- | Return the union of two maps, with a given combining function for keys that+-- exist in both maps simultaneously. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@ -- respectively.@@ -262,8 +388,19 @@   = SomeIntMapWith (IntMap $ IntMap.unionWithKey (f . reallyUnsafeRefine) m1 m2)     $ UnionProof unsafeSubset unsafeSubsetWith2 --- | For keys that appear in both maps, the given function decides whether the--- key is removed from the first map.+-- | Return the first map, but for keys that appear in both maps, the given+-- function decides whether the key is removed.+differenceWith+  :: forall s t a b. (a -> b -> Maybe a)+  -> IntMap s a+  -> IntMap t b+  -> SomeIntMapWith (PartialDifferenceProof 'Int s t) a+differenceWith f (IntMap m1) (IntMap m2) = SomeIntMapWith+  (IntMap $ IntMap.differenceWith f m1 m2)+  $ PartialDifferenceProof unsafeSubset unsafeSubset++-- | Return the first map, but for keys that appear in both maps, the given+-- function decides whether the key is removed. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@ -- respectively.@@ -280,6 +417,16 @@   $ PartialDifferenceProof unsafeSubset unsafeSubset  -- | Return the intersection of two maps with the given combining function.+intersectionWith+  :: forall s t a b c. (a -> b -> c)+  -> IntMap s a+  -> IntMap t b+  -> SomeIntMapWith (IntersectionProof 'Int s t) c+intersectionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith+  (IntMap $ IntMap.intersectionWith f m1 m2)+  $ IntersectionProof unsafeSubset unsafeSubsetWith2++-- | Return the intersection of two maps with the given combining function. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@ -- respectively.@@ -295,6 +442,10 @@   (IntMap $ IntMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)   $ IntersectionProof unsafeSubset unsafeSubsetWith2 +-- | Apply a function to all values in a map. The set of keys remains the same.+map :: forall s a b. (a -> b) -> IntMap s a -> IntMap s b+map = coerce $ IntMap.map @a @b+ -- | Apply a function to all values in a map, together with their corresponding -- keys, that are proven to be in the map. The set of keys remains the same. mapWithKey :: forall s a b. (Key s -> a -> b) -> IntMap s a -> IntMap s b@@ -328,6 +479,27 @@ mapAccumRWithKey = gcoerceWith (unsafeCastKey @s) $ coerce   $ IntMap.mapAccumRWithKey @a @b @c +-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results+-- into a new map. For keys that were mapped to the same new key, the value+-- corresponding to the greatest of the original keys is retained.+mapKeys+  :: forall s a. (Key s -> Int)+  -> IntMap s a+  -> SomeIntMapWith (MapProof 'Int s Int Int) a+mapKeys g (IntMap m)+  = SomeIntMapWith (IntMap $ IntMap.mapKeys (g . unsafeKey) m)+    $ MapProof (unsafeKey . g) \k2 ->+      case IntMap.lookup (unrefine k2) backMap of+        Nothing -> error+          "mapKeys: bug: Data.IntMap.Strict.Refined has been subverted"+        Just k1 -> k1+  where+    ~backMap = IntMap.fromList+      [ (k2, unsafeKey k1)+      | k1 <- IntMap.keys m+      , let !k2 = g $ unsafeKey k1+      ]+ -- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the -- results into a new map. For keys that were mapped to the same new key, @c@ -- acts as the combining function for corresponding values.@@ -350,6 +522,15 @@       , let !k2 = g $ unsafeKey k1       ] +-- | Apply a function to all values in a map and collect only the 'Just'+-- results, returning a potentially smaller map.+mapMaybe+  :: forall s a b. (a -> Maybe b)+  -> IntMap s a+  -> SomeIntMapWith (SupersetProof 'Int s) b+mapMaybe f (IntMap m) = SomeIntMapWith (IntMap $ IntMap.mapMaybe f m)+  $ SupersetProof unsafeSubset+ -- | Apply a function to all values in a map, together with their corresponding -- keys, and collect only the 'Just' results, returning a potentially smaller -- map.@@ -360,6 +541,23 @@ mapMaybeWithKey f (IntMap m)   = SomeIntMapWith (IntMap $ IntMap.mapMaybeWithKey (f . unsafeKey) m)     $ SupersetProof unsafeSubset++-- | Apply a function to all values in a map and collect the 'Left' and 'Right'+-- results into separate (disjoint) maps.+mapEither+  :: forall s a b c. (a -> Either b c)+  -> IntMap s a+  -> Some2IntMapWith (PartitionProof 'Int s Int) b c+mapEither p (IntMap m)+  = case IntMap.mapEither p m of+    (m1, m2) -> Some2IntMapWith (IntMap m1) (IntMap m2) $ PartitionProof+      do \k -> case IntMap.lookup (unrefine k) m of+          Nothing -> error+            "mapEither: bug: Data.IntMap.Refined has been subverted"+          Just x -> case p x of+            Left _ -> Left $ unsafeKey $ unrefine k+            Right _ -> Right $ unsafeKey $ unrefine k+      unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g  -- | Apply a function to all values in a map, together with their corresponding -- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

@@ -169,7 +169,7 @@ -- you a way to refer to the set (the parameter @s@), e.g.: -- -- @--- 'withIntSet' ('fromIntSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s+-- 'withIntSet' ('fromIntSet' ...) $ \\(_ :: 'Proxy' s) -> doSomethingWith \@s -- @ withIntSet   :: forall r. SomeIntSet -> (forall s. KnownIntSet s => Proxy s -> r) -> r

@@ -16,13 +16,19 @@ import qualified Data.Map as Map import           Data.Proxy import           Data.Reflection+import qualified Data.Set as Set import           Data.Traversable.WithIndex import           Data.Type.Coercion import           Data.Type.Equality ((:~:)(..))+import           Prelude hiding (zipWith) import           Refined import           Refined.Unsafe import           Unsafe.Coerce +#if MIN_VERSION_containers(0, 6, 3)+import           Data.Bifoldable+#endif+ #if MIN_VERSION_containers(0, 6, 2) #elif MIN_VERSION_containers(0, 5, 8) import           Data.Functor.Const (Const(..))@@ -33,7 +39,11 @@ import qualified Data.Map.Strict as MapStrict #endif +#if MIN_VERSION_containers(0, 5, 9) || MIN_VERSION_hashable(1, 4, 0)+import           Data.Functor.Classes+#endif + -- | A wrapper around a regular 'Data.Map.Map' with a type parameter @s@ -- identifying the set of keys present in the map. --@@ -50,6 +60,12 @@ #if MIN_VERSION_hashable(1, 3, 4)   deriving newtype (Hashable.Hashable) #endif+#if MIN_VERSION_containers(0, 6, 3)+  deriving newtype (Bifoldable)+#endif+#if MIN_VERSION_containers(0, 5, 9) || MIN_VERSION_hashable(1, 4, 0)+  deriving newtype (Eq1, Eq2, Ord1, Ord2, Show1, Show2)+#endif   deriving stock (Traversable) type role Map nominal nominal representational @@ -94,7 +110,7 @@ -- parameter @s@), e.g.: -- -- @--- 'withMap' ('fromMap' ...) $ \(m :: 'Map' s k a) -> doSomethingWith \@s+-- 'withMap' ('fromMap' ...) $ \\(m :: 'Map' s k a) -> doSomethingWith \@s -- @ withMap :: forall k a r. SomeMap k a -> (forall s. Map s k a -> r) -> r withMap (SomeMap m) k = k m@@ -103,6 +119,14 @@ fromMap :: forall k a. Map.Map k a -> SomeMap k a fromMap m = SomeMap (Map m) +-- | Given a set of keys @s@ known ahead of time, verify whether a regular+-- 'Data.Map.Map' has exactly that set of keys.+verifyMap+  :: forall s k a. (Eq k, KnownSet s k) => Map.Map k a -> Maybe (Map s k a)+verifyMap m+  | Map.keys m == Set.toList (reflect $ Proxy @s) = Just (Map m)+  | otherwise = Nothing+ -- | An existential wrapper for a 'Map' with an as-yet-unknown set of keys, -- together with a proof of some fact @p@ about the set. Pattern matching on it -- gives you a way to refer to the set (the parameter @s@). Functions that@@ -236,21 +260,33 @@  -- | Given two maps proven to have the same keys, for each key apply the -- function to the associated values, to obtain a new map with the same keys.-zipWithKey+zipWith   :: forall s k a b c. Ord k-  => (Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c-zipWithKey f (Map m1) (Map m2) = Map-  $ Map.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)+  => (a -> b -> c) -> Map s k a -> Map s k b -> Map s k c+zipWith f (Map m1) (Map m2) = Map+  $ Map.mergeWithKey (\_ x y -> Just $ f x y)     (\m -> if Map.null m       then Map.empty-      else error "zipWithKey: bug: Data.Map.Refined has been subverted")+      else error "zipWith: bug: Data.Map.Refined has been subverted")     (\m -> if Map.null m       then Map.empty-      else error "zipWithKey: bug: Data.Map.Refined has been subverted")+      else error "zipWith: bug: Data.Map.Refined has been subverted")     --  ^ Work around https://github.com/haskell/containers/issues/979     m1     m2 +-- | Return the union of two maps. For keys that exist in both maps, the value+-- is taken from the first map.+--+-- @+-- 'union' = unionWith 'const'+-- @+union+  :: forall s t k a. Ord k+  => Map s k a -> Map t k a -> SomeMapWith (UnionProof 'Regular s t) k a+union (Map m1) (Map m2) = SomeMapWith (Map $ Map.union m1 m2)+  $ UnionProof unsafeSubset unsafeSubsetWith2+ -- | Remove the keys that appear in the second map from the first map. difference   :: forall s t k a b. Ord k@@ -258,6 +294,20 @@ difference (Map m1) (Map m2) = SomeMapWith (Map $ Map.difference m1 m2)   $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset +-- | Return the intersection of two maps, taking values from the first map.+--+-- @+-- 'intersection' = intersectionWith 'const'+-- @+intersection+  :: forall s t k a b. Ord k+  => Map s k a+  -> Map t k b+  -> SomeMapWith (IntersectionProof 'Regular s t) k a+intersection (Map m1) (Map m2)+  = SomeMapWith (Map $ Map.intersection m1 m2)+    $ IntersectionProof unsafeSubset unsafeSubsetWith2+ -- | Apply a function to all values in a map, together with their corresponding -- keys, that are proven to be in the map. The set of keys remains the same. mapWithKey :: forall s k a b. (Key s k -> a -> b) -> Map s k a -> Map s k b@@ -314,6 +364,29 @@ toDescList :: forall s k a. Map s k a -> [(Key s k, a)] toDescList = gcoerceWith (unsafeCastKey @s @k) $ coerce $ Map.toDescList @k @a +-- | Retain only the values that satisfy the predicate, returning a potentially+-- smaller map.+filter+  :: forall s k a. (a -> Bool)+  -> Map s k a+  -> SomeMapWith (SupersetProof 'Regular s) k a+filter p (Map m) = SomeMapWith (Map $ Map.filter p m)+  $ SupersetProof unsafeSubset++-- | Retain only the keys that satisfy the predicate, returning a potentially+-- smaller map.+filterKeys+  :: forall s k a. (Key s k -> Bool)+  -> Map s k a+  -> SomeMapWith (SupersetProof 'Regular s) k a+filterKeys p (Map m) = SomeMapWith+#if MIN_VERSION_containers(0, 8, 0)+  (Map $ Map.filterKeys (p . unsafeKey) m)+#else+  (Map $ Map.filterWithKey (\k _ -> p (unsafeKey k)) m)+#endif+  $ SupersetProof unsafeSubset+ -- | Retain only the key-value pairs that satisfy the predicate, returning a -- potentially smaller map. filterWithKey@@ -348,6 +421,22 @@ #endif   $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset +-- | Partition a map into two disjoint submaps: those whose values satisfy the+-- predicate, and those whose don't.+partition+  :: forall s k a. Ord k -- TODO: this is only used in the proof+  => (a -> Bool)+  -> Map s k a+  -> Some2MapWith (PartitionProof 'Regular s k) k a a+partition p (Map m) = case Map.partition p m of+  (m1, m2) -> Some2MapWith (Map m1) (Map m2) $ PartitionProof+    do \k -> case Map.lookup (unrefine k) m of+        Nothing -> error "partition: bug: Data.Map.Refined has been subverted"+        Just x -> if p x+          then Left $ unsafeKey $ unrefine k+          else Right $ unsafeKey $ unrefine k+    unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g+ -- | Partition a map into two disjoint submaps: those whose key-value pairs -- satisfy the predicate, and those whose don't. partitionWithKey@@ -365,6 +454,43 @@           else Right $ unsafeKey $ unrefine k     unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g +-- | Take the a submap of keys up to a point where the predicate stops holding.+--+-- If @p@ is antitone ( \(\forall x y, x < y \implies p(x) \ge p(y)\) ), then+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is+-- chosen in an unspecified way.+takeWhileAntitone+  :: forall s k a. (Key s k -> Bool)+  -> Map s k a+  -> SomeMapWith (SupersetProof 'Regular s) k a+takeWhileAntitone p (Map m) = SomeMapWith+#if MIN_VERSION_containers(0, 5, 8)+  (Map $ Map.takeWhileAntitone (p . unsafeKey) m)+#else+  (Map $ Map.fromDistinctAscList+    $ List.takeWhile (p . unsafeKey . fst) $ Map.toAscList m)+#endif+  $ SupersetProof unsafeSubset++-- | Take the a submap of keys starting from a point where the predicate stops+-- holding.+--+-- If @p@ is antitone ( \(\forall x y, x < y \implies p(x) \ge p(y)\) ), then+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is+-- chosen in an unspecified way.+dropWhileAntitone+  :: forall s k a. (Key s k -> Bool)+  -> Map s k a+  -> SomeMapWith (SupersetProof 'Regular s) k a+dropWhileAntitone p (Map m) = SomeMapWith+#if MIN_VERSION_containers(0, 5, 8)+  (Map $ Map.dropWhileAntitone (p . unsafeKey) m)+#else+  (Map $ Map.fromDistinctAscList+    $ List.dropWhile (p . unsafeKey . fst) $ Map.toAscList m)+#endif+  $ SupersetProof unsafeSubset+ -- | Divide a map into two disjoint submaps at a point where the predicate on -- the keys stops holding. --@@ -437,15 +563,15 @@ castKey = castRefined  -- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps--- can be interconverted too. For example, 'zipWithKey' can be implemented via--- 'Data.Map.Refined.intersectionWithKey' by proving that the set of keys--- remains unchanged:+-- can be interconverted too. For example, 'Data.Map.Refined.zipWithKey' can be+-- implemented via 'Data.Map.Refined.intersectionWithKey' by proving that the+-- set of keys remains unchanged: -- -- @--- 'zipWithKey'+-- 'Data.Map.Refined.zipWithKey' --   :: forall s k a b c. 'Ord' k --   => ('Key' s k -> a -> b -> c) -> 'Map' s k a -> 'Map' s k b -> 'Map' s k c--- 'zipWithKey' f m1 m2+-- 'Data.Map.Refined.zipWithKey' f m1 m2 --   | v'SomeMapWith' @r m proof <- 'Data.Map.Refined.intersectionWithKey' (f . 'andLeft') m1 m2 --   , v'IntersectionProof' p1 p2 <- proof --   , ( v'Coercion' :: t'Coercion' ('Map' r k c) ('Map' s k c))@@ -470,10 +596,10 @@   itraverse = traverseWithKey  -- | Similar to the instance for functions -- zip corresponding keys. To use--- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWithKey'.+-- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWith'. instance (Ord k, KnownSet s k) => Applicative (Map s k) where   pure x = fromSet \_ -> x-  (<*>) = zipWithKey (const id)+  (<*>) = zipWith id  -- | @'bind' m f@ is a map that for each key @k :: 'Key' s k@, contains the -- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.@@ -493,7 +619,7 @@  -- | Append the values at the corresponding keys instance (Ord k, Semigroup a) => Semigroup (Map s k a) where-  (<>) = zipWithKey (const (<>))+  (<>) = zipWith (<>)  instance (Ord k, KnownSet s k, Monoid a) => Monoid (Map s k a) where   mempty = fromSet \_ -> mempty

@@ -43,18 +43,26 @@   , SingletonProof(..)   , fromSet   , Common.fromMap+  , Common.verifyMap+  , fromTraversable+  , fromTraversableWith   , fromTraversableWithKey   , FromTraversableProof(..)   -- * Insertion   , insert+  , insertWith+  , insertWithKey   , InsertProof(..)   , reinsert   , insertLookupWithKey   -- * Deletion/Update   , Common.delete+  , adjust'   , adjust   , adjustWithKey+  , update'   , update+  , updateWithKey   , updateLookupWithKey   -- * Query   , Common.lookup@@ -70,21 +78,29 @@   , Common.disjoint   , DisjointProof(..)   -- * Combine+  , zipWith   , zipWithKey   , bind+  , Common.union+  , unionWith   , unionWithKey   , UnionProof(..)   , Common.difference   , DifferenceProof(..)+  , differenceWith   , differenceWithKey   , PartialDifferenceProof(..)+  , Common.intersection+  , intersectionWith   , intersectionWithKey   , IntersectionProof(..)   -- * Traversal+  , map   , mapWithKey   , traverseWithKey   , mapAccumLWithKey   , mapAccumRWithKey+  , mapKeys   , mapKeysWith   , MapProof(..)   , backpermuteKeys@@ -102,12 +118,19 @@   -- * Filter   , Common.restrictKeys   , Common.withoutKeys+  , Common.filter+  , Common.filterKeys   , Common.filterWithKey+  , Common.partition   , Common.partitionWithKey   , PartitionProof(..)+  , Common.takeWhileAntitone+  , Common.dropWhileAntitone   , Common.spanAntitone   , PartialPartitionProof(..)+  , mapMaybe   , mapMaybeWithKey+  , mapEither   , mapEitherWithKey   , Common.splitLookup   , SplitProof(..)@@ -131,12 +154,12 @@ import qualified Data.Map as Map import           Data.Map.Common.Refined   ( Map(..), Key, unsafeCastKey, unsafeKey, SomeMapWith(..), Some2MapWith(..)-  , fromSet, (!), zipWithKey, mapWithKey, traverseWithKey, bind+  , fromSet, (!), zipWith, mapWithKey, traverseWithKey, bind   ) import qualified Data.Map.Common.Refined as Common import           Data.Traversable import           Data.Type.Coercion-import           Prelude hiding (lookup, null)+import           Prelude hiding (lookup, map, null, zipWith) import           Refined import           Refined.Unsafe @@ -147,7 +170,41 @@ singleton k v = SomeMapWith (Map $ Map.singleton k v)   $ SingletonProof (unsafeKey k) --- | Create a map from an arbitrary traversable of key-value pairs.+-- | Create a map from an arbitrary traversable of key-value pairs. If a key is+-- repeated, the retained value is the last one in traversal order. If you're+-- looking for @fromList@, this is the function you want.+fromTraversable+  :: forall t k a. (Traversable t, Ord k)+  => t (k, a) -> SomeMapWith (FromTraversableProof 'Regular t k) k a+fromTraversable xs = SomeMapWith (Map m) $ FromTraversableProof proof+  where+    (m, proof) = mapAccumL+      (\s (k, v) -> let !s' = Map.insert k v s in (s', unsafeKey k))+      Map.empty+      xs++-- | Create a map from an arbitrary traversable of key-value pairs, with a+-- function for combining values for repeated keys. The function is called as if+-- by 'foldl1', but flipped:+--+-- @+-- 'fromTraversableWith' f [(k, x1), (k, x2), (k, x3)]+--   = 'singleton' k (f x3 (f x2 x1))+-- @+fromTraversableWith+  :: forall t k a. (Traversable t, Ord k)+  => (a -> a -> a)+  -> t (k, a)+  -> SomeMapWith (FromTraversableProof 'Regular t k) k a+fromTraversableWith f xs = SomeMapWith (Map m) $ FromTraversableProof proof+  where+    (m, proof) = mapAccumL+      (\s (k, v) -> let !s' = Map.insertWith f k v s in (s', unsafeKey k))+      Map.empty+      xs++-- | Create a map from an arbitrary traversable of key-value pairs. Like+-- 'fromTraversableWith', but the combining function has access to the key. fromTraversableWithKey   :: forall t k a. (Traversable t, Ord k)   => (k -> a -> a -> a)@@ -169,8 +226,40 @@ insert k v (Map m) = SomeMapWith (Map $ Map.insert k v m)   $ InsertProof (unsafeKey k) unsafeSubset +-- | Insert a key-value pair into the map to obtain a potentially larger map,+-- guaranteed to contain the given key. If the key was already present, the+-- supplied function is used to combine the new value with the old (in that+-- order).+insertWith+  :: forall s k a. Ord k+  => (a -> a -> a)+  -> k+  -> a+  -> Map s k a+  -> SomeMapWith (InsertProof 'Regular k s) k a+insertWith f k v (Map m) = SomeMapWith (Map $ Map.insertWith f k v m)+  $ InsertProof (unsafeKey k) unsafeSubset++-- | Insert a key-value pair into the map to obtain a potentially larger map,+-- guaranteed to contain the given key. Like 'insertWith', but the combining+-- function has access to the key, which is guaranteed to be in the old map.+insertWithKey+  :: forall s k a. Ord k+  => (Key s k -> a -> a -> a)+  -> k+  -> a+  -> Map s k a+  -> SomeMapWith (InsertProof 'Regular k s) k a+insertWithKey f k v (Map m) = SomeMapWith+  (Map $ Map.insertWithKey (f . unsafeKey) k v m)+  $ InsertProof (unsafeKey k) unsafeSubset+ -- | Overwrite a key-value pair that is known to already be in the map. The set -- of keys remains the same.+--+-- @+-- 'reinsert' k v = 'adjust (const v) k'+-- @ reinsert   :: forall s k a. Ord k   => Key s k -> a -> Map s k a -> Map s k a@@ -191,10 +280,15 @@     (v', !m') -> ((unsafeKey k,) <$> v',)       $ SomeMapWith (Map m') $ InsertProof (unsafeKey k) unsafeSubset +-- | If the given key is in the map, update the value at that key using the+-- given function. In any case, the set of keys remains the same.+adjust' :: forall s k a. Ord k => (a -> a) -> k -> Map s k a -> Map s k a+adjust' = coerce $ Map.adjust @k @a+ -- | Update the value at a specific key known the be in the map using the given -- function. The set of keys remains the same. adjust :: forall s k a. Ord k => (a -> a) -> Key s k -> Map s k a -> Map s k a-adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ Map.adjust @k @a+adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ adjust' @s @k @a  -- | If the given key is in the map, update the associated value using the given -- function with a proof that the key was in the map; otherwise return the map@@ -204,6 +298,17 @@ adjustWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce   $ Map.adjustWithKey @k @a +-- | If a key is present in the map, update its value or delete it using the+-- given function, returning a potentially smaller map.+update'+  :: forall s k a. Ord k+  => (a -> Maybe a)+  -> k+  -> Map s k a+  -> SomeMapWith (SupersetProof 'Regular s) k a+update' f k (Map m) = SomeMapWith (Map $ Map.update f k m)+  $ SupersetProof unsafeSubset+ -- | Update or delete a key known to be in the map using the given function, -- returning a potentially smaller map. update@@ -212,7 +317,19 @@   -> Key s k   -> Map s k a   -> SomeMapWith (SupersetProof 'Regular s) k a-update f k (Map m) = SomeMapWith (Map $ Map.update f (unrefine k) m)+update = gcoerceWith (unsafeCastKey @s @k) $ coerce $ update' @s @k @a++-- | If a key is present in the map, update its value or delete it using the+-- given function with a proof that the key was in the map, returning a+-- potentially smaller map.+updateWithKey+  :: forall s k a. Ord k+  => (Key s k -> a -> Maybe a)+  -> k+  -> Map s k a+  -> SomeMapWith (SupersetProof 'Regular s) k a+updateWithKey f k (Map m) = SomeMapWith+  (Map $ Map.updateWithKey (f . unsafeKey) k m)   $ SupersetProof unsafeSubset  -- | If the given key is in the map, update or delete it using the given@@ -230,8 +347,36 @@     (v', !m') -> ((unsafeKey k,) <$> v',)       $ SomeMapWith (Map m') $ SupersetProof unsafeSubset +-- | Given two maps proven to have the same keys, for each key apply the+-- function to the associated values, to obtain a new map with the same keys.+zipWithKey+  :: forall s k a b c. Ord k+  => (Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c+zipWithKey f (Map m1) (Map m2) = Map+  $ Map.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)+    (\m -> if Map.null m+      then Map.empty+      else error "zipWithKey: bug: Data.Map.Refined has been subverted")+    (\m -> if Map.null m+      then Map.empty+      else error "zipWithKey: bug: Data.Map.Refined has been subverted")+    --  ^ Work around https://github.com/haskell/containers/issues/979+    m1+    m2+ -- | Return the union of two maps, with a given combining function for keys that -- exist in both maps simultaneously.+unionWith+  :: forall s t k a. Ord k+  => (a -> a -> a)+  -> Map s k a+  -> Map t k a+  -> SomeMapWith (UnionProof 'Regular s t) k a+unionWith f (Map m1) (Map m2) = SomeMapWith (Map $ Map.unionWith f m1 m2)+  $ UnionProof unsafeSubset unsafeSubsetWith2++-- | Return the union of two maps, with a given combining function for keys that+-- exist in both maps simultaneously. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@ -- respectively.@@ -245,8 +390,20 @@   = SomeMapWith (Map $ Map.unionWithKey (f . reallyUnsafeRefine) m1 m2)     $ UnionProof unsafeSubset unsafeSubsetWith2 --- | For keys that appear in both maps, the given function decides whether the--- key is removed from the first map.+-- | Return the first map, but for keys that appear in both maps, the given+-- function decides whether the key is removed.+differenceWith+  :: forall s t k a b. Ord k+  => (a -> b -> Maybe a)+  -> Map s k a+  -> Map t k b+  -> SomeMapWith (PartialDifferenceProof 'Regular s t) k a+differenceWith f (Map m1) (Map m2)+  = SomeMapWith (Map $ Map.differenceWith f m1 m2)+    $ PartialDifferenceProof unsafeSubset unsafeSubset++-- | Return the first map, but for keys that appear in both maps, the given+-- function decides whether the key is removed. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@ -- respectively.@@ -261,6 +418,17 @@     $ PartialDifferenceProof unsafeSubset unsafeSubset  -- | Return the intersection of two maps with the given combining function.+intersectionWith+  :: forall s t k a b c. Ord k+  => (a -> b -> c)+  -> Map s k a+  -> Map t k b+  -> SomeMapWith (IntersectionProof 'Regular s t) k c+intersectionWith f (Map m1) (Map m2)+  = SomeMapWith (Map $ Map.intersectionWith f m1 m2)+    $ IntersectionProof unsafeSubset unsafeSubsetWith2++-- | Return the intersection of two maps with the given combining function. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@ -- respectively.@@ -274,6 +442,10 @@   = SomeMapWith (Map $ Map.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)     $ IntersectionProof unsafeSubset unsafeSubsetWith2 +-- | Apply a function to all values in a map. The set of keys remains the same.+map :: forall s k a b. (a -> b) -> Map s k a -> Map s k b+map = coerce $ Map.map @a @b @k+ -- | Thread an accumularing argument through the map in ascending order of keys. mapAccumLWithKey   :: forall s k a b c. (a -> Key s k -> b -> (a, c))@@ -293,6 +465,26 @@ mapAccumRWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce   $ Map.mapAccumRWithKey @a @k @b @c +-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results+-- into a new map. For keys that were mapped to the same new key, the value+-- corresponding to the greatest of the original keys is retained.+mapKeys+  :: forall s k1 k2 a. Ord k2+  => (Key s k1 -> k2)+  -> Map s k1 a+  -> SomeMapWith (MapProof 'Regular s k1 k2) k2 a+mapKeys g (Map m)+  = SomeMapWith (Map $ Map.mapKeys (g . unsafeKey) m)+    $ MapProof (unsafeKey . g) \k2 -> case Map.lookup (unrefine k2) backMap of+      Nothing -> error "mapKeys: bug: Data.Map.Refined has been subverted"+      Just k1 -> k1+  where+    ~backMap = Map.fromList+      [ (k2, unsafeKey k1)+      | k1 <- Map.keys m+      , let !k2 = g $ unsafeKey k1+      ]+ -- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the -- results into a new map. For keys that were mapped to the same new key, @c@ -- acts as the combining function for corresponding values.@@ -314,6 +506,15 @@       , let !k2 = g $ unsafeKey k1       ] +-- | Apply a function to all values in a map and collect only the 'Just'+-- results, returning a potentially smaller map.+mapMaybe+  :: forall s k a b. (a -> Maybe b)+  -> Map s k a+  -> SomeMapWith (SupersetProof 'Regular s) k b+mapMaybe f (Map m) = SomeMapWith (Map $ Map.mapMaybe f m)+  $ SupersetProof unsafeSubset+ -- | Apply a function to all values in a map, together with their corresponding -- keys, and collect only the 'Just' results, returning a potentially smaller -- map.@@ -324,6 +525,23 @@ mapMaybeWithKey f (Map m)   = SomeMapWith (Map $ Map.mapMaybeWithKey (f . unsafeKey) m)     $ SupersetProof unsafeSubset++-- | Apply a function to all values in a map and collect the 'Left' and 'Right'+-- results into separate (disjoint) maps.+mapEither+  :: forall s k a b c. Ord k -- TODO: this is only used in the proof+  => (a -> Either b c)+  -> Map s k a+  -> Some2MapWith (PartitionProof 'Regular s k) k b c+mapEither p (Map m) = case Map.mapEither p m of+  (m1, m2) -> Some2MapWith (Map m1) (Map m2) $ PartitionProof+    do \k -> case Map.lookup (unrefine k) m of+        Nothing -> error+          "mapEither: bug: Data.Map.Refined has been subverted"+        Just x -> case p x of+          Left _ -> Left $ unsafeKey $ unrefine k+          Right _ -> Right $ unsafeKey $ unrefine k+    unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g  -- | Apply a function to all values in a map, together with their corresponding -- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

@@ -43,18 +43,26 @@   , SingletonProof(..)   , fromSet   , Common.fromMap+  , Common.verifyMap+  , fromTraversable+  , fromTraversableWith   , fromTraversableWithKey   , FromTraversableProof(..)   -- * Insertion   , insert+  , insertWith+  , insertWithKey   , InsertProof(..)   , reinsert   , insertLookupWithKey   -- * Deletion/Update   , Common.delete+  , adjust'   , adjust   , adjustWithKey+  , update'   , update+  , updateWithKey   , updateLookupWithKey   -- * Query   , Common.lookup@@ -72,19 +80,26 @@   -- * Combine   , zipWithKey   , bind+  , Common.union+  , unionWith   , unionWithKey   , UnionProof(..)   , Common.difference   , DifferenceProof(..)+  , differenceWith   , differenceWithKey   , PartialDifferenceProof(..)+  , Common.intersection+  , intersectionWith   , intersectionWithKey   , IntersectionProof(..)   -- * Traversal+  , map   , mapWithKey   , traverseWithKey   , mapAccumLWithKey   , mapAccumRWithKey+  , mapKeys   , mapKeysWith   , MapProof(..)   , backpermuteKeys@@ -102,12 +117,19 @@   -- * Filter   , Common.restrictKeys   , Common.withoutKeys+  , Common.filter+  , Common.filterKeys   , Common.filterWithKey+  , Common.partition   , Common.partitionWithKey   , PartitionProof(..)+  , Common.takeWhileAntitone+  , Common.dropWhileAntitone   , Common.spanAntitone   , PartialPartitionProof(..)+  , mapMaybe   , mapMaybeWithKey+  , mapEither   , mapEitherWithKey   , Common.splitLookup   , SplitProof(..)@@ -138,7 +160,7 @@ import           Data.Reflection import           Data.Traversable import           Data.Type.Coercion-import           Prelude hiding (lookup, null)+import           Prelude hiding (lookup, map, null) import           Refined import           Refined.Unsafe @@ -154,7 +176,41 @@ fromSet :: forall s k a. KnownSet s k => (Key s k -> a) -> Map s k a fromSet f = Map $ Map.fromSet (f . unsafeKey) (reflect $ Proxy @s) --- | Create a map from an arbitrary traversable of key-value pairs.+-- | Create a map from an arbitrary traversable of key-value pairs. If a key is+-- repeated, the retained value is the last one in traversal order. If you're+-- looking for @fromList@, this is the function you want.+fromTraversable+  :: forall t k a. (Traversable t, Ord k)+  => t (k, a) -> SomeMapWith (FromTraversableProof 'Regular t k) k a+fromTraversable xs = SomeMapWith (Map m) $ FromTraversableProof proof+  where+    (m, proof) = mapAccumL+      (\s (k, v) -> let !s' = Map.insert k v s in (s', unsafeKey k))+      Map.empty+      xs++-- | Create a map from an arbitrary traversable of key-value pairs, with a+-- function for combining values for repeated keys. The function is called as if+-- by 'foldl1', but flipped:+--+-- @+-- 'fromTraversableWith' f [(k, x1), (k, x2), (k, x3)]+--   = 'singleton' k (f x3 (f x2 x1))+-- @+fromTraversableWith+  :: forall t k a. (Traversable t, Ord k)+  => (a -> a -> a)+  -> t (k, a)+  -> SomeMapWith (FromTraversableProof 'Regular t k) k a+fromTraversableWith f xs = SomeMapWith (Map m) $ FromTraversableProof proof+  where+    (m, proof) = mapAccumL+      (\s (k, v) -> let !s' = Map.insertWith f k v s in (s', unsafeKey k))+      Map.empty+      xs++-- | Create a map from an arbitrary traversable of key-value pairs. Like+-- 'fromTraversableWith', but the combining function has access to the key. fromTraversableWithKey   :: forall t k a. (Traversable t, Ord k)   => (k -> a -> a -> a)@@ -176,8 +232,40 @@ insert k v (Map m) = SomeMapWith (Map $ Map.insert k v m)   $ InsertProof (unsafeKey k) unsafeSubset +-- | Insert a key-value pair into the map to obtain a potentially larger map,+-- guaranteed to contain the given key. If the key was already present, the+-- supplied function is used to combine the new value with the old (in that+-- order).+insertWith+  :: forall s k a. Ord k+  => (a -> a -> a)+  -> k+  -> a+  -> Map s k a+  -> SomeMapWith (InsertProof 'Regular k s) k a+insertWith f k v (Map m) = SomeMapWith (Map $ Map.insertWith f k v m)+  $ InsertProof (unsafeKey k) unsafeSubset++-- | Insert a key-value pair into the map to obtain a potentially larger map,+-- guaranteed to contain the given key. Like 'insertWith', but the combining+-- function has access to the key, which is guaranteed to be in the old map.+insertWithKey+  :: forall s k a. Ord k+  => (Key s k -> a -> a -> a)+  -> k+  -> a+  -> Map s k a+  -> SomeMapWith (InsertProof 'Regular k s) k a+insertWithKey f k v (Map m) = SomeMapWith+  (Map $ Map.insertWithKey (f . unsafeKey) k v m)+  $ InsertProof (unsafeKey k) unsafeSubset+ -- | Overwrite a key-value pair that is known to already be in the map. The set -- of keys remains the same.+--+-- @+-- 'reinsert' k v = 'adjust (const v) k'+-- @ reinsert   :: forall s k a. Ord k   => Key s k -> a -> Map s k a -> Map s k a@@ -198,10 +286,15 @@     (v', !m') -> ((unsafeKey k,) <$> v',)       $ SomeMapWith (Map m') $ InsertProof (unsafeKey k) unsafeSubset +-- | If the given key is in the map, update the value at that key using the+-- given function. In any case, the set of keys remains the same.+adjust' :: forall s k a. Ord k => (a -> a) -> k -> Map s k a -> Map s k a+adjust' = coerce $ Map.adjust @k @a+ -- | Update the value at a specific key known the be in the map using the given -- function. The set of keys remains the same. adjust :: forall s k a. Ord k => (a -> a) -> Key s k -> Map s k a -> Map s k a-adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ Map.adjust @k @a+adjust = gcoerceWith (unsafeCastKey @s @k) $ coerce $ adjust' @s @k @a  -- | If the given key is in the map, update the associated value using the given -- function with a proof that the key was in the map; otherwise return the map@@ -211,6 +304,17 @@ adjustWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce   $ Map.adjustWithKey @k @a +-- | If a key is present in the map, update its value or delete it using the+-- given function, returning a potentially smaller map.+update'+  :: forall s k a. Ord k+  => (a -> Maybe a)+  -> k+  -> Map s k a+  -> SomeMapWith (SupersetProof 'Regular s) k a+update' f k (Map m) = SomeMapWith (Map $ Map.update f k m)+  $ SupersetProof unsafeSubset+ -- | Update or delete a key known to be in the map using the given function, -- returning a potentially smaller map. update@@ -219,7 +323,19 @@   -> Key s k   -> Map s k a   -> SomeMapWith (SupersetProof 'Regular s) k a-update f k (Map m) = SomeMapWith (Map $ Map.update f (unrefine k) m)+update = gcoerceWith (unsafeCastKey @s @k) $ coerce $ update' @s @k @a++-- | If a key is present in the map, update its value or delete it using the+-- given function with a proof that the key was in the map, returning a+-- potentially smaller map.+updateWithKey+  :: forall s k a. Ord k+  => (Key s k -> a -> Maybe a)+  -> k+  -> Map s k a+  -> SomeMapWith (SupersetProof 'Regular s) k a+updateWithKey f k (Map m) = SomeMapWith+  (Map $ Map.updateWithKey (f . unsafeKey) k m)   $ SupersetProof unsafeSubset  -- | If the given key is in the map, update or delete it using the given@@ -256,6 +372,17 @@  -- | Return the union of two maps, with a given combining function for keys that -- exist in both maps simultaneously.+unionWith+  :: forall s t k a. Ord k+  => (a -> a -> a)+  -> Map s k a+  -> Map t k a+  -> SomeMapWith (UnionProof 'Regular s t) k a+unionWith f (Map m1) (Map m2) = SomeMapWith (Map $ Map.unionWith f m1 m2)+  $ UnionProof unsafeSubset unsafeSubsetWith2++-- | Return the union of two maps, with a given combining function for keys that+-- exist in both maps simultaneously. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@ -- respectively.@@ -269,8 +396,20 @@   = SomeMapWith (Map $ Map.unionWithKey (f . reallyUnsafeRefine) m1 m2)     $ UnionProof unsafeSubset unsafeSubsetWith2 --- | For keys that appear in both maps, the given function decides whether the--- key is removed from the first map.+-- | Return the first map, but for keys that appear in both maps, the given+-- function decides whether the key is removed.+differenceWith+  :: forall s t k a b. Ord k+  => (a -> b -> Maybe a)+  -> Map s k a+  -> Map t k b+  -> SomeMapWith (PartialDifferenceProof 'Regular s t) k a+differenceWith f (Map m1) (Map m2)+  = SomeMapWith (Map $ Map.differenceWith f m1 m2)+    $ PartialDifferenceProof unsafeSubset unsafeSubset++-- | Return the first map, but for keys that appear in both maps, the given+-- function decides whether the key is removed. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@ -- respectively.@@ -285,6 +424,17 @@     $ PartialDifferenceProof unsafeSubset unsafeSubset  -- | Return the intersection of two maps with the given combining function.+intersectionWith+  :: forall s t k a b c. Ord k+  => (a -> b -> c)+  -> Map s k a+  -> Map t k b+  -> SomeMapWith (IntersectionProof 'Regular s t) k c+intersectionWith f (Map m1) (Map m2)+  = SomeMapWith (Map $ Map.intersectionWith f m1 m2)+    $ IntersectionProof unsafeSubset unsafeSubsetWith2++-- | Return the intersection of two maps with the given combining function. -- -- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@ -- respectively.@@ -298,6 +448,10 @@   = SomeMapWith (Map $ Map.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)     $ IntersectionProof unsafeSubset unsafeSubsetWith2 +-- | Apply a function to all values in a map. The set of keys remains the same.+map :: forall s k a b. (a -> b) -> Map s k a -> Map s k b+map = coerce $ Map.map @a @b @k+ -- | Apply a function to all values in a map, together with their corresponding -- keys, that are proven to be in the map. The set of keys remains the same. mapWithKey :: forall s k a b. (Key s k -> a -> b) -> Map s k a -> Map s k b@@ -331,6 +485,27 @@ mapAccumRWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce   $ Map.mapAccumRWithKey @a @k @b @c +-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results+-- into a new map. For keys that were mapped to the same new key, the value+-- corresponding to the greatest of the original keys is retained.+mapKeys+  :: forall s k1 k2 a. Ord k2+  => (Key s k1 -> k2)+  -> Map s k1 a+  -> SomeMapWith (MapProof 'Regular s k1 k2) k2 a+mapKeys g (Map m)+  = SomeMapWith (Map $ Map.mapKeys (g . unsafeKey) m)+    $ MapProof (unsafeKey . g) \k2 -> case Map.lookup (unrefine k2) backMap of+      Nothing -> error+        "mapKeys: bug: Data.Map.Strict.Refined has been subverted"+      Just k1 -> k1+  where+    ~backMap = Map.fromList+      [ (k2, unsafeKey k1)+      | k1 <- Map.keys m+      , let !k2 = g $ unsafeKey k1+      ]+ -- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the -- results into a new map. For keys that were mapped to the same new key, @c@ -- acts as the combining function for corresponding values.@@ -353,6 +528,15 @@       , let !k2 = g $ unsafeKey k1       ] +-- | Apply a function to all values in a map and collect only the 'Just'+-- results, returning a potentially smaller map.+mapMaybe+  :: forall s k a b. (a -> Maybe b)+  -> Map s k a+  -> SomeMapWith (SupersetProof 'Regular s) k b+mapMaybe f (Map m) = SomeMapWith (Map $ Map.mapMaybe f m)+  $ SupersetProof unsafeSubset+ -- | Apply a function to all values in a map, together with their corresponding -- keys, and collect only the 'Just' results, returning a potentially smaller -- map.@@ -363,6 +547,23 @@ mapMaybeWithKey f (Map m)   = SomeMapWith (Map $ Map.mapMaybeWithKey (f . unsafeKey) m)     $ SupersetProof unsafeSubset++-- | Apply a function to all values in a map and collect the 'Left' and 'Right'+-- results into separate (disjoint) maps.+mapEither+  :: forall s k a b c. Ord k -- TODO: this is only used in the proof+  => (a -> Either b c)+  -> Map s k a+  -> Some2MapWith (PartitionProof 'Regular s k) k b c+mapEither p (Map m) = case Map.mapEither p m of+  (m1, m2) -> Some2MapWith (Map m1) (Map m2) $ PartitionProof+    do \k -> case Map.lookup (unrefine k) m of+        Nothing -> error+          "mapEither: bug: Data.Map.Strict.Refined has been subverted"+        Just x -> case p x of+          Left _ -> Left $ unsafeKey $ unrefine k+          Right _ -> Right $ unsafeKey $ unrefine k+    unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g  -- | Apply a function to all values in a map, together with their corresponding -- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

@@ -185,7 +185,7 @@ -- you a way to refer to the set (the parameter @s@), e.g.: -- -- @--- 'withSet' ('fromSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s+-- 'withSet' ('fromSet' ...) $ \\(_ :: 'Proxy' s) -> doSomethingWith \@s -- @ withSet   :: forall a r. SomeSet a -> (forall s. KnownSet s a => Proxy s -> r) -> r