{-# LANGUAGE CPP #-}
-- | This module implements a way of tracking the contents of an
-- 'Data.IntSet.IntSet' at the type level, and provides utilities for
-- manipulating such sets.
--
-- The contents of a set are associated with a type parameter, e.g. @s@, so that
-- whenever you see the same type parameter, you know you are working with the
-- same set. The type @s@ itself has no internal structure, rather it is merely
-- a skolem type variable (rank-2 polymorphism 'Control.Monad.ST.runST' trick)
-- introduced by "Data.Reflection".
module Data.IntSet.Refined
  (
  -- * Set type
    KnownIntSet
  , IntSet
  -- * Refinement type
  , InSet(..)
  , Flavor(Int)
  , Element
  , revealPredicate
  -- * Existentials and common proofs
  , SomeIntSet(..)
  , withIntSet
  , SomeIntSetWith(..)
  , withIntSetWith
  , Some2IntSetWith(..)
  , with2IntSetWith
  , (:->)
  , SupersetProof(..)
  , EmptyProof(..)
  -- * Construction
  , empty
  , singleton
  , SingletonProof(..)
  , fromIntSet
  , fromTraversable
  , FromTraversableProof(..)
  -- * Insertion
  , insert
  , InsertProof(..)
  -- * Deletion
  , delete
  -- * Query
  , member
  , lookupLT
  , lookupGT
  , lookupLE
  , lookupGE
  , null
  , isSubsetOf
  , SubsetProof(..)
  , disjoint
  , DisjointProof(..)
  -- * Combine
  , union
  , UnionProof(..)
  , difference
  , DifferenceProof(..)
  , intersection
  , IntersectionProof(..)
  -- * Filter
  , filter
  , partition
  , PartitionProof(..)
  , spanAntitone
  , PartialPartitionProof(..)
  , splitMember
  , SplitProof(..)
  -- * Map
  , map
  , MapProof(..)
  -- * Folds
  , foldMap
  , foldr
  , foldl
  , foldr'
  , foldl'
  -- * Min/Max
  , minView
  , maxView
  -- * Conversion
  , toList
  , toDescList
  , asSet
  , asHashSet
  -- * Casts
  , 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


-- | To use "Refined" machinery that uses the 'Predicate' typeclass you will
-- need to pattern match on this 'Dict'.
--
-- The reason is that in the default /fast/ implementation of reflection, we
-- don't have @'Data.Typeable.Typeable' s@, which "Refined" wants for
-- pretty-printing exceptions. We /can/ provide @'Data.TypeableTypeable' s@, but
-- at the cost of using the /slow/ implementation of reflection.
revealPredicate
  :: forall s. KnownIntSet s => Dict (Predicate (InSet 'Int s) Int)
revealPredicate :: forall s. KnownIntSet s => Dict (Predicate (InSet 'Int s) Int)
revealPredicate = forall a r.
Typeable a =>
a -> (forall s. (Typeable s, Reifies s a) => Proxy s -> r) -> r
reifyTypeable (forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect (forall {k} (t :: k). Proxy t
Proxy @s))
  \(Proxy s
_ :: Proxy s') ->
    forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect (forall {k} (t :: k). Proxy t
Proxy @s') seq :: forall a b. a -> b -> b
`seq`
    --  ^ Work around https://github.com/ekmett/reflection/issues/54
      case forall a b. a -> b
unsafeCoerce forall {k} (a :: k). a :~: a
Refl :: s :~: s' of
        s :~: s
Refl -> forall (a :: Constraint). a => Dict a
Dict

-- | @'Element' s@ is an t'Int' that has been verified to be an element of @s@.
--
-- Thus, @'Element' 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 'Element's (however see
-- 'revealPredicate').
--
-- The underlying t'Int' can be obtained with 'unrefine'. An t'Int' can be
-- validated into an @'Element' s@ with 'member'.
type Element s = Refined (InSet 'Int s) Int

unsafeCastElement :: forall s. Coercion Int (Element s)
unsafeCastElement :: forall s. Coercion Int (Element s)
unsafeCastElement = forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined

unsafeElement :: Int -> Element s
unsafeElement :: forall s. Int -> Element s
unsafeElement = forall a b. Coercion a b -> a -> b
coerceWith forall s. Coercion Int (Element s)
unsafeCastElement

-- | An existential wrapper for an as-yet-unknown set. Pattern maching on it
-- gives you a way to refer to the set, e.g.
--
-- @
-- case 'fromIntSet' ... of
--   'SomeIntSet' \@s _ -> doSomethingWith \@s
--
-- case 'fromIntSet' ... of
--   'SomeIntSet' (_ :: 'Proxy#' s) -> doSomethingWith \@s
-- @
data SomeIntSet where
  SomeIntSet :: forall s. KnownIntSet s => Proxy# s -> SomeIntSet

-- | Apply an unknown set to a continuation that can accept any set. This gives
-- you a way to refer to the set (the parameter @s@), e.g.:
--
-- @
-- 'withIntSet' ('fromIntSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s
-- @
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 = forall s. KnownIntSet s => Proxy s -> r
k forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s

-- | Construct a set from a regular 'Data.IntSet.IntSet'.
fromIntSet :: IntSet.IntSet -> SomeIntSet
fromIntSet :: IntSet -> SomeIntSet
fromIntSet IntSet
s = 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 forall {k} (a :: k). Proxy# a
proxy#

-- | An existential wrapper for an as-yet-unknown set, 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@). Most functions will return a set in this way,
-- together with a proof that somehow relates the set to the function's inputs.
data SomeIntSetWith p where
  SomeIntSetWith :: forall s p. KnownIntSet s => !(p s) -> SomeIntSetWith p

-- | Apply an unknown set with proof to a continuation that can accept any set
-- satisfying the proof. This gives you a way to refer to the set (the parameter
-- @s@).
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 = forall s. KnownIntSet s => p s -> r
k p s
p

-- | An existential wrapper for an as-yet-unknown pair of sets, together with
-- a proof of some fact @p@ relating them.
data Some2IntSetWith p where
  Some2IntSetWith
    :: forall s t p. (KnownIntSet s, KnownIntSet t)
    => !(p s t) -> Some2IntSetWith p

-- | Apply a pair of unknown sets with proof to a continuation that can accept
-- any pair of sets satisfying the proof. This gives you a way to refer to the
-- sets (the parameters @s@ and @t@).
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 = forall s t. (KnownIntSet s, KnownIntSet t) => p s t -> r
k p s t
p

-- | An empty set.
empty :: SomeIntSetWith (EmptyProof 'Int)
empty :: SomeIntSetWith (EmptyProof 'Int)
empty = 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 forall a b. (a -> b) -> a -> b
$ forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof forall p q. p :-> q
unsafeSubset


-- | Create a set with a single element.
singleton :: Int -> SomeIntSetWith (SingletonProof 'Int Int)
singleton :: Int -> SomeIntSetWith (SingletonProof 'Int Int)
singleton Int
x = 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 forall a b. (a -> b) -> a -> b
$ forall (f :: Flavor) a r.
Refined (InSet f r) a -> SingletonProof f a r
SingletonProof forall a b. (a -> b) -> a -> b
$ forall s. Int -> Element s
unsafeElement Int
x

-- | Create a set from the elements of an arbitrary traversable.
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 = 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 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
    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) = 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', forall s. Int -> Element s
unsafeElement Int
x))
      IntSet
IntSet.empty
      t Int
xs

-- | Insert an element in a set.
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 = forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Int -> IntSet -> IntSet
IntSet.insert Int
x forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s) \(Proxy s
_ :: Proxy r)
  -> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r 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 -> Element s
unsafeElement Int
x) forall p q. p :-> q
unsafeSubset

-- | Delete an element from a set.
delete :: forall s. KnownIntSet s
  => Int -> SomeIntSetWith (SupersetProof 'Int s)
delete :: forall s.
KnownIntSet s =>
Int -> SomeIntSetWith (SupersetProof 'Int s)
delete Int
x = forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Int -> IntSet -> IntSet
IntSet.delete Int
x forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s) \(Proxy s
_ :: Proxy r)
  -> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @s 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

-- | If an element is in the set, return the proof that it is.
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` forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect (forall {k} (t :: k). Proxy t
Proxy @s) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall s. Int -> Element s
unsafeElement Int
x
  | Bool
otherwise = forall a. Maybe a
Nothing

-- | Find the largest element smaller than the given one.
lookupLT :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupLT :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupLT Int
x = forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s. Coercion Int (Element s)
unsafeCastElement @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
$ Int -> IntSet -> Maybe Int
IntSet.lookupLT Int
x (forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s)

-- | Find the smallest element greater than the given one.
lookupGT :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupGT :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupGT Int
x = forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s. Coercion Int (Element s)
unsafeCastElement @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
$ Int -> IntSet -> Maybe Int
IntSet.lookupGT Int
x (forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s)

-- | Find the largest element smaller or equal to the given one.
lookupLE :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupLE :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupLE Int
x = forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s. Coercion Int (Element s)
unsafeCastElement @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
$ Int -> IntSet -> Maybe Int
IntSet.lookupLE Int
x (forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s)

-- | Find the smallest element greater or equal to the given one.
lookupGE :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupGE :: forall s. KnownIntSet s => Int -> Maybe (Element s)
lookupGE Int
x = forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s. Coercion Int (Element s)
unsafeCastElement @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
$ Int -> IntSet -> Maybe Int
IntSet.lookupGE Int
x (forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s)

-- | If the set is empty, return the proof that it is.
null :: forall s. KnownIntSet s => Maybe (EmptyProof 'Int s)
null :: forall s. KnownIntSet s => Maybe (EmptyProof 'Int s)
null
  | IntSet -> Bool
IntSet.null forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof forall p q. p :-> q
unsafeSubset
  | Bool
otherwise = forall a. Maybe a
Nothing

-- | If @s@ is a subset of @t@ (or is equal to), return a proof of that.
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
  | forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect (forall {k} (t :: k). Proxy t
Proxy @s) IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect (forall {k} (t :: k). Proxy t
Proxy @t)
  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (f :: Flavor) s r.
(InSet f s :-> InSet f r) -> SubsetProof f s r
SubsetProof forall p q. p :-> q
unsafeSubset
  | Bool
otherwise = forall a. Maybe a
Nothing

-- | If @s@ and @t@ are disjoint (i.e. their intersection is empty), return a
-- proof of that.
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 (forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s) (forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @t)
#else
  | IntSet.null $ IntSet.intersection (reflect $ Proxy @s) (reflect $ Proxy @t)
#endif
  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (f :: Flavor) s r.
(forall t.
 (InSet f t :-> InSet f s)
 -> (InSet f t :-> InSet f r) -> forall u. InSet f t :-> InSet f u)
-> DisjointProof f s r
DisjointProof \InSet 'Int t :-> InSet 'Int s
f InSet 'Int t :-> InSet 'Int t
g -> 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 t
g
  | Bool
otherwise = forall a. Maybe a
Nothing

-- | The union of two sets.
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 = forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect (forall {k} (t :: k). Proxy t
Proxy @s) IntSet -> IntSet -> IntSet
`IntSet.union` forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect (forall {k} (t :: k). Proxy t
Proxy @t))
  \(Proxy s
_ :: Proxy r) -> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r
    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

-- unions :: ?

-- | Set with elements of @s@ that are not in @t@.
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 = forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect (forall {k} (t :: k). Proxy t
Proxy @s) IntSet -> IntSet -> IntSet
`IntSet.difference` forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect (forall {k} (t :: k). Proxy t
Proxy @t))
  \(Proxy s
_ :: Proxy r) -> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r
    forall a b. (a -> b) -> a -> b
$ 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. InSet f u :-> InSet f v)
-> (InSet f s :-> (InSet f t || InSet f r))
-> DifferenceProof f s t r
DifferenceProof forall p q. p :-> q
unsafeSubset (\InSet 'Int u :-> InSet 'Int s
f InSet 'Int u :-> InSet 'Int t
g -> forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 InSet 'Int u :-> InSet 'Int s
f InSet 'Int u :-> InSet 'Int t
g) forall p q. p :-> q
unsafeSubset

-- | Intersection of two sets.
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
  = forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect (forall {k} (t :: k). Proxy t
Proxy @s) IntSet -> IntSet -> IntSet
`IntSet.intersection` forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect (forall {k} (t :: k). Proxy t
Proxy @t))
    \(Proxy s
_ :: Proxy r) -> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r
      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

-- | Return a subset of elements that satisfy the given predicate.
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 = forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify ((Int -> Bool) -> IntSet -> IntSet
IntSet.filter (Element s -> Bool
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Int -> Element s
unsafeElement) forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s)
  \(Proxy s
_ :: Proxy r) -> forall s (p :: * -> *). KnownIntSet s => p s -> SomeIntSetWith p
SomeIntSetWith @r 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

-- | Partition a set into two disjoint subsets: those that satisfy the
-- predicate, and those that don't.
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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Int -> Element s
unsafeElement) forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s of
  (IntSet
r, IntSet
q) -> forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
r \(Proxy s
_ :: Proxy r) -> 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 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 \Element s
x -> if Element s -> Bool
p Element s
x
          then forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall s. Int -> Element s
unsafeElement forall a b. (a -> b) -> a -> b
$ forall {k} (p :: k) x. Refined p x -> x
unrefine Element s
x
          else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall s. Int -> Element s
unsafeElement forall a b. (a -> b) -> a -> b
$ forall {k} (p :: k) x. Refined p x -> x
unrefine Element s
x
      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 s
f InSet 'Int t :-> InSet 'Int s
g -> 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

-- | Divide a set into two disjoint subsets at a point where the predicate 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. 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 IntSet.spanAntitone (p . unsafeElement) $ reflect $ Proxy @s of
    (r, q)
#else
  case forall a. (a -> Bool) -> [a] -> ([a], [a])
List.span (Element s -> Bool
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Int -> Element s
unsafeElement)
    forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IntSet.toAscList forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s of
    ([Int]
rs, [Int]
qs)
      | let r :: IntSet
r = [Int] -> IntSet
IntSet.fromDistinctAscList [Int]
rs
      , let q :: IntSet
q = [Int] -> IntSet
IntSet.fromDistinctAscList [Int]
qs
#endif
      -> forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
r \(Proxy s
_ :: Proxy r) -> 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 forall a b. (a -> b) -> a -> b
$ 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. InSet f t :-> InSet f u)
-> PartialPartitionProof f s r q
PartialPartitionProof
          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 s
f InSet 'Int t :-> InSet 'Int s
g -> 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

-- | Return two disjoint subsets: those less than the given element, and those
-- greater than the given element; along with the proof that the given element
-- was in the set, if it was.
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 forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s of
  (IntSet
r, Bool
m, IntSet
q) -> forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify IntSet
r \(Proxy s
_ :: Proxy r) -> 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 forall a b. (a -> b) -> a -> b
$ 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. InSet f t :-> InSet f u)
-> SplitProof f s e r q
SplitProof
      (if Bool
m then forall a. a -> Maybe a
Just (forall s. Int -> Element s
unsafeElement Int
x) else forall a. Maybe a
Nothing)
      forall p q. p :-> q
unsafeSubset \InSet 'Int t :-> InSet 'Int s
f InSet 'Int t :-> InSet 'Int s
g -> 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

-- | Apply the given function to each element of the set and collect the
-- results. Note that the resulting set can be smaller.
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 = forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (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
  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 -> Element s
unsafeElement forall b c a. (b -> c) -> (a -> b) -> a -> c
. Element s -> Int
f) \Refined (InSet 'Int s) Int
y -> case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (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 -> 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 = forall a. [(Int, a)] -> IntMap a
IntMap.fromList
      [ (Int
y, forall s. Int -> Element s
unsafeElement Int
x)
      | Int
x <- IntSet -> [Int]
IntSet.toList forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s
      , let !y :: Int
y = Element s -> Int
f forall a b. (a -> b) -> a -> b
$ forall s. Int -> Element s
unsafeElement Int
x
      ]


-- | Map each element of @s@ into a monoid (with proof that it was an element),
-- and combine the results using 'Data.Monoid.<>'.
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 forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ 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'] -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap (Element s -> m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Int -> Element s
unsafeElement) forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IntSet.toAscList IntSet
s'
      [IntSet]
xs -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap IntSet -> m
go [IntSet]
xs

-- | Right associative fold with a lazy accumulator.
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 = forall b. (Int -> b -> b) -> b -> IntSet -> b
IntSet.foldr (Element s -> a -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Int -> Element s
unsafeElement) a
z forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s

-- | Left associative fold with a lazy accumulator.
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 = forall a. (a -> Int -> a) -> a -> IntSet -> a
IntSet.foldl ((forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Int -> Element s
unsafeElement) forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Element s -> a
f) a
z forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s

-- | Right associative fold with a strict accumulator.
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 = forall b. (Int -> b -> b) -> b -> IntSet -> b
IntSet.foldr' (Element s -> a -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Int -> Element s
unsafeElement) a
z forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s

-- | Left associative fold with a strict accumulator.
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 = forall a. (a -> Int -> a) -> a -> IntSet -> a
IntSet.foldl' ((forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Int -> Element s
unsafeElement) forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Element s -> a
f) a
z forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s

-- | Retrieves the smallest element of the set, and the set with that element
-- removed; or a proof that the set was empty.
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 forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s of
  Maybe (Int, IntSet)
Nothing -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof forall p q. p :-> q
unsafeSubset
  Just (Int
x, IntSet
xs) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ (forall s. Int -> Element s
unsafeElement Int
x,) forall a b. (a -> b) -> a -> b
$ 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 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

-- | Retrieves the greatest element of the set, and the set with that element
-- removed; or a proof that the set was empty.
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 forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s of
  Maybe (Int, IntSet)
Nothing -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof forall p q. p :-> q
unsafeSubset
  Just (Int
x, IntSet
xs) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ (forall s. Int -> Element s
unsafeElement Int
x,) forall a b. (a -> b) -> a -> b
$ 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 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

-- | List of elements in the set in ascending order.
toList :: forall s. KnownIntSet s => [Element s]
toList :: forall s. KnownIntSet s => [Element s]
toList = forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s. Coercion Int (Element s)
unsafeCastElement @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
$ IntSet -> [Int]
IntSet.toAscList forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s

-- | List of elements in the set in descending order.
toDescList :: forall s. KnownIntSet s => [Element s]
toDescList :: forall s. KnownIntSet s => [Element s]
toDescList = forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s. Coercion Int (Element s)
unsafeCastElement @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
$ IntSet -> [Int]
IntSet.toDescList forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s

-- | Convert an 'IntSet' into a 'Set', retaining its set of elements, which can
-- be converted with 'castFlavor'.
asSet :: forall s. KnownIntSet s => Set s Int
asSet :: forall s. KnownIntSet s => Set s Int
asSet = forall s. KnownIntSet s => Set s Int
intSet2Set

-- | Convert an 'IntSet' into a 'HashSet', retaining its set of elements, which
-- can be converted with 'castFlavor'.
asHashSet :: forall s. KnownIntSet s => HashSet s Int
asHashSet :: forall s. KnownIntSet s => HashSet s Int
asHashSet = forall s. KnownIntSet s => HashSet s Int
intSet2HashSet

-- | 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 @'Element' s@ can be safely
-- interconverted with @'Element' t@.
--
-- The requirement that the weakenings are natural transformations ensures that
-- they don't actually alter the elements. To build these you can compose
-- ':->''s from proofs returned by functions in this module, or "Refined"
-- functions like 'andLeft' or 'leftOr'.
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 = forall a p q.
(p :-> q) -> (q :-> p) -> Coercion (Refined p a) (Refined q a)
castRefined

-- | If elements can be interconverted (e.g. as proved by 'castElement'), then
-- the sets can be interconverted too. For example we can establish that the
-- intersection of a set with itself is interconvertible with that set:
--
-- @
-- castIntersection
--   :: t'IntersectionProof' ''Data.IntSet.Refined.Int' s s r
--   -> 'Coercion' ('IntSet' r) ('IntSet' s)
-- castIntersection ( v'IntersectionProof' p1 p2)
--   = 'cast' $ 'castElement' ('andLeft' . p1) (p2 'id' 'id')
-- @
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
unsafeEqualityProof @s @t of UnsafeEquality s t
UnsafeRefl -> forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
#else
  = repr $ unsafeCoerce Refl
#endif