c9496f3...main · typeable/refined-containers

git.iko.soy/typeable/refined-containers

13 files changed+835−58

since splitsnapshots

unifiedsplit

refined-containers.cabal+1−1 src/Data/HashMap/Common/Refined.hs+67−15 src/Data/HashMap/Refined.hs+88−2 src/Data/HashMap/Strict/Refined.hs+87−1 src/Data/HashSet/Refined.hs+1−1 src/Data/IntMap/Common/Refined.hs+106−15 src/Data/IntMap/Refined.hs+95−2 src/Data/IntMap/Strict/Refined.hs+96−1 src/Data/IntSet/Refined.hs+1−1 src/Data/Map/Common/Refined.hs+106−15 src/Data/Map/Refined.hs+93−2 src/Data/Map/Strict/Refined.hs+93−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+67−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.

@@ -270,6 +270,20 @@ difference (HashMap m1) (HashMap m2)

270270 = SomeHashMapWith (HashMap $ HashMap.difference m1 m2)

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

272272

273+-- | Return the intersection of two maps, taking values from the first map.

274+--

275+-- @

276+-- 'intersection' = intersectionWith 'const'

277+-- @

278+intersection

279+ :: forall s t k a b. Hashable k

280+ => HashMap s k a

281+ -> HashMap t k b

282+ -> SomeHashMapWith (IntersectionProof 'Hashed s t) k a

283+intersection (HashMap m1) (HashMap m2) = SomeHashMapWith

284+ (HashMap $ HashMap.intersection m1 m2)

285+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

286+

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

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

275289mapWithKey

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

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

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

330344

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+

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

332365-- potentially smaller map.

333366filterWithKey

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

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

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

357390

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+

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

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

360412partitionWithKey

@@ -389,15 +441,15 @@ castKey

389441castKey = castRefined

390442

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

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

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

394−-- 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:

395447--

396448-- @

397−-- 'zipWithKey'

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

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

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

400−-- 'zipWithKey' f m1 m2

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

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

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

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

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

422474 itraverse = traverseWithKey

423475

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

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

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

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

427479 pure x = fromSet \_ -> x

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

480+ (<*>) = zipWith id

429481

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

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

@@ -434,8 +486,8 @@ bind

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

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

436488

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

438−-- 'bind'.

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

490+-- see 'bind'.

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

440492 (>>=) = bind

441493

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

448500

449501-- | Append the values at the corresponding keys

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

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

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

452504

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

454506 => Monoid (HashMap s k a) where

src/Data/HashMap/Refined.hs+88−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

@@ -85,13 +86,17 @@ module Data.HashMap.Refined

8586 , differenceWith

8687 , differenceWithKey

8788 , PartialDifferenceProof(..)

89+ , Common.intersection

90+ , intersectionWith

8891 , intersectionWithKey

8992 , IntersectionProof(..)

9093 -- * Traversal

94+ , map

9195 , mapWithKey

9296 , traverseWithKey

9397 , mapAccumLWithKey

9498 , mapAccumRWithKey

99+ , mapKeys

95100 , mapKeysWith

96101 , MapProof(..)

97102 , backpermuteKeys

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

108113 -- * Filter

109114 , Common.restrictKeys

110115 , Common.withoutKeys

116+ , Common.filter

117+ , Common.filterKeys

111118 , Common.filterWithKey

119+ , Common.partition

112120 , Common.partitionWithKey

113121 , PartitionProof(..)

122+ , mapMaybe

114123 , mapMaybeWithKey

124+ , mapEither

115125 , mapEitherWithKey

116126 -- * Casts

117127 , Common.castKey

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

126136import Data.Functor

127137import Data.HashMap.Common.Refined

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

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

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

130140 , bind

131141 )

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

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

134144import Data.Traversable

135145import Data.Traversable.WithIndex

136146import Data.Type.Coercion

137−import Prelude hiding (lookup, null)

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

138148import Refined

139149import Refined.Unsafe

140150

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

333343 $ SupersetProof unsafeSubset

334344 )

335345

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+

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

337356-- exist in both maps simultaneously.

338357unionWith

@@ -390,6 +409,17 @@ differenceWithKey f (HashMap m1) (HashMap m2) = SomeHashMapWith

390409 (HashMap.mapWithKey (,) m2))

391410 $ PartialDifferenceProof unsafeSubset unsafeSubset

392411

412+-- | Return the intersection of two maps with the given combining function.

413+intersectionWith

414+ :: forall s t k a b c. Hashable k

415+ => (a -> b -> c)

416+ -> HashMap s k a

417+ -> HashMap t k b

418+ -> SomeHashMapWith (IntersectionProof 'Hashed s t) k c

419+intersectionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith

420+ (HashMap $ HashMap.intersectionWith f m1 m2)

421+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

422+

393423-- | Return the intersection of two maps with the given combining function.

394424--

395425-- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@

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

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

405435 $ IntersectionProof unsafeSubset unsafeSubsetWith2

406436

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+

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

408442-- hashes.

409443mapAccumLWithKey

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

422456 -> (a, HashMap s k c)

423457mapAccumRWithKey f = imapAccumR (flip f)

424458

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+

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

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

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

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

446502 , let !k2 = g $ unsafeKey k1

447503 ]

448504

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+

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

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

451516-- map.

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

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

458523 $ SupersetProof unsafeSubset

459524

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+

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

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

462548-- maps.

src/Data/HashMap/Strict/Refined.hs+87−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

@@ -85,13 +86,17 @@ module Data.HashMap.Strict.Refined

8586 , differenceWith

8687 , differenceWithKey

8788 , PartialDifferenceProof(..)

89+ , Common.intersection

90+ , intersectionWith

8891 , intersectionWithKey

8992 , IntersectionProof(..)

9093 -- * Traversal

94+ , map

9195 , mapWithKey

9296 , traverseWithKey

9397 , mapAccumLWithKey

9498 , mapAccumRWithKey

99+ , mapKeys

95100 , mapKeysWith

96101 , MapProof(..)

97102 , backpermuteKeys

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

108113 -- * Filter

109114 , Common.restrictKeys

110115 , Common.withoutKeys

116+ , Common.filter

117+ , Common.filterKeys

111118 , Common.filterWithKey

119+ , Common.partition

112120 , Common.partitionWithKey

113121 , PartitionProof(..)

122+ , mapMaybe

114123 , mapMaybeWithKey

124+ , mapEither

115125 , mapEitherWithKey

116126 -- * Casts

117127 , Common.castKey

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

136146import Data.Traversable

137147import Data.Traversable.WithIndex

138148import Data.Type.Coercion

139−import Prelude hiding (lookup, null)

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

140150import Refined

141151import Refined.Unsafe

142152

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

343353

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

345355-- 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.

346364zipWithKey

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

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

@@ -406,6 +424,17 @@ differenceWithKey f (HashMap m1) (HashMap m2) = SomeHashMapWith

406424 (HashMap.mapWithKey (,) m2))

407425 $ PartialDifferenceProof unsafeSubset unsafeSubset

408426

427+-- | Return the intersection of two maps with the given combining function.

428+intersectionWith

429+ :: forall s t k a b c. Hashable k

430+ => (a -> b -> c)

431+ -> HashMap s k a

432+ -> HashMap t k b

433+ -> SomeHashMapWith (IntersectionProof 'Hashed s t) k c

434+intersectionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith

435+ (HashMap $ HashMap.intersectionWith f m1 m2)

436+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

437+

409438-- | Return the intersection of two maps with the given combining function.

410439--

411440-- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@

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

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

421450 $ IntersectionProof unsafeSubset unsafeSubsetWith2

422451

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+

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

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

425458mapWithKey

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

454487 -> (a, HashMap s k c)

455488mapAccumRWithKey f = imapAccumR (flip f)

456489

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+

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

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

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

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

478534 , let !k2 = g $ unsafeKey k1

479535 ]

480536

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+

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

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

483548-- map.

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

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

490555 $ SupersetProof unsafeSubset

491556

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+

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

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

494580-- 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+106−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

@@ -288,6 +290,19 @@ difference (IntMap m1) (IntMap m2) = SomeIntMapWith

288290 (IntMap $ IntMap.difference m1 m2)

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

290292

293+-- | Return the intersection of two maps, taking values from the first map.

294+--

295+-- @

296+-- 'intersection' = intersectionWith 'const'

297+-- @

298+intersection

299+ :: forall s t a b. IntMap s a

300+ -> IntMap t b

301+ -> SomeIntMapWith (IntersectionProof 'Int s t) a

302+intersection (IntMap m1) (IntMap m2) = SomeIntMapWith

303+ (IntMap $ IntMap.intersection m1 m2)

304+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

305+

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

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

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

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

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

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

346361

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+

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

348386-- potentially smaller map.

349387filterWithKey

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

379417#endif

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

381419

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+

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

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

384438partitionWithKey

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

396450 else Right $ unsafeKey $ unrefine k

397451 unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

398452

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+

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

400491-- the keys stops holding.

401492--

@@ -470,17 +561,17 @@ castKey

470561castKey = castRefined

471562

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

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

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

475−-- 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:

476567--

477568-- @

478−-- 'zipWithKey'

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

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

480571-- -> 'IntMap' s a

481572-- -> 'IntMap' s b

482573-- -> 'IntMap' s c

483−-- 'zipWithKey' f m1 m2

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

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

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

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

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

507598 itraverse = traverseWithKey

508599

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

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

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

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

512603 pure x = fromSet \_ -> x

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

604+ (<*>) = zipWith id

514605

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

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

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

530621

531622-- | Append the values at the corresponding keys

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

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

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

534625

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

536627 mempty = fromSet \_ -> mempty

src/Data/IntMap/Refined.hs+95−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

@@ -80,13 +81,17 @@ module Data.IntMap.Refined

8081 , differenceWith

8182 , differenceWithKey

8283 , PartialDifferenceProof(..)

84+ , Common.intersection

85+ , intersectionWith

8386 , intersectionWithKey

8487 , IntersectionProof(..)

8588 -- * Traversal

89+ , map

8690 , mapWithKey

8791 , traverseWithKey

8892 , mapAccumLWithKey

8993 , mapAccumRWithKey

94+ , mapKeys

9095 , mapKeysWith

9196 , MapProof(..)

9297 , backpermuteKeys

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

104109 -- * Filter

105110 , Common.restrictKeys

106111 , Common.withoutKeys

112+ , Common.filter

113+ , Common.filterKeys

107114 , Common.filterWithKey

115+ , Common.partition

108116 , Common.partitionWithKey

109117 , PartitionProof(..)

118+ , Common.takeWhileAntitone

119+ , Common.dropWhileAntitone

110120 , Common.spanAntitone

111121 , PartialPartitionProof(..)

122+ , mapMaybe

112123 , mapMaybeWithKey

124+ , mapEither

113125 , mapEitherWithKey

114126 , Common.splitLookup

115127 , SplitProof(..)

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

133145import qualified Data.IntMap as IntMap

134146import Data.IntMap.Common.Refined

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

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

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

137149 , bind

138150 )

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

140152import Data.Traversable

141153import Data.Type.Coercion

142−import Prelude hiding (lookup, null)

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

143155import Refined

144156import Refined.Unsafe

145157

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

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

325337 $ SomeIntMapWith (IntMap m') $ SupersetProof unsafeSubset

326338

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+

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

328360-- exist in both maps simultaneously.

329361unionWith

@@ -377,6 +409,16 @@ differenceWithKey f (IntMap m1) (IntMap m2) = SomeIntMapWith

377409 (IntMap $ IntMap.differenceWithKey (f . reallyUnsafeRefine) m1 m2)

378410 $ PartialDifferenceProof unsafeSubset unsafeSubset

379411

412+-- | Return the intersection of two maps with the given combining function.

413+intersectionWith

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

415+ -> IntMap s a

416+ -> IntMap t b

417+ -> SomeIntMapWith (IntersectionProof 'Int s t) c

418+intersectionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith

419+ (IntMap $ IntMap.intersectionWith f m1 m2)

420+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

421+

380422-- | Return the intersection of two maps with the given combining function.

381423--

382424-- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@

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

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

394436 $ IntersectionProof unsafeSubset unsafeSubsetWith2

395437

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+

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

397443mapAccumLWithKey

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

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

412458mapAccumRWithKey = gcoerceWith (unsafeCastKey @s) $ coerce

413459 $ IntMap.mapAccumRWithKey @a @b @c

414460

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+

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

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

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

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

434501 , let !k2 = g $ unsafeKey k1

435502 ]

436503

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+

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

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

439515-- map.

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

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

446522 $ SupersetProof unsafeSubset

447523

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+

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

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

450543-- maps.

src/Data/IntMap/Strict/Refined.hs+96−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

@@ -80,13 +81,17 @@ module Data.IntMap.Strict.Refined

8081 , differenceWith

8182 , differenceWithKey

8283 , PartialDifferenceProof(..)

84+ , Common.intersection

85+ , intersectionWith

8386 , intersectionWithKey

8487 , IntersectionProof(..)

8588 -- * Traversal

89+ , map

8690 , mapWithKey

8791 , traverseWithKey

8892 , mapAccumLWithKey

8993 , mapAccumRWithKey

94+ , mapKeys

9095 , mapKeysWith

9196 , MapProof(..)

9297 , backpermuteKeys

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

104109 -- * Filter

105110 , Common.restrictKeys

106111 , Common.withoutKeys

112+ , Common.filter

113+ , Common.filterKeys

107114 , Common.filterWithKey

115+ , Common.partition

108116 , Common.partitionWithKey

109117 , PartitionProof(..)

118+ , Common.takeWhileAntitone

119+ , Common.dropWhileAntitone

110120 , Common.spanAntitone

111121 , PartialPartitionProof(..)

122+ , mapMaybe

112123 , mapMaybeWithKey

124+ , mapEither

113125 , mapEitherWithKey

114126 , Common.splitLookup

115127 , SplitProof(..)

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

140152import Data.Reflection

141153import Data.Traversable

142154import Data.Type.Coercion

143−import Prelude hiding (lookup, null)

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

144156import Refined

145157import Refined.Unsafe

146158

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

332344

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

334346-- 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.

335369zipWithKey

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

337371 -> IntMap s a

@@ -404,6 +438,16 @@ differenceWithKey f (IntMap m1) (IntMap m2) = SomeIntMapWith

404438 (IntMap $ IntMap.differenceWithKey (f . reallyUnsafeRefine) m1 m2)

405439 $ PartialDifferenceProof unsafeSubset unsafeSubset

406440

441+-- | Return the intersection of two maps with the given combining function.

442+intersectionWith

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

444+ -> IntMap s a

445+ -> IntMap t b

446+ -> SomeIntMapWith (IntersectionProof 'Int s t) c

447+intersectionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith

448+ (IntMap $ IntMap.intersectionWith f m1 m2)

449+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

450+

407451-- | Return the intersection of two maps with the given combining function.

408452--

409453-- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@

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

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

421465 $ IntersectionProof unsafeSubset unsafeSubsetWith2

422466

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+

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

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

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

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

453501mapAccumRWithKey = gcoerceWith (unsafeCastKey @s) $ coerce

454502 $ IntMap.mapAccumRWithKey @a @b @c

455503

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+

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

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

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

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

475544 , let !k2 = g $ unsafeKey k1

476545 ]

477546

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+

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

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

480558-- map.

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

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

487565 $ SupersetProof unsafeSubset

488566

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+

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

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

491586-- 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+106−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

@@ -293,6 +294,20 @@ difference

293294difference (Map m1) (Map m2) = SomeMapWith (Map $ Map.difference m1 m2)

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

295296

297+-- | Return the intersection of two maps, taking values from the first map.

298+--

299+-- @

300+-- 'intersection' = intersectionWith 'const'

301+-- @

302+intersection

303+ :: forall s t k a b. Ord k

304+ => Map s k a

305+ -> Map t k b

306+ -> SomeMapWith (IntersectionProof 'Regular s t) k a

307+intersection (Map m1) (Map m2)

308+ = SomeMapWith (Map $ Map.intersection m1 m2)

309+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

310+

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

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

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

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

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

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

351366

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+

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

353391-- potentially smaller map.

354392filterWithKey

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

383421#endif

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

385423

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+

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

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

388442partitionWithKey

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

400454 else Right $ unsafeKey $ unrefine k

401455 unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

402456

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+

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

404495-- the keys stops holding.

405496--

@@ -472,15 +563,15 @@ castKey

472563castKey = castRefined

473564

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

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

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

477−-- 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:

478569--

479570-- @

480−-- 'zipWithKey'

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

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

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

483−-- 'zipWithKey' f m1 m2

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

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

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

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

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

505596 itraverse = traverseWithKey

506597

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

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

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

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

510601 pure x = fromSet \_ -> x

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

602+ (<*>) = zipWith id

512603

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

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

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

528619

529620-- | Append the values at the corresponding keys

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

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

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

532623

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

534625 mempty = fromSet \_ -> mempty

src/Data/Map/Refined.hs+93−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

@@ -89,13 +90,17 @@ module Data.Map.Refined

8990 , differenceWith

9091 , differenceWithKey

9192 , PartialDifferenceProof(..)

93+ , Common.intersection

94+ , intersectionWith

9295 , intersectionWithKey

9396 , IntersectionProof(..)

9497 -- * Traversal

98+ , map

9599 , mapWithKey

96100 , traverseWithKey

97101 , mapAccumLWithKey

98102 , mapAccumRWithKey

103+ , mapKeys

99104 , mapKeysWith

100105 , MapProof(..)

101106 , backpermuteKeys

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

113118 -- * Filter

114119 , Common.restrictKeys

115120 , Common.withoutKeys

121+ , Common.filter

122+ , Common.filterKeys

116123 , Common.filterWithKey

124+ , Common.partition

117125 , Common.partitionWithKey

118126 , PartitionProof(..)

127+ , Common.takeWhileAntitone

128+ , Common.dropWhileAntitone

119129 , Common.spanAntitone

120130 , PartialPartitionProof(..)

131+ , mapMaybe

121132 , mapMaybeWithKey

133+ , mapEither

122134 , mapEitherWithKey

123135 , Common.splitLookup

124136 , SplitProof(..)

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

142154import qualified Data.Map as Map

143155import Data.Map.Common.Refined

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

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

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

146158 )

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

148160import Data.Traversable

149161import Data.Type.Coercion

150−import Prelude hiding (lookup, null)

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

151163import Refined

152164import Refined.Unsafe

153165

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

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

336348 $ SomeMapWith (Map m') $ SupersetProof unsafeSubset

337349

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+

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

339369-- exist in both maps simultaneously.

340370unionWith

@@ -388,6 +418,17 @@ differenceWithKey f (Map m1) (Map m2)

388418 = SomeMapWith (Map $ Map.differenceWithKey (f . reallyUnsafeRefine) m1 m2)

389419 $ PartialDifferenceProof unsafeSubset unsafeSubset

390420

421+-- | Return the intersection of two maps with the given combining function.

422+intersectionWith

423+ :: forall s t k a b c. Ord k

424+ => (a -> b -> c)

425+ -> Map s k a

426+ -> Map t k b

427+ -> SomeMapWith (IntersectionProof 'Regular s t) k c

428+intersectionWith f (Map m1) (Map m2)

429+ = SomeMapWith (Map $ Map.intersectionWith f m1 m2)

430+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

431+

391432-- | Return the intersection of two maps with the given combining function.

392433--

393434-- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@

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

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

403444 $ IntersectionProof unsafeSubset unsafeSubsetWith2

404445

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+

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

406451mapAccumLWithKey

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

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

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

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

423468

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+

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

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

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

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

442507 , let !k2 = g $ unsafeKey k1

443508 ]

444509

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+

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

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

447521-- map.

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

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

454528 $ SupersetProof unsafeSubset

455529

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+

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

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

458549-- maps.

src/Data/Map/Strict/Refined.hs+93−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

@@ -89,13 +90,17 @@ module Data.Map.Strict.Refined

8990 , differenceWith

9091 , differenceWithKey

9192 , PartialDifferenceProof(..)

93+ , Common.intersection

94+ , intersectionWith

9295 , intersectionWithKey

9396 , IntersectionProof(..)

9497 -- * Traversal

98+ , map

9599 , mapWithKey

96100 , traverseWithKey

97101 , mapAccumLWithKey

98102 , mapAccumRWithKey

103+ , mapKeys

99104 , mapKeysWith

100105 , MapProof(..)

101106 , backpermuteKeys

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

113118 -- * Filter

114119 , Common.restrictKeys

115120 , Common.withoutKeys

121+ , Common.filter

122+ , Common.filterKeys

116123 , Common.filterWithKey

124+ , Common.partition

117125 , Common.partitionWithKey

118126 , PartitionProof(..)

127+ , Common.takeWhileAntitone

128+ , Common.dropWhileAntitone

119129 , Common.spanAntitone

120130 , PartialPartitionProof(..)

131+ , mapMaybe

121132 , mapMaybeWithKey

133+ , mapEither

122134 , mapEitherWithKey

123135 , Common.splitLookup

124136 , SplitProof(..)

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

149161import Data.Reflection

150162import Data.Traversable

151163import Data.Type.Coercion

152−import Prelude hiding (lookup, null)

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

153165import Refined

154166import Refined.Unsafe

155167

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

344356

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

346358-- 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.

347377zipWithKey

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

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

@@ -412,6 +442,17 @@ differenceWithKey f (Map m1) (Map m2)

412442 = SomeMapWith (Map $ Map.differenceWithKey (f . reallyUnsafeRefine) m1 m2)

413443 $ PartialDifferenceProof unsafeSubset unsafeSubset

414444

445+-- | Return the intersection of two maps with the given combining function.

446+intersectionWith

447+ :: forall s t k a b c. Ord k

448+ => (a -> b -> c)

449+ -> Map s k a

450+ -> Map t k b

451+ -> SomeMapWith (IntersectionProof 'Regular s t) k c

452+intersectionWith f (Map m1) (Map m2)

453+ = SomeMapWith (Map $ Map.intersectionWith f m1 m2)

454+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

455+

415456-- | Return the intersection of two maps with the given combining function.

416457--

417458-- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@

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

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

427468 $ IntersectionProof unsafeSubset unsafeSubsetWith2

428469

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+

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

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

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

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

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

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

461506

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+

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

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

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

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

481547 , let !k2 = g $ unsafeKey k1

482548 ]

483549

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+

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

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

486561-- map.

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

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

493568 $ SupersetProof unsafeSubset

494569

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+

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

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

497589-- 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