{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Map.Common.Refined where
import Control.Monad.Reader
import Control.DeepSeq
import Data.Coerce
import Data.Constraint (Dict(..))
import Data.Container.Refined.Proofs
import Data.Container.Refined.Unsafe
import Data.Distributive
import Data.Foldable.WithIndex
import Data.Functor.Rep
import Data.Functor.WithIndex
import qualified Data.Hashable as Hashable
import qualified Data.Map as Map
import Data.Proxy
import Data.Reflection
import Data.Traversable.WithIndex
import Data.Type.Coercion
import Data.Type.Equality ((:~:)(..))
import Refined
import Refined.Unsafe
import Unsafe.Coerce
#if MIN_VERSION_containers(0, 6, 2)
#elif MIN_VERSION_containers(0, 5, 8)
import Data.Functor.Const (Const(..))
import Data.Monoid (Any(..))
import qualified Data.Map.Merge.Lazy as Map
#else
import qualified Data.List as List
import qualified Data.Map.Strict as MapStrict
#endif
newtype Map s k a = Map (Map.Map k a)
deriving newtype (Map s k a -> Map s k a -> Bool
(Map s k a -> Map s k a -> Bool)
-> (Map s k a -> Map s k a -> Bool) -> Eq (Map s k a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s k a. (Eq k, Eq a) => Map s k a -> Map s k a -> Bool
$c== :: forall s k a. (Eq k, Eq a) => Map s k a -> Map s k a -> Bool
== :: Map s k a -> Map s k a -> Bool
$c/= :: forall s k a. (Eq k, Eq a) => Map s k a -> Map s k a -> Bool
/= :: Map s k a -> Map s k a -> Bool
Eq, Eq (Map s k a)
Eq (Map s k a) =>
(Map s k a -> Map s k a -> Ordering)
-> (Map s k a -> Map s k a -> Bool)
-> (Map s k a -> Map s k a -> Bool)
-> (Map s k a -> Map s k a -> Bool)
-> (Map s k a -> Map s k a -> Bool)
-> (Map s k a -> Map s k a -> Map s k a)
-> (Map s k a -> Map s k a -> Map s k a)
-> Ord (Map s k a)
Map s k a -> Map s k a -> Bool
Map s k a -> Map s k a -> Ordering
Map s k a -> Map s k a -> Map s k a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s k a. (Ord k, Ord a) => Eq (Map s k a)
forall s k a. (Ord k, Ord a) => Map s k a -> Map s k a -> Bool
forall s k a. (Ord k, Ord a) => Map s k a -> Map s k a -> Ordering
forall s k a. (Ord k, Ord a) => Map s k a -> Map s k a -> Map s k a
$ccompare :: forall s k a. (Ord k, Ord a) => Map s k a -> Map s k a -> Ordering
compare :: Map s k a -> Map s k a -> Ordering
$c< :: forall s k a. (Ord k, Ord a) => Map s k a -> Map s k a -> Bool
< :: Map s k a -> Map s k a -> Bool
$c<= :: forall s k a. (Ord k, Ord a) => Map s k a -> Map s k a -> Bool
<= :: Map s k a -> Map s k a -> Bool
$c> :: forall s k a. (Ord k, Ord a) => Map s k a -> Map s k a -> Bool
> :: Map s k a -> Map s k a -> Bool
$c>= :: forall s k a. (Ord k, Ord a) => Map s k a -> Map s k a -> Bool
>= :: Map s k a -> Map s k a -> Bool
$cmax :: forall s k a. (Ord k, Ord a) => Map s k a -> Map s k a -> Map s k a
max :: Map s k a -> Map s k a -> Map s k a
$cmin :: forall s k a. (Ord k, Ord a) => Map s k a -> Map s k a -> Map s k a
min :: Map s k a -> Map s k a -> Map s k a
Ord, Int -> Map s k a -> ShowS
[Map s k a] -> ShowS
Map s k a -> String
(Int -> Map s k a -> ShowS)
-> (Map s k a -> String)
-> ([Map s k a] -> ShowS)
-> Show (Map s k a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s k a. (Show k, Show a) => Int -> Map s k a -> ShowS
forall s k a. (Show k, Show a) => [Map s k a] -> ShowS
forall s k a. (Show k, Show a) => Map s k a -> String
$cshowsPrec :: forall s k a. (Show k, Show a) => Int -> Map s k a -> ShowS
showsPrec :: Int -> Map s k a -> ShowS
$cshow :: forall s k a. (Show k, Show a) => Map s k a -> String
show :: Map s k a -> String
$cshowList :: forall s k a. (Show k, Show a) => [Map s k a] -> ShowS
showList :: [Map s k a] -> ShowS
Show, (forall a b. (a -> b) -> Map s k a -> Map s k b)
-> (forall a b. a -> Map s k b -> Map s k a) -> Functor (Map s k)
forall a b. a -> Map s k b -> Map s k a
forall a b. (a -> b) -> Map s k a -> Map s k b
forall s k a b. a -> Map s k b -> Map s k a
forall s k a b. (a -> b) -> Map s k a -> Map s k b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall s k a b. (a -> b) -> Map s k a -> Map s k b
fmap :: forall a b. (a -> b) -> Map s k a -> Map s k b
$c<$ :: forall s k a b. a -> Map s k b -> Map s k a
<$ :: forall a b. a -> Map s k b -> Map s k a
Functor, (forall m. Monoid m => Map s k m -> m)
-> (forall m a. Monoid m => (a -> m) -> Map s k a -> m)
-> (forall m a. Monoid m => (a -> m) -> Map s k a -> m)
-> (forall a b. (a -> b -> b) -> b -> Map s k a -> b)
-> (forall a b. (a -> b -> b) -> b -> Map s k a -> b)
-> (forall b a. (b -> a -> b) -> b -> Map s k a -> b)
-> (forall b a. (b -> a -> b) -> b -> Map s k a -> b)
-> (forall a. (a -> a -> a) -> Map s k a -> a)
-> (forall a. (a -> a -> a) -> Map s k a -> a)
-> (forall a. Map s k a -> [a])
-> (forall a. Map s k a -> Bool)
-> (forall a. Map s k a -> Int)
-> (forall a. Eq a => a -> Map s k a -> Bool)
-> (forall a. Ord a => Map s k a -> a)
-> (forall a. Ord a => Map s k a -> a)
-> (forall a. Num a => Map s k a -> a)
-> (forall a. Num a => Map s k a -> a)
-> Foldable (Map s k)
forall a. Eq a => a -> Map s k a -> Bool
forall a. Num a => Map s k a -> a
forall a. Ord a => Map s k a -> a
forall m. Monoid m => Map s k m -> m
forall a. Map s k a -> Bool
forall a. Map s k a -> Int
forall a. Map s k a -> [a]
forall a. (a -> a -> a) -> Map s k a -> a
forall m a. Monoid m => (a -> m) -> Map s k a -> m
forall b a. (b -> a -> b) -> b -> Map s k a -> b
forall a b. (a -> b -> b) -> b -> Map s k a -> b
forall s k a. Eq a => a -> Map s k a -> Bool
forall s k a. Num a => Map s k a -> a
forall s k a. Ord a => Map s k a -> a
forall s k m. Monoid m => Map s k m -> m
forall s k a. Map s k a -> Bool
forall s k a. Map s k a -> Int
forall s k a. Map s k a -> [a]
forall s k a. (a -> a -> a) -> Map s k a -> a
forall s k m a. Monoid m => (a -> m) -> Map s k a -> m
forall s k b a. (b -> a -> b) -> b -> Map s k a -> b
forall s k a b. (a -> b -> b) -> b -> Map s k a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall s k m. Monoid m => Map s k m -> m
fold :: forall m. Monoid m => Map s k m -> m
$cfoldMap :: forall s k m a. Monoid m => (a -> m) -> Map s k a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Map s k a -> m
$cfoldMap' :: forall s k m a. Monoid m => (a -> m) -> Map s k a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Map s k a -> m
$cfoldr :: forall s k a b. (a -> b -> b) -> b -> Map s k a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Map s k a -> b
$cfoldr' :: forall s k a b. (a -> b -> b) -> b -> Map s k a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Map s k a -> b
$cfoldl :: forall s k b a. (b -> a -> b) -> b -> Map s k a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Map s k a -> b
$cfoldl' :: forall s k b a. (b -> a -> b) -> b -> Map s k a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Map s k a -> b
$cfoldr1 :: forall s k a. (a -> a -> a) -> Map s k a -> a
foldr1 :: forall a. (a -> a -> a) -> Map s k a -> a
$cfoldl1 :: forall s k a. (a -> a -> a) -> Map s k a -> a
foldl1 :: forall a. (a -> a -> a) -> Map s k a -> a
$ctoList :: forall s k a. Map s k a -> [a]
toList :: forall a. Map s k a -> [a]
$cnull :: forall s k a. Map s k a -> Bool
null :: forall a. Map s k a -> Bool
$clength :: forall s k a. Map s k a -> Int
length :: forall a. Map s k a -> Int
$celem :: forall s k a. Eq a => a -> Map s k a -> Bool
elem :: forall a. Eq a => a -> Map s k a -> Bool
$cmaximum :: forall s k a. Ord a => Map s k a -> a
maximum :: forall a. Ord a => Map s k a -> a
$cminimum :: forall s k a. Ord a => Map s k a -> a
minimum :: forall a. Ord a => Map s k a -> a
$csum :: forall s k a. Num a => Map s k a -> a
sum :: forall a. Num a => Map s k a -> a
$cproduct :: forall s k a. Num a => Map s k a -> a
product :: forall a. Num a => Map s k a -> a
Foldable, Map s k a -> ()
(Map s k a -> ()) -> NFData (Map s k a)
forall a. (a -> ()) -> NFData a
forall s k a. (NFData k, NFData a) => Map s k a -> ()
$crnf :: forall s k a. (NFData k, NFData a) => Map s k a -> ()
rnf :: Map s k a -> ()
NFData)
#if MIN_VERSION_hashable(1, 3, 4)
deriving newtype (Eq (Map s k a)
Eq (Map s k a) =>
(Int -> Map s k a -> Int)
-> (Map s k a -> Int) -> Hashable (Map s k a)
Int -> Map s k a -> Int
Map s k a -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall s k a. (Hashable k, Hashable a) => Eq (Map s k a)
forall s k a. (Hashable k, Hashable a) => Int -> Map s k a -> Int
forall s k a. (Hashable k, Hashable a) => Map s k a -> Int
$chashWithSalt :: forall s k a. (Hashable k, Hashable a) => Int -> Map s k a -> Int
hashWithSalt :: Int -> Map s k a -> Int
$chash :: forall s k a. (Hashable k, Hashable a) => Map s k a -> Int
hash :: Map s k a -> Int
Hashable.Hashable)
#endif
deriving stock (Functor (Map s k)
Foldable (Map s k)
(Functor (Map s k), Foldable (Map s k)) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map s k a -> f (Map s k b))
-> (forall (f :: * -> *) a.
Applicative f =>
Map s k (f a) -> f (Map s k a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map s k a -> m (Map s k b))
-> (forall (m :: * -> *) a.
Monad m =>
Map s k (m a) -> m (Map s k a))
-> Traversable (Map s k)
forall s k. Functor (Map s k)
forall s k. Foldable (Map s k)
forall s k (m :: * -> *) a.
Monad m =>
Map s k (m a) -> m (Map s k a)
forall s k (f :: * -> *) a.
Applicative f =>
Map s k (f a) -> f (Map s k a)
forall s k (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map s k a -> m (Map s k b)
forall s k (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map s k a -> f (Map s k b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Map s k (m a) -> m (Map s k a)
forall (f :: * -> *) a.
Applicative f =>
Map s k (f a) -> f (Map s k a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map s k a -> m (Map s k b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map s k a -> f (Map s k b)
$ctraverse :: forall s k (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map s k a -> f (Map s k b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map s k a -> f (Map s k b)
$csequenceA :: forall s k (f :: * -> *) a.
Applicative f =>
Map s k (f a) -> f (Map s k a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Map s k (f a) -> f (Map s k a)
$cmapM :: forall s k (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map s k a -> m (Map s k b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map s k a -> m (Map s k b)
$csequence :: forall s k (m :: * -> *) a.
Monad m =>
Map s k (m a) -> m (Map s k a)
sequence :: forall (m :: * -> *) a. Monad m => Map s k (m a) -> m (Map s k a)
Traversable)
type role Map nominal nominal representational
toMap :: forall s k a. Map s k a -> Map.Map k a
toMap :: forall s k a. Map s k a -> Map k a
toMap (Map Map k a
m) = Map k a
m
type Key s = Refined (InSet 'Regular s)
unsafeCastKey :: forall s k. Coercion k (Key s k)
unsafeCastKey :: forall s k. Coercion k (Key s k)
unsafeCastKey = Coercion k (Refined (InSet 'Regular s) k)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined
unsafeKey :: k -> Key s k
unsafeKey :: forall k s. k -> Key s k
unsafeKey = Coercion k (Key s k) -> k -> Key s k
forall a b. Coercion a b -> a -> b
coerceWith Coercion k (Key s k)
forall s k. Coercion k (Key s k)
unsafeCastKey
data SomeMap k a where
SomeMap :: forall s k a. !(Map s k a) -> SomeMap k a
withMap :: forall k a r. SomeMap k a -> (forall s. Map s k a -> r) -> r
withMap :: forall k a r. SomeMap k a -> (forall s. Map s k a -> r) -> r
withMap (SomeMap Map s k a
m) forall s. Map s k a -> r
k = Map s k a -> r
forall s. Map s k a -> r
k Map s k a
m
fromMap :: forall k a. Map.Map k a -> SomeMap k a
fromMap :: forall k a. Map k a -> SomeMap k a
fromMap Map k a
m = Map Any k a -> SomeMap k a
forall s k a. Map s k a -> SomeMap k a
SomeMap (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map Map k a
m)
data SomeMapWith p k a where
SomeMapWith :: forall s k a p. !(Map s k a) -> !(p s) -> SomeMapWith p k a
withMapWith
:: forall k a r p. SomeMapWith p k a -> (forall s. Map s k a -> p s -> r) -> r
withMapWith :: forall k a r (p :: * -> *).
SomeMapWith p k a -> (forall s. Map s k a -> p s -> r) -> r
withMapWith (SomeMapWith Map s k a
m p s
p) forall s. Map s k a -> p s -> r
k = Map s k a -> p s -> r
forall s. Map s k a -> p s -> r
k Map s k a
m p s
p
data Some2MapWith p k a b where
Some2MapWith
:: forall s t k a b p. !(Map s k a)
-> !(Map t k b)
-> !(p s t)
-> Some2MapWith p k a b
with2MapWith
:: forall k a b r p. Some2MapWith p k a b
-> (forall s t. Map s k a -> Map t k b -> p s t -> r)
-> r
with2MapWith :: forall k a b r (p :: * -> * -> *).
Some2MapWith p k a b
-> (forall s t. Map s k a -> Map t k b -> p s t -> r) -> r
with2MapWith (Some2MapWith Map s k a
m1 Map t k b
m2 p s t
p) forall s t. Map s k a -> Map t k b -> p s t -> r
k = Map s k a -> Map t k b -> p s t -> r
forall s t. Map s k a -> Map t k b -> p s t -> r
k Map s k a
m1 Map t k b
m2 p s t
p
empty :: forall k a. SomeMapWith (EmptyProof 'Regular) k a
empty :: forall k a. SomeMapWith (EmptyProof 'Regular) k a
empty = Map Any k a
-> EmptyProof 'Regular Any -> SomeMapWith (EmptyProof 'Regular) 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
forall k a. Map k a
Map.empty) (EmptyProof 'Regular Any -> SomeMapWith (EmptyProof 'Regular) k a)
-> EmptyProof 'Regular Any -> SomeMapWith (EmptyProof 'Regular) k a
forall a b. (a -> b) -> a -> b
$ (forall s. InSet 'Regular Any :-> InSet 'Regular s)
-> EmptyProof 'Regular Any
forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof Refined (InSet 'Regular Any) x -> Refined (InSet 'Regular s) x
forall s. InSet 'Regular Any :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset
fromSet :: forall s k a. KnownSet s k => (Key s k -> a) -> Map s k a
fromSet :: forall s k a. KnownSet s k => (Key s k -> a) -> Map s k a
fromSet Key s k -> a
f = 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) -> Set k -> Map k a
forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (Key s k -> a
f (Key s k -> a) -> (k -> Key s k) -> k -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Key s k
forall k s. k -> Key s k
unsafeKey) (Proxy s -> Set k
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set k
reflect (Proxy s -> Set k) -> Proxy s -> Set k
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s)
delete
:: forall s k a. Ord k
=> k -> Map s k a -> SomeMapWith (SupersetProof 'Regular s) k a
delete :: forall s k a.
Ord k =>
k -> Map s k a -> SomeMapWith (SupersetProof 'Regular s) k a
delete 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
$ k -> Map k a -> Map k a
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete 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
lookup :: forall s k a. Ord k => k -> Map s k a -> Maybe (Key s k, a)
lookup :: forall s k a. Ord k => k -> Map s k a -> Maybe (Key s k, a)
lookup k
k (Map 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
<$> k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k Map k a
m
(!) :: forall s k a. Ord k => Map s k a -> Key s k -> a
! :: forall s k a. Ord k => Map s k a -> Key s k -> a
(!) (Map Map k a
m) 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 -> String -> a
forall a. HasCallStack => String -> a
error String
"(!): bug: Data.Map.Refined has been subverted"
Just a
x -> a
x
member :: forall s k a. Ord k => k -> Map s k a -> Maybe (Key s k)
member :: forall s k a. Ord k => k -> Map s k a -> Maybe (Key s k)
member k
k (Map Map k a
m)
| k
k k -> Map k a -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map k a
m = Key s k -> Maybe (Key s k)
forall a. a -> Maybe a
Just (k -> Key s k
forall k s. k -> Key s k
unsafeKey k
k)
| Bool
otherwise = Maybe (Key s k)
forall a. Maybe a
Nothing
lookupLT :: forall s k a. Ord k => k -> Map s k a -> Maybe (Key s k, a)
lookupLT :: forall s k a. Ord k => k -> Map s k a -> Maybe (Key s k, a)
lookupLT = Coercion k (Key s k)
-> (Coercible k (Key s k) => k -> Map s k a -> Maybe (Key s k, a))
-> k
-> Map s k a
-> Maybe (Key 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) => k -> Map s k a -> Maybe (Key s k, a))
-> k -> Map s k a -> Maybe (Key s k, a))
-> (Coercible k (Key s k) => k -> Map s k a -> Maybe (Key s k, a))
-> k
-> Map s k a
-> Maybe (Key s k, a)
forall a b. (a -> b) -> a -> b
$ (k -> Map k a -> Maybe (k, a))
-> k -> Map s k a -> Maybe (Key s k, a)
forall a b. Coercible a b => a -> b
coerce ((k -> Map k a -> Maybe (k, a))
-> k -> Map s k a -> Maybe (Key s k, a))
-> (k -> Map k a -> Maybe (k, a))
-> k
-> Map s k a
-> Maybe (Key s k, a)
forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupLT @k @a
lookupGT :: forall s k a. Ord k => k -> Map s k a -> Maybe (Key s k, a)
lookupGT :: forall s k a. Ord k => k -> Map s k a -> Maybe (Key s k, a)
lookupGT = Coercion k (Key s k)
-> (Coercible k (Key s k) => k -> Map s k a -> Maybe (Key s k, a))
-> k
-> Map s k a
-> Maybe (Key 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) => k -> Map s k a -> Maybe (Key s k, a))
-> k -> Map s k a -> Maybe (Key s k, a))
-> (Coercible k (Key s k) => k -> Map s k a -> Maybe (Key s k, a))
-> k
-> Map s k a
-> Maybe (Key s k, a)
forall a b. (a -> b) -> a -> b
$ (k -> Map k a -> Maybe (k, a))
-> k -> Map s k a -> Maybe (Key s k, a)
forall a b. Coercible a b => a -> b
coerce ((k -> Map k a -> Maybe (k, a))
-> k -> Map s k a -> Maybe (Key s k, a))
-> (k -> Map k a -> Maybe (k, a))
-> k
-> Map s k a
-> Maybe (Key s k, a)
forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupGT @k @a
lookupLE :: forall s k a. Ord k => k -> Map s k a -> Maybe (Key s k, a)
lookupLE :: forall s k a. Ord k => k -> Map s k a -> Maybe (Key s k, a)
lookupLE = Coercion k (Key s k)
-> (Coercible k (Key s k) => k -> Map s k a -> Maybe (Key s k, a))
-> k
-> Map s k a
-> Maybe (Key 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) => k -> Map s k a -> Maybe (Key s k, a))
-> k -> Map s k a -> Maybe (Key s k, a))
-> (Coercible k (Key s k) => k -> Map s k a -> Maybe (Key s k, a))
-> k
-> Map s k a
-> Maybe (Key s k, a)
forall a b. (a -> b) -> a -> b
$ (k -> Map k a -> Maybe (k, a))
-> k -> Map s k a -> Maybe (Key s k, a)
forall a b. Coercible a b => a -> b
coerce ((k -> Map k a -> Maybe (k, a))
-> k -> Map s k a -> Maybe (Key s k, a))
-> (k -> Map k a -> Maybe (k, a))
-> k
-> Map s k a
-> Maybe (Key s k, a)
forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupLE @k @a
lookupGE :: forall s k a. Ord k => k -> Map s k a -> Maybe (Key s k, a)
lookupGE :: forall s k a. Ord k => k -> Map s k a -> Maybe (Key s k, a)
lookupGE = Coercion k (Key s k)
-> (Coercible k (Key s k) => k -> Map s k a -> Maybe (Key s k, a))
-> k
-> Map s k a
-> Maybe (Key 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) => k -> Map s k a -> Maybe (Key s k, a))
-> k -> Map s k a -> Maybe (Key s k, a))
-> (Coercible k (Key s k) => k -> Map s k a -> Maybe (Key s k, a))
-> k
-> Map s k a
-> Maybe (Key s k, a)
forall a b. (a -> b) -> a -> b
$ (k -> Map k a -> Maybe (k, a))
-> k -> Map s k a -> Maybe (Key s k, a)
forall a b. Coercible a b => a -> b
coerce ((k -> Map k a -> Maybe (k, a))
-> k -> Map s k a -> Maybe (Key s k, a))
-> (k -> Map k a -> Maybe (k, a))
-> k
-> Map s k a
-> Maybe (Key s k, a)
forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupGE @k @a
null :: forall s k a. Map s k a -> Maybe (EmptyProof 'Regular s)
null :: forall s k a. Map s k a -> Maybe (EmptyProof 'Regular s)
null (Map Map k a
m)
| Map k a -> Bool
forall k a. Map k a -> Bool
Map.null Map k a
m = EmptyProof 'Regular s -> Maybe (EmptyProof 'Regular s)
forall a. a -> Maybe a
Just (EmptyProof 'Regular s -> Maybe (EmptyProof 'Regular s))
-> EmptyProof 'Regular s -> Maybe (EmptyProof 'Regular s)
forall a b. (a -> b) -> a -> b
$ (forall s. InSet 'Regular s :-> InSet 'Regular s)
-> EmptyProof 'Regular s
forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular s) x
forall s. InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset
| Bool
otherwise = Maybe (EmptyProof 'Regular s)
forall a. Maybe a
Nothing
isSubmapOfBy
:: forall s t k a b. Ord k
=> (a -> b -> Bool)
-> Map s k a
-> Map t k b
-> Maybe (SubsetProof 'Regular s t)
isSubmapOfBy :: forall s t k a b.
Ord k =>
(a -> b -> Bool)
-> Map s k a -> Map t k b -> Maybe (SubsetProof 'Regular s t)
isSubmapOfBy a -> b -> Bool
f (Map Map k a
m1) (Map Map k b
m2)
| (a -> b -> Bool) -> Map k a -> Map k b -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy a -> b -> Bool
f Map k a
m1 Map k b
m2 = SubsetProof 'Regular s t -> Maybe (SubsetProof 'Regular s t)
forall a. a -> Maybe a
Just (SubsetProof 'Regular s t -> Maybe (SubsetProof 'Regular s t))
-> SubsetProof 'Regular s t -> Maybe (SubsetProof 'Regular s t)
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular s :-> InSet 'Regular t) -> SubsetProof 'Regular s t
forall (f :: Flavor) s r.
(InSet f s :-> InSet f r) -> SubsetProof f s r
SubsetProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular t) x
InSet 'Regular s :-> InSet 'Regular t
forall p q x. Refined p x -> Refined q x
unsafeSubset
| Bool
otherwise = Maybe (SubsetProof 'Regular s t)
forall a. Maybe a
Nothing
disjoint
:: forall s t k a b. Ord k
=> Map s k a -> Map t k b -> Maybe (DisjointProof 'Regular s t)
disjoint :: forall s t k a b.
Ord k =>
Map s k a -> Map t k b -> Maybe (DisjointProof 'Regular s t)
disjoint (Map Map k a
m1) (Map Map k b
m2)
#if MIN_VERSION_containers(0, 6, 2)
| Map k a -> Map k b -> Bool
forall k a b. Ord k => Map k a -> Map k b -> Bool
Map.disjoint Map k a
m1 Map k b
m2
#elif MIN_VERSION_containers(0, 5, 8)
| Const (Any False) <- Map.mergeA
(Map.traverseMissing \_ _ -> Const mempty)
(Map.traverseMissing \_ _ -> Const mempty)
(Map.zipWithAMatched \_ _ _ -> Const $ Any True)
m1
m2
#else
| Map.null $ MapStrict.intersectionWith (\_ _ -> ()) m1 m2
#endif
= DisjointProof 'Regular s t -> Maybe (DisjointProof 'Regular s t)
forall a. a -> Maybe a
Just (DisjointProof 'Regular s t -> Maybe (DisjointProof 'Regular s t))
-> DisjointProof 'Regular s t -> Maybe (DisjointProof 'Regular s t)
forall a b. (a -> b) -> a -> b
$ (forall t.
(InSet 'Regular t :-> InSet 'Regular s)
-> (InSet 'Regular t :-> InSet 'Regular t)
-> forall u x.
Refined (InSet 'Regular t) x -> Refined (InSet 'Regular u) x)
-> DisjointProof 'Regular s t
forall (f :: Flavor) s r.
(forall t.
(InSet f t :-> InSet f s)
-> (InSet f t :-> InSet f r)
-> forall u x. Refined (InSet f t) x -> Refined (InSet f u) x)
-> DisjointProof f s r
DisjointProof \InSet 'Regular t :-> InSet 'Regular s
f InSet 'Regular t :-> InSet 'Regular t
g -> (InSet 'Regular t :-> InSet 'Regular s)
-> (InSet 'Regular t :-> InSet 'Regular t)
-> 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 s) x
InSet 'Regular t :-> InSet 'Regular s
f Refined (InSet 'Regular t) x -> Refined (InSet 'Regular t) x
InSet 'Regular t :-> InSet 'Regular t
g
| Bool
otherwise = Maybe (DisjointProof 'Regular s t)
forall a. Maybe a
Nothing
zipWithKey
:: forall s k a b c. Ord k
=> (Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c
zipWithKey :: forall s k a b c.
Ord k =>
(Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c
zipWithKey Key s k -> a -> b -> c
f (Map Map k a
m1) (Map Map k b
m2) = Map k c -> Map s k c
forall s k a. Map k a -> Map s k a
Map
(Map k c -> Map s k c) -> Map k c -> Map s k c
forall a b. (a -> b) -> a -> b
$ (k -> a -> b -> Maybe c)
-> (Map k a -> Map k c)
-> (Map k b -> Map k c)
-> Map k a
-> Map k b
-> Map k c
forall k a b c.
Ord k =>
(k -> a -> b -> Maybe c)
-> (Map k a -> Map k c)
-> (Map k b -> Map k c)
-> Map k a
-> Map k b
-> Map k c
Map.mergeWithKey (\k
k a
x b
y -> c -> Maybe c
forall a. a -> Maybe a
Just (c -> Maybe c) -> c -> Maybe c
forall a b. (a -> b) -> a -> b
$ Key s k -> a -> b -> c
f (k -> Key s k
forall k s. k -> Key s k
unsafeKey k
k) a
x b
y)
(String -> Map k a -> Map k c
forall a. HasCallStack => String -> a
error String
"zipWithKey: bug: Data.Map.Refined has been subverted")
(String -> Map k b -> Map k c
forall a. HasCallStack => String -> a
error String
"zipWithKey: bug: Data.Map.Refined has been subverted")
Map k a
m1
Map k b
m2
difference
:: forall s t k a b. Ord k
=> Map s k a -> Map t k b -> SomeMapWith (DifferenceProof 'Regular s t) k a
difference :: forall s t k a b.
Ord k =>
Map s k a
-> Map t k b -> SomeMapWith (DifferenceProof 'Regular s t) k a
difference (Map Map k a
m1) (Map Map k b
m2) = Map Any k a
-> DifferenceProof 'Regular s t Any
-> SomeMapWith (DifferenceProof '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
$ Map k a -> Map k b -> Map k a
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference Map k a
m1 Map k b
m2)
(DifferenceProof 'Regular s t Any
-> SomeMapWith (DifferenceProof 'Regular s t) k a)
-> DifferenceProof 'Regular s t Any
-> SomeMapWith (DifferenceProof 'Regular s t) k a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular Any :-> InSet 'Regular s)
-> (forall u.
(InSet 'Regular u :-> InSet 'Regular Any)
-> (InSet 'Regular u :-> InSet 'Regular t)
-> forall v x.
Refined (InSet 'Regular u) x -> Refined (InSet 'Regular v) x)
-> (InSet 'Regular s :-> (InSet 'Regular t || InSet 'Regular Any))
-> DifferenceProof 'Regular s t Any
forall (f :: Flavor) s t r.
(InSet f r :-> InSet f s)
-> (forall u.
(InSet f u :-> InSet f r)
-> (InSet f u :-> InSet f t)
-> forall v x. Refined (InSet f u) x -> Refined (InSet f v) x)
-> (InSet f s :-> (InSet f t || InSet f r))
-> DifferenceProof f s t r
DifferenceProof 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 (\InSet 'Regular u :-> InSet 'Regular Any
f InSet 'Regular u :-> InSet 'Regular t
g -> (InSet 'Regular u :-> InSet 'Regular Any)
-> (InSet 'Regular u :-> InSet 'Regular t)
-> InSet 'Regular u :-> InSet 'Regular v
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Regular u) x -> Refined (InSet 'Regular Any) x
InSet 'Regular u :-> InSet 'Regular Any
f Refined (InSet 'Regular u) x -> Refined (InSet 'Regular t) x
InSet 'Regular u :-> InSet 'Regular t
g) 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
mapWithKey :: forall s k a b. (Key s k -> a -> b) -> Map s k a -> Map s k b
mapWithKey :: forall s k a b. (Key s k -> a -> b) -> Map s k a -> Map s k b
mapWithKey = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
(Key s k -> a -> b) -> Map s k a -> Map s k b)
-> (Key s k -> a -> b)
-> Map s k a
-> Map s k b
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 -> b) -> Map s k a -> Map s k b)
-> (Key s k -> a -> b) -> Map s k a -> Map s k b)
-> (Coercible k (Key s k) =>
(Key s k -> a -> b) -> Map s k a -> Map s k b)
-> (Key s k -> a -> b)
-> Map s k a
-> Map s k b
forall a b. (a -> b) -> a -> b
$ ((k -> a -> b) -> Map k a -> Map k b)
-> (Key s k -> a -> b) -> Map s k a -> Map s k b
forall a b. Coercible a b => a -> b
coerce
(((k -> a -> b) -> Map k a -> Map k b)
-> (Key s k -> a -> b) -> Map s k a -> Map s k b)
-> ((k -> a -> b) -> Map k a -> Map k b)
-> (Key s k -> a -> b)
-> Map s k a
-> Map s k b
forall a b. (a -> b) -> a -> b
$ forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey @k @a @b
traverseWithKey
:: forall s f k a b. Applicative f
=> (Key s k -> a -> f b) -> Map s k a -> f (Map s k b)
traverseWithKey :: forall s (f :: * -> *) k a b.
Applicative f =>
(Key s k -> a -> f b) -> Map s k a -> f (Map s k b)
traverseWithKey Key s k -> a -> f b
f (Map Map k a
m) = Map k b -> Map s k b
forall s k a. Map k a -> Map s k a
Map (Map k b -> Map s k b) -> f (Map k b) -> f (Map s k b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (k -> a -> f b) -> Map k a -> f (Map k b)
forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
Map.traverseWithKey (Key s k -> a -> f b
f (Key s k -> a -> f b) -> (k -> Key s k) -> k -> a -> f 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
foldMapWithKey
:: forall s k a m. Monoid m => (Key s k -> a -> m) -> Map s k a -> m
foldMapWithKey :: forall s k a m. Monoid m => (Key s k -> a -> m) -> Map s k a -> m
foldMapWithKey = Coercion k (Key s k)
-> (Coercible k (Key s k) => (Key s k -> a -> m) -> Map s k a -> m)
-> (Key s k -> a -> m)
-> Map s k a
-> m
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 -> m) -> Map s k a -> m)
-> (Key s k -> a -> m) -> Map s k a -> m)
-> (Coercible k (Key s k) => (Key s k -> a -> m) -> Map s k a -> m)
-> (Key s k -> a -> m)
-> Map s k a
-> m
forall a b. (a -> b) -> a -> b
$ ((k -> a -> m) -> Map k a -> m)
-> (Key s k -> a -> m) -> Map s k a -> m
forall a b. Coercible a b => a -> b
coerce
(((k -> a -> m) -> Map k a -> m)
-> (Key s k -> a -> m) -> Map s k a -> m)
-> ((k -> a -> m) -> Map k a -> m)
-> (Key s k -> a -> m)
-> Map s k a
-> m
forall a b. (a -> b) -> a -> b
$ forall m k a. Monoid m => (k -> a -> m) -> Map k a -> m
Map.foldMapWithKey @m @k @a
foldrWithKey :: forall s k a b. (Key s k -> a -> b -> b) -> b -> Map s k a -> b
foldrWithKey :: forall s k a b. (Key s k -> a -> b -> b) -> b -> Map s k a -> b
foldrWithKey = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
(Key s k -> a -> b -> b) -> b -> Map s k a -> b)
-> (Key s k -> a -> b -> b)
-> b
-> Map s k a
-> b
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 -> b -> b) -> b -> Map s k a -> b)
-> (Key s k -> a -> b -> b) -> b -> Map s k a -> b)
-> (Coercible k (Key s k) =>
(Key s k -> a -> b -> b) -> b -> Map s k a -> b)
-> (Key s k -> a -> b -> b)
-> b
-> Map s k a
-> b
forall a b. (a -> b) -> a -> b
$ ((k -> a -> b -> b) -> b -> Map k a -> b)
-> (Key s k -> a -> b -> b) -> b -> Map s k a -> b
forall a b. Coercible a b => a -> b
coerce
(((k -> a -> b -> b) -> b -> Map k a -> b)
-> (Key s k -> a -> b -> b) -> b -> Map s k a -> b)
-> ((k -> a -> b -> b) -> b -> Map k a -> b)
-> (Key s k -> a -> b -> b)
-> b
-> Map s k a
-> b
forall a b. (a -> b) -> a -> b
$ forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey @k @a @b
foldlWithKey :: forall s k a b. (b -> Key s k -> a -> b) -> b -> Map s k a -> b
foldlWithKey :: forall s k a b. (b -> Key s k -> a -> b) -> b -> Map s k a -> b
foldlWithKey = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
(b -> Key s k -> a -> b) -> b -> Map s k a -> b)
-> (b -> Key s k -> a -> b)
-> b
-> Map s k a
-> b
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) =>
(b -> Key s k -> a -> b) -> b -> Map s k a -> b)
-> (b -> Key s k -> a -> b) -> b -> Map s k a -> b)
-> (Coercible k (Key s k) =>
(b -> Key s k -> a -> b) -> b -> Map s k a -> b)
-> (b -> Key s k -> a -> b)
-> b
-> Map s k a
-> b
forall a b. (a -> b) -> a -> b
$ ((b -> k -> a -> b) -> b -> Map k a -> b)
-> (b -> Key s k -> a -> b) -> b -> Map s k a -> b
forall a b. Coercible a b => a -> b
coerce
(((b -> k -> a -> b) -> b -> Map k a -> b)
-> (b -> Key s k -> a -> b) -> b -> Map s k a -> b)
-> ((b -> k -> a -> b) -> b -> Map k a -> b)
-> (b -> Key s k -> a -> b)
-> b
-> Map s k a
-> b
forall a b. (a -> b) -> a -> b
$ forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey @b @k @a
foldrWithKey' :: forall s k a b. (Key s k -> a -> b -> b) -> b -> Map s k a -> b
foldrWithKey' :: forall s k a b. (Key s k -> a -> b -> b) -> b -> Map s k a -> b
foldrWithKey' = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
(Key s k -> a -> b -> b) -> b -> Map s k a -> b)
-> (Key s k -> a -> b -> b)
-> b
-> Map s k a
-> b
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 -> b -> b) -> b -> Map s k a -> b)
-> (Key s k -> a -> b -> b) -> b -> Map s k a -> b)
-> (Coercible k (Key s k) =>
(Key s k -> a -> b -> b) -> b -> Map s k a -> b)
-> (Key s k -> a -> b -> b)
-> b
-> Map s k a
-> b
forall a b. (a -> b) -> a -> b
$ ((k -> a -> b -> b) -> b -> Map k a -> b)
-> (Key s k -> a -> b -> b) -> b -> Map s k a -> b
forall a b. Coercible a b => a -> b
coerce
(((k -> a -> b -> b) -> b -> Map k a -> b)
-> (Key s k -> a -> b -> b) -> b -> Map s k a -> b)
-> ((k -> a -> b -> b) -> b -> Map k a -> b)
-> (Key s k -> a -> b -> b)
-> b
-> Map s k a
-> b
forall a b. (a -> b) -> a -> b
$ forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey' @k @a @b
foldlWithKey' :: forall s k a b. (b -> Key s k -> a -> b) -> b -> Map s k a -> b
foldlWithKey' :: forall s k a b. (b -> Key s k -> a -> b) -> b -> Map s k a -> b
foldlWithKey' = Coercion k (Key s k)
-> (Coercible k (Key s k) =>
(b -> Key s k -> a -> b) -> b -> Map s k a -> b)
-> (b -> Key s k -> a -> b)
-> b
-> Map s k a
-> b
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) =>
(b -> Key s k -> a -> b) -> b -> Map s k a -> b)
-> (b -> Key s k -> a -> b) -> b -> Map s k a -> b)
-> (Coercible k (Key s k) =>
(b -> Key s k -> a -> b) -> b -> Map s k a -> b)
-> (b -> Key s k -> a -> b)
-> b
-> Map s k a
-> b
forall a b. (a -> b) -> a -> b
$ ((b -> k -> a -> b) -> b -> Map k a -> b)
-> (b -> Key s k -> a -> b) -> b -> Map s k a -> b
forall a b. Coercible a b => a -> b
coerce
(((b -> k -> a -> b) -> b -> Map k a -> b)
-> (b -> Key s k -> a -> b) -> b -> Map s k a -> b)
-> ((b -> k -> a -> b) -> b -> Map k a -> b)
-> (b -> Key s k -> a -> b)
-> b
-> Map s k a
-> b
forall a b. (a -> b) -> a -> b
$ forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' @b @k @a
keysSet :: forall s k a. Map s k a -> Set s k
keysSet :: forall s k a. Map s k a -> Set s k
keysSet (Map Map k a
m) = Set k
-> (forall s. Reifies s (Set k) => Proxy s -> Set s k) -> Set s k
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Map k a -> Set k
forall k a. Map k a -> Set k
Map.keysSet Map k a
m)
\(Proxy s
_ :: Proxy s') -> case (Any :~: Any) -> s :~: s
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: s :~: s' of
s :~: s
Refl -> Set s k
forall (a :: Constraint). a => Dict a
Dict
toList :: forall s k a. Map s k a -> [(Key s k, a)]
toList :: forall s k a. Map s k a -> [(Key s k, a)]
toList = Coercion k (Key s k)
-> (Coercible k (Key s k) => Map s k a -> [(Key s k, a)])
-> Map s k a
-> [(Key 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) => Map s k a -> [(Key s k, a)])
-> Map s k a -> [(Key s k, a)])
-> (Coercible k (Key s k) => Map s k a -> [(Key s k, a)])
-> Map s k a
-> [(Key s k, a)]
forall a b. (a -> b) -> a -> b
$ (Map k a -> [(k, a)]) -> Map s k a -> [(Key s k, a)]
forall a b. Coercible a b => a -> b
coerce ((Map k a -> [(k, a)]) -> Map s k a -> [(Key s k, a)])
-> (Map k a -> [(k, a)]) -> Map s k a -> [(Key s k, a)]
forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toAscList @k @a
toDescList :: forall s k a. Map s k a -> [(Key s k, a)]
toDescList :: forall s k a. Map s k a -> [(Key s k, a)]
toDescList = Coercion k (Key s k)
-> (Coercible k (Key s k) => Map s k a -> [(Key s k, a)])
-> Map s k a
-> [(Key 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) => Map s k a -> [(Key s k, a)])
-> Map s k a -> [(Key s k, a)])
-> (Coercible k (Key s k) => Map s k a -> [(Key s k, a)])
-> Map s k a
-> [(Key s k, a)]
forall a b. (a -> b) -> a -> b
$ (Map k a -> [(k, a)]) -> Map s k a -> [(Key s k, a)]
forall a b. Coercible a b => a -> b
coerce ((Map k a -> [(k, a)]) -> Map s k a -> [(Key s k, a)])
-> (Map k a -> [(k, a)]) -> Map s k a -> [(Key s k, a)]
forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toDescList @k @a
filterWithKey
:: forall s k a. (Key s k -> a -> Bool)
-> Map s k a
-> SomeMapWith (SupersetProof 'Regular s) k a
filterWithKey :: forall s k a.
(Key s k -> a -> Bool)
-> Map s k a -> SomeMapWith (SupersetProof 'Regular s) k a
filterWithKey Key s k -> a -> Bool
p (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 -> Bool) -> Map k a -> Map k a
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (Key s k -> a -> Bool
p (Key s k -> a -> Bool) -> (k -> Key s k) -> k -> a -> Bool
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
restrictKeys
:: forall s t k a. (Ord k, KnownSet t k)
=> Map s k a -> SomeMapWith (IntersectionProof 'Regular s t) k a
restrictKeys :: forall s t k a.
(Ord k, KnownSet t k) =>
Map s k a -> SomeMapWith (IntersectionProof 'Regular s t) k a
restrictKeys (Map Map k a
m) = Map Any k a
-> IntersectionProof 'Regular s t Any
-> SomeMapWith (IntersectionProof 'Regular s t) k a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith
#if MIN_VERSION_containers(0, 5, 8)
(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
$ Map k a -> Set k -> Map k a
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map k a
m (Set k -> Map k a) -> Set k -> Map k a
forall a b. (a -> b) -> a -> b
$ Proxy t -> Set k
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> Set k
reflect (Proxy t -> Set k) -> Proxy t -> Set k
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t)
#else
(Map $ Map.intersectionWith const m $ Map.fromSet id $ reflect $ Proxy @t)
#endif
(IntersectionProof 'Regular s t Any
-> SomeMapWith (IntersectionProof 'Regular s t) k a)
-> IntersectionProof 'Regular s t Any
-> SomeMapWith (IntersectionProof 'Regular s t) k a
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
withoutKeys
:: forall s t k a. (Ord k, KnownSet t k)
=> Map s k a -> SomeMapWith (DifferenceProof 'Regular s t) k a
withoutKeys :: forall s t k a.
(Ord k, KnownSet t k) =>
Map s k a -> SomeMapWith (DifferenceProof 'Regular s t) k a
withoutKeys (Map Map k a
m) = Map Any k a
-> DifferenceProof 'Regular s t Any
-> SomeMapWith (DifferenceProof 'Regular s t) k a
forall s k a (p :: * -> *). Map s k a -> p s -> SomeMapWith p k a
SomeMapWith
#if MIN_VERSION_containers(0, 5, 8)
(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
$ Map k a -> Set k -> Map k a
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys Map k a
m (Set k -> Map k a) -> Set k -> Map k a
forall a b. (a -> b) -> a -> b
$ Proxy t -> Set k
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> Set k
reflect (Proxy t -> Set k) -> Proxy t -> Set k
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t)
#else
(Map $ Map.difference m $ Map.fromSet id $ reflect $ Proxy @t)
#endif
(DifferenceProof 'Regular s t Any
-> SomeMapWith (DifferenceProof 'Regular s t) k a)
-> DifferenceProof 'Regular s t Any
-> SomeMapWith (DifferenceProof 'Regular s t) k a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular Any :-> InSet 'Regular s)
-> (forall u.
(InSet 'Regular u :-> InSet 'Regular Any)
-> (InSet 'Regular u :-> InSet 'Regular t)
-> forall v x.
Refined (InSet 'Regular u) x -> Refined (InSet 'Regular v) x)
-> (InSet 'Regular s :-> (InSet 'Regular t || InSet 'Regular Any))
-> DifferenceProof 'Regular s t Any
forall (f :: Flavor) s t r.
(InSet f r :-> InSet f s)
-> (forall u.
(InSet f u :-> InSet f r)
-> (InSet f u :-> InSet f t)
-> forall v x. Refined (InSet f u) x -> Refined (InSet f v) x)
-> (InSet f s :-> (InSet f t || InSet f r))
-> DifferenceProof f s t r
DifferenceProof 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 (\InSet 'Regular u :-> InSet 'Regular Any
f InSet 'Regular u :-> InSet 'Regular t
g -> (InSet 'Regular u :-> InSet 'Regular Any)
-> (InSet 'Regular u :-> InSet 'Regular t)
-> InSet 'Regular u :-> InSet 'Regular v
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Regular u) x -> Refined (InSet 'Regular Any) x
InSet 'Regular u :-> InSet 'Regular Any
f Refined (InSet 'Regular u) x -> Refined (InSet 'Regular t) x
InSet 'Regular u :-> InSet 'Regular t
g) 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
partitionWithKey
:: forall s k a. Ord k
=> (Key s k -> a -> Bool)
-> Map s k a
-> Some2MapWith (PartitionProof 'Regular s k) k a a
partitionWithKey :: forall s k a.
Ord k =>
(Key s k -> a -> Bool)
-> Map s k a -> Some2MapWith (PartitionProof 'Regular s k) k a a
partitionWithKey Key s k -> a -> Bool
p (Map Map k a
m) = case (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (Key s k -> a -> Bool
p (Key s k -> a -> Bool) -> (k -> Key s k) -> k -> a -> Bool
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 a
m1, Map k a
m2) -> Map Any k a
-> Map Any k a
-> PartitionProof 'Regular s k Any Any
-> Some2MapWith (PartitionProof 'Regular s k) k a a
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 a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map Map k a
m1) (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map Map k a
m2) (PartitionProof 'Regular s k Any Any
-> Some2MapWith (PartitionProof 'Regular s k) k a a)
-> PartitionProof 'Regular s k Any Any
-> Some2MapWith (PartitionProof 'Regular s k) k a a
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
-> String
-> Either
(Refined (InSet 'Regular Any) k) (Refined (InSet 'Regular Any) k)
forall a. HasCallStack => String -> a
error String
"partitionWithKey: bug: Data.Map.Refined has been subverted"
Just a
x -> if Key s k -> a -> Bool
p Key s k
k a
x
then 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
else 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
spanAntitone
:: forall s k a. (Key s k -> Bool)
-> Map s k a
-> Some2MapWith (PartialPartitionProof 'Regular s) k a a
spanAntitone :: forall s k a.
(Key s k -> Bool)
-> Map s k a
-> Some2MapWith (PartialPartitionProof 'Regular s) k a a
spanAntitone Key s k -> Bool
p (Map Map k a
m) =
#if MIN_VERSION_containers(0, 5, 8)
case (k -> Bool) -> Map k a -> (Map k a, Map k a)
forall k a. (k -> Bool) -> Map k a -> (Map k a, Map k a)
Map.spanAntitone (Key s k -> Bool
p (Key s k -> Bool) -> (k -> Key s k) -> k -> Bool
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 a
m1, Map k a
m2)
#else
case List.span (p . unsafeKey . fst) $ Map.toAscList m of
(xs1, xs2)
| let m1 = Map.fromDistinctAscList xs1
, let m2 = Map.fromDistinctAscList xs2
#endif
-> Map Any k a
-> Map Any k a
-> PartialPartitionProof 'Regular s Any Any
-> Some2MapWith (PartialPartitionProof 'Regular s) k a a
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 a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map Map k a
m1) (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map Map k a
m2) (PartialPartitionProof 'Regular s Any Any
-> Some2MapWith (PartialPartitionProof 'Regular s) k a a)
-> PartialPartitionProof 'Regular s Any Any
-> Some2MapWith (PartialPartitionProof 'Regular s) k a a
forall a b. (a -> b) -> a -> b
$ ((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)
-> PartialPartitionProof 'Regular s Any Any
forall (f :: Flavor) s r q.
((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)
-> PartialPartitionProof f s r q
PartialPartitionProof
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
splitLookup
:: forall s k a. Ord k
=> k -> Map s k a -> Some2MapWith (SplitProof 'Regular s (Key s k, a)) k a a
splitLookup :: forall s k a.
Ord k =>
k
-> Map s k a
-> Some2MapWith (SplitProof 'Regular s (Key s k, a)) k a a
splitLookup k
k (Map Map k a
m) = case k -> Map k a -> (Map k a, Maybe a, Map k a)
forall k a. Ord k => k -> Map k a -> (Map k a, Maybe a, Map k a)
Map.splitLookup k
k Map k a
m of
(!Map k a
m1, Maybe a
v, !Map k a
m2) -> Map Any k a
-> Map Any k a
-> SplitProof 'Regular s (Key s k, a) Any Any
-> Some2MapWith (SplitProof 'Regular s (Key s k, a)) k a a
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 a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map Map k a
m1) (Map k a -> Map Any k a
forall s k a. Map k a -> Map s k a
Map Map k a
m2) (SplitProof 'Regular s (Key s k, a) Any Any
-> Some2MapWith (SplitProof 'Regular s (Key s k, a)) k a a)
-> SplitProof 'Regular s (Key s k, a) Any Any
-> Some2MapWith (SplitProof 'Regular s (Key s k, a)) k a a
forall a b. (a -> b) -> a -> b
$ Maybe (Key s k, a)
-> ((InSet 'Regular Any || InSet 'Regular Any)
:-> InSet 'Regular s)
-> (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)
-> SplitProof 'Regular s (Key s k, a) Any Any
forall (f :: Flavor) s e r q.
Maybe e
-> ((InSet f r || InSet f q) :-> InSet f s)
-> (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)
-> SplitProof f s e r q
SplitProof
((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) 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 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
minViewWithKey
:: forall s k a. Map s k a
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
minViewWithKey :: forall s k a.
Map s k a
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
minViewWithKey (Map Map k a
m) = case Map k a -> Maybe ((k, a), Map k a)
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.minViewWithKey Map k a
m of
Maybe ((k, a), Map k a)
Nothing -> EmptyProof 'Regular s
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
forall a b. a -> Either a b
Left (EmptyProof 'Regular s
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a))
-> EmptyProof 'Regular s
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
forall a b. (a -> b) -> a -> b
$ (forall s. InSet 'Regular s :-> InSet 'Regular s)
-> EmptyProof 'Regular s
forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular s) x
forall s. InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset
Just ((k, a)
kv, Map k a
m') -> ((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
forall a b. b -> Either a b
Right (((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a))
-> ((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
forall a b. (a -> b) -> a -> b
$ (Coercion k (Key s k)
-> (Coercible k (Key s k) => (Key s k, a)) -> (Key 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)) -> (Key s k, a))
-> (Coercible k (Key s k) => (Key s k, a)) -> (Key s k, a)
forall a b. (a -> b) -> a -> b
$ (k, a) -> (Key s k, a)
forall a b. Coercible a b => a -> b
coerce (k, a)
kv,)
(SomeMapWith (SupersetProof 'Regular s) k a
-> ((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a))
-> SomeMapWith (SupersetProof 'Regular s) k a
-> ((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
maxViewWithKey
:: forall s k a. Map s k a
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
maxViewWithKey :: forall s k a.
Map s k a
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
maxViewWithKey (Map Map k a
m) = case Map k a -> Maybe ((k, a), Map k a)
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.maxViewWithKey Map k a
m of
Maybe ((k, a), Map k a)
Nothing -> EmptyProof 'Regular s
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
forall a b. a -> Either a b
Left (EmptyProof 'Regular s
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a))
-> EmptyProof 'Regular s
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
forall a b. (a -> b) -> a -> b
$ (forall s. InSet 'Regular s :-> InSet 'Regular s)
-> EmptyProof 'Regular s
forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular s) x
forall s. InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset
Just ((k, a)
kv, Map k a
m') -> ((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
forall a b. b -> Either a b
Right (((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a))
-> ((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
-> Either
(EmptyProof 'Regular s)
((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a)
forall a b. (a -> b) -> a -> b
$ (Coercion k (Key s k)
-> (Coercible k (Key s k) => (Key s k, a)) -> (Key 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)) -> (Key s k, a))
-> (Coercible k (Key s k) => (Key s k, a)) -> (Key s k, a)
forall a b. (a -> b) -> a -> b
$ (k, a) -> (Key s k, a)
forall a b. Coercible a b => a -> b
coerce (k, a)
kv,)
(SomeMapWith (SupersetProof 'Regular s) k a
-> ((Key s k, a), SomeMapWith (SupersetProof 'Regular s) k a))
-> SomeMapWith (SupersetProof 'Regular s) k a
-> ((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
castKey
:: forall s t k. (forall x. Key s x -> Key t x)
-> (forall x. Key t x -> Key s x)
-> Coercion (Key s k) (Key t k)
castKey :: forall s t k.
(forall x. Key s x -> Key t x)
-> (forall x. Key t x -> Key s x) -> Coercion (Key s k) (Key t k)
castKey = (InSet 'Regular s :-> InSet 'Regular t)
-> (InSet 'Regular t :-> InSet 'Regular s)
-> Coercion
(Refined (InSet 'Regular s) k) (Refined (InSet 'Regular t) k)
forall a p q.
(p :-> q) -> (q :-> p) -> Coercion (Refined p a) (Refined q a)
castRefined
cast
:: forall s t k. (forall x. Coercion (Key s x) (Key t x))
-> Coercion (Map s k) (Map t k)
cast :: forall s t k.
(forall x. Coercion (Key s x) (Key t x))
-> Coercion (Map s k) (Map t k)
cast Coercion (Key s Any) (Key t Any)
forall x. Coercion (Key s x) (Key t x)
Coercion = Coercion (Map s k) (Map t k)
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
instance FunctorWithIndex (Key s k) (Map s k) where
imap :: forall a b. (Key s k -> a -> b) -> Map s k a -> Map s k b
imap = (Key s k -> a -> b) -> Map s k a -> Map s k b
forall s k a b. (Key s k -> a -> b) -> Map s k a -> Map s k b
mapWithKey
instance FoldableWithIndex (Key s k) (Map s k) where
ifoldMap :: forall m a. Monoid m => (Key s k -> a -> m) -> Map s k a -> m
ifoldMap = (Key s k -> a -> m) -> Map s k a -> m
forall s k a m. Monoid m => (Key s k -> a -> m) -> Map s k a -> m
foldMapWithKey
instance TraversableWithIndex (Key s k) (Map s k) where
itraverse :: forall (f :: * -> *) a b.
Applicative f =>
(Key s k -> a -> f b) -> Map s k a -> f (Map s k b)
itraverse = (Key s k -> a -> f b) -> Map s k a -> f (Map s k b)
forall s (f :: * -> *) k a b.
Applicative f =>
(Key s k -> a -> f b) -> Map s k a -> f (Map s k b)
traverseWithKey
instance (Ord k, KnownSet s k) => Applicative (Map s k) where
pure :: forall a. a -> Map s k a
pure a
x = (Key s k -> a) -> Map s k a
forall s k a. KnownSet s k => (Key s k -> a) -> Map s k a
fromSet \Key s k
_ -> a
x
<*> :: forall a b. Map s k (a -> b) -> Map s k a -> Map s k b
(<*>) = (Key s k -> (a -> b) -> a -> b)
-> Map s k (a -> b) -> Map s k a -> Map s k b
forall s k a b c.
Ord k =>
(Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c
zipWithKey (((a -> b) -> a -> b) -> Key s k -> (a -> b) -> a -> b
forall a b. a -> b -> a
const (a -> b) -> a -> b
forall a. a -> a
id)
bind :: forall s k a b. Ord k => Map s k a -> (a -> Map s k b) -> Map s k b
bind :: forall s k a b. Ord k => Map s k a -> (a -> Map s k b) -> Map s k b
bind Map s k a
m a -> Map s k b
f = (Key s k -> a -> b) -> Map s k a -> Map s k b
forall s k a b. (Key s k -> a -> b) -> Map s k a -> Map s k b
mapWithKey (\Key s k
k a
x -> a -> Map s k b
f a
x Map s k b -> Key s k -> b
forall s k a. Ord k => Map s k a -> Key s k -> a
! Key s k
k) Map s k a
m
instance (Ord k, KnownSet s k) => Monad (Map s k) where
>>= :: forall a b. Map s k a -> (a -> Map s k b) -> Map s k b
(>>=) = Map s k a -> (a -> Map s k b) -> Map s k b
forall s k a b. Ord k => Map s k a -> (a -> Map s k b) -> Map s k b
bind
instance (Ord k, KnownSet s k) => MonadReader (Key s k) (Map s k) where
ask :: Map s k (Key s k)
ask = (Key s k -> Key s k) -> Map s k (Key s k)
forall s k a. KnownSet s k => (Key s k -> a) -> Map s k a
fromSet Key s k -> Key s k
forall a. a -> a
id
local :: forall a. (Key s k -> Key s k) -> Map s k a -> Map s k a
local Key s k -> Key s k
f Map s k a
m = (Key s k -> a -> a) -> Map s k a -> Map s k a
forall s k a b. (Key s k -> a -> b) -> Map s k a -> Map s k b
mapWithKey (\Key s k
k a
_ -> Map s k a
m Map s k a -> Key s k -> a
forall s k a. Ord k => Map s k a -> Key s k -> a
! Key s k -> Key s k
f Key s k
k) Map s k a
m
instance (Ord k, Semigroup a) => Semigroup (Map s k a) where
<> :: Map s k a -> Map s k a -> Map s k a
(<>) = (Key s k -> a -> a -> a) -> Map s k a -> Map s k a -> Map s k a
forall s k a b c.
Ord k =>
(Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c
zipWithKey ((a -> a -> a) -> Key s k -> a -> a -> a
forall a b. a -> b -> a
const a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>))
instance (Ord k, KnownSet s k, Monoid a) => Monoid (Map s k a) where
mempty :: Map s k a
mempty = (Key s k -> a) -> Map s k a
forall s k a. KnownSet s k => (Key s k -> a) -> Map s k a
fromSet \Key s k
_ -> a
forall a. Monoid a => a
mempty
instance (Ord k, KnownSet s k) => Distributive (Map s k) where
collect :: forall (f :: * -> *) a b.
Functor f =>
(a -> Map s k b) -> f a -> Map s k (f b)
collect = (a -> Map s k b) -> f a -> Map s k (f b)
forall (f :: * -> *) (w :: * -> *) a b.
(Representable f, Functor w) =>
(a -> f b) -> w a -> f (w b)
collectRep
distribute :: forall (f :: * -> *) a. Functor f => f (Map s k a) -> Map s k (f a)
distribute = f (Map s k a) -> Map s k (f a)
forall (f :: * -> *) (w :: * -> *) a.
(Representable f, Functor w) =>
w (f a) -> f (w a)
distributeRep
instance (Ord k, KnownSet s k) => Representable (Map s k) where
type Rep (Map s k) = Key s k
index :: forall a. Map s k a -> Rep (Map s k) -> a
index = Map s k a -> Rep (Map s k) -> a
Map s k a -> Key s k -> a
forall s k a. Ord k => Map s k a -> Key s k -> a
(!)
tabulate :: forall a. (Rep (Map s k) -> a) -> Map s k a
tabulate = (Rep (Map s k) -> a) -> Map s k a
(Key s k -> a) -> Map s k a
forall s k a. KnownSet s k => (Key s k -> a) -> Map s k a
fromSet
#if MIN_VERSION_hashable(1, 3, 4)
#else
instance (Hashable.Hashable a, Hashable.Hashable k)
=> Hashable.Hashable (Map s k a) where
hashWithSalt s (Map m) = Map.foldlWithKey'
(\s' k v -> Hashable.hashWithSalt (Hashable.hashWithSalt s' k) v)
(Hashable.hashWithSalt s (Map.size m))
m
#endif