a959064...main · typeable/refined-containers

git.iko.soy/typeable/refined-containers

13 files changed+718−58

since splitsnapshots

unifiedsplit

refined-containers.cabal+1−1 src/Data/HashMap/Common/Refined.hs+53−15 src/Data/HashMap/Refined.hs+75−2 src/Data/HashMap/Strict/Refined.hs+74−1 src/Data/HashSet/Refined.hs+1−1 src/Data/IntMap/Common/Refined.hs+93−15 src/Data/IntMap/Refined.hs+83−2 src/Data/IntMap/Strict/Refined.hs+84−1 src/Data/IntSet/Refined.hs+1−1 src/Data/Map/Common/Refined.hs+92−15 src/Data/Map/Refined.hs+80−2 src/Data/Map/Strict/Refined.hs+80−1 src/Data/Set/Refined.hs+1−1

refined-containers.cabal+1−1

@@ -23,7 +23,7 @@ license: MIT

2323license-file: LICENSE

2424author: mniip@typeable.io

2525maintainer: mniip@typeable.io

26−version: 0.1.0.2

26+version: 0.1.2.0

2727build-type: Simple

2828

2929tested-with:

src/Data/HashMap/Common/Refined.hs+53−15

@@ -24,6 +24,7 @@ import Data.Reflection

2424import Data.Traversable.WithIndex

2525import Data.Type.Coercion

2626import Data.Type.Equality ((:~:)(..))

27+import Prelude hiding (zipWith)

2728import Refined

2829import Refined.Unsafe

2930import Unsafe.Coerce

@@ -95,7 +96,7 @@ data SomeHashMap k a where

9596--

9697-- @

9798-- 'withHashMap' ('fromHashMap' ...

98−-- $ \(m :: 'HashMap' s k a) -> doSomethingWith \@s

99+-- $ \\(m :: 'HashMap' s k a) -> doSomethingWith \@s

99100-- @

100101withHashMap

101102 :: forall k a r. SomeHashMap k a -> (forall s. HashMap s k a -> r) -> r

@@ -239,11 +240,10 @@ disjoint (HashMap m1) (HashMap m2)

239240

240241-- | Given two maps proven to have the same keys, for each key apply the

241242-- function to the associated values, to obtain a new map with the same keys.

242−zipWithKey

243+zipWith

243244 :: forall s k a b c. Hashable k

244− => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c

245−zipWithKey f (HashMap m1) (HashMap m2) = HashMap

246− $ HashMap.intersectionWithKey (f . unsafeKey) m1 m2

245+ => (a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c

246+zipWith f (HashMap m1) (HashMap m2) = HashMap $ HashMap.intersectionWith f m1 m2

247247

248248-- | Return the union of two maps. For keys that exist in both maps, the value

249249-- is taken from the first map.

@@ -342,6 +342,25 @@ keysSet (HashMap m) = reify (HashMap.keysSet m)

342342toList :: forall s k a. HashMap s k a -> [(Key s k, a)]

343343toList = gcoerceWith (unsafeCastKey @s @k) $ coerce $ HashMap.toList @k @a

344344

345+-- | Retain only the values that satisfy the predicate, returning a potentially

346+-- smaller map.

347+filter

348+ :: forall s k a. (a -> Bool)

349+ -> HashMap s k a

350+ -> SomeHashMapWith (SupersetProof 'Hashed s) k a

351+filter p (HashMap m) = SomeHashMapWith (HashMap $ HashMap.filter p m)

352+ $ SupersetProof unsafeSubset

353+

354+-- | Retain only the keys that satisfy the predicate, returning a potentially

355+-- smaller map.

356+filterKeys

357+ :: forall s k a. (Key s k -> Bool)

358+ -> HashMap s k a

359+ -> SomeHashMapWith (SupersetProof 'Hashed s) k a

360+filterKeys p (HashMap m) = SomeHashMapWith

361+ (HashMap $ HashMap.filterWithKey (\k _ -> p (unsafeKey k)) m)

362+ $ SupersetProof unsafeSubset

363+

345364-- | Retain only the key-value pairs that satisfy the predicate, returning a

346365-- potentially smaller map.

347366filterWithKey

@@ -369,6 +388,25 @@ withoutKeys (HashMap m) = SomeHashMapWith

369388 (HashMap $ HashMap.difference m $ HashSet.toMap $ reflect $ Proxy @t)

370389 $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset

371390

391+-- | Partition a map into two disjoint submaps: those whose key-value pairs

392+-- satisfy the predicate, and those whose don't.

393+partition

394+ :: forall s k a. Hashable k -- TODO: this is only used in the proof

395+ => (a -> Bool)

396+ -> HashMap s k a

397+ -> Some2HashMapWith (PartitionProof 'Hashed s k) k a a

398+partition p (HashMap m) = Some2HashMapWith

399+ (HashMap $ HashMap.filter p m)

400+ (HashMap $ HashMap.filter (not . p) m)

401+ $ PartitionProof

402+ do \k -> case HashMap.lookup (unrefine k) m of

403+ Nothing -> error

404+ "partition: bug: Data.HashMap.Refined has been subverted"

405+ Just x -> if p x

406+ then Left $ unsafeKey $ unrefine k

407+ else Right $ unsafeKey $ unrefine k

408+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

409+

372410-- | Partition a map into two disjoint submaps: those whose key-value pairs

373411-- satisfy the predicate, and those whose don't.

374412partitionWithKey

@@ -403,15 +441,15 @@ castKey

403441castKey = castRefined

404442

405443-- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps

406−-- can be interconverted too. For example, 'zipWithKey' can be implemented via

407−-- 'Data.HashMap.Refined.intersectionWithKey' by proving that the set of keys

408−-- remains unchanged:

444+-- can be interconverted too. For example, 'Data.HashMap.Refined.zipWithKey' can

445+-- be implemented via 'Data.HashMap.Refined.intersectionWithKey' by proving that

446+-- the set of keys remains unchanged:

409447--

410448-- @

411−-- 'zipWithKey'

449+-- 'Data.HashMap.Refined.zipWithKey'

412450-- :: forall s k a b c. 'Hashable' k

413451-- => ('Key' s k -> a -> b -> c) -> 'HashMap' s k a -> 'HashMap' s k b -> 'HashMap' s k c

414−-- 'zipWithKey' f m1 m2

452+-- 'Data.HashMap.Refined.zipWithKey' f m1 m2

415453-- | v'SomeHashMapWith' @r m proof <- 'Data.HashMap.Refined.intersectionWithKey' (f . 'andLeft') m1 m2

416454-- , v'IntersectionProof' p1 p2 <- proof

417455-- , ( v'Coercion' :: t'Coercion' ('HashMap' r k c) ('HashMap' s k c))

@@ -436,10 +474,10 @@ instance TraversableWithIndex (Key s k) (HashMap s k) where

436474 itraverse = traverseWithKey

437475

438476-- | Similar to the instance for functions -- zip corresponding keys. To use

439−-- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWithKey'.

477+-- '<*>'/'Control.Applicative.liftA2' without 'KnownHashSet' see 'zipWith'.

440478instance (Hashable k, KnownHashSet s k) => Applicative (HashMap s k) where

441479 pure x = fromSet \_ -> x

442− (<*>) = zipWithKey (const id)

480+ (<*>) = zipWith id

443481

444482-- | @'bind' m f@ is a map that for each key @k :: 'Key' s k@, contains the

445483-- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.

@@ -448,8 +486,8 @@ bind

448486 => HashMap s k a -> (a -> HashMap s k b) -> HashMap s k b

449487bind m f = mapWithKey (\k x -> f x ! k) m

450488

451−-- | Similar to the instance for functions. To use '>>=' without 'KnownSet' see

452−-- 'bind'.

489+-- | Similar to the instance for functions. To use '>>=' without 'KnownHashSet'

490+-- see 'bind'.

453491instance (Hashable k, KnownHashSet s k) => Monad (HashMap s k) where

454492 (>>=) = bind

455493

@@ -462,7 +500,7 @@ instance (Hashable k, KnownHashSet s k)

462500

463501-- | Append the values at the corresponding keys

464502instance (Hashable k, Semigroup a) => Semigroup (HashMap s k a) where

465− (<>) = zipWithKey (const (<>))

503+ (<>) = zipWith (<>)

466504

467505instance (Hashable k, KnownHashSet s k, Monoid a)

468506 => Monoid (HashMap s k a) where

src/Data/HashMap/Refined.hs+75−2

@@ -74,6 +74,7 @@ module Data.HashMap.Refined

7474 , Common.disjoint

7575 , DisjointProof(..)

7676 -- * Combine

77+ , zipWith

7778 , zipWithKey

7879 , bind

7980 , Common.union

@@ -90,10 +91,12 @@ module Data.HashMap.Refined

9091 , intersectionWithKey

9192 , IntersectionProof(..)

9293 -- * Traversal

94+ , map

9395 , mapWithKey

9496 , traverseWithKey

9597 , mapAccumLWithKey

9698 , mapAccumRWithKey

99+ , mapKeys

97100 , mapKeysWith

98101 , MapProof(..)

99102 , backpermuteKeys

@@ -110,10 +113,15 @@ module Data.HashMap.Refined

110113 -- * Filter

111114 , Common.restrictKeys

112115 , Common.withoutKeys

116+ , Common.filter

117+ , Common.filterKeys

113118 , Common.filterWithKey

119+ , Common.partition

114120 , Common.partitionWithKey

115121 , PartitionProof(..)

122+ , mapMaybe

116123 , mapMaybeWithKey

124+ , mapEither

117125 , mapEitherWithKey

118126 -- * Casts

119127 , Common.castKey

@@ -128,7 +136,7 @@ import Data.Container.Refined.Unsafe

128136import Data.Functor

129137import Data.HashMap.Common.Refined

130138 ( HashMap(..), Key, unsafeCastKey, unsafeKey, SomeHashMapWith(..)

131− , Some2HashMapWith(..), fromSet, (!), zipWithKey, mapWithKey, traverseWithKey

139+ , Some2HashMapWith(..), fromSet, (!), zipWith, mapWithKey, traverseWithKey

132140 , bind

133141 )

134142import qualified Data.HashMap.Common.Refined as Common

@@ -136,7 +144,7 @@ import qualified Data.HashMap.Lazy as HashMap

136144import Data.Traversable

137145import Data.Traversable.WithIndex

138146import Data.Type.Coercion

139−import Prelude hiding (lookup, null)

147+import Prelude hiding (lookup, map, null, zipWith)

140148import Refined

141149import Refined.Unsafe

142150

@@ -335,6 +343,15 @@ updateLookupWithKey f k (HashMap m) =

335343 $ SupersetProof unsafeSubset

336344 )

337345

346+-- | Given two maps proven to have the same keys, for each key apply the

347+-- function to the associated values and the key, to obtain a new map with the

348+-- same keys.

349+zipWithKey

350+ :: forall s k a b c. Hashable k

351+ => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c

352+zipWithKey f (HashMap m1) (HashMap m2) = HashMap

353+ $ HashMap.intersectionWithKey (f . unsafeKey) m1 m2

354+

338355-- | Return the union of two maps, with a given combining function for keys that

339356-- exist in both maps simultaneously.

340357unionWith

@@ -417,6 +434,10 @@ intersectionWithKey f (HashMap m1) (HashMap m2) = SomeHashMapWith

417434 (HashMap $ HashMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)

418435 $ IntersectionProof unsafeSubset unsafeSubsetWith2

419436

437+-- | Apply a function to all values in a map. The set of keys remains the same.

438+map :: forall s k a b. (a -> b) -> HashMap s k a -> HashMap s k b

439+map = coerce $ HashMap.map @a @b @k

440+

420441-- | Thread an accumularing argument through the map in ascending order of

421442-- hashes.

422443mapAccumLWithKey

@@ -435,6 +456,28 @@ mapAccumRWithKey

435456 -> (a, HashMap s k c)

436457mapAccumRWithKey f = imapAccumR (flip f)

437458

459+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results

460+-- into a new map. For keys that were mapped to the same new key, the value is

461+-- picked in an unspecified way.

462+mapKeys

463+ :: forall s k1 k2 a. Hashable k2

464+ => (Key s k1 -> k2)

465+ -> HashMap s k1 a

466+ -> SomeHashMapWith (MapProof 'Hashed s k1 k2) k2 a

467+mapKeys g (HashMap m) = SomeHashMapWith

468+ (HashMap $ HashMap.fromList

469+ $ HashMap.foldrWithKey (\k x xs -> (g $ unsafeKey k, x) : xs) [] m)

470+ $ MapProof (unsafeKey . g) \k2 ->

471+ case HashMap.lookup (unrefine k2) backMap of

472+ Nothing -> error "mapKeys: bug: Data.HashMap.Refined has been subverted"

473+ Just k1 -> k1

474+ where

475+ ~backMap = HashMap.fromList

476+ [ (k2, unsafeKey k1)

477+ | k1 <- HashMap.keys m

478+ , let !k2 = g $ unsafeKey k1

479+ ]

480+

438481-- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the

439482-- results into a new map. For keys that were mapped to the same new key, @c@

440483-- acts as the combining function for corresponding values.

@@ -459,6 +502,15 @@ mapKeysWith f g (HashMap m) = SomeHashMapWith

459502 , let !k2 = g $ unsafeKey k1

460503 ]

461504

505+-- | Apply a function to all values in a map and collect only the 'Just'

506+-- results, returning a potentially smaller map.

507+mapMaybe

508+ :: forall s k a b. (a -> Maybe b)

509+ -> HashMap s k a

510+ -> SomeHashMapWith (SupersetProof 'Hashed s) k b

511+mapMaybe f (HashMap m) = SomeHashMapWith (HashMap $ HashMap.mapMaybe f m)

512+ $ SupersetProof unsafeSubset

513+

462514-- | Apply a function to all values in a map, together with their corresponding

463515-- keys, and collect only the 'Just' results, returning a potentially smaller

464516-- map.

@@ -470,6 +522,27 @@ mapMaybeWithKey f (HashMap m)

470522 = SomeHashMapWith (HashMap $ HashMap.mapMaybeWithKey (f . unsafeKey) m)

471523 $ SupersetProof unsafeSubset

472524

525+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'

526+-- results into separate (disjoint) maps.

527+mapEither

528+ :: forall s k a b c. Hashable k -- TODO: this is only used in the proof

529+ => (a -> Either b c)

530+ -> HashMap s k a

531+ -> Some2HashMapWith (PartitionProof 'Hashed s k) k b c

532+mapEither p (HashMap m)

533+ | m' <- HashMap.map p m

534+ = Some2HashMapWith

535+ (HashMap $ HashMap.mapMaybe (either Just (const Nothing)) m')

536+ (HashMap $ HashMap.mapMaybe (either (const Nothing) Just) m')

537+ $ PartitionProof

538+ do \k -> case HashMap.lookup (unrefine k) m of

539+ Nothing -> error

540+ "mapEither: bug: Data.HashMap.Refined has been subverted"

541+ Just x -> case p x of

542+ Left _ -> Left $ unsafeKey $ unrefine k

543+ Right _ -> Right $ unsafeKey $ unrefine k

544+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

545+

473546-- | Apply a function to all values in a map, together with their corresponding

474547-- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

475548-- maps.

src/Data/HashMap/Strict/Refined.hs+74−1

@@ -74,6 +74,7 @@ module Data.HashMap.Strict.Refined

7474 , Common.disjoint

7575 , DisjointProof(..)

7676 -- * Combine

77+ , zipWith

7778 , zipWithKey

7879 , bind

7980 , Common.union

@@ -90,10 +91,12 @@ module Data.HashMap.Strict.Refined

9091 , intersectionWithKey

9192 , IntersectionProof(..)

9293 -- * Traversal

94+ , map

9395 , mapWithKey

9496 , traverseWithKey

9597 , mapAccumLWithKey

9698 , mapAccumRWithKey

99+ , mapKeys

97100 , mapKeysWith

98101 , MapProof(..)

99102 , backpermuteKeys

@@ -110,10 +113,15 @@ module Data.HashMap.Strict.Refined

110113 -- * Filter

111114 , Common.restrictKeys

112115 , Common.withoutKeys

116+ , Common.filter

117+ , Common.filterKeys

113118 , Common.filterWithKey

119+ , Common.partition

114120 , Common.partitionWithKey

115121 , PartitionProof(..)

122+ , mapMaybe

116123 , mapMaybeWithKey

124+ , mapEither

117125 , mapEitherWithKey

118126 -- * Casts

119127 , Common.castKey

@@ -138,7 +146,7 @@ import Data.Reflection

138146import Data.Traversable

139147import Data.Traversable.WithIndex

140148import Data.Type.Coercion

141−import Prelude hiding (lookup, null)

149+import Prelude hiding (lookup, map, null, zipWith)

142150import Refined

143151import Refined.Unsafe

144152

@@ -345,6 +353,14 @@ updateLookupWithKey f k (HashMap m) =

345353

346354-- | Given two maps proven to have the same keys, for each key apply the

347355-- function to the associated values, to obtain a new map with the same keys.

356+zipWith

357+ :: forall s k a b c. Hashable k

358+ => (a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c

359+zipWith f (HashMap m1) (HashMap m2) = HashMap $ HashMap.intersectionWith f m1 m2

360+

361+-- | Given two maps proven to have the same keys, for each key apply the

362+-- function to the associated values and the key, to obtain a new map with the

363+-- same keys.

348364zipWithKey

349365 :: forall s k a b c. Hashable k

350366 => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c

@@ -433,6 +449,10 @@ intersectionWithKey f (HashMap m1) (HashMap m2) = SomeHashMapWith

433449 (HashMap $ HashMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)

434450 $ IntersectionProof unsafeSubset unsafeSubsetWith2

435451

452+-- | Apply a function to all values in a map. The set of keys remains the same.

453+map :: forall s k a b. (a -> b) -> HashMap s k a -> HashMap s k b

454+map = coerce $ HashMap.map @a @b @k

455+

436456-- | Apply a function to all values in a map, together with their corresponding

437457-- keys, that are proven to be in the map. The set of keys remains the same.

438458mapWithKey

@@ -467,6 +487,29 @@ mapAccumRWithKey

467487 -> (a, HashMap s k c)

468488mapAccumRWithKey f = imapAccumR (flip f)

469489

490+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results

491+-- into a new map. For keys that were mapped to the same new key, the value is

492+-- picked in an unspecified way.

493+mapKeys

494+ :: forall s k1 k2 a. Hashable k2

495+ => (Key s k1 -> k2)

496+ -> HashMap s k1 a

497+ -> SomeHashMapWith (MapProof 'Hashed s k1 k2) k2 a

498+mapKeys g (HashMap m) = SomeHashMapWith

499+ (HashMap $ HashMap.fromList

500+ $ HashMap.foldrWithKey (\k x xs -> (g $ unsafeKey k, x) : xs) [] m)

501+ $ MapProof (unsafeKey . g) \k2 ->

502+ case HashMap.lookup (unrefine k2) backMap of

503+ Nothing -> error

504+ "mapKeys: bug: Data.HashMap.Strict.Refined has been subverted"

505+ Just k1 -> k1

506+ where

507+ ~backMap = HashMap.fromList

508+ [ (k2, unsafeKey k1)

509+ | k1 <- HashMap.keys m

510+ , let !k2 = g $ unsafeKey k1

511+ ]

512+

470513-- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the

471514-- results into a new map. For keys that were mapped to the same new key, @c@

472515-- acts as the combining function for corresponding values.

@@ -491,6 +534,15 @@ mapKeysWith f g (HashMap m) = SomeHashMapWith

491534 , let !k2 = g $ unsafeKey k1

492535 ]

493536

537+-- | Apply a function to all values in a map and collect only the 'Just'

538+-- results, returning a potentially smaller map.

539+mapMaybe

540+ :: forall s k a b. (a -> Maybe b)

541+ -> HashMap s k a

542+ -> SomeHashMapWith (SupersetProof 'Hashed s) k b

543+mapMaybe f (HashMap m) = SomeHashMapWith (HashMap $ HashMap.mapMaybe f m)

544+ $ SupersetProof unsafeSubset

545+

494546-- | Apply a function to all values in a map, together with their corresponding

495547-- keys, and collect only the 'Just' results, returning a potentially smaller

496548-- map.

@@ -502,6 +554,27 @@ mapMaybeWithKey f (HashMap m)

502554 = SomeHashMapWith (HashMap $ HashMap.mapMaybeWithKey (f . unsafeKey) m)

503555 $ SupersetProof unsafeSubset

504556

557+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'

558+-- results into separate (disjoint) maps.

559+mapEither

560+ :: forall s k a b c. Hashable k -- TODO: this is only used in the proof

561+ => (a -> Either b c)

562+ -> HashMap s k a

563+ -> Some2HashMapWith (PartitionProof 'Hashed s k) k b c

564+mapEither p (HashMap m)

565+ | m' <- HashMap.map p m

566+ = Some2HashMapWith

567+ (HashMap $ HashMap.mapMaybe (either Just (const Nothing)) m')

568+ (HashMap $ HashMap.mapMaybe (either (const Nothing) Just) m')

569+ $ PartitionProof

570+ do \k -> case HashMap.lookup (unrefine k) m of

571+ Nothing -> error

572+ "mapEither: bug: Data.HashMap.Refined has been subverted"

573+ Just x -> case p x of

574+ Left _ -> Left $ unsafeKey $ unrefine k

575+ Right _ -> Right $ unsafeKey $ unrefine k

576+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

577+

505578-- | Apply a function to all values in a map, together with their corresponding

506579-- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

507580-- maps.

src/Data/HashSet/Refined.hs+1−1

@@ -165,7 +165,7 @@ data SomeHashSet a where

165165-- you a way to refer to the set (the parameter @s@), e.g.:

166166--

167167-- @

168−-- 'withHashSet' ('fromHashSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s

168+-- 'withHashSet' ('fromHashSet' ...) $ \\(_ :: 'Proxy' s) -> doSomethingWith \@s

169169-- @

170170withHashSet

171171 :: forall a r. SomeHashSet a

src/Data/IntMap/Common/Refined.hs+93−15

@@ -20,6 +20,7 @@ import Data.Reflection

2020import Data.Traversable.WithIndex

2121import Data.Type.Coercion

2222import Data.Type.Equality ((:~:)(..))

23+import Prelude hiding (zipWith)

2324import Refined

2425import Refined.Unsafe

2526import Unsafe.Coerce

@@ -103,7 +104,8 @@ data SomeIntMap a where

103104-- parameter @s@), e.g.:

104105--

105106-- @

106−-- 'withIntMap' ('fromIntMap' ...) $ \(m :: 'IntMap' s a) -> doSomethingWith \@s

107+-- 'withIntMap' ('fromIntMap' ...)

108+-- $ \\(m :: 'IntMap' s a) -> doSomethingWith \@s

107109-- @

108110withIntMap :: forall a r. SomeIntMap a -> (forall s. IntMap s a -> r) -> r

109111withIntMap (SomeIntMap m) k = k m

@@ -249,19 +251,19 @@ disjoint (IntMap m1) (IntMap m2)

249251

250252-- | Given two maps proven to have the same keys, for each key apply the

251253-- function to the associated values, to obtain a new map with the same keys.

252−zipWithKey

253− :: forall s a b c. (Key s -> a -> b -> c)

254+zipWith

255+ :: forall s a b c. (a -> b -> c)

254256 -> IntMap s a

255257 -> IntMap s b

256258 -> IntMap s c

257−zipWithKey f (IntMap m1) (IntMap m2) = IntMap

258− $ IntMap.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)

259+zipWith f (IntMap m1) (IntMap m2) = IntMap

260+ $ IntMap.mergeWithKey (\_ x y -> Just $ f x y)

259261 (\m -> if IntMap.null m

260262 then IntMap.empty

261− else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")

263+ else error "zipWith: bug: Data.IntMap.Refined has been subverted")

262264 (\m -> if IntMap.null m

263265 then IntMap.empty

264− else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")

266+ else error "zipWith: bug: Data.IntMap.Refined has been subverted")

265267 -- ^ Work around https://github.com/haskell/containers/issues/979

266268 m1

267269 m2

@@ -357,6 +359,29 @@ toList = gcoerceWith (unsafeCastKey @s) $ coerce $ IntMap.toAscList @a

357359toDescList :: forall s a. IntMap s a -> [(Key s, a)]

358360toDescList = gcoerceWith (unsafeCastKey @s) $ coerce $ IntMap.toDescList @a

359361

362+-- | Retain only the key-value pairs that satisfy the predicate, returning a

363+-- potentially smaller map.

364+filter

365+ :: forall s a. (a -> Bool)

366+ -> IntMap s a

367+ -> SomeIntMapWith (SupersetProof 'Int s) a

368+filter p (IntMap m) = SomeIntMapWith (IntMap $ IntMap.filter p m)

369+ $ SupersetProof unsafeSubset

370+

371+-- | Retain only the key-value pairs that satisfy the predicate, returning a

372+-- potentially smaller map.

373+filterKeys

374+ :: forall s a. (Key s -> Bool)

375+ -> IntMap s a

376+ -> SomeIntMapWith (SupersetProof 'Int s) a

377+filterKeys p (IntMap m) = SomeIntMapWith

378+#if MIN_VERSION_containers(0, 8, 0)

379+ (IntMap $ IntMap.filterKeys (p . unsafeKey) m)

380+#else

381+ (IntMap $ IntMap.filterWithKey (\k _ -> p (unsafeKey k)) m)

382+#endif

383+ $ SupersetProof unsafeSubset

384+

360385-- | Retain only the key-value pairs that satisfy the predicate, returning a

361386-- potentially smaller map.

362387filterWithKey

@@ -392,6 +417,22 @@ withoutKeys (IntMap m) = SomeIntMapWith

392417#endif

393418 $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset

394419

420+-- | Partition a map into two disjoint submaps: those whose values satisfy the

421+-- predicate, and those whose don't.

422+partition

423+ :: forall s a. (a -> Bool)

424+ -> IntMap s a

425+ -> Some2IntMapWith (PartitionProof 'Int s Int) a a

426+partition p (IntMap m) = case IntMap.partition p m of

427+ (m1, m2) -> Some2IntMapWith (IntMap m1) (IntMap m2) $ PartitionProof

428+ do \k -> case IntMap.lookup (unrefine k) m of

429+ Nothing -> error

430+ "partition: bug: Data.IntMap.Refined has been subverted"

431+ Just x -> if p x

432+ then Left $ unsafeKey $ unrefine k

433+ else Right $ unsafeKey $ unrefine k

434+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

435+

395436-- | Partition a map into two disjoint submaps: those whose key-value pairs

396437-- satisfy the predicate, and those whose don't.

397438partitionWithKey

@@ -409,6 +450,43 @@ partitionWithKey p (IntMap m)

409450 else Right $ unsafeKey $ unrefine k

410451 unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

411452

453+-- | Take the a submap of keys up to a point where the predicate stops holding.

454+--

455+-- If @p@ is antitone ( $\forall x y, x < y \implies p(x) \ge p(y)$ ), then

456+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is

457+-- chosen in an unspecified way.

458+takeWhileAntitone

459+ :: forall s a. (Key s -> Bool)

460+ -> IntMap s a

461+ -> SomeIntMapWith (SupersetProof 'Int s) a

462+takeWhileAntitone p (IntMap m) = SomeIntMapWith

463+#if MIN_VERSION_containers(0, 6, 7)

464+ (IntMap $ IntMap.takeWhileAntitone (p . unsafeKey) m)

465+#else

466+ (IntMap $ IntMap.fromDistinctAscList

467+ $ List.takeWhile (p . unsafeKey . fst) $ IntMap.toAscList m)

468+#endif

469+ $ SupersetProof unsafeSubset

470+

471+-- | Take the a submap of keys starting from a point where the predicate stops

472+-- holding.

473+--

474+-- If @p@ is antitone ( $\forall x y, x < y \implies p(x) \ge p(y)$ ), then

475+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is

476+-- chosen in an unspecified way.

477+dropWhileAntitone

478+ :: forall s a. (Key s -> Bool)

479+ -> IntMap s a

480+ -> SomeIntMapWith (SupersetProof 'Int s) a

481+dropWhileAntitone p (IntMap m) = SomeIntMapWith

482+#if MIN_VERSION_containers(0, 6, 7)

483+ (IntMap $ IntMap.dropWhileAntitone (p . unsafeKey) m)

484+#else

485+ (IntMap $ IntMap.fromDistinctAscList

486+ $ List.dropWhile (p . unsafeKey . fst) $ IntMap.toAscList m)

487+#endif

488+ $ SupersetProof unsafeSubset

489+

412490-- | Divide a map into two disjoint submaps at a point where the predicate on

413491-- the keys stops holding.

414492--

@@ -483,17 +561,17 @@ castKey

483561castKey = castRefined

484562

485563-- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps

486−-- can be interconverted too. For example, 'zipWithKey' can be implemented via

487−-- 'Data.IntMap.Refined.intersectionWithKey' by proving that the set of keys

488−-- remains unchanged:

564+-- can be interconverted too. For example, 'Data.IntMap.Refined.zipWithKey' can

565+-- be implemented via 'Data.IntMap.Refined.intersectionWithKey' by proving that

566+-- the set of keys remains unchanged:

489567--

490568-- @

491−-- 'zipWithKey'

569+-- 'Data.IntMap.Refined.zipWithKey'

492570-- :: forall s a b c. ('Key' s -> a -> b -> c)

493571-- -> 'IntMap' s a

494572-- -> 'IntMap' s b

495573-- -> 'IntMap' s c

496−-- 'zipWithKey' f m1 m2

574+-- 'Data.IntMap.Refined.zipWithKey' f m1 m2

497575-- | v'SomeIntMapWith' @r m proof <- 'Data.IntMap.Refined.intersectionWithKey' (f . 'andLeft') m1 m2

498576-- , v'IntersectionProof' p1 p2 <- proof

499577-- , ( v'Coercion' :: t'Coercion' ('IntMap' r c) ('IntMap' s c))

@@ -520,10 +598,10 @@ instance TraversableWithIndex (Key s) (IntMap s) where

520598 itraverse = traverseWithKey

521599

522600-- | Similar to the instance for functions -- zip corresponding keys. To use

523−-- '<*>'/'Control.Applicative.liftA2' without 'KnownIntSet' see 'zipWithKey'.

601+-- '<*>'/'Control.Applicative.liftA2' without 'KnownIntSet' see 'zipWith'.

524602instance KnownIntSet s => Applicative (IntMap s) where

525603 pure x = fromSet \_ -> x

526− (<*>) = zipWithKey (const id)

604+ (<*>) = zipWith id

527605

528606-- | @'bind' m f@ is a map that for each key @k :: 'Key' s@, contains the

529607-- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.

@@ -543,7 +621,7 @@ instance KnownIntSet s => MonadReader (Key s) (IntMap s) where

543621

544622-- | Append the values at the corresponding keys

545623instance Semigroup a => Semigroup (IntMap s a) where

546− (<>) = zipWithKey (const (<>))

624+ (<>) = zipWith (<>)

547625

548626instance (KnownIntSet s, Monoid a) => Monoid (IntMap s a) where

549627 mempty = fromSet \_ -> mempty

src/Data/IntMap/Refined.hs+83−2

@@ -69,6 +69,7 @@ module Data.IntMap.Refined

6969 , Common.disjoint

7070 , DisjointProof(..)

7171 -- * Combine

72+ , zipWith

7273 , zipWithKey

7374 , bind

7475 , Common.union

@@ -85,10 +86,12 @@ module Data.IntMap.Refined

8586 , intersectionWithKey

8687 , IntersectionProof(..)

8788 -- * Traversal

89+ , map

8890 , mapWithKey

8991 , traverseWithKey

9092 , mapAccumLWithKey

9193 , mapAccumRWithKey

94+ , mapKeys

9295 , mapKeysWith

9396 , MapProof(..)

9497 , backpermuteKeys

@@ -106,12 +109,19 @@ module Data.IntMap.Refined

106109 -- * Filter

107110 , Common.restrictKeys

108111 , Common.withoutKeys

112+ , Common.filter

113+ , Common.filterKeys

109114 , Common.filterWithKey

115+ , Common.partition

110116 , Common.partitionWithKey

111117 , PartitionProof(..)

118+ , Common.takeWhileAntitone

119+ , Common.dropWhileAntitone

112120 , Common.spanAntitone

113121 , PartialPartitionProof(..)

122+ , mapMaybe

114123 , mapMaybeWithKey

124+ , mapEither

115125 , mapEitherWithKey

116126 , Common.splitLookup

117127 , SplitProof(..)

@@ -135,13 +145,13 @@ import Data.Functor

135145import qualified Data.IntMap as IntMap

136146import Data.IntMap.Common.Refined

137147 ( IntMap(..), Key, unsafeCastKey, unsafeKey, SomeIntMapWith(..)

138− , Some2IntMapWith(..), fromSet, (!), zipWithKey, mapWithKey, traverseWithKey

148+ , Some2IntMapWith(..), fromSet, (!), zipWith, mapWithKey, traverseWithKey

139149 , bind

140150 )

141151import qualified Data.IntMap.Common.Refined as Common

142152import Data.Traversable

143153import Data.Type.Coercion

144−import Prelude hiding (lookup, null)

154+import Prelude hiding (lookup, map, null, zipWith)

145155import Refined

146156import Refined.Unsafe

147157

@@ -326,6 +336,26 @@ updateLookupWithKey f k (IntMap m)

326336 (v', !m') -> ((unsafeKey k,) <$> v',)

327337 $ SomeIntMapWith (IntMap m') $ SupersetProof unsafeSubset

328338

339+-- | Given two maps proven to have the same keys, for each key apply the

340+-- function to the associated values and the key, to obtain a new map with the

341+-- same keys.

342+zipWithKey

343+ :: forall s a b c. (Key s -> a -> b -> c)

344+ -> IntMap s a

345+ -> IntMap s b

346+ -> IntMap s c

347+zipWithKey f (IntMap m1) (IntMap m2) = IntMap

348+ $ IntMap.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)

349+ (\m -> if IntMap.null m

350+ then IntMap.empty

351+ else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")

352+ (\m -> if IntMap.null m

353+ then IntMap.empty

354+ else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")

355+ -- ^ Work around https://github.com/haskell/containers/issues/979

356+ m1

357+ m2

358+

329359-- | Return the union of two maps, with a given combining function for keys that

330360-- exist in both maps simultaneously.

331361unionWith

@@ -405,6 +435,10 @@ intersectionWithKey f (IntMap m1) (IntMap m2) = SomeIntMapWith

405435 (IntMap $ IntMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)

406436 $ IntersectionProof unsafeSubset unsafeSubsetWith2

407437

438+-- | Apply a function to all values in a map. The set of keys remains the same.

439+map :: forall s a b. (a -> b) -> IntMap s a -> IntMap s b

440+map = coerce $ IntMap.map @a @b

441+

408442-- | Thread an accumularing argument through the map in ascending order of keys.

409443mapAccumLWithKey

410444 :: forall s a b c. (a -> Key s -> b -> (a, c))

@@ -424,6 +458,27 @@ mapAccumRWithKey

424458mapAccumRWithKey = gcoerceWith (unsafeCastKey @s) $ coerce

425459 $ IntMap.mapAccumRWithKey @a @b @c

426460

461+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results

462+-- into a new map. For keys that were mapped to the same new key, the value

463+-- corresponding to the greatest of the original keys is retained.

464+mapKeys

465+ :: forall s a. (Key s -> Int)

466+ -> IntMap s a

467+ -> SomeIntMapWith (MapProof 'Int s Int Int) a

468+mapKeys g (IntMap m)

469+ = SomeIntMapWith (IntMap $ IntMap.mapKeys (g . unsafeKey) m)

470+ $ MapProof (unsafeKey . g) \k2 ->

471+ case IntMap.lookup (unrefine k2) backMap of

472+ Nothing -> error

473+ "mapKeys: bug: Data.IntMap.Refined has been subverted"

474+ Just k1 -> k1

475+ where

476+ ~backMap = IntMap.fromList

477+ [ (k2, unsafeKey k1)

478+ | k1 <- IntMap.keys m

479+ , let !k2 = g $ unsafeKey k1

480+ ]

481+

427482-- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the

428483-- results into a new map. For keys that were mapped to the same new key, @c@

429484-- acts as the combining function for corresponding values.

@@ -446,6 +501,15 @@ mapKeysWith f g (IntMap m)

446501 , let !k2 = g $ unsafeKey k1

447502 ]

448503

504+-- | Apply a function to all values in a map and collect only the 'Just'

505+-- results, returning a potentially smaller map.

506+mapMaybe

507+ :: forall s a b. (a -> Maybe b)

508+ -> IntMap s a

509+ -> SomeIntMapWith (SupersetProof 'Int s) b

510+mapMaybe f (IntMap m) = SomeIntMapWith (IntMap $ IntMap.mapMaybe f m)

511+ $ SupersetProof unsafeSubset

512+

449513-- | Apply a function to all values in a map, together with their corresponding

450514-- keys, and collect only the 'Just' results, returning a potentially smaller

451515-- map.

@@ -457,6 +521,23 @@ mapMaybeWithKey f (IntMap m)

457521 = SomeIntMapWith (IntMap $ IntMap.mapMaybeWithKey (f . unsafeKey) m)

458522 $ SupersetProof unsafeSubset

459523

524+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'

525+-- results into separate (disjoint) maps.

526+mapEither

527+ :: forall s a b c. (a -> Either b c)

528+ -> IntMap s a

529+ -> Some2IntMapWith (PartitionProof 'Int s Int) b c

530+mapEither p (IntMap m)

531+ = case IntMap.mapEither p m of

532+ (m1, m2) -> Some2IntMapWith (IntMap m1) (IntMap m2) $ PartitionProof

533+ do \k -> case IntMap.lookup (unrefine k) m of

534+ Nothing -> error

535+ "mapEither: bug: Data.IntMap.Refined has been subverted"

536+ Just x -> case p x of

537+ Left _ -> Left $ unsafeKey $ unrefine k

538+ Right _ -> Right $ unsafeKey $ unrefine k

539+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

540+

460541-- | Apply a function to all values in a map, together with their corresponding

461542-- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

462543-- maps.

src/Data/IntMap/Strict/Refined.hs+84−1

@@ -69,6 +69,7 @@ module Data.IntMap.Strict.Refined

6969 , Common.disjoint

7070 , DisjointProof(..)

7171 -- * Combine

72+ , zipWith

7273 , zipWithKey

7374 , bind

7475 , Common.union

@@ -85,10 +86,12 @@ module Data.IntMap.Strict.Refined

8586 , intersectionWithKey

8687 , IntersectionProof(..)

8788 -- * Traversal

89+ , map

8890 , mapWithKey

8991 , traverseWithKey

9092 , mapAccumLWithKey

9193 , mapAccumRWithKey

94+ , mapKeys

9295 , mapKeysWith

9396 , MapProof(..)

9497 , backpermuteKeys

@@ -106,12 +109,19 @@ module Data.IntMap.Strict.Refined

106109 -- * Filter

107110 , Common.restrictKeys

108111 , Common.withoutKeys

112+ , Common.filter

113+ , Common.filterKeys

109114 , Common.filterWithKey

115+ , Common.partition

110116 , Common.partitionWithKey

111117 , PartitionProof(..)

118+ , Common.takeWhileAntitone

119+ , Common.dropWhileAntitone

112120 , Common.spanAntitone

113121 , PartialPartitionProof(..)

122+ , mapMaybe

114123 , mapMaybeWithKey

124+ , mapEither

115125 , mapEitherWithKey

116126 , Common.splitLookup

117127 , SplitProof(..)

@@ -142,7 +152,7 @@ import Data.Proxy

142152import Data.Reflection

143153import Data.Traversable

144154import Data.Type.Coercion

145−import Prelude hiding (lookup, null)

155+import Prelude hiding (lookup, map, null, zipWith)

146156import Refined

147157import Refined.Unsafe

148158

@@ -334,6 +344,28 @@ updateLookupWithKey f k (IntMap m)

334344

335345-- | Given two maps proven to have the same keys, for each key apply the

336346-- function to the associated values, to obtain a new map with the same keys.

347+zipWith

348+ :: forall s a b c. (a -> b -> c)

349+ -> IntMap s a

350+ -> IntMap s b

351+ -> IntMap s c

352+zipWith f (IntMap m1) (IntMap m2) = IntMap

353+ $ IntMap.mergeWithKey (\_ x y -> Just $ f x y)

354+ (\m -> if IntMap.null m

355+ then IntMap.empty

356+ else

357+ error "zipWith: bug: Data.IntMap.Strict.Refined has been subverted")

358+ (\m -> if IntMap.null m

359+ then IntMap.empty

360+ else

361+ error "zipWith: bug: Data.IntMap.Strict.Refined has been subverted")

362+ -- ^ Work around https://github.com/haskell/containers/issues/979

363+ m1

364+ m2

365+

366+-- | Given two maps proven to have the same keys, for each key apply the

367+-- function to the associated values and the key, to obtain a new map with the

368+-- same keys.

337369zipWithKey

338370 :: forall s a b c. (Key s -> a -> b -> c)

339371 -> IntMap s a

@@ -432,6 +464,10 @@ intersectionWithKey f (IntMap m1) (IntMap m2) = SomeIntMapWith

432464 (IntMap $ IntMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)

433465 $ IntersectionProof unsafeSubset unsafeSubsetWith2

434466

467+-- | Apply a function to all values in a map. The set of keys remains the same.

468+map :: forall s a b. (a -> b) -> IntMap s a -> IntMap s b

469+map = coerce $ IntMap.map @a @b

470+

435471-- | Apply a function to all values in a map, together with their corresponding

436472-- keys, that are proven to be in the map. The set of keys remains the same.

437473mapWithKey :: forall s a b. (Key s -> a -> b) -> IntMap s a -> IntMap s b

@@ -465,6 +501,27 @@ mapAccumRWithKey

465501mapAccumRWithKey = gcoerceWith (unsafeCastKey @s) $ coerce

466502 $ IntMap.mapAccumRWithKey @a @b @c

467503

504+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results

505+-- into a new map. For keys that were mapped to the same new key, the value

506+-- corresponding to the greatest of the original keys is retained.

507+mapKeys

508+ :: forall s a. (Key s -> Int)

509+ -> IntMap s a

510+ -> SomeIntMapWith (MapProof 'Int s Int Int) a

511+mapKeys g (IntMap m)

512+ = SomeIntMapWith (IntMap $ IntMap.mapKeys (g . unsafeKey) m)

513+ $ MapProof (unsafeKey . g) \k2 ->

514+ case IntMap.lookup (unrefine k2) backMap of

515+ Nothing -> error

516+ "mapKeys: bug: Data.IntMap.Strict.Refined has been subverted"

517+ Just k1 -> k1

518+ where

519+ ~backMap = IntMap.fromList

520+ [ (k2, unsafeKey k1)

521+ | k1 <- IntMap.keys m

522+ , let !k2 = g $ unsafeKey k1

523+ ]

524+

468525-- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the

469526-- results into a new map. For keys that were mapped to the same new key, @c@

470527-- acts as the combining function for corresponding values.

@@ -487,6 +544,15 @@ mapKeysWith f g (IntMap m)

487544 , let !k2 = g $ unsafeKey k1

488545 ]

489546

547+-- | Apply a function to all values in a map and collect only the 'Just'

548+-- results, returning a potentially smaller map.

549+mapMaybe

550+ :: forall s a b. (a -> Maybe b)

551+ -> IntMap s a

552+ -> SomeIntMapWith (SupersetProof 'Int s) b

553+mapMaybe f (IntMap m) = SomeIntMapWith (IntMap $ IntMap.mapMaybe f m)

554+ $ SupersetProof unsafeSubset

555+

490556-- | Apply a function to all values in a map, together with their corresponding

491557-- keys, and collect only the 'Just' results, returning a potentially smaller

492558-- map.

@@ -498,6 +564,23 @@ mapMaybeWithKey f (IntMap m)

498564 = SomeIntMapWith (IntMap $ IntMap.mapMaybeWithKey (f . unsafeKey) m)

499565 $ SupersetProof unsafeSubset

500566

567+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'

568+-- results into separate (disjoint) maps.

569+mapEither

570+ :: forall s a b c. (a -> Either b c)

571+ -> IntMap s a

572+ -> Some2IntMapWith (PartitionProof 'Int s Int) b c

573+mapEither p (IntMap m)

574+ = case IntMap.mapEither p m of

575+ (m1, m2) -> Some2IntMapWith (IntMap m1) (IntMap m2) $ PartitionProof

576+ do \k -> case IntMap.lookup (unrefine k) m of

577+ Nothing -> error

578+ "mapEither: bug: Data.IntMap.Refined has been subverted"

579+ Just x -> case p x of

580+ Left _ -> Left $ unsafeKey $ unrefine k

581+ Right _ -> Right $ unsafeKey $ unrefine k

582+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

583+

501584-- | Apply a function to all values in a map, together with their corresponding

502585-- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

503586-- maps.

src/Data/IntSet/Refined.hs+1−1

@@ -169,7 +169,7 @@ data SomeIntSet where

169169-- you a way to refer to the set (the parameter @s@), e.g.:

170170--

171171-- @

172−-- 'withIntSet' ('fromIntSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s

172+-- 'withIntSet' ('fromIntSet' ...) $ \\(_ :: 'Proxy' s) -> doSomethingWith \@s

173173-- @

174174withIntSet

175175 :: forall r. SomeIntSet -> (forall s. KnownIntSet s => Proxy s -> r) -> r

src/Data/Map/Common/Refined.hs+92−15

@@ -20,6 +20,7 @@ import qualified Data.Set as Set

2020import Data.Traversable.WithIndex

2121import Data.Type.Coercion

2222import Data.Type.Equality ((:~:)(..))

23+import Prelude hiding (zipWith)

2324import Refined

2425import Refined.Unsafe

2526import Unsafe.Coerce

@@ -109,7 +110,7 @@ data SomeMap k a where

109110-- parameter @s@), e.g.:

110111--

111112-- @

112−-- 'withMap' ('fromMap' ...) $ \(m :: 'Map' s k a) -> doSomethingWith \@s

113+-- 'withMap' ('fromMap' ...) $ \\(m :: 'Map' s k a) -> doSomethingWith \@s

113114-- @

114115withMap :: forall k a r. SomeMap k a -> (forall s. Map s k a -> r) -> r

115116withMap (SomeMap m) k = k m

@@ -259,17 +260,17 @@ disjoint (Map m1) (Map m2)

259260

260261-- | Given two maps proven to have the same keys, for each key apply the

261262-- function to the associated values, to obtain a new map with the same keys.

262−zipWithKey

263+zipWith

263264 :: forall s k a b c. Ord k

264− => (Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c

265−zipWithKey f (Map m1) (Map m2) = Map

266− $ Map.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)

265+ => (a -> b -> c) -> Map s k a -> Map s k b -> Map s k c

266+zipWith f (Map m1) (Map m2) = Map

267+ $ Map.mergeWithKey (\_ x y -> Just $ f x y)

267268 (\m -> if Map.null m

268269 then Map.empty

269− else error "zipWithKey: bug: Data.Map.Refined has been subverted")

270+ else error "zipWith: bug: Data.Map.Refined has been subverted")

270271 (\m -> if Map.null m

271272 then Map.empty

272− else error "zipWithKey: bug: Data.Map.Refined has been subverted")

273+ else error "zipWith: bug: Data.Map.Refined has been subverted")

273274 -- ^ Work around https://github.com/haskell/containers/issues/979

274275 m1

275276 m2

@@ -363,6 +364,29 @@ toList = gcoerceWith (unsafeCastKey @s @k) $ coerce $ Map.toAscList @k @a

363364toDescList :: forall s k a. Map s k a -> [(Key s k, a)]

364365toDescList = gcoerceWith (unsafeCastKey @s @k) $ coerce $ Map.toDescList @k @a

365366

367+-- | Retain only the values that satisfy the predicate, returning a potentially

368+-- smaller map.

369+filter

370+ :: forall s k a. (a -> Bool)

371+ -> Map s k a

372+ -> SomeMapWith (SupersetProof 'Regular s) k a

373+filter p (Map m) = SomeMapWith (Map $ Map.filter p m)

374+ $ SupersetProof unsafeSubset

375+

376+-- | Retain only the keys that satisfy the predicate, returning a potentially

377+-- smaller map.

378+filterKeys

379+ :: forall s k a. (Key s k -> Bool)

380+ -> Map s k a

381+ -> SomeMapWith (SupersetProof 'Regular s) k a

382+filterKeys p (Map m) = SomeMapWith

383+#if MIN_VERSION_containers(0, 8, 0)

384+ (Map $ Map.filterKeys (p . unsafeKey) m)

385+#else

386+ (Map $ Map.filterWithKey (\k _ -> p (unsafeKey k)) m)

387+#endif

388+ $ SupersetProof unsafeSubset

389+

366390-- | Retain only the key-value pairs that satisfy the predicate, returning a

367391-- potentially smaller map.

368392filterWithKey

@@ -397,6 +421,22 @@ withoutKeys (Map m) = SomeMapWith

397421#endif

398422 $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset

399423

424+-- | Partition a map into two disjoint submaps: those whose values satisfy the

425+-- predicate, and those whose don't.

426+partition

427+ :: forall s k a. Ord k -- TODO: this is only used in the proof

428+ => (a -> Bool)

429+ -> Map s k a

430+ -> Some2MapWith (PartitionProof 'Regular s k) k a a

431+partition p (Map m) = case Map.partition p m of

432+ (m1, m2) -> Some2MapWith (Map m1) (Map m2) $ PartitionProof

433+ do \k -> case Map.lookup (unrefine k) m of

434+ Nothing -> error "partition: bug: Data.Map.Refined has been subverted"

435+ Just x -> if p x

436+ then Left $ unsafeKey $ unrefine k

437+ else Right $ unsafeKey $ unrefine k

438+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

439+

400440-- | Partition a map into two disjoint submaps: those whose key-value pairs

401441-- satisfy the predicate, and those whose don't.

402442partitionWithKey

@@ -414,6 +454,43 @@ partitionWithKey p (Map m) = case Map.partitionWithKey (p . unsafeKey) m of

414454 else Right $ unsafeKey $ unrefine k

415455 unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

416456

457+-- | Take the a submap of keys up to a point where the predicate stops holding.

458+--

459+-- If @p@ is antitone ( $\forall x y, x < y \implies p(x) \ge p(y)$ ), then

460+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is

461+-- chosen in an unspecified way.

462+takeWhileAntitone

463+ :: forall s k a. (Key s k -> Bool)

464+ -> Map s k a

465+ -> SomeMapWith (SupersetProof 'Regular s) k a

466+takeWhileAntitone p (Map m) = SomeMapWith

467+#if MIN_VERSION_containers(0, 5, 8)

468+ (Map $ Map.takeWhileAntitone (p . unsafeKey) m)

469+#else

470+ (Map $ Map.fromDistinctAscList

471+ $ List.takeWhile (p . unsafeKey . fst) $ Map.toAscList m)

472+#endif

473+ $ SupersetProof unsafeSubset

474+

475+-- | Take the a submap of keys starting from a point where the predicate stops

476+-- holding.

477+--

478+-- If @p@ is antitone ( $\forall x y, x < y \implies p(x) \ge p(y)$ ), then

479+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is

480+-- chosen in an unspecified way.

481+dropWhileAntitone

482+ :: forall s k a. (Key s k -> Bool)

483+ -> Map s k a

484+ -> SomeMapWith (SupersetProof 'Regular s) k a

485+dropWhileAntitone p (Map m) = SomeMapWith

486+#if MIN_VERSION_containers(0, 5, 8)

487+ (Map $ Map.dropWhileAntitone (p . unsafeKey) m)

488+#else

489+ (Map $ Map.fromDistinctAscList

490+ $ List.dropWhile (p . unsafeKey . fst) $ Map.toAscList m)

491+#endif

492+ $ SupersetProof unsafeSubset

493+

417494-- | Divide a map into two disjoint submaps at a point where the predicate on

418495-- the keys stops holding.

419496--

@@ -486,15 +563,15 @@ castKey

486563castKey = castRefined

487564

488565-- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps

489−-- can be interconverted too. For example, 'zipWithKey' can be implemented via

490−-- 'Data.Map.Refined.intersectionWithKey' by proving that the set of keys

491−-- remains unchanged:

566+-- can be interconverted too. For example, 'Data.Map.Refined.zipWithKey' can be

567+-- implemented via 'Data.Map.Refined.intersectionWithKey' by proving that the

568+-- set of keys remains unchanged:

492569--

493570-- @

494−-- 'zipWithKey'

571+-- 'Data.Map.Refined.zipWithKey'

495572-- :: forall s k a b c. 'Ord' k

496573-- => ('Key' s k -> a -> b -> c) -> 'Map' s k a -> 'Map' s k b -> 'Map' s k c

497−-- 'zipWithKey' f m1 m2

574+-- 'Data.Map.Refined.zipWithKey' f m1 m2

498575-- | v'SomeMapWith' @r m proof <- 'Data.Map.Refined.intersectionWithKey' (f . 'andLeft') m1 m2

499576-- , v'IntersectionProof' p1 p2 <- proof

500577-- , ( v'Coercion' :: t'Coercion' ('Map' r k c) ('Map' s k c))

@@ -519,10 +596,10 @@ instance TraversableWithIndex (Key s k) (Map s k) where

519596 itraverse = traverseWithKey

520597

521598-- | Similar to the instance for functions -- zip corresponding keys. To use

522−-- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWithKey'.

599+-- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWith'.

523600instance (Ord k, KnownSet s k) => Applicative (Map s k) where

524601 pure x = fromSet \_ -> x

525− (<*>) = zipWithKey (const id)

602+ (<*>) = zipWith id

526603

527604-- | @'bind' m f@ is a map that for each key @k :: 'Key' s k@, contains the

528605-- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.

@@ -542,7 +619,7 @@ instance (Ord k, KnownSet s k) => MonadReader (Key s k) (Map s k) where

542619

543620-- | Append the values at the corresponding keys

544621instance (Ord k, Semigroup a) => Semigroup (Map s k a) where

545− (<>) = zipWithKey (const (<>))

622+ (<>) = zipWith (<>)

546623

547624instance (Ord k, KnownSet s k, Monoid a) => Monoid (Map s k a) where

548625 mempty = fromSet \_ -> mempty

src/Data/Map/Refined.hs+80−2

@@ -78,6 +78,7 @@ module Data.Map.Refined

7878 , Common.disjoint

7979 , DisjointProof(..)

8080 -- * Combine

81+ , zipWith

8182 , zipWithKey

8283 , bind

8384 , Common.union

@@ -94,10 +95,12 @@ module Data.Map.Refined

9495 , intersectionWithKey

9596 , IntersectionProof(..)

9697 -- * Traversal

98+ , map

9799 , mapWithKey

98100 , traverseWithKey

99101 , mapAccumLWithKey

100102 , mapAccumRWithKey

103+ , mapKeys

101104 , mapKeysWith

102105 , MapProof(..)

103106 , backpermuteKeys

@@ -115,12 +118,19 @@ module Data.Map.Refined

115118 -- * Filter

116119 , Common.restrictKeys

117120 , Common.withoutKeys

121+ , Common.filter

122+ , Common.filterKeys

118123 , Common.filterWithKey

124+ , Common.partition

119125 , Common.partitionWithKey

120126 , PartitionProof(..)

127+ , Common.takeWhileAntitone

128+ , Common.dropWhileAntitone

121129 , Common.spanAntitone

122130 , PartialPartitionProof(..)

131+ , mapMaybe

123132 , mapMaybeWithKey

133+ , mapEither

124134 , mapEitherWithKey

125135 , Common.splitLookup

126136 , SplitProof(..)

@@ -144,12 +154,12 @@ import Data.Functor

144154import qualified Data.Map as Map

145155import Data.Map.Common.Refined

146156 ( Map(..), Key, unsafeCastKey, unsafeKey, SomeMapWith(..), Some2MapWith(..)

147− , fromSet, (!), zipWithKey, mapWithKey, traverseWithKey, bind

157+ , fromSet, (!), zipWith, mapWithKey, traverseWithKey, bind

148158 )

149159import qualified Data.Map.Common.Refined as Common

150160import Data.Traversable

151161import Data.Type.Coercion

152−import Prelude hiding (lookup, null)

162+import Prelude hiding (lookup, map, null, zipWith)

153163import Refined

154164import Refined.Unsafe

155165

@@ -337,6 +347,24 @@ updateLookupWithKey f k (Map m)

337347 (v', !m') -> ((unsafeKey k,) <$> v',)

338348 $ SomeMapWith (Map m') $ SupersetProof unsafeSubset

339349

350+-- | Given two maps proven to have the same keys, for each key apply the

351+-- function to the associated values and the key, to obtain a new map with the

352+-- same keys.

353+zipWithKey

354+ :: forall s k a b c. Ord k

355+ => (Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c

356+zipWithKey f (Map m1) (Map m2) = Map

357+ $ Map.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)

358+ (\m -> if Map.null m

359+ then Map.empty

360+ else error "zipWithKey: bug: Data.Map.Refined has been subverted")

361+ (\m -> if Map.null m

362+ then Map.empty

363+ else error "zipWithKey: bug: Data.Map.Refined has been subverted")

364+ -- ^ Work around https://github.com/haskell/containers/issues/979

365+ m1

366+ m2

367+

340368-- | Return the union of two maps, with a given combining function for keys that

341369-- exist in both maps simultaneously.

342370unionWith

@@ -415,6 +443,10 @@ intersectionWithKey f (Map m1) (Map m2)

415443 = SomeMapWith (Map $ Map.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)

416444 $ IntersectionProof unsafeSubset unsafeSubsetWith2

417445

446+-- | Apply a function to all values in a map. The set of keys remains the same.

447+map :: forall s k a b. (a -> b) -> Map s k a -> Map s k b

448+map = coerce $ Map.map @a @b @k

449+

418450-- | Thread an accumularing argument through the map in ascending order of keys.

419451mapAccumLWithKey

420452 :: forall s k a b c. (a -> Key s k -> b -> (a, c))

@@ -434,6 +466,26 @@ mapAccumRWithKey

434466mapAccumRWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce

435467 $ Map.mapAccumRWithKey @a @k @b @c

436468

469+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results

470+-- into a new map. For keys that were mapped to the same new key, the value

471+-- corresponding to the greatest of the original keys is retained.

472+mapKeys

473+ :: forall s k1 k2 a. Ord k2

474+ => (Key s k1 -> k2)

475+ -> Map s k1 a

476+ -> SomeMapWith (MapProof 'Regular s k1 k2) k2 a

477+mapKeys g (Map m)

478+ = SomeMapWith (Map $ Map.mapKeys (g . unsafeKey) m)

479+ $ MapProof (unsafeKey . g) \k2 -> case Map.lookup (unrefine k2) backMap of

480+ Nothing -> error "mapKeys: bug: Data.Map.Refined has been subverted"

481+ Just k1 -> k1

482+ where

483+ ~backMap = Map.fromList

484+ [ (k2, unsafeKey k1)

485+ | k1 <- Map.keys m

486+ , let !k2 = g $ unsafeKey k1

487+ ]

488+

437489-- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the

438490-- results into a new map. For keys that were mapped to the same new key, @c@

439491-- acts as the combining function for corresponding values.

@@ -455,6 +507,15 @@ mapKeysWith f g (Map m)

455507 , let !k2 = g $ unsafeKey k1

456508 ]

457509

510+-- | Apply a function to all values in a map and collect only the 'Just'

511+-- results, returning a potentially smaller map.

512+mapMaybe

513+ :: forall s k a b. (a -> Maybe b)

514+ -> Map s k a

515+ -> SomeMapWith (SupersetProof 'Regular s) k b

516+mapMaybe f (Map m) = SomeMapWith (Map $ Map.mapMaybe f m)

517+ $ SupersetProof unsafeSubset

518+

458519-- | Apply a function to all values in a map, together with their corresponding

459520-- keys, and collect only the 'Just' results, returning a potentially smaller

460521-- map.

@@ -466,6 +527,23 @@ mapMaybeWithKey f (Map m)

466527 = SomeMapWith (Map $ Map.mapMaybeWithKey (f . unsafeKey) m)

467528 $ SupersetProof unsafeSubset

468529

530+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'

531+-- results into separate (disjoint) maps.

532+mapEither

533+ :: forall s k a b c. Ord k -- TODO: this is only used in the proof

534+ => (a -> Either b c)

535+ -> Map s k a

536+ -> Some2MapWith (PartitionProof 'Regular s k) k b c

537+mapEither p (Map m) = case Map.mapEither p m of

538+ (m1, m2) -> Some2MapWith (Map m1) (Map m2) $ PartitionProof

539+ do \k -> case Map.lookup (unrefine k) m of

540+ Nothing -> error

541+ "mapEither: bug: Data.Map.Refined has been subverted"

542+ Just x -> case p x of

543+ Left _ -> Left $ unsafeKey $ unrefine k

544+ Right _ -> Right $ unsafeKey $ unrefine k

545+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

546+

469547-- | Apply a function to all values in a map, together with their corresponding

470548-- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

471549-- maps.

src/Data/Map/Strict/Refined.hs+80−1

@@ -78,6 +78,7 @@ module Data.Map.Strict.Refined

7878 , Common.disjoint

7979 , DisjointProof(..)

8080 -- * Combine

81+ , zipWith

8182 , zipWithKey

8283 , bind

8384 , Common.union

@@ -94,10 +95,12 @@ module Data.Map.Strict.Refined

9495 , intersectionWithKey

9596 , IntersectionProof(..)

9697 -- * Traversal

98+ , map

9799 , mapWithKey

98100 , traverseWithKey

99101 , mapAccumLWithKey

100102 , mapAccumRWithKey

103+ , mapKeys

101104 , mapKeysWith

102105 , MapProof(..)

103106 , backpermuteKeys

@@ -115,12 +118,19 @@ module Data.Map.Strict.Refined

115118 -- * Filter

116119 , Common.restrictKeys

117120 , Common.withoutKeys

121+ , Common.filter

122+ , Common.filterKeys

118123 , Common.filterWithKey

124+ , Common.partition

119125 , Common.partitionWithKey

120126 , PartitionProof(..)

127+ , Common.takeWhileAntitone

128+ , Common.dropWhileAntitone

121129 , Common.spanAntitone

122130 , PartialPartitionProof(..)

131+ , mapMaybe

123132 , mapMaybeWithKey

133+ , mapEither

124134 , mapEitherWithKey

125135 , Common.splitLookup

126136 , SplitProof(..)

@@ -151,7 +161,7 @@ import Data.Proxy

151161import Data.Reflection

152162import Data.Traversable

153163import Data.Type.Coercion

154−import Prelude hiding (lookup, null)

164+import Prelude hiding (lookup, map, null, zipWith)

155165import Refined

156166import Refined.Unsafe

157167

@@ -346,6 +356,24 @@ updateLookupWithKey f k (Map m)

346356

347357-- | Given two maps proven to have the same keys, for each key apply the

348358-- function to the associated values, to obtain a new map with the same keys.

359+zipWith

360+ :: forall s k a b c. Ord k

361+ => (a -> b -> c) -> Map s k a -> Map s k b -> Map s k c

362+zipWith f (Map m1) (Map m2) = Map

363+ $ Map.mergeWithKey (\_ x y -> Just $ f x y)

364+ (\m -> if Map.null m

365+ then Map.empty

366+ else error "zipWith: bug: Data.Map.Strict.Refined has been subverted")

367+ (\m -> if Map.null m

368+ then Map.empty

369+ else error "zipWith: bug: Data.Map.Strict.Refined has been subverted")

370+ -- ^ Work around https://github.com/haskell/containers/issues/979

371+ m1

372+ m2

373+

374+-- | Given two maps proven to have the same keys, for each key apply the

375+-- function to the associated values and the key, to obtain a new map with the

376+-- same keys.

349377zipWithKey

350378 :: forall s k a b c. Ord k

351379 => (Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c

@@ -439,6 +467,10 @@ intersectionWithKey f (Map m1) (Map m2)

439467 = SomeMapWith (Map $ Map.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)

440468 $ IntersectionProof unsafeSubset unsafeSubsetWith2

441469

470+-- | Apply a function to all values in a map. The set of keys remains the same.

471+map :: forall s k a b. (a -> b) -> Map s k a -> Map s k b

472+map = coerce $ Map.map @a @b @k

473+

442474-- | Apply a function to all values in a map, together with their corresponding

443475-- keys, that are proven to be in the map. The set of keys remains the same.

444476mapWithKey :: forall s k a b. (Key s k -> a -> b) -> Map s k a -> Map s k b

@@ -472,6 +504,27 @@ mapAccumRWithKey

472504mapAccumRWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce

473505 $ Map.mapAccumRWithKey @a @k @b @c

474506

507+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results

508+-- into a new map. For keys that were mapped to the same new key, the value

509+-- corresponding to the greatest of the original keys is retained.

510+mapKeys

511+ :: forall s k1 k2 a. Ord k2

512+ => (Key s k1 -> k2)

513+ -> Map s k1 a

514+ -> SomeMapWith (MapProof 'Regular s k1 k2) k2 a

515+mapKeys g (Map m)

516+ = SomeMapWith (Map $ Map.mapKeys (g . unsafeKey) m)

517+ $ MapProof (unsafeKey . g) \k2 -> case Map.lookup (unrefine k2) backMap of

518+ Nothing -> error

519+ "mapKeys: bug: Data.Map.Strict.Refined has been subverted"

520+ Just k1 -> k1

521+ where

522+ ~backMap = Map.fromList

523+ [ (k2, unsafeKey k1)

524+ | k1 <- Map.keys m

525+ , let !k2 = g $ unsafeKey k1

526+ ]

527+

475528-- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the

476529-- results into a new map. For keys that were mapped to the same new key, @c@

477530-- acts as the combining function for corresponding values.

@@ -494,6 +547,15 @@ mapKeysWith f g (Map m)

494547 , let !k2 = g $ unsafeKey k1

495548 ]

496549

550+-- | Apply a function to all values in a map and collect only the 'Just'

551+-- results, returning a potentially smaller map.

552+mapMaybe

553+ :: forall s k a b. (a -> Maybe b)

554+ -> Map s k a

555+ -> SomeMapWith (SupersetProof 'Regular s) k b

556+mapMaybe f (Map m) = SomeMapWith (Map $ Map.mapMaybe f m)

557+ $ SupersetProof unsafeSubset

558+

497559-- | Apply a function to all values in a map, together with their corresponding

498560-- keys, and collect only the 'Just' results, returning a potentially smaller

499561-- map.

@@ -505,6 +567,23 @@ mapMaybeWithKey f (Map m)

505567 = SomeMapWith (Map $ Map.mapMaybeWithKey (f . unsafeKey) m)

506568 $ SupersetProof unsafeSubset

507569

570+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'

571+-- results into separate (disjoint) maps.

572+mapEither

573+ :: forall s k a b c. Ord k -- TODO: this is only used in the proof

574+ => (a -> Either b c)

575+ -> Map s k a

576+ -> Some2MapWith (PartitionProof 'Regular s k) k b c

577+mapEither p (Map m) = case Map.mapEither p m of

578+ (m1, m2) -> Some2MapWith (Map m1) (Map m2) $ PartitionProof

579+ do \k -> case Map.lookup (unrefine k) m of

580+ Nothing -> error

581+ "mapEither: bug: Data.Map.Strict.Refined has been subverted"

582+ Just x -> case p x of

583+ Left _ -> Left $ unsafeKey $ unrefine k

584+ Right _ -> Right $ unsafeKey $ unrefine k

585+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

586+

508587-- | Apply a function to all values in a map, together with their corresponding

509588-- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

510589-- maps.

src/Data/Set/Refined.hs+1−1

@@ -185,7 +185,7 @@ data SomeSet a where

185185-- you a way to refer to the set (the parameter @s@), e.g.:

186186--

187187-- @

188−-- 'withSet' ('fromSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s

188+-- 'withSet' ('fromSet' ...) $ \\(_ :: 'Proxy' s) -> doSomethingWith \@s

189189-- @

190190withSet

191191 :: forall a r. SomeSet a -> (forall s. KnownSet s a => Proxy s -> r) -> r