{-# 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


-- | A wrapper around a regular 'Data.IntMap.IntMap' with a type parameter @s@
-- identifying the set of keys present in the map.
--
-- An t'Int' key may not be present in the map, but a @'Key' s@ is guaranteed to
-- be present (if the @s@ parameters match). Thus the map is isomorphic to a
-- (total) function @'Key' s -> a@, which motivates many of the instances below.
--
-- An 'IntMap' always knows its set of keys, so given @'IntMap' s a@ we can
-- always derive @'KnownIntSet' s@ by pattern matching on the 'Dict' returned by
-- 'keysSet'.
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

-- | Convert to a regular 'Data.IntMap.IntMap', forgetting its set of keys.
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

-- | @'Key' s@ is a key of type t'Int' that has been verified to be an element
-- of the set @s@, and thus verified to be present in all @'IntMap' s k@ maps.
--
-- Thus, @'Key' s@ is a \"refinement\" type of t'Int', and this library
-- integrates with an implementation of refimenement types in "Refined", so
-- the machinery from there can be used to manipulate 'Key's (however see
-- 'Data.IntSet.Refined.revealPredicate').
--
-- The underlying t'Int' value can be obtained with 'unrefine'. An t'Int' can be
-- validated into an @'Key' s@ with 'member'.
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

-- | An existential wrapper for an 'IntMap' with an as-yet-unknown set of keys.
-- Pattern maching on it gives you a way to refer to the set (the parameter
-- @s@), e.g.
--
-- @
-- case 'fromIntMap' ... of
--   'SomeIntMap' \@s m -> doSomethingWith \@s
--
-- case 'fromIntMap' ... of
--   'SomeIntMap' (m :: 'IntMap' s a) -> doSomethingWith \@s
-- @
data SomeIntMap a where
  SomeIntMap :: forall s a. !(IntMap s a) -> SomeIntMap a

-- | Apply a map with an unknown set of keys to a continuation that can accept
-- a map with any set of keys. This gives you a way to refer to the set (the
-- parameter @s@), e.g.:
--
-- @
-- 'withIntMap' ('fromIntMap' ...) $ \(m :: 'IntMap' s a) -> doSomethingWith \@s
-- @
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

-- | Construct a map from a regular 'Data.IntMap.IntMap'.
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)

-- | An existential wrapper for an 'IntMap' with an as-yet-unknown set of keys,
-- together with a proof of some fact @p@ about the set. Pattern matching on it
-- gives you a way to refer to the set (the parameter @s@). Functions that
-- change the set of keys in a map will return the map in this way, together
-- with a proof that somehow relates the keys set to the function's inputs.
data SomeIntMapWith p a where
  SomeIntMapWith :: forall s a p. !(IntMap s a) -> !(p s) -> SomeIntMapWith p a

-- | Apply a map with proof for an unknown set of keys to a continuation that
-- can accept a map with any set of keys satisfying the proof. This gives you a
-- way to refer to the set (the parameter @s@).
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

-- | An existential wrapper for a pair of maps with as-yet-unknown sets of keys,
-- together with a proof of some fact @p@ relating them.
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

-- | Apply a pair of maps with proof for unknown sets of keys to a continuation
-- that can accept any pair of maps with any sets of keys satisfying the proof.
-- This gives you a way to refer to the sets (the parameters @s@ and @t@).
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

-- | An empty map.
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

-- | Create a map from a set of keys, and a function that for each key computes
-- the corresponding value.
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 a key and its value from the map if present, returning a potentially
-- smaller map.
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

-- | If the key is in the map, return the proof of this, and the associated
-- value; otherwise return 'Nothing'.
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

-- | Given a key that is proven to be in the map, return the associated value.
--
-- Unlike 'Data.IntMap.!' from "Data.IntMap", this function is total, as it is
-- impossible to obtain a @'Key' s@ for a key that is not in the map
-- @'IntMap' s a@.
(!) :: 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

-- | If a key is in the map, return the proof that it is.
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

-- | Find the largest key smaller than the given one, and return the
-- associated key-value pair.
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

-- | Find the smallest key greater than the given one, and return the
-- associated key-value pair.
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

-- | Find the largest key smaller or equal to the given one, and return the
-- associated key-value pair.
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

-- | Find the smallest key greater or equal to the given one, and return the
-- associated key-value pair.
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

-- | If a map is empty, return a proof that it is.
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

-- | If all keys of the first map are also present in the second map, and the
-- given function returns 'True' for their associated values, return a proof
-- that the keys form a subset.
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

-- | If two maps are disjoint (i.e. their intersection is empty), return a proof
-- of that.
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

-- | Given two maps proven to have the same keys, for each key apply the
-- function to the associated values, to obtain a new map with the same keys.
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

-- | Remove the keys that appear in the second map from the first map.
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

-- | Apply a function to all values in a map, together with their corresponding
-- keys, that are proven to be in the map. The set of keys remains the same.
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

-- | Map an 'Applicative' transformation in ascending order of keys, with access
-- to each value's corresponding key and a proof that it is in the map. The set
-- of keys remains unchanged.
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

-- | Map each key-value pair of a map into a monoid (with proof that the key was
-- in the map), and combine the results using '<>'.
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

-- | Right associative fold with a lazy accumulator.
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

-- | Left associative fold with a lazy accumulator.
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

-- | Right associative fold with a strict accumulator.
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

-- | Left associative fold with a strict accumulator.
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

-- | Return the set of keys in the map, with the contents of the set still
-- tracked by the @s@ parameter. See "Data.IntSet.Refined".
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

-- | Convert to a list of key-value pairs in ascending order of keys.
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

-- | Convert to a list of key-value pairs in descending order of keys.
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

-- | Retain only the key-value pairs that satisfy the predicate, returning a
-- potentially smaller map.
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

-- | Restrict a map to only those keys that are elements of @t@.
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

-- | Remove all keys that are elements of @t@ from the map.
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

-- | Partition a map into two disjoint submaps: those whose key-value pairs
-- satisfy the predicate, and those whose don't.
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

-- | Divide a map into two disjoint submaps at a point where the predicate on
-- the keys stops holding.
--
-- If @p@ is antitone ( \(\forall x y, x < y \implies p(x) \ge p(y)\) ), then
-- this point is uniquely defined. If @p@ is not antitone, a splitting point is
-- chosen in an unspecified way.
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

-- | Return two disjoint submaps: those whose keys are less than the given key,
-- and those whose keys are greater than the given key. If the key was in the
-- map, also return the associated value and the proof that it was in the map.
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

-- | Retrieves the key-value pair corresponding to the smallest key of the map,
-- and the map with that pair removed; or a proof that the map was empty.
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

-- | Retrieves the key-value pair corresponding to the greatest key of the map,
-- and the map with that pair removed; or a proof that the map was empty.
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

-- | If elements of @s@ can be weakened to elements of @t@ and vice versa, then
-- @s@ and @t@ actually stand for the same set and @'Key' s@ can be safely
-- interconverted with @'Key' t@.
--
-- The requirement that the weakenings are natural transformations ensures that
-- they don't actually alter the keys. To build these you can compose ':->''s
-- from proofs returned by functions in this module, or "Refined" functions like
-- 'andLeft' or 'leftOr'.
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

-- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps
-- can be interconverted too. For example, 'zipWithKey' can be implemented via
-- 'Data.IntMap.Refined.intersectionWithKey' by proving that the set of keys
-- remains unchanged:
--
-- @
-- 'zipWithKey'
--   :: forall s a b c. ('Key' s -> a -> b -> c)
--   -> 'IntMap' s a
--   -> 'IntMap' s b
--   -> 'IntMap' s c
-- 'zipWithKey' f m1 m2
--   | v'SomeIntMapWith' @r m proof <- 'Data.IntMap.Refined.intersectionWithKey' (f . 'andLeft') m1 m2
--   , v'IntersectionProof' p1 p2 <- proof
--   , ( v'Coercion' :: t'Coercion' ('IntMap' r c) ('IntMap' s c))
--     <- app $ 'cast' $ 'castKey' ('andLeft' . p1) (p2 'id' 'id')
--   = 'coerce' m
--   where
--     app :: t'Coercion' f g -> t'Coercion' (f x) (g x)
--     app v'Coercion' = v'Coercion'
-- @
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

-- | Similar to the instance for functions -- zip corresponding keys. To use
-- '<*>'/'liftA2' without 'KnownIntSet' see 'zipWithKey'.
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' m f@ is a map that for each key @k :: 'Key' s@, contains the
-- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.
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

-- | Similar to the instance for functions. To use '>>=' without 'KnownIntSet'
-- see 'bind'.
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

-- | Similar to the instance for functions. See also
-- 'Data.IntMap.Refined.backpermuteKeys'.
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

-- | Append the values at the corresponding keys
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

-- | Similar to the instance for functions
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

-- | Witness isomorphism with functions from @'Key' s@
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