module Data.Map.Refined
(
Common.Map
, Common.Key
, Common.SomeMap(..)
, Common.withMap
, Common.SomeMapWith(..)
, Common.withMapWith
, Common.Some2MapWith(..)
, Common.with2MapWith
, SupersetProof(..)
, EmptyProof(..)
, Common.empty
, singleton
, SingletonProof(..)
, fromSet
, Common.fromMap
, fromTraversableWithKey
, FromTraversableProof(..)
, insert
, InsertProof(..)
, reinsert
, insertLookupWithKey
, Common.delete
, adjust
, adjustWithKey
, update
, updateLookupWithKey
, Common.lookup
, (Common.!)
, Common.member
, Common.lookupLT
, Common.lookupGT
, Common.lookupLE
, Common.lookupGE
, Common.null
, Common.isSubmapOfBy
, SubsetProof(..)
, Common.disjoint
, DisjointProof(..)
, zipWithKey
, bind
, unionWithKey
, UnionProof(..)
, Common.difference
, DifferenceProof(..)
, differenceWithKey
, PartialDifferenceProof(..)
, intersectionWithKey
, IntersectionProof(..)
, mapWithKey
, traverseWithKey
, mapAccumLWithKey
, mapAccumRWithKey
, mapKeysWith
, MapProof(..)
, backpermuteKeys
, Common.foldMapWithKey
, Common.foldrWithKey
, Common.foldlWithKey
, Common.foldrWithKey'
, Common.foldlWithKey'
, Common.toMap
, Common.keysSet
, Common.toList
, Common.toDescList
, Common.restrictKeys
, Common.withoutKeys
, Common.filterWithKey
, Common.partitionWithKey
, PartitionProof(..)
, Common.spanAntitone
, PartialPartitionProof(..)
, mapMaybeWithKey
, mapEitherWithKey
, Common.splitLookup
, SplitProof(..)
, updateMinWithKey
, updateMaxWithKey
, adjustMinWithKey
, adjustMaxWithKey
, Common.minViewWithKey
, Common.maxViewWithKey
, Common.castKey
, Common.cast
, castFlavor
) where
import Data.Coerce
import Data.Container.Refined.Proofs
import Data.Container.Refined.Unsafe
import Data.Functor
import qualified Data.Map as Map
import Data.Map.Common.Refined
( Map(..), Key, unsafeCastKey, unsafeKey, SomeMapWith(..), Some2MapWith(..)
, fromSet, (!), zipWithKey, mapWithKey, traverseWithKey, bind
)
import qualified Data.Map.Common.Refined as Common
import Data.Traversable
import Data.Type.Coercion
import Prelude hiding (lookup, null)
import Refined
import Refined.Unsafe
singleton :: forall k a. k -> a -> SomeMapWith (SingletonProof 'Regular k) k a
singleton :: forall k a. k -> a -> SomeMapWith (SingletonProof 'Regular k) k a
singleton k
k a
v = Map Any k a
-> SingletonProof 'Regular k Any
-> SomeMapWith (SingletonProof 'Regular k) k a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map (Map k a -> Map Any k a) -> Map k a -> Map Any k a
forall a b. (a -> b) -> a -> b
$ k -> a -> Map k a
forall k a. k -> a -> Map k a
Map.singleton k
k a
v)
(SingletonProof 'Regular k Any
-> SomeMapWith (SingletonProof 'Regular k) k a)
-> SingletonProof 'Regular k Any
-> SomeMapWith (SingletonProof 'Regular k) k a
forall a b. (a -> b) -> a -> b
$ Refined (InSet 'Regular Any) k -> SingletonProof 'Regular k Any
forall (f :: Flavor) a r.
Refined (InSet f r) a -> SingletonProof f a r
SingletonProof (k -> Refined (InSet 'Regular Any) k
forall k s. k -> Key s k
unsafeKey k
k)
fromTraversableWithKey
:: forall t k a. (Traversable t, Ord k)
=> (k -> a -> a -> a)
-> t (k, a)
-> SomeMapWith (FromTraversableProof 'Regular t k) k a
fromTraversableWithKey :: forall (t :: * -> *) k a.
(Traversable t, Ord k) =>
(k -> a -> a -> a)
-> t (k, a) -> SomeMapWith (FromTraversableProof 'Regular t k) k a
fromTraversableWithKey k -> a -> a -> a
f t (k, a)
xs = Map Any k a
-> FromTraversableProof 'Regular t k Any
-> SomeMapWith (FromTraversableProof 'Regular t k) k a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map Map k a
m) (FromTraversableProof 'Regular t k Any
-> SomeMapWith (FromTraversableProof 'Regular t k) k a)
-> FromTraversableProof 'Regular t k Any
-> SomeMapWith (FromTraversableProof 'Regular t k) k a
forall a b. (a -> b) -> a -> b
$ t (Refined (InSet 'Regular Any) k)
-> FromTraversableProof 'Regular t k Any
forall (f :: Flavor) (t :: * -> *) a r.
t (Refined (InSet f r) a) -> FromTraversableProof f t a r
FromTraversableProof t (Refined (InSet 'Regular Any) k)
proof
where
(Map k a
m, t (Refined (InSet 'Regular Any) k)
proof) = (Map k a -> (k, a) -> (Map k a, Refined (InSet 'Regular Any) k))
-> Map k a
-> t (k, a)
-> (Map k a, t (Refined (InSet 'Regular Any) k))
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
(\Map k a
s (k
k, a
v) -> let !s' :: Map k a
s' = (k -> a -> a -> a) -> k -> a -> Map k a -> Map k a
forall k a.
Ord k =>
(k -> a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWithKey k -> a -> a -> a
f k
k a
v Map k a
s in (Map k a
s', k -> Refined (InSet 'Regular Any) k
forall k s. k -> Key s k
unsafeKey k
k))
Map k a
forall k a. Map k a
Map.empty
t (k, a)
xs
insert
:: forall s k a. Ord k
=> k -> a -> Map s k a -> SomeMapWith (InsertProof 'Regular k s) k a
insert :: forall s k a.
Ord k =>
k -> a -> Map s k a -> SomeMapWith (InsertProof 'Regular k s) k a
insert k
k a
v (Map Map k a
m) = Map Any k a
-> InsertProof 'Regular k s Any
-> SomeMapWith (InsertProof 'Regular k s) k a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map (Map k a -> Map Any k a) -> Map k a -> Map Any k a
forall a b. (a -> b) -> a -> b
$ k -> a -> Map k a -> Map k a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k a
v Map k a
m)
(InsertProof 'Regular k s Any
-> SomeMapWith (InsertProof 'Regular k s) k a)
-> InsertProof 'Regular k s Any
-> SomeMapWith (InsertProof 'Regular k s) k a
forall a b. (a -> b) -> a -> b
$ Refined (InSet 'Regular Any) k
-> (InSet 'Regular s :-> InSet 'Regular Any)
-> InsertProof 'Regular k s Any
forall (f :: Flavor) a s r.
Refined (InSet f r) a
-> (InSet f s :-> InSet f r) -> InsertProof f a s r
InsertProof (k -> Refined (InSet 'Regular Any) k
forall k s. k -> Key s k
unsafeKey k
k) Refined (InSet 'Regular s) x -> Refined (InSet 'Regular Any) x
InSet 'Regular s :-> InSet 'Regular Any
forall p q x. Refined p x -> Refined q x
unsafeSubset
reinsert
:: forall s k a. Ord k
=> Key s k -> a -> Map s k a -> Map s k a
reinsert :: forall s k a. Ord k => Key s k -> a -> Map s k a -> Map s k a
reinsert = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
Key s k -> a -> Map s k a -> Map s k a)
-> Key s k
-> a
-> Map s k a
-> Map s k a
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s k. Coercion k (Key s k)
unsafeCastKey @s @k) ((Coercible k (Key s k) => Key s k -> a -> Map s k a -> Map s k a)
-> Key s k -> a -> Map s k a -> Map s k a)
-> (Coercible k (Key s k) =>
Key s k -> a -> Map s k a -> Map s k a)
-> Key s k
-> a
-> Map s k a
-> Map s k a
forall a b. (a -> b) -> a -> b
$ (k -> a -> Map k a -> Map k a)
-> Key s k -> a -> Map s k a -> Map s k a
forall a b. Coercible a b => a -> b
coerce ((k -> a -> Map k a -> Map k a)
-> Key s k -> a -> Map s k a -> Map s k a)
-> (k -> a -> Map k a -> Map k a)
-> Key s k
-> a
-> Map s k a
-> Map s k a
forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert @k @a
insertLookupWithKey
:: forall s k a. Ord k
=> (Key s k -> a -> a -> a)
-> k
-> a
-> Map s k a
-> (Maybe (Key s k, a), SomeMapWith (InsertProof 'Regular k s) k a)
insertLookupWithKey :: forall s k a.
Ord k =>
(Key s k -> a -> a -> a)
-> k
-> a
-> Map s k a
-> (Maybe (Key s k, a), SomeMapWith (InsertProof 'Regular k s) k a)
insertLookupWithKey Key s k -> a -> a -> a
f k
k a
v (Map Map k a
m)
= case (k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
forall k a.
Ord k =>
(k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
Map.insertLookupWithKey (Key s k -> a -> a -> a
f (Key s k -> a -> a -> a) -> (k -> Key s k) -> k -> a -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) k
k a
v Map k a
m of
(Maybe a
v', !Map k a
m') -> ((k -> Key s k
forall k s. k -> Key s k
unsafeKey k
k,) (a -> (Key s k, a)) -> Maybe a -> Maybe (Key s k, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
v',)
(SomeMapWith (InsertProof 'Regular k s) k a
-> (Maybe (Key s k, a),
SomeMapWith (InsertProof 'Regular k s) k a))
-> SomeMapWith (InsertProof 'Regular k s) k a
-> (Maybe (Key s k, a), SomeMapWith (InsertProof 'Regular k s) k a)
forall a b. (a -> b) -> a -> b
$ Map Any k a
-> InsertProof 'Regular k s Any
-> SomeMapWith (InsertProof 'Regular k s) k a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map Map k a
m') (InsertProof 'Regular k s Any
-> SomeMapWith (InsertProof 'Regular k s) k a)
-> InsertProof 'Regular k s Any
-> SomeMapWith (InsertProof 'Regular k s) k a
forall a b. (a -> b) -> a -> b
$ Refined (InSet 'Regular Any) k
-> (InSet 'Regular s :-> InSet 'Regular Any)
-> InsertProof 'Regular k s Any
forall (f :: Flavor) a s r.
Refined (InSet f r) a
-> (InSet f s :-> InSet f r) -> InsertProof f a s r
InsertProof (k -> Refined (InSet 'Regular Any) k
forall k s. k -> Key s k
unsafeKey k
k) Refined (InSet 'Regular s) x -> Refined (InSet 'Regular Any) x
InSet 'Regular s :-> InSet 'Regular Any
forall p q x. Refined p x -> Refined q x
unsafeSubset
adjust :: forall s k a. Ord k => (a -> a) -> Key s k -> Map s k a -> Map s k a
adjust :: forall s k a.
Ord k =>
(a -> a) -> Key s k -> Map s k a -> Map s k a
adjust = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
(a -> a) -> Key s k -> Map s k a -> Map s k a)
-> (a -> a)
-> Key s k
-> Map s k a
-> Map s k a
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s k. Coercion k (Key s k)
unsafeCastKey @s @k) ((Coercible k (Key s k) =>
(a -> a) -> Key s k -> Map s k a -> Map s k a)
-> (a -> a) -> Key s k -> Map s k a -> Map s k a)
-> (Coercible k (Key s k) =>
(a -> a) -> Key s k -> Map s k a -> Map s k a)
-> (a -> a)
-> Key s k
-> Map s k a
-> Map s k a
forall a b. (a -> b) -> a -> b
$ ((a -> a) -> k -> Map k a -> Map k a)
-> (a -> a) -> Key s k -> Map s k a -> Map s k a
forall a b. Coercible a b => a -> b
coerce (((a -> a) -> k -> Map k a -> Map k a)
-> (a -> a) -> Key s k -> Map s k a -> Map s k a)
-> ((a -> a) -> k -> Map k a -> Map k a)
-> (a -> a)
-> Key s k
-> Map s k a
-> Map s k a
forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust @k @a
adjustWithKey
:: forall s k a. Ord k => (Key s k -> a -> a) -> k -> Map s k a -> Map s k a
adjustWithKey :: forall s k a.
Ord k =>
(Key s k -> a -> a) -> k -> Map s k a -> Map s k a
adjustWithKey = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
(Key s k -> a -> a) -> k -> Map s k a -> Map s k a)
-> (Key s k -> a -> a)
-> k
-> Map s k a
-> Map s k a
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s k. Coercion k (Key s k)
unsafeCastKey @s @k) ((Coercible k (Key s k) =>
(Key s k -> a -> a) -> k -> Map s k a -> Map s k a)
-> (Key s k -> a -> a) -> k -> Map s k a -> Map s k a)
-> (Coercible k (Key s k) =>
(Key s k -> a -> a) -> k -> Map s k a -> Map s k a)
-> (Key s k -> a -> a)
-> k
-> Map s k a
-> Map s k a
forall a b. (a -> b) -> a -> b
$ ((k -> a -> a) -> k -> Map k a -> Map k a)
-> (Key s k -> a -> a) -> k -> Map s k a -> Map s k a
forall a b. Coercible a b => a -> b
coerce
(((k -> a -> a) -> k -> Map k a -> Map k a)
-> (Key s k -> a -> a) -> k -> Map s k a -> Map s k a)
-> ((k -> a -> a) -> k -> Map k a -> Map k a)
-> (Key s k -> a -> a)
-> k
-> Map s k a
-> Map s k a
forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (k -> a -> a) -> k -> Map k a -> Map k a
Map.adjustWithKey @k @a
update
:: forall s k a. Ord k
=> (a -> Maybe a)
-> Key s k
-> Map s k a
-> SomeMapWith (SupersetProof 'Regular s) k a
update :: forall s k a.
Ord k =>
(a -> Maybe a)
-> Key s k
-> Map s k a
-> SomeMapWith (SupersetProof 'Regular s) k a
update a -> Maybe a
f Key s k
k (Map Map k a
m) = Map Any k a
-> SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map (Map k a -> Map Any k a) -> Map k a -> Map Any k a
forall a b. (a -> b) -> a -> b
$ (a -> Maybe a) -> k -> Map k a -> Map k a
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update a -> Maybe a
f (Key s k -> k
forall {k} (p :: k) x. Refined p x -> x
unrefine Key s k
k) Map k a
m)
(SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k a)
-> SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular Any :-> InSet 'Regular s)
-> SupersetProof 'Regular s Any
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Regular Any) x -> Refined (InSet 'Regular s) x
InSet 'Regular Any :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset
updateLookupWithKey
:: forall s k a. Ord k
=> (Key s k -> a -> Maybe a)
-> k
-> Map s k a
-> (Maybe (Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
updateLookupWithKey :: forall s k a.
Ord k =>
(Key s k -> a -> Maybe a)
-> k
-> Map s k a
-> (Maybe (Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
updateLookupWithKey Key s k -> a -> Maybe a
f k
k (Map Map k a
m)
= case (k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
forall k a.
Ord k =>
(k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
Map.updateLookupWithKey (Key s k -> a -> Maybe a
f (Key s k -> a -> Maybe a) -> (k -> Key s k) -> k -> a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) k
k Map k a
m of
(Maybe a
v', !Map k a
m') -> ((k -> Key s k
forall k s. k -> Key s k
unsafeKey k
k,) (a -> (Key s k, a)) -> Maybe a -> Maybe (Key s k, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
v',)
(SomeMapWith (SupersetProof 'Regular s) k a
-> (Maybe (Key s k, a),
SomeMapWith (SupersetProof 'Regular s) k a))
-> SomeMapWith (SupersetProof 'Regular s) k a
-> (Maybe (Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
forall a b. (a -> b) -> a -> b
$ Map Any k a
-> SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map Map k a
m') (SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k a)
-> SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular Any :-> InSet 'Regular s)
-> SupersetProof 'Regular s Any
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Regular Any) x -> Refined (InSet 'Regular s) x
InSet 'Regular Any :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset
unionWithKey
:: forall s t k a. Ord k
=> (Refined (InSet 'Regular s && InSet 'Regular t) k -> a -> a -> a)
-> Map s k a
-> Map t k a
-> SomeMapWith (UnionProof 'Regular s t) k a
unionWithKey :: forall s t k a.
Ord k =>
(Refined (InSet 'Regular s && InSet 'Regular t) k -> a -> a -> a)
-> Map s k a
-> Map t k a
-> SomeMapWith (UnionProof 'Regular s t) k a
unionWithKey Refined (InSet 'Regular s && InSet 'Regular t) k -> a -> a -> a
f (Map Map k a
m1) (Map Map k a
m2)
= Map Any k a
-> UnionProof 'Regular s t Any
-> SomeMapWith (UnionProof 'Regular s t) k a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map (Map k a -> Map Any k a) -> Map k a -> Map Any k a
forall a b. (a -> b) -> a -> b
$ (k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
forall k a.
Ord k =>
(k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWithKey (Refined (InSet 'Regular s && InSet 'Regular t) k -> a -> a -> a
f (Refined (InSet 'Regular s && InSet 'Regular t) k -> a -> a -> a)
-> (k -> Refined (InSet 'Regular s && InSet 'Regular t) k)
-> k
-> a
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Refined (InSet 'Regular s && InSet 'Regular t) k
forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine) Map k a
m1 Map k a
m2)
(UnionProof 'Regular s t Any
-> SomeMapWith (UnionProof 'Regular s t) k a)
-> UnionProof 'Regular s t Any
-> SomeMapWith (UnionProof 'Regular s t) k a
forall a b. (a -> b) -> a -> b
$ ((InSet 'Regular s || InSet 'Regular t) :-> InSet 'Regular Any)
-> (forall u.
(InSet 'Regular s :-> InSet 'Regular u)
-> (InSet 'Regular t :-> InSet 'Regular u)
-> InSet 'Regular Any :-> InSet 'Regular u)
-> UnionProof 'Regular s t Any
forall (f :: Flavor) s t r.
((InSet f s || InSet f t) :-> InSet f r)
-> (forall u.
(InSet f s :-> InSet f u)
-> (InSet f t :-> InSet f u) -> InSet f r :-> InSet f u)
-> UnionProof f s t r
UnionProof Refined (InSet 'Regular s || InSet 'Regular t) x
-> Refined (InSet 'Regular Any) x
(InSet 'Regular s || InSet 'Regular t) :-> InSet 'Regular Any
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Regular s :-> InSet 'Regular u)
-> (InSet 'Regular t :-> InSet 'Regular u)
-> Refined (InSet 'Regular Any) x
-> Refined (InSet 'Regular u) x
(InSet 'Regular s :-> InSet 'Regular u)
-> (InSet 'Regular t :-> InSet 'Regular u)
-> InSet 'Regular Any :-> InSet 'Regular u
forall u.
(InSet 'Regular s :-> InSet 'Regular u)
-> (InSet 'Regular t :-> InSet 'Regular u)
-> InSet 'Regular Any :-> InSet 'Regular u
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2
differenceWithKey
:: forall s t k a b. Ord k
=> (Refined (InSet 'Regular s && InSet 'Regular t) k -> a -> b -> Maybe a)
-> Map s k a
-> Map t k b
-> SomeMapWith (PartialDifferenceProof 'Regular s t) k a
differenceWithKey :: forall s t k a b.
Ord k =>
(Refined (InSet 'Regular s && InSet 'Regular t) k
-> a -> b -> Maybe a)
-> Map s k a
-> Map t k b
-> SomeMapWith (PartialDifferenceProof 'Regular s t) k a
differenceWithKey Refined (InSet 'Regular s && InSet 'Regular t) k
-> a -> b -> Maybe a
f (Map Map k a
m1) (Map Map k b
m2)
= Map Any k a
-> PartialDifferenceProof 'Regular s t Any
-> SomeMapWith (PartialDifferenceProof 'Regular s t) k a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map (Map k a -> Map Any k a) -> Map k a -> Map Any k a
forall a b. (a -> b) -> a -> b
$ (k -> a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
forall k a b.
Ord k =>
(k -> a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWithKey (Refined (InSet 'Regular s && InSet 'Regular t) k
-> a -> b -> Maybe a
f (Refined (InSet 'Regular s && InSet 'Regular t) k
-> a -> b -> Maybe a)
-> (k -> Refined (InSet 'Regular s && InSet 'Regular t) k)
-> k
-> a
-> b
-> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Refined (InSet 'Regular s && InSet 'Regular t) k
forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine) Map k a
m1 Map k b
m2)
(PartialDifferenceProof 'Regular s t Any
-> SomeMapWith (PartialDifferenceProof 'Regular s t) k a)
-> PartialDifferenceProof 'Regular s t Any
-> SomeMapWith (PartialDifferenceProof 'Regular s t) k a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular Any :-> InSet 'Regular s)
-> (InSet 'Regular s :-> (InSet 'Regular t || InSet 'Regular Any))
-> PartialDifferenceProof 'Regular s t Any
forall (f :: Flavor) s t r.
(InSet f r :-> InSet f s)
-> (InSet f s :-> (InSet f t || InSet f r))
-> PartialDifferenceProof f s t r
PartialDifferenceProof Refined (InSet 'Regular Any) x -> Refined (InSet 'Regular s) x
InSet 'Regular Any :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset Refined (InSet 'Regular s) x
-> Refined (InSet 'Regular t || InSet 'Regular Any) x
InSet 'Regular s :-> (InSet 'Regular t || InSet 'Regular Any)
forall p q x. Refined p x -> Refined q x
unsafeSubset
intersectionWithKey
:: forall s t k a b c. Ord k
=> (Refined (InSet 'Regular s && InSet 'Regular t) k -> a -> b -> c)
-> Map s k a
-> Map t k b
-> SomeMapWith (IntersectionProof 'Regular s t) k c
intersectionWithKey :: forall s t k a b c.
Ord k =>
(Refined (InSet 'Regular s && InSet 'Regular t) k -> a -> b -> c)
-> Map s k a
-> Map t k b
-> SomeMapWith (IntersectionProof 'Regular s t) k c
intersectionWithKey Refined (InSet 'Regular s && InSet 'Regular t) k -> a -> b -> c
f (Map Map k a
m1) (Map Map k b
m2)
= Map Any k c
-> IntersectionProof 'Regular s t Any
-> SomeMapWith (IntersectionProof 'Regular s t) k c
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k c -> Map Any k c
forall s k a. Map k a -> Map s k a
Map (Map k c -> Map Any k c) -> Map k c -> Map Any k c
forall a b. (a -> b) -> a -> b
$ (k -> a -> b -> c) -> Map k a -> Map k b -> Map k c
forall k a b c.
Ord k =>
(k -> a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWithKey (Refined (InSet 'Regular s && InSet 'Regular t) k -> a -> b -> c
f (Refined (InSet 'Regular s && InSet 'Regular t) k -> a -> b -> c)
-> (k -> Refined (InSet 'Regular s && InSet 'Regular t) k)
-> k
-> a
-> b
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Refined (InSet 'Regular s && InSet 'Regular t) k
forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine) Map k a
m1 Map k b
m2)
(IntersectionProof 'Regular s t Any
-> SomeMapWith (IntersectionProof 'Regular s t) k c)
-> IntersectionProof 'Regular s t Any
-> SomeMapWith (IntersectionProof 'Regular s t) k c
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular Any :-> (InSet 'Regular s && InSet 'Regular t))
-> (forall u.
(InSet 'Regular u :-> InSet 'Regular s)
-> (InSet 'Regular u :-> InSet 'Regular t)
-> InSet 'Regular u :-> InSet 'Regular Any)
-> IntersectionProof 'Regular s t Any
forall (f :: Flavor) s t r.
(InSet f r :-> (InSet f s && InSet f t))
-> (forall u.
(InSet f u :-> InSet f s)
-> (InSet f u :-> InSet f t) -> InSet f u :-> InSet f r)
-> IntersectionProof f s t r
IntersectionProof Refined (InSet 'Regular Any) x
-> Refined (InSet 'Regular s && InSet 'Regular t) x
InSet 'Regular Any :-> (InSet 'Regular s && InSet 'Regular t)
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Regular u :-> InSet 'Regular s)
-> (InSet 'Regular u :-> InSet 'Regular t)
-> Refined (InSet 'Regular u) x
-> Refined (InSet 'Regular Any) x
(InSet 'Regular u :-> InSet 'Regular s)
-> (InSet 'Regular u :-> InSet 'Regular t)
-> InSet 'Regular u :-> InSet 'Regular Any
forall u.
(InSet 'Regular u :-> InSet 'Regular s)
-> (InSet 'Regular u :-> InSet 'Regular t)
-> InSet 'Regular u :-> InSet 'Regular Any
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2
mapAccumLWithKey
:: forall s k a b c. (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c)
mapAccumLWithKey :: forall s k a b c.
(a -> Key s k -> b -> (a, c)) -> a -> Map s k b -> (a, Map s k c)
mapAccumLWithKey = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
(a -> Key s k -> b -> (a, c)) -> a -> Map s k b -> (a, Map s k c))
-> (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c)
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s k. Coercion k (Key s k)
unsafeCastKey @s @k) ((Coercible k (Key s k) =>
(a -> Key s k -> b -> (a, c)) -> a -> Map s k b -> (a, Map s k c))
-> (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c))
-> (Coercible k (Key s k) =>
(a -> Key s k -> b -> (a, c)) -> a -> Map s k b -> (a, Map s k c))
-> (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c)
forall a b. (a -> b) -> a -> b
$ ((a -> k -> b -> (a, c)) -> a -> Map k b -> (a, Map k c))
-> (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c)
forall a b. Coercible a b => a -> b
coerce
(((a -> k -> b -> (a, c)) -> a -> Map k b -> (a, Map k c))
-> (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c))
-> ((a -> k -> b -> (a, c)) -> a -> Map k b -> (a, Map k c))
-> (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c)
forall a b. (a -> b) -> a -> b
$ forall a k b c.
(a -> k -> b -> (a, c)) -> a -> Map k b -> (a, Map k c)
Map.mapAccumWithKey @a @k @b @c
mapAccumRWithKey
:: forall s k a b c. (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c)
mapAccumRWithKey :: forall s k a b c.
(a -> Key s k -> b -> (a, c)) -> a -> Map s k b -> (a, Map s k c)
mapAccumRWithKey = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
(a -> Key s k -> b -> (a, c)) -> a -> Map s k b -> (a, Map s k c))
-> (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c)
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s k. Coercion k (Key s k)
unsafeCastKey @s @k) ((Coercible k (Key s k) =>
(a -> Key s k -> b -> (a, c)) -> a -> Map s k b -> (a, Map s k c))
-> (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c))
-> (Coercible k (Key s k) =>
(a -> Key s k -> b -> (a, c)) -> a -> Map s k b -> (a, Map s k c))
-> (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c)
forall a b. (a -> b) -> a -> b
$ ((a -> k -> b -> (a, c)) -> a -> Map k b -> (a, Map k c))
-> (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c)
forall a b. Coercible a b => a -> b
coerce
(((a -> k -> b -> (a, c)) -> a -> Map k b -> (a, Map k c))
-> (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c))
-> ((a -> k -> b -> (a, c)) -> a -> Map k b -> (a, Map k c))
-> (a -> Key s k -> b -> (a, c))
-> a
-> Map s k b
-> (a, Map s k c)
forall a b. (a -> b) -> a -> b
$ forall a k b c.
(a -> k -> b -> (a, c)) -> a -> Map k b -> (a, Map k c)
Map.mapAccumRWithKey @a @k @b @c
mapKeysWith
:: forall s k1 k2 a. Ord k2
=> (a -> a -> a)
-> (Key s k1 -> k2)
-> Map s k1 a
-> SomeMapWith (MapProof 'Regular s k1 k2) k2 a
mapKeysWith :: forall s k1 k2 a.
Ord k2 =>
(a -> a -> a)
-> (Key s k1 -> k2)
-> Map s k1 a
-> SomeMapWith (MapProof 'Regular s k1 k2) k2 a
mapKeysWith a -> a -> a
f Key s k1 -> k2
g (Map Map k1 a
m)
= Map Any k2 a
-> MapProof 'Regular s k1 k2 Any
-> SomeMapWith (MapProof 'Regular s k1 k2) k2 a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k2 a -> Map Any k2 a
forall s k a. Map k a -> Map s k a
Map (Map k2 a -> Map Any k2 a) -> Map k2 a -> Map Any k2 a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> (k1 -> k2) -> Map k1 a -> Map k2 a
forall k2 a k1.
Ord k2 =>
(a -> a -> a) -> (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysWith a -> a -> a
f (Key s k1 -> k2
g (Key s k1 -> k2) -> (k1 -> Key s k1) -> k1 -> k2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k1 -> Key s k1
forall k s. k -> Key s k
unsafeKey) Map k1 a
m)
(MapProof 'Regular s k1 k2 Any
-> SomeMapWith (MapProof 'Regular s k1 k2) k2 a)
-> MapProof 'Regular s k1 k2 Any
-> SomeMapWith (MapProof 'Regular s k1 k2) k2 a
forall a b. (a -> b) -> a -> b
$ (Key s k1 -> Refined (InSet 'Regular Any) k2)
-> (Refined (InSet 'Regular Any) k2 -> Key s k1)
-> MapProof 'Regular s k1 k2 Any
forall (f :: Flavor) s a b r.
(Refined (InSet f s) a -> Refined (InSet f r) b)
-> (Refined (InSet f r) b -> Refined (InSet f s) a)
-> MapProof f s a b r
MapProof (k2 -> Refined (InSet 'Regular Any) k2
forall k s. k -> Key s k
unsafeKey (k2 -> Refined (InSet 'Regular Any) k2)
-> (Key s k1 -> k2) -> Key s k1 -> Refined (InSet 'Regular Any) k2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Key s k1 -> k2
g) \Refined (InSet 'Regular Any) k2
k2 -> case k2 -> Map k2 (Key s k1) -> Maybe (Key s k1)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Refined (InSet 'Regular Any) k2 -> k2
forall {k} (p :: k) x. Refined p x -> x
unrefine Refined (InSet 'Regular Any) k2
k2) Map k2 (Key s k1)
backMap of
Maybe (Key s k1)
Nothing -> [Char] -> Key s k1
forall a. HasCallStack => [Char] -> a
error [Char]
"mapKeysWith: bug: Data.Map.Refined has been subverted"
Just Key s k1
k1 -> Key s k1
k1
where
~Map k2 (Key s k1)
backMap = [(k2, Key s k1)] -> Map k2 (Key s k1)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[ (k2
k2, k1 -> Key s k1
forall k s. k -> Key s k
unsafeKey k1
k1)
| k1
k1 <- Map k1 a -> [k1]
forall k a. Map k a -> [k]
Map.keys Map k1 a
m
, let !k2 :: k2
k2 = Key s k1 -> k2
g (Key s k1 -> k2) -> Key s k1 -> k2
forall a b. (a -> b) -> a -> b
$ k1 -> Key s k1
forall k s. k -> Key s k
unsafeKey k1
k1
]
mapMaybeWithKey
:: forall s k a b. (Key s k -> a -> Maybe b)
-> Map s k a
-> SomeMapWith (SupersetProof 'Regular s) k b
mapMaybeWithKey :: forall s k a b.
(Key s k -> a -> Maybe b)
-> Map s k a -> SomeMapWith (SupersetProof 'Regular s) k b
mapMaybeWithKey Key s k -> a -> Maybe b
f (Map Map k a
m)
= Map Any k b
-> SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k b
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k b -> Map Any k b
forall s k a. Map k a -> Map s k a
Map (Map k b -> Map Any k b) -> Map k b -> Map Any k b
forall a b. (a -> b) -> a -> b
$ (k -> a -> Maybe b) -> Map k a -> Map k b
forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybeWithKey (Key s k -> a -> Maybe b
f (Key s k -> a -> Maybe b) -> (k -> Key s k) -> k -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) Map k a
m)
(SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k b)
-> SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k b
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular Any :-> InSet 'Regular s)
-> SupersetProof 'Regular s Any
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Regular Any) x -> Refined (InSet 'Regular s) x
InSet 'Regular Any :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset
mapEitherWithKey
:: forall s k a b c. Ord k
=> (Key s k -> a -> Either b c)
-> Map s k a
-> Some2MapWith (PartitionProof 'Regular s k) k b c
mapEitherWithKey :: forall s k a b c.
Ord k =>
(Key s k -> a -> Either b c)
-> Map s k a -> Some2MapWith (PartitionProof 'Regular s k) k b c
mapEitherWithKey Key s k -> a -> Either b c
p (Map Map k a
m) = case (k -> a -> Either b c) -> Map k a -> (Map k b, Map k c)
forall k a b c.
(k -> a -> Either b c) -> Map k a -> (Map k b, Map k c)
Map.mapEitherWithKey (Key s k -> a -> Either b c
p (Key s k -> a -> Either b c)
-> (k -> Key s k) -> k -> a -> Either b c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) Map k a
m of
(Map k b
m1, Map k c
m2) -> Map Any k b
-> Map Any k c
-> PartitionProof 'Regular s k Any Any
-> Some2MapWith (PartitionProof 'Regular s k) k b c
forall s t k a b (p :: * -> * -> *).
Map s k a -> Map t k b -> p s t -> Some2MapWith p k a b
Some2MapWith (Map k b -> Map Any k b
forall s k a. Map k a -> Map s k a
Map Map k b
m1) (Map k c -> Map Any k c
forall s k a. Map k a -> Map s k a
Map Map k c
m2) (PartitionProof 'Regular s k Any Any
-> Some2MapWith (PartitionProof 'Regular s k) k b c)
-> PartitionProof 'Regular s k Any Any
-> Some2MapWith (PartitionProof 'Regular s k) k b c
forall a b. (a -> b) -> a -> b
$ (Key s k
-> Either
(Refined (InSet 'Regular Any) k) (Refined (InSet 'Regular Any) k))
-> ((InSet 'Regular Any || InSet 'Regular Any)
:-> InSet 'Regular s)
-> (forall t.
(InSet 'Regular Any :-> InSet 'Regular t)
-> (InSet 'Regular Any :-> InSet 'Regular t)
-> InSet 'Regular s :-> InSet 'Regular t)
-> (forall t.
(InSet 'Regular t :-> InSet 'Regular Any)
-> (InSet 'Regular t :-> InSet 'Regular Any)
-> forall u x.
Refined (InSet 'Regular t) x -> Refined (InSet 'Regular u) x)
-> PartitionProof 'Regular s k Any Any
forall (f :: Flavor) s a r q.
(Refined (InSet f s) a
-> Either (Refined (InSet f r) a) (Refined (InSet f q) a))
-> ((InSet f r || InSet f q) :-> InSet f s)
-> (forall t.
(InSet f r :-> InSet f t)
-> (InSet f q :-> InSet f t) -> InSet f s :-> InSet f t)
-> (forall t.
(InSet f t :-> InSet f r)
-> (InSet f t :-> InSet f q)
-> forall u x. Refined (InSet f t) x -> Refined (InSet f u) x)
-> PartitionProof f s a r q
PartitionProof
do \Key s k
k -> case k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Key s k -> k
forall {k} (p :: k) x. Refined p x -> x
unrefine Key s k
k) Map k a
m of
Maybe a
Nothing
-> [Char]
-> Either
(Refined (InSet 'Regular Any) k) (Refined (InSet 'Regular Any) k)
forall a. HasCallStack => [Char] -> a
error [Char]
"mapEitherWithKey: bug: Data.Map.Refined has been subverted"
Just a
x -> case Key s k -> a -> Either b c
p Key s k
k a
x of
Left b
_ -> Refined (InSet 'Regular Any) k
-> Either
(Refined (InSet 'Regular Any) k) (Refined (InSet 'Regular Any) k)
forall a b. a -> Either a b
Left (Refined (InSet 'Regular Any) k
-> Either
(Refined (InSet 'Regular Any) k) (Refined (InSet 'Regular Any) k))
-> Refined (InSet 'Regular Any) k
-> Either
(Refined (InSet 'Regular Any) k) (Refined (InSet 'Regular Any) k)
forall a b. (a -> b) -> a -> b
$ k -> Refined (InSet 'Regular Any) k
forall k s. k -> Key s k
unsafeKey (k -> Refined (InSet 'Regular Any) k)
-> k -> Refined (InSet 'Regular Any) k
forall a b. (a -> b) -> a -> b
$ Key s k -> k
forall {k} (p :: k) x. Refined p x -> x
unrefine Key s k
k
Right c
_ -> Refined (InSet 'Regular Any) k
-> Either
(Refined (InSet 'Regular Any) k) (Refined (InSet 'Regular Any) k)
forall a b. b -> Either a b
Right (Refined (InSet 'Regular Any) k
-> Either
(Refined (InSet 'Regular Any) k) (Refined (InSet 'Regular Any) k))
-> Refined (InSet 'Regular Any) k
-> Either
(Refined (InSet 'Regular Any) k) (Refined (InSet 'Regular Any) k)
forall a b. (a -> b) -> a -> b
$ k -> Refined (InSet 'Regular Any) k
forall k s. k -> Key s k
unsafeKey (k -> Refined (InSet 'Regular Any) k)
-> k -> Refined (InSet 'Regular Any) k
forall a b. (a -> b) -> a -> b
$ Key s k -> k
forall {k} (p :: k) x. Refined p x -> x
unrefine Key s k
k
Refined (InSet 'Regular Any || InSet 'Regular Any) x
-> Refined (InSet 'Regular s) x
(InSet 'Regular Any || InSet 'Regular Any) :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Regular Any :-> InSet 'Regular t)
-> (InSet 'Regular Any :-> InSet 'Regular t)
-> Refined (InSet 'Regular s) x
-> Refined (InSet 'Regular t) x
(InSet 'Regular Any :-> InSet 'Regular t)
-> (InSet 'Regular Any :-> InSet 'Regular t)
-> InSet 'Regular s :-> InSet 'Regular t
forall t.
(InSet 'Regular Any :-> InSet 'Regular t)
-> (InSet 'Regular Any :-> InSet 'Regular t)
-> InSet 'Regular s :-> InSet 'Regular t
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 \InSet 'Regular t :-> InSet 'Regular Any
f InSet 'Regular t :-> InSet 'Regular Any
g -> (InSet 'Regular t :-> InSet 'Regular Any)
-> (InSet 'Regular t :-> InSet 'Regular Any)
-> InSet 'Regular t :-> InSet 'Regular u
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Regular t) x -> Refined (InSet 'Regular Any) x
InSet 'Regular t :-> InSet 'Regular Any
f Refined (InSet 'Regular t) x -> Refined (InSet 'Regular Any) x
InSet 'Regular t :-> InSet 'Regular Any
g
updateMinWithKey
:: forall s k a. (Key s k -> a -> Maybe a)
-> Map s k a
-> SomeMapWith (SupersetProof 'Regular s) k a
updateMinWithKey :: forall s k a.
(Key s k -> a -> Maybe a)
-> Map s k a -> SomeMapWith (SupersetProof 'Regular s) k a
updateMinWithKey Key s k -> a -> Maybe a
f (Map Map k a
m)
= Map Any k a
-> SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map (Map k a -> Map Any k a) -> Map k a -> Map Any k a
forall a b. (a -> b) -> a -> b
$ (k -> a -> Maybe a) -> Map k a -> Map k a
forall k a. (k -> a -> Maybe a) -> Map k a -> Map k a
Map.updateMinWithKey (Key s k -> a -> Maybe a
f (Key s k -> a -> Maybe a) -> (k -> Key s k) -> k -> a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) Map k a
m)
(SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k a)
-> SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular Any :-> InSet 'Regular s)
-> SupersetProof 'Regular s Any
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Regular Any) x -> Refined (InSet 'Regular s) x
InSet 'Regular Any :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset
updateMaxWithKey
:: forall s k a. (Key s k -> a -> Maybe a)
-> Map s k a
-> SomeMapWith (SupersetProof 'Regular s) k a
updateMaxWithKey :: forall s k a.
(Key s k -> a -> Maybe a)
-> Map s k a -> SomeMapWith (SupersetProof 'Regular s) k a
updateMaxWithKey Key s k -> a -> Maybe a
f (Map Map k a
m)
= Map Any k a
-> SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map (Map k a -> Map Any k a) -> Map k a -> Map Any k a
forall a b. (a -> b) -> a -> b
$ (k -> a -> Maybe a) -> Map k a -> Map k a
forall k a. (k -> a -> Maybe a) -> Map k a -> Map k a
Map.updateMaxWithKey (Key s k -> a -> Maybe a
f (Key s k -> a -> Maybe a) -> (k -> Key s k) -> k -> a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) Map k a
m)
(SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k a)
-> SupersetProof 'Regular s Any
-> SomeMapWith (SupersetProof 'Regular s) k a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular Any :-> InSet 'Regular s)
-> SupersetProof 'Regular s Any
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Regular Any) x -> Refined (InSet 'Regular s) x
InSet 'Regular Any :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset
adjustMinWithKey :: forall s k a. (Key s k -> a -> a) -> Map s k a -> Map s k a
adjustMinWithKey :: forall s k a. (Key s k -> a -> a) -> Map s k a -> Map s k a
adjustMinWithKey Key s k -> a -> a
f (Map Map k a
m)
= Map k a -> Map s k a
forall s k a. Map k a -> Map s k a
Map (Map k a -> Map s k a) -> Map k a -> Map s k a
forall a b. (a -> b) -> a -> b
$ (k -> a -> Maybe a) -> Map k a -> Map k a
forall k a. (k -> a -> Maybe a) -> Map k a -> Map k a
Map.updateMinWithKey ((a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> (a -> a) -> a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((a -> a) -> a -> Maybe a) -> (k -> a -> a) -> k -> a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Key s k -> a -> a
f (Key s k -> a -> a) -> (k -> Key s k) -> k -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) Map k a
m
adjustMaxWithKey :: forall s k a. (Key s k -> a -> a) -> Map s k a -> Map s k a
adjustMaxWithKey :: forall s k a. (Key s k -> a -> a) -> Map s k a -> Map s k a
adjustMaxWithKey Key s k -> a -> a
f (Map Map k a
m)
= Map k a -> Map s k a
forall s k a. Map k a -> Map s k a
Map (Map k a -> Map s k a) -> Map k a -> Map s k a
forall a b. (a -> b) -> a -> b
$ (k -> a -> Maybe a) -> Map k a -> Map k a
forall k a. (k -> a -> Maybe a) -> Map k a -> Map k a
Map.updateMaxWithKey ((a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> (a -> a) -> a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((a -> a) -> a -> Maybe a) -> (k -> a -> a) -> k -> a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Key s k -> a -> a
f (Key s k -> a -> a) -> (k -> Key s k) -> k -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) Map k a
m
backpermuteKeys
:: forall s1 s2 k1 k2 a. (Ord k1, KnownSet s2 k2)
=> (Key s2 k2 -> Key s1 k1) -> Map s1 k1 a -> Map s2 k2 a
backpermuteKeys :: forall s1 s2 k1 k2 a.
(Ord k1, KnownSet s2 k2) =>
(Key s2 k2 -> Key s1 k1) -> Map s1 k1 a -> Map s2 k2 a
backpermuteKeys Key s2 k2 -> Key s1 k1
f Map s1 k1 a
m = (Key s2 k2 -> a) -> Map s2 k2 a
forall s k a. KnownSet s k => (Key s k -> a) -> Map s k a
fromSet \Key s2 k2
k -> Map s1 k1 a
m Map s1 k1 a -> Key s1 k1 -> a
forall s k a. Ord k => Map s k a -> Key s k -> a
! Key s2 k2 -> Key s1 k1
f Key s2 k2
k