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