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