{-# LANGUAGE CPP #-}
module Data.IntSet.Refined
(
KnownIntSet
, IntSet
, InSet(..)
, Flavor(Int)
, Element
, revealPredicate
, SomeIntSet(..)
, withIntSet
, SomeIntSetWith(..)
, withIntSetWith
, Some2IntSetWith(..)
, with2IntSetWith
, (:->)
, SupersetProof(..)
, EmptyProof(..)
, empty
, singleton
, SingletonProof(..)
, fromIntSet
, fromTraversable
, FromTraversableProof(..)
, insert
, InsertProof(..)
, delete
, member
, lookupLT
, lookupGT
, lookupLE
, lookupGE
, null
, isSubsetOf
, SubsetProof(..)
, disjoint
, DisjointProof(..)
, union
, UnionProof(..)
, difference
, DifferenceProof(..)
, intersection
, IntersectionProof(..)
, filter
, partition
, PartitionProof(..)
, spanAntitone
, PartialPartitionProof(..)
, splitMember
, SplitProof(..)
, map
, MapProof(..)
, foldMap
, foldr
, foldl
, foldr'
, foldl'
, minView
, maxView
, toList
, toDescList
, asSet
, asHashSet
, castElement
, cast
, castFlavor
) where
import Data.Coerce
import Data.Constraint (Dict(..))
import Data.Container.Refined.Conversion
import Data.Container.Refined.Proofs
import Data.Container.Refined.Unsafe
import qualified Data.Foldable as Foldable
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import Data.Proxy
import Data.Reflection
import Data.Traversable
import Data.Type.Coercion
import Data.Type.Equality ((:~:)(..))
import GHC.Exts (Proxy#, proxy#)
import Prelude hiding (filter, foldl, foldMap, foldr, map, null)
import Refined
import Refined.Unsafe
import Unsafe.Coerce
#if MIN_VERSION_containers(0, 6, 7)
#else
import qualified Data.List as List
#endif
revealPredicate
:: forall s. KnownIntSet s => Dict (Predicate (InSet 'Int s) Int)
revealPredicate :: forall s. KnownIntSet s => Dict (Predicate (InSet 'Int s) Int)
revealPredicate = IntSet
-> (forall s.
(Typeable s, Reifies s IntSet) =>
Proxy s -> Dict (Predicate (InSet 'Int s) Int))
-> Dict (Predicate (InSet 'Int s) Int)
forall a r.
Typeable a =>
a -> (forall s. (Typeable s, Reifies s a) => Proxy s -> r) -> r
reifyTypeable (Proxy s -> IntSet
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> IntSet
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s))
\(Proxy s
_ :: Proxy s') ->
Proxy s -> IntSet
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> IntSet
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s') IntSet
-> Dict (Predicate (InSet 'Int s) Int)
-> Dict (Predicate (InSet 'Int s) Int)
forall a b. a -> b -> b
`seq`
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 -> Dict (Predicate (InSet 'Int s) Int)
forall (a :: Constraint). a => Dict a
Dict
type Element s = Refined (InSet 'Int s) Int
unsafeCastElement :: forall s. Coercion Int (Element s)
unsafeCastElement :: forall s. Coercion Int (Element s)
unsafeCastElement = Coercion Int (Refined (InSet 'Int s) Int)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined
unsafeElement :: Int -> Element s
unsafeElement :: forall s. Int -> Element s
unsafeElement = Coercion Int (Element s) -> Int -> Element s
forall a b. Coercion a b -> a -> b
coerceWith Coercion Int (Element s)
forall s. Coercion Int (Element s)
unsafeCastElement
data SomeIntSet where
SomeIntSet :: forall s. KnownIntSet s => Proxy# s -> SomeIntSet
withIntSet
:: forall r. SomeIntSet -> (forall s. KnownIntSet s => Proxy s -> r) -> r
withIntSet :: forall r.
SomeIntSet -> (forall s. KnownIntSet s => Proxy s -> r) -> r
withIntSet (SomeIntSet (Proxy# s
_ :: Proxy# s)) forall s. KnownIntSet s => Proxy s -> r
k = Proxy s -> r
forall s. KnownIntSet s => Proxy s -> r
k (Proxy s -> r) -> Proxy s -> r
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s
fromIntSet :: IntSet.IntSet -> SomeIntSet
fromIntSet :: IntSet -> SomeIntSet
fromIntSet IntSet
s = IntSet
-> (forall s. Reifies s IntSet => Proxy s -> SomeIntSet)
-> SomeIntSet
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
s \(Proxy s
_ :: Proxy s) -> forall s. KnownIntSet s => Proxy# s -> SomeIntSet
SomeIntSet @s Proxy# s
forall {k} (a :: k). Proxy# a
proxy#
data SomeIntSetWith p where
SomeIntSetWith :: forall s p. KnownIntSet s => !(p s) -> SomeIntSetWith p
withIntSetWith
:: forall r p. SomeIntSetWith p -> (forall s. KnownIntSet s => p s -> r) -> r
withIntSetWith :: forall r (p :: * -> *).
SomeIntSetWith p -> (forall s. KnownIntSet s => p s -> r) -> r
withIntSetWith (SomeIntSetWith p s
p) forall s. KnownIntSet s => p s -> r
k = p s -> r
forall s. KnownIntSet s => p s -> r
k p s
p
data Some2IntSetWith p where
Some2IntSetWith
:: forall s t p. (KnownIntSet s, KnownIntSet t)
=> !(p s t) -> Some2IntSetWith p
with2IntSetWith
:: forall r p. Some2IntSetWith p
-> (forall s t. (KnownIntSet s, KnownIntSet t) => p s t -> r)
-> r
with2IntSetWith :: forall r (p :: * -> * -> *).
Some2IntSetWith p
-> (forall s t. (KnownIntSet s, KnownIntSet t) => p s t -> r) -> r
with2IntSetWith (Some2IntSetWith p s t
p) forall s t. (KnownIntSet s, KnownIntSet t) => p s t -> r
k = p s t -> r
forall s t. (KnownIntSet s, KnownIntSet t) => p s t -> r
k p s t
p
empty :: SomeIntSetWith (EmptyProof 'Int)
empty :: SomeIntSetWith (EmptyProof 'Int)
empty = IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> SomeIntSetWith (EmptyProof 'Int))
-> SomeIntSetWith (EmptyProof 'Int)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
IntSet.empty \(Proxy s
_ :: Proxy r)
-> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r (EmptyProof 'Int s -> SomeIntSetWith (EmptyProof 'Int))
-> EmptyProof 'Int s -> SomeIntSetWith (EmptyProof 'Int)
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
singleton :: Int -> SomeIntSetWith (SingletonProof 'Int Int)
singleton :: Int -> SomeIntSetWith (SingletonProof 'Int Int)
singleton Int
x = IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> SomeIntSetWith (SingletonProof 'Int Int))
-> SomeIntSetWith (SingletonProof 'Int Int)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Int -> IntSet
IntSet.singleton Int
x) \(Proxy s
_ :: Proxy r)
-> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r (SingletonProof 'Int Int s
-> SomeIntSetWith (SingletonProof 'Int Int))
-> SingletonProof 'Int Int s
-> SomeIntSetWith (SingletonProof 'Int Int)
forall a b. (a -> b) -> a -> b
$ Refined (InSet 'Int s) Int -> SingletonProof 'Int Int s
forall (f :: Flavor) a r.
Refined (InSet f r) a -> SingletonProof f a r
SingletonProof (Refined (InSet 'Int s) Int -> SingletonProof 'Int Int s)
-> Refined (InSet 'Int s) Int -> SingletonProof 'Int Int s
forall a b. (a -> b) -> a -> b
$ Int -> Refined (InSet 'Int s) Int
forall s. Int -> Element s
unsafeElement Int
x
fromTraversable
:: forall t. Traversable t
=> t Int -> SomeIntSetWith (FromTraversableProof 'Int t Int)
fromTraversable :: forall (t :: * -> *).
Traversable t =>
t Int -> SomeIntSetWith (FromTraversableProof 'Int t Int)
fromTraversable t Int
xs = IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> SomeIntSetWith (FromTraversableProof 'Int t Int))
-> SomeIntSetWith (FromTraversableProof 'Int t Int)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
set \(Proxy s
_ :: Proxy r)
-> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r (FromTraversableProof 'Int t Int s
-> SomeIntSetWith (FromTraversableProof 'Int t Int))
-> FromTraversableProof 'Int t Int s
-> SomeIntSetWith (FromTraversableProof 'Int t Int)
forall a b. (a -> b) -> a -> b
$ t (Refined (InSet 'Int s) Int) -> FromTraversableProof 'Int t Int s
forall (f :: Flavor) (t :: * -> *) a r.
t (Refined (InSet f r) a) -> FromTraversableProof f t a r
FromTraversableProof
(t (Refined (InSet 'Int s) Int)
-> FromTraversableProof 'Int t Int s)
-> t (Refined (InSet 'Int s) Int)
-> FromTraversableProof 'Int t Int s
forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce @(t (Element _)) @(t (Element r)) t (Element Any)
proof
where
(IntSet
set, t (Element Any)
proof) = (IntSet -> Int -> (IntSet, Element Any))
-> IntSet -> t Int -> (IntSet, t (Element Any))
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
(\IntSet
s Int
x -> let !s' :: IntSet
s' = Int -> IntSet -> IntSet
IntSet.insert Int
x IntSet
s in (IntSet
s', Int -> Element Any
forall s. Int -> Element s
unsafeElement Int
x))
IntSet
IntSet.empty
t Int
xs
insert :: forall s. KnownIntSet s
=> Int -> SomeIntSetWith (InsertProof 'Int Int s)
insert :: forall s.
KnownIntSet s =>
Int -> SomeIntSetWith (InsertProof 'Int Int s)
insert Int
x = IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> SomeIntSetWith (InsertProof 'Int Int s))
-> SomeIntSetWith (InsertProof 'Int Int s)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Int -> IntSet -> IntSet
IntSet.insert Int
x (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ 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) \(Proxy s
_ :: Proxy r)
-> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r (InsertProof 'Int Int s s
-> SomeIntSetWith (InsertProof 'Int Int s))
-> InsertProof 'Int Int s s
-> SomeIntSetWith (InsertProof 'Int Int s)
forall a b. (a -> b) -> a -> b
$ Refined (InSet 'Int s) Int
-> (InSet 'Int s :-> InSet 'Int s) -> InsertProof 'Int Int s s
forall (f :: Flavor) a s r.
Refined (InSet f r) a
-> (InSet f s :-> InSet f r) -> InsertProof f a s r
InsertProof (Int -> Refined (InSet 'Int s) Int
forall s. Int -> Element s
unsafeElement Int
x) Refined (InSet 'Int s) x -> Refined (InSet 'Int s) x
InSet 'Int s :-> InSet 'Int s
forall p q x. Refined p x -> Refined q x
unsafeSubset
delete :: forall s. KnownIntSet s
=> Int -> SomeIntSetWith (SupersetProof 'Int s)
delete :: forall s.
KnownIntSet s =>
Int -> SomeIntSetWith (SupersetProof 'Int s)
delete Int
x = IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> SomeIntSetWith (SupersetProof 'Int s))
-> SomeIntSetWith (SupersetProof 'Int s)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Int -> IntSet -> IntSet
IntSet.delete Int
x (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ 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) \(Proxy s
_ :: Proxy r)
-> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @s (SupersetProof 'Int s s -> SomeIntSetWith (SupersetProof 'Int s))
-> SupersetProof 'Int s s -> SomeIntSetWith (SupersetProof 'Int s)
forall a b. (a -> b) -> a -> b
$ (InSet 'Int s :-> InSet 'Int s) -> SupersetProof 'Int s s
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Int s) x -> Refined (InSet 'Int s) x
InSet 'Int s :-> InSet 'Int s
forall p q x. Refined p x -> Refined q x
unsafeSubset
member :: forall s. KnownIntSet s => Int -> Maybe (Element s)
member :: forall s. KnownIntSet s => Int -> Maybe (Element s)
member Int
x
| Int
x Int -> IntSet -> Bool
`IntSet.member` Proxy s -> IntSet
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> IntSet
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) = Element s -> Maybe (Element s)
forall a. a -> Maybe a
Just (Element s -> Maybe (Element s)) -> Element s -> Maybe (Element s)
forall a b. (a -> b) -> a -> b
$ Int -> Element s
forall s. Int -> Element s
unsafeElement Int
x
| Bool
otherwise = Maybe (Element s)
forall a. Maybe a
Nothing
lookupLT :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupLT :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupLT Int
x = Coercion Int (Element s)
-> (Coercible Int (Element s) => Maybe (Element s))
-> Maybe (Element s)
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s. Coercion Int (Element s)
unsafeCastElement @s) ((Coercible Int (Element s) => Maybe (Element s))
-> Maybe (Element s))
-> (Coercible Int (Element s) => Maybe (Element s))
-> Maybe (Element s)
forall a b. (a -> b) -> a -> b
$ Maybe Int -> Maybe (Element s)
forall a b. Coercible a b => a -> b
coerce
(Maybe Int -> Maybe (Element s)) -> Maybe Int -> Maybe (Element s)
forall a b. (a -> b) -> a -> b
$ Int -> IntSet -> Maybe Int
IntSet.lookupLT Int
x (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)
lookupGT :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupGT :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupGT Int
x = Coercion Int (Element s)
-> (Coercible Int (Element s) => Maybe (Element s))
-> Maybe (Element s)
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s. Coercion Int (Element s)
unsafeCastElement @s) ((Coercible Int (Element s) => Maybe (Element s))
-> Maybe (Element s))
-> (Coercible Int (Element s) => Maybe (Element s))
-> Maybe (Element s)
forall a b. (a -> b) -> a -> b
$ Maybe Int -> Maybe (Element s)
forall a b. Coercible a b => a -> b
coerce
(Maybe Int -> Maybe (Element s)) -> Maybe Int -> Maybe (Element s)
forall a b. (a -> b) -> a -> b
$ Int -> IntSet -> Maybe Int
IntSet.lookupGT Int
x (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)
lookupLE :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupLE :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupLE Int
x = Coercion Int (Element s)
-> (Coercible Int (Element s) => Maybe (Element s))
-> Maybe (Element s)
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s. Coercion Int (Element s)
unsafeCastElement @s) ((Coercible Int (Element s) => Maybe (Element s))
-> Maybe (Element s))
-> (Coercible Int (Element s) => Maybe (Element s))
-> Maybe (Element s)
forall a b. (a -> b) -> a -> b
$ Maybe Int -> Maybe (Element s)
forall a b. Coercible a b => a -> b
coerce
(Maybe Int -> Maybe (Element s)) -> Maybe Int -> Maybe (Element s)
forall a b. (a -> b) -> a -> b
$ Int -> IntSet -> Maybe Int
IntSet.lookupLE Int
x (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)
lookupGE :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupGE :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupGE Int
x = Coercion Int (Element s)
-> (Coercible Int (Element s) => Maybe (Element s))
-> Maybe (Element s)
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s. Coercion Int (Element s)
unsafeCastElement @s) ((Coercible Int (Element s) => Maybe (Element s))
-> Maybe (Element s))
-> (Coercible Int (Element s) => Maybe (Element s))
-> Maybe (Element s)
forall a b. (a -> b) -> a -> b
$ Maybe Int -> Maybe (Element s)
forall a b. Coercible a b => a -> b
coerce
(Maybe Int -> Maybe (Element s)) -> Maybe Int -> Maybe (Element s)
forall a b. (a -> b) -> a -> b
$ Int -> IntSet -> Maybe Int
IntSet.lookupGE Int
x (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)
null :: forall s. KnownIntSet s => Maybe (EmptyProof 'Int s)
null :: forall s. KnownIntSet s => Maybe (EmptyProof 'Int s)
null
| IntSet -> Bool
IntSet.null (IntSet -> Bool) -> IntSet -> Bool
forall a b. (a -> b) -> a -> b
$ 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 = 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
isSubsetOf
:: forall s t. (KnownIntSet s, KnownIntSet t) => Maybe (SubsetProof 'Int s t)
isSubsetOf :: forall s t.
(KnownIntSet s, KnownIntSet t) =>
Maybe (SubsetProof 'Int s t)
isSubsetOf
| Proxy s -> IntSet
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> IntSet
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` Proxy t -> IntSet
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> IntSet
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t)
= SubsetProof 'Int s t -> Maybe (SubsetProof 'Int s t)
forall a. a -> Maybe a
Just (SubsetProof 'Int s t -> Maybe (SubsetProof 'Int s t))
-> SubsetProof 'Int s t -> Maybe (SubsetProof 'Int s t)
forall a b. (a -> b) -> a -> b
$ (InSet 'Int s :-> InSet 'Int t) -> SubsetProof 'Int s t
forall (f :: Flavor) s r.
(InSet f s :-> InSet f r) -> SubsetProof f s r
SubsetProof Refined (InSet 'Int s) x -> Refined (InSet 'Int t) x
InSet 'Int s :-> InSet 'Int t
forall p q x. Refined p x -> Refined q x
unsafeSubset
| Bool
otherwise = Maybe (SubsetProof 'Int s t)
forall a. Maybe a
Nothing
disjoint
:: forall s t. (KnownIntSet s, KnownIntSet t)
=> Maybe (DisjointProof 'Int s t)
disjoint :: forall s t.
(KnownIntSet s, KnownIntSet t) =>
Maybe (DisjointProof 'Int s t)
disjoint
#if MIN_VERSION_containers(0, 5, 11)
| IntSet -> IntSet -> Bool
IntSet.disjoint (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) (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
| IntSet.null $ IntSet.intersection (reflect $ Proxy @s) (reflect $ Proxy @t)
#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
union
:: forall s t. (KnownIntSet s, KnownIntSet t)
=> SomeIntSetWith (UnionProof 'Int s t)
union :: forall s t.
(KnownIntSet s, KnownIntSet t) =>
SomeIntSetWith (UnionProof 'Int s t)
union = IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> SomeIntSetWith (UnionProof 'Int s t))
-> SomeIntSetWith (UnionProof 'Int s t)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Proxy s -> IntSet
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> IntSet
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) IntSet -> IntSet -> IntSet
`IntSet.union` Proxy t -> IntSet
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> IntSet
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))
\(Proxy s
_ :: Proxy r) -> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r
(UnionProof 'Int s t s -> SomeIntSetWith (UnionProof 'Int s t))
-> UnionProof 'Int s t s -> SomeIntSetWith (UnionProof 'Int s t)
forall a b. (a -> b) -> a -> b
$ ((InSet 'Int s || InSet 'Int t) :-> InSet 'Int s)
-> (forall u.
(InSet 'Int s :-> InSet 'Int u)
-> (InSet 'Int t :-> InSet 'Int u)
-> InSet 'Int s :-> InSet 'Int u)
-> UnionProof 'Int s t s
forall (f :: Flavor) s t r.
((InSet f s || InSet f t) :-> InSet f r)
-> (forall u.
(InSet f s :-> InSet f u)
-> (InSet f t :-> InSet f u) -> InSet f r :-> InSet f u)
-> UnionProof f s t r
UnionProof Refined (InSet 'Int s || InSet 'Int t) x
-> Refined (InSet 'Int s) x
(InSet 'Int s || InSet 'Int t) :-> InSet 'Int s
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Int s :-> InSet 'Int u)
-> (InSet 'Int t :-> InSet 'Int u)
-> Refined (InSet 'Int s) x
-> Refined (InSet 'Int u) x
(InSet 'Int s :-> InSet 'Int u)
-> (InSet 'Int t :-> InSet 'Int u) -> InSet 'Int s :-> InSet 'Int u
forall u.
(InSet 'Int s :-> InSet 'Int u)
-> (InSet 'Int t :-> InSet 'Int u) -> InSet 'Int s :-> InSet 'Int u
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2
difference
:: forall s t. (KnownIntSet s, KnownIntSet t)
=> SomeIntSetWith (DifferenceProof 'Int s t)
difference :: forall s t.
(KnownIntSet s, KnownIntSet t) =>
SomeIntSetWith (DifferenceProof 'Int s t)
difference = IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> SomeIntSetWith (DifferenceProof 'Int s t))
-> SomeIntSetWith (DifferenceProof 'Int s t)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Proxy s -> IntSet
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> IntSet
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) IntSet -> IntSet -> IntSet
`IntSet.difference` Proxy t -> IntSet
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> IntSet
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))
\(Proxy s
_ :: Proxy r) -> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r
(DifferenceProof 'Int s t s
-> SomeIntSetWith (DifferenceProof 'Int s t))
-> DifferenceProof 'Int s t s
-> SomeIntSetWith (DifferenceProof 'Int s t)
forall a b. (a -> b) -> a -> b
$ (InSet 'Int s :-> InSet 'Int s)
-> (forall u.
(InSet 'Int u :-> InSet 'Int s)
-> (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 s))
-> DifferenceProof 'Int s t s
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 s) x -> Refined (InSet 'Int s) x
InSet 'Int s :-> InSet 'Int s
forall p q x. Refined p x -> Refined q x
unsafeSubset (\InSet 'Int u :-> InSet 'Int s
f InSet 'Int u :-> InSet 'Int t
g -> (InSet 'Int u :-> InSet 'Int s)
-> (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 s) x
InSet 'Int u :-> InSet 'Int s
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 s) x
InSet 'Int s :-> (InSet 'Int t || InSet 'Int s)
forall p q x. Refined p x -> Refined q x
unsafeSubset
intersection
:: forall s t. (KnownIntSet s, KnownIntSet t)
=> SomeIntSetWith (IntersectionProof 'Int s t)
intersection :: forall s t.
(KnownIntSet s, KnownIntSet t) =>
SomeIntSetWith (IntersectionProof 'Int s t)
intersection
= IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> SomeIntSetWith (IntersectionProof 'Int s t))
-> SomeIntSetWith (IntersectionProof 'Int s t)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Proxy s -> IntSet
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> IntSet
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) IntSet -> IntSet -> IntSet
`IntSet.intersection` Proxy t -> IntSet
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> IntSet
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))
\(Proxy s
_ :: Proxy r) -> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r
(IntersectionProof 'Int s t s
-> SomeIntSetWith (IntersectionProof 'Int s t))
-> IntersectionProof 'Int s t s
-> SomeIntSetWith (IntersectionProof 'Int s t)
forall a b. (a -> b) -> a -> b
$ (InSet 'Int s :-> (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 s)
-> IntersectionProof 'Int s t s
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 s) x
-> Refined (InSet 'Int s && InSet 'Int t) x
InSet 'Int s :-> (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 s) x
(InSet 'Int u :-> InSet 'Int s)
-> (InSet 'Int u :-> InSet 'Int t) -> InSet 'Int u :-> InSet 'Int s
forall u.
(InSet 'Int u :-> InSet 'Int s)
-> (InSet 'Int u :-> InSet 'Int t) -> InSet 'Int u :-> InSet 'Int s
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2
filter
:: forall s. KnownIntSet s
=> (Element s -> Bool) -> SomeIntSetWith (SupersetProof 'Int s)
filter :: forall s.
KnownIntSet s =>
(Element s -> Bool) -> SomeIntSetWith (SupersetProof 'Int s)
filter Element s -> Bool
p = IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> SomeIntSetWith (SupersetProof 'Int s))
-> SomeIntSetWith (SupersetProof 'Int s)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify ((Int -> Bool) -> IntSet -> IntSet
IntSet.filter (Element s -> Bool
p (Element s -> Bool) -> (Int -> Element s) -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Element s
forall s. Int -> Element s
unsafeElement) (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ 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)
\(Proxy s
_ :: Proxy r) -> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r (SupersetProof 'Int s s -> SomeIntSetWith (SupersetProof 'Int s))
-> SupersetProof 'Int s s -> SomeIntSetWith (SupersetProof 'Int s)
forall a b. (a -> b) -> a -> b
$ (InSet 'Int s :-> InSet 'Int s) -> SupersetProof 'Int s s
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Int s) x -> Refined (InSet 'Int s) x
InSet 'Int s :-> InSet 'Int s
forall p q x. Refined p x -> Refined q x
unsafeSubset
partition
:: forall s. KnownIntSet s
=> (Element s -> Bool) -> Some2IntSetWith (PartitionProof 'Int s Int)
partition :: forall s.
KnownIntSet s =>
(Element s -> Bool) -> Some2IntSetWith (PartitionProof 'Int s Int)
partition Element s -> Bool
p = case (Int -> Bool) -> IntSet -> (IntSet, IntSet)
IntSet.partition (Element s -> Bool
p (Element s -> Bool) -> (Int -> Element s) -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Element s
forall s. Int -> Element s
unsafeElement) (IntSet -> (IntSet, IntSet)) -> IntSet -> (IntSet, IntSet)
forall a b. (a -> b) -> a -> b
$ 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 of
(IntSet
r, IntSet
q) -> IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> Some2IntSetWith (PartitionProof 'Int s Int))
-> Some2IntSetWith (PartitionProof 'Int s Int)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
r \(Proxy s
_ :: Proxy r) -> IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> Some2IntSetWith (PartitionProof 'Int s Int))
-> Some2IntSetWith (PartitionProof 'Int s Int)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
q \(Proxy s
_ :: Proxy q)
-> forall s t (p :: * -> * -> *).
(KnownIntSet s, KnownIntSet t) =>
p s t -> Some2IntSetWith p
Some2IntSetWith @s @r (PartitionProof 'Int s Int s s
-> Some2IntSetWith (PartitionProof 'Int s Int))
-> PartitionProof 'Int s Int s s
-> Some2IntSetWith (PartitionProof 'Int s Int)
forall a b. (a -> b) -> a -> b
$ (Element s -> Either (Element s) (Refined (InSet 'Int s) Int))
-> ((InSet 'Int s || InSet 'Int s) :-> InSet 'Int s)
-> (forall t.
(InSet 'Int s :-> InSet 'Int t)
-> (InSet 'Int s :-> InSet 'Int t)
-> InSet 'Int s :-> InSet 'Int t)
-> (forall t.
(InSet 'Int t :-> InSet 'Int s)
-> (InSet 'Int t :-> InSet 'Int s)
-> forall u x.
Refined (InSet 'Int t) x -> Refined (InSet 'Int u) x)
-> PartitionProof 'Int s Int s s
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 \Element s
x -> if Element s -> Bool
p Element s
x
then Element s -> Either (Element s) (Refined (InSet 'Int s) Int)
forall a b. a -> Either a b
Left (Element s -> Either (Element s) (Refined (InSet 'Int s) Int))
-> Element s -> Either (Element s) (Refined (InSet 'Int s) Int)
forall a b. (a -> b) -> a -> b
$ Int -> Element s
forall s. Int -> Element s
unsafeElement (Int -> Element s) -> Int -> Element s
forall a b. (a -> b) -> a -> b
$ Element s -> Int
forall {k} (p :: k) x. Refined p x -> x
unrefine Element s
x
else Refined (InSet 'Int s) Int
-> Either (Element s) (Refined (InSet 'Int s) Int)
forall a b. b -> Either a b
Right (Refined (InSet 'Int s) Int
-> Either (Element s) (Refined (InSet 'Int s) Int))
-> Refined (InSet 'Int s) Int
-> Either (Element s) (Refined (InSet 'Int s) Int)
forall a b. (a -> b) -> a -> b
$ Int -> Refined (InSet 'Int s) Int
forall s. Int -> Element s
unsafeElement (Int -> Refined (InSet 'Int s) Int)
-> Int -> Refined (InSet 'Int s) Int
forall a b. (a -> b) -> a -> b
$ Element s -> Int
forall {k} (p :: k) x. Refined p x -> x
unrefine Element s
x
Refined (InSet 'Int s || InSet 'Int s) x
-> Refined (InSet 'Int s) x
(InSet 'Int s || InSet 'Int s) :-> InSet 'Int s
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Int s :-> InSet 'Int t)
-> (InSet 'Int s :-> InSet 'Int t)
-> Refined (InSet 'Int s) x
-> Refined (InSet 'Int t) x
(InSet 'Int s :-> InSet 'Int t)
-> (InSet 'Int s :-> InSet 'Int t) -> InSet 'Int s :-> InSet 'Int t
forall t.
(InSet 'Int s :-> InSet 'Int t)
-> (InSet 'Int s :-> 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 s
f InSet 'Int t :-> InSet 'Int s
g -> (InSet 'Int t :-> InSet 'Int s)
-> (InSet 'Int t :-> InSet 'Int s) -> 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 s) x
InSet 'Int t :-> InSet 'Int s
g
spanAntitone
:: forall s. KnownIntSet s
=> (Element s -> Bool) -> Some2IntSetWith (PartialPartitionProof 'Int s)
spanAntitone :: forall s.
KnownIntSet s =>
(Element s -> Bool)
-> Some2IntSetWith (PartialPartitionProof 'Int s)
spanAntitone Element s -> Bool
p =
#if MIN_VERSION_containers(0, 6, 7)
case (Int -> Bool) -> IntSet -> (IntSet, IntSet)
IntSet.spanAntitone (Element s -> Bool
p (Element s -> Bool) -> (Int -> Element s) -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Element s
forall s. Int -> Element s
unsafeElement) (IntSet -> (IntSet, IntSet)) -> IntSet -> (IntSet, IntSet)
forall a b. (a -> b) -> a -> b
$ 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 of
(IntSet
r, IntSet
q)
#else
case List.span (p . unsafeElement)
$ IntSet.toAscList $ reflect $ Proxy @s of
(rs, qs)
| let r = IntSet.fromDistinctAscList rs
, let q = IntSet.fromDistinctAscList qs
#endif
-> IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> Some2IntSetWith (PartialPartitionProof 'Int s))
-> Some2IntSetWith (PartialPartitionProof 'Int s)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
r \(Proxy s
_ :: Proxy r) -> IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> Some2IntSetWith (PartialPartitionProof 'Int s))
-> Some2IntSetWith (PartialPartitionProof 'Int s)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
q \(Proxy s
_ :: Proxy q)
-> forall s t (p :: * -> * -> *).
(KnownIntSet s, KnownIntSet t) =>
p s t -> Some2IntSetWith p
Some2IntSetWith @r @q (PartialPartitionProof 'Int s s s
-> Some2IntSetWith (PartialPartitionProof 'Int s))
-> PartialPartitionProof 'Int s s s
-> Some2IntSetWith (PartialPartitionProof 'Int s)
forall a b. (a -> b) -> a -> b
$ ((InSet 'Int s || InSet 'Int s) :-> InSet 'Int s)
-> (forall t.
(InSet 'Int s :-> InSet 'Int t)
-> (InSet 'Int s :-> InSet 'Int t)
-> InSet 'Int s :-> InSet 'Int t)
-> (forall t.
(InSet 'Int t :-> InSet 'Int s)
-> (InSet 'Int t :-> InSet 'Int s)
-> forall u x.
Refined (InSet 'Int t) x -> Refined (InSet 'Int u) x)
-> PartialPartitionProof 'Int s s s
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 s || InSet 'Int s) x
-> Refined (InSet 'Int s) x
(InSet 'Int s || InSet 'Int s) :-> InSet 'Int s
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Int s :-> InSet 'Int t)
-> (InSet 'Int s :-> InSet 'Int t)
-> Refined (InSet 'Int s) x
-> Refined (InSet 'Int t) x
(InSet 'Int s :-> InSet 'Int t)
-> (InSet 'Int s :-> InSet 'Int t) -> InSet 'Int s :-> InSet 'Int t
forall t.
(InSet 'Int s :-> InSet 'Int t)
-> (InSet 'Int s :-> 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 s
f InSet 'Int t :-> InSet 'Int s
g -> (InSet 'Int t :-> InSet 'Int s)
-> (InSet 'Int t :-> InSet 'Int s) -> 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 s) x
InSet 'Int t :-> InSet 'Int s
g
splitMember
:: forall s. KnownIntSet s
=> Int -> Some2IntSetWith (SplitProof 'Int s (Element s))
splitMember :: forall s.
KnownIntSet s =>
Int -> Some2IntSetWith (SplitProof 'Int s (Element s))
splitMember Int
x = case Int -> IntSet -> (IntSet, Bool, IntSet)
IntSet.splitMember Int
x (IntSet -> (IntSet, Bool, IntSet))
-> IntSet -> (IntSet, Bool, IntSet)
forall a b. (a -> b) -> a -> b
$ 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 of
(IntSet
r, Bool
m, IntSet
q) -> IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> Some2IntSetWith (SplitProof 'Int s (Element s)))
-> Some2IntSetWith (SplitProof 'Int s (Element s))
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
r \(Proxy s
_ :: Proxy r) -> IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> Some2IntSetWith (SplitProof 'Int s (Element s)))
-> Some2IntSetWith (SplitProof 'Int s (Element s))
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
q \(Proxy s
_ :: Proxy q)
-> forall s t (p :: * -> * -> *).
(KnownIntSet s, KnownIntSet t) =>
p s t -> Some2IntSetWith p
Some2IntSetWith @r @q (SplitProof 'Int s (Element s) s s
-> Some2IntSetWith (SplitProof 'Int s (Element s)))
-> SplitProof 'Int s (Element s) s s
-> Some2IntSetWith (SplitProof 'Int s (Element s))
forall a b. (a -> b) -> a -> b
$ Maybe (Element s)
-> ((InSet 'Int s || InSet 'Int s) :-> InSet 'Int s)
-> (forall t.
(InSet 'Int t :-> InSet 'Int s)
-> (InSet 'Int t :-> InSet 'Int s)
-> forall u x.
Refined (InSet 'Int t) x -> Refined (InSet 'Int u) x)
-> SplitProof 'Int s (Element s) s s
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
(if Bool
m then Element s -> Maybe (Element s)
forall a. a -> Maybe a
Just (Int -> Element s
forall s. Int -> Element s
unsafeElement Int
x) else Maybe (Element s)
forall a. Maybe a
Nothing)
Refined (InSet 'Int s || InSet 'Int s) x
-> Refined (InSet 'Int s) x
(InSet 'Int s || InSet 'Int s) :-> InSet 'Int s
forall p q x. Refined p x -> Refined q x
unsafeSubset \InSet 'Int t :-> InSet 'Int s
f InSet 'Int t :-> InSet 'Int s
g -> (InSet 'Int t :-> InSet 'Int s)
-> (InSet 'Int t :-> InSet 'Int s) -> 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 s) x
InSet 'Int t :-> InSet 'Int s
g
map
:: forall s. KnownIntSet s
=> (Element s -> Int) -> SomeIntSetWith (MapProof 'Int s Int Int)
map :: forall s.
KnownIntSet s =>
(Element s -> Int) -> SomeIntSetWith (MapProof 'Int s Int Int)
map Element s -> Int
f = IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> SomeIntSetWith (MapProof 'Int s Int Int))
-> SomeIntSetWith (MapProof 'Int s Int Int)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (IntMap (Element s) -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet IntMap (Element s)
m) \(Proxy s
_ :: Proxy r) -> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r
(MapProof 'Int s Int Int s
-> SomeIntSetWith (MapProof 'Int s Int Int))
-> MapProof 'Int s Int Int s
-> SomeIntSetWith (MapProof 'Int s Int Int)
forall a b. (a -> b) -> a -> b
$ (Element s -> Refined (InSet 'Int s) Int)
-> (Refined (InSet 'Int s) Int -> Element s)
-> MapProof 'Int s Int Int s
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 (Int -> Refined (InSet 'Int s) Int
forall s. Int -> Element s
unsafeElement (Int -> Refined (InSet 'Int s) Int)
-> (Element s -> Int) -> Element s -> Refined (InSet 'Int s) Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Element s -> Int
f) \Refined (InSet 'Int s) Int
y -> case Int -> IntMap (Element s) -> Maybe (Element s)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Refined (InSet 'Int s) Int -> Int
forall {k} (p :: k) x. Refined p x -> x
unrefine Refined (InSet 'Int s) Int
y) IntMap (Element s)
m of
Maybe (Element s)
Nothing -> [Char] -> Element s
forall a. HasCallStack => [Char] -> a
error [Char]
"map: bug: Data.IntSet.Refined has been subverted"
Just Element s
x -> Element s
x
where
!m :: IntMap (Element s)
m = [(Int, Element s)] -> IntMap (Element s)
forall a. [(Int, a)] -> IntMap a
IntMap.fromList
[ (Int
y, Int -> Element s
forall s. Int -> Element s
unsafeElement Int
x)
| Int
x <- IntSet -> [Int]
IntSet.toList (IntSet -> [Int]) -> IntSet -> [Int]
forall a b. (a -> b) -> a -> b
$ 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
, let !y :: Int
y = Element s -> Int
f (Element s -> Int) -> Element s -> Int
forall a b. (a -> b) -> a -> b
$ Int -> Element s
forall s. Int -> Element s
unsafeElement Int
x
]
foldMap :: forall s m. (KnownIntSet s, Monoid m) => (Element s -> m) -> m
foldMap :: forall s m. (KnownIntSet s, Monoid m) => (Element s -> m) -> m
foldMap Element s -> m
f = IntSet -> m
go (IntSet -> m) -> IntSet -> m
forall a b. (a -> b) -> a -> b
$ 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
where
go :: IntSet -> m
go IntSet
s = case IntSet -> [IntSet]
IntSet.splitRoot IntSet
s of
[IntSet
s'] -> (Int -> m) -> [Int] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap (Element s -> m
f (Element s -> m) -> (Int -> Element s) -> Int -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Element s
forall s. Int -> Element s
unsafeElement) ([Int] -> m) -> [Int] -> m
forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IntSet.toAscList IntSet
s'
[IntSet]
xs -> (IntSet -> m) -> [IntSet] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap IntSet -> m
go [IntSet]
xs
foldr :: forall s a. KnownIntSet s => (Element s -> a -> a) -> a -> a
foldr :: forall s a. KnownIntSet s => (Element s -> a -> a) -> a -> a
foldr Element s -> a -> a
f a
z = (Int -> a -> a) -> a -> IntSet -> a
forall b. (Int -> b -> b) -> b -> IntSet -> b
IntSet.foldr (Element s -> a -> a
f (Element s -> a -> a) -> (Int -> Element s) -> Int -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Element s
forall s. Int -> Element s
unsafeElement) a
z (IntSet -> a) -> IntSet -> a
forall a b. (a -> b) -> a -> b
$ 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
foldl :: forall s a. KnownIntSet s => (a -> Element s -> a) -> a -> a
foldl :: forall s a. KnownIntSet s => (a -> Element s -> a) -> a -> a
foldl a -> Element s -> a
f a
z = (a -> Int -> a) -> a -> IntSet -> a
forall a. (a -> Int -> a) -> a -> IntSet -> a
IntSet.foldl (((Element s -> a) -> (Int -> Element s) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Element s
forall s. Int -> Element s
unsafeElement) ((Element s -> a) -> Int -> a)
-> (a -> Element s -> a) -> a -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Element s -> a
f) a
z (IntSet -> a) -> IntSet -> a
forall a b. (a -> b) -> a -> b
$ 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
foldr' :: forall s a. KnownIntSet s => (Element s -> a -> a) -> a -> a
foldr' :: forall s a. KnownIntSet s => (Element s -> a -> a) -> a -> a
foldr' Element s -> a -> a
f a
z = (Int -> a -> a) -> a -> IntSet -> a
forall b. (Int -> b -> b) -> b -> IntSet -> b
IntSet.foldr' (Element s -> a -> a
f (Element s -> a -> a) -> (Int -> Element s) -> Int -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Element s
forall s. Int -> Element s
unsafeElement) a
z (IntSet -> a) -> IntSet -> a
forall a b. (a -> b) -> a -> b
$ 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
foldl' :: forall s a. KnownIntSet s => (a -> Element s -> a) -> a -> a
foldl' :: forall s a. KnownIntSet s => (a -> Element s -> a) -> a -> a
foldl' a -> Element s -> a
f a
z = (a -> Int -> a) -> a -> IntSet -> a
forall a. (a -> Int -> a) -> a -> IntSet -> a
IntSet.foldl' (((Element s -> a) -> (Int -> Element s) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Element s
forall s. Int -> Element s
unsafeElement) ((Element s -> a) -> Int -> a)
-> (a -> Element s -> a) -> a -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Element s -> a
f) a
z (IntSet -> a) -> IntSet -> a
forall a b. (a -> b) -> a -> b
$ 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
minView
:: forall s. KnownIntSet s
=> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s))
minView :: forall s.
KnownIntSet s =>
Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s))
minView = case IntSet -> Maybe (Int, IntSet)
IntSet.minView (IntSet -> Maybe (Int, IntSet)) -> IntSet -> Maybe (Int, IntSet)
forall a b. (a -> b) -> a -> b
$ 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 of
Maybe (Int, IntSet)
Nothing -> EmptyProof 'Int s
-> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s))
forall a b. a -> Either a b
Left (EmptyProof 'Int s
-> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s)))
-> EmptyProof 'Int s
-> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof '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
Just (Int
x, IntSet
xs) -> (Element s, SomeIntSetWith (SupersetProof 'Int s))
-> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s))
forall a b. b -> Either a b
Right ((Element s, SomeIntSetWith (SupersetProof 'Int s))
-> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s)))
-> (Element s, SomeIntSetWith (SupersetProof 'Int s))
-> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s))
forall a b. (a -> b) -> a -> b
$ (Int -> Element s
forall s. Int -> Element s
unsafeElement Int
x,) (SomeIntSetWith (SupersetProof 'Int s)
-> (Element s, SomeIntSetWith (SupersetProof 'Int s)))
-> SomeIntSetWith (SupersetProof 'Int s)
-> (Element s, SomeIntSetWith (SupersetProof 'Int s))
forall a b. (a -> b) -> a -> b
$ IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> SomeIntSetWith (SupersetProof 'Int s))
-> SomeIntSetWith (SupersetProof 'Int s)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
xs \(Proxy s
_ :: Proxy r)
-> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r (SupersetProof 'Int s s -> SomeIntSetWith (SupersetProof 'Int s))
-> SupersetProof 'Int s s -> SomeIntSetWith (SupersetProof 'Int s)
forall a b. (a -> b) -> a -> b
$ (InSet 'Int s :-> InSet 'Int s) -> SupersetProof 'Int s s
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Int s) x -> Refined (InSet 'Int s) x
InSet 'Int s :-> InSet 'Int s
forall p q x. Refined p x -> Refined q x
unsafeSubset
maxView
:: forall s. KnownIntSet s
=> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s))
maxView :: forall s.
KnownIntSet s =>
Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s))
maxView = case IntSet -> Maybe (Int, IntSet)
IntSet.maxView (IntSet -> Maybe (Int, IntSet)) -> IntSet -> Maybe (Int, IntSet)
forall a b. (a -> b) -> a -> b
$ 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 of
Maybe (Int, IntSet)
Nothing -> EmptyProof 'Int s
-> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s))
forall a b. a -> Either a b
Left (EmptyProof 'Int s
-> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s)))
-> EmptyProof 'Int s
-> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof '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
Just (Int
x, IntSet
xs) -> (Element s, SomeIntSetWith (SupersetProof 'Int s))
-> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s))
forall a b. b -> Either a b
Right ((Element s, SomeIntSetWith (SupersetProof 'Int s))
-> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s)))
-> (Element s, SomeIntSetWith (SupersetProof 'Int s))
-> Either
(EmptyProof 'Int s)
(Element s, SomeIntSetWith (SupersetProof 'Int s))
forall a b. (a -> b) -> a -> b
$ (Int -> Element s
forall s. Int -> Element s
unsafeElement Int
x,) (SomeIntSetWith (SupersetProof 'Int s)
-> (Element s, SomeIntSetWith (SupersetProof 'Int s)))
-> SomeIntSetWith (SupersetProof 'Int s)
-> (Element s, SomeIntSetWith (SupersetProof 'Int s))
forall a b. (a -> b) -> a -> b
$ IntSet
-> (forall s.
Reifies s IntSet =>
Proxy s -> SomeIntSetWith (SupersetProof 'Int s))
-> SomeIntSetWith (SupersetProof 'Int s)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
xs \(Proxy s
_ :: Proxy r)
-> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r (SupersetProof 'Int s s -> SomeIntSetWith (SupersetProof 'Int s))
-> SupersetProof 'Int s s -> SomeIntSetWith (SupersetProof 'Int s)
forall a b. (a -> b) -> a -> b
$ (InSet 'Int s :-> InSet 'Int s) -> SupersetProof 'Int s s
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Int s) x -> Refined (InSet 'Int s) x
InSet 'Int s :-> InSet 'Int s
forall p q x. Refined p x -> Refined q x
unsafeSubset
toList :: forall s. KnownIntSet s => [Element s]
toList :: forall s. KnownIntSet s => [Element s]
toList = Coercion Int (Element s)
-> (Coercible Int (Element s) => [Element s]) -> [Element s]
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s. Coercion Int (Element s)
unsafeCastElement @s) ((Coercible Int (Element s) => [Element s]) -> [Element s])
-> (Coercible Int (Element s) => [Element s]) -> [Element s]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Element s]
forall a b. Coercible a b => a -> b
coerce
([Int] -> [Element s]) -> [Int] -> [Element s]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IntSet.toAscList (IntSet -> [Int]) -> IntSet -> [Int]
forall a b. (a -> b) -> a -> b
$ 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
toDescList :: forall s. KnownIntSet s => [Element s]
toDescList :: forall s. KnownIntSet s => [Element s]
toDescList = Coercion Int (Element s)
-> (Coercible Int (Element s) => [Element s]) -> [Element s]
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s. Coercion Int (Element s)
unsafeCastElement @s) ((Coercible Int (Element s) => [Element s]) -> [Element s])
-> (Coercible Int (Element s) => [Element s]) -> [Element s]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Element s]
forall a b. Coercible a b => a -> b
coerce
([Int] -> [Element s]) -> [Int] -> [Element s]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IntSet.toDescList (IntSet -> [Int]) -> IntSet -> [Int]
forall a b. (a -> b) -> a -> b
$ 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
asSet :: forall s. KnownIntSet s => Set s Int
asSet :: forall s. KnownIntSet s => Set s Int
asSet = Set s Int
forall s. KnownIntSet s => Set s Int
intSet2Set
asHashSet :: forall s. KnownIntSet s => HashSet s Int
asHashSet :: forall s. KnownIntSet s => HashSet s Int
asHashSet = HashSet s Int
forall s. KnownIntSet s => HashSet s Int
intSet2HashSet
castElement
:: forall s t a.
(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) a) (Refined (InSet 'Int t) a)
castElement :: forall s t a.
(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) a) (Refined (InSet 'Int t) a)
castElement = (InSet 'Int s :-> InSet 'Int t)
-> (InSet 'Int t :-> InSet 'Int s)
-> Coercion (Refined (InSet 'Int s) a) (Refined (InSet 'Int t) a)
forall a p q.
(p :-> q) -> (q :-> p) -> Coercion (Refined p a) (Refined q a)
castRefined
cast
:: forall s t. (forall x. Coercion
(Refined (InSet 'Int s) x)
(Refined (InSet 'Int t) x))
-> Coercion (IntSet s) (IntSet t)
cast :: forall s t.
(forall x.
Coercion (Refined (InSet 'Int s) x) (Refined (InSet 'Int t) x))
-> Coercion (IntSet s) (IntSet t)
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
#if MIN_VERSION_base(4, 15, 0)
= case forall {k} (a :: k) (b :: k). UnsafeEquality a b
forall a b. UnsafeEquality a b
unsafeEqualityProof @s @t of UnsafeEquality s t
UnsafeRefl -> Coercion (IntSet s) (IntSet t)
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
#else
= repr $ unsafeCoerce Refl
#endif