{-# LANGUAGE CPP #-}
-- | This module implements a way of tracking the contents of a 'Data.Set.Set'
-- 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".
--
-- = Warning
-- This module together with "Data.Set" rely on 'Eq' and 'Ord' instances being
-- lawful: that '==' is an equivalence relation, and that the 'Ord' operations
-- define a total order on the quotient defined by this equivalence relation; at
-- least for the subset of values that are actually encountered at runtime. If
-- this assumption is violated, this module may not be able to uphold its
-- invariants and may throw errors. In particular beware of NaN in 'Float' and
-- 'Double'.
module Data.Set.Refined
  (
  -- * Set type
    KnownSet
  , Set
  -- * Refinement type
  , InSet(..)
  , Flavor(Regular)
  , Element
  , revealPredicate
  -- * Existentials and common proofs
  , SomeSet(..)
  , withSet
  , SomeSetWith(..)
  , withSetWith
  , Some2SetWith(..)
  , with2SetWith
  , (:->)
  , SupersetProof(..)
  , EmptyProof(..)
  -- * Construction
  , empty
  , singleton
  , SingletonProof(..)
  , fromSet
  , 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(..)
  , cartesianProduct
  , ProductProof(..)
  , disjointUnion
  , CoproductProof(..)
  -- * Filter
  , filter
  , partition
  , PartitionProof(..)
  , spanAntitone
  , PartialPartitionProof(..)
  , splitMember
  , SplitProof(..)
  -- * Map
  , map
  , MapProof(..)
  -- * Folds
  , foldMap
  , foldr
  , foldl
  , foldr'
  , foldl'
  -- * Min/Max
  , minView
  , maxView
  -- * Conversion
  , toList
  , toDescList
  , asIntSet
  , asHashSet
  -- * Casts
  , castElement
  , cast
  , castFlavor
  ) where

import           Data.Coerce
import           Data.Constraint (Dict(..))
import           Data.Container.Refined.Conversion
import           Data.Container.Refined.Hashable
import           Data.Container.Refined.Proofs
import           Data.Container.Refined.Unsafe
import qualified Data.Foldable as Foldable
import qualified Data.Map as Map
import           Data.Proxy
import           Data.Reflection
import qualified Data.Set as Set
import           Data.Traversable
import           Data.Type.Coercion
import           Data.Type.Equality ((:~:)(..))
import           Data.Typeable (Typeable)
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, 5, 8)
#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 @'Typeable' s@, which "Refined" wants for pretty-printing
-- exceptions. We /can/ provide @'Typeable' s@, but at the cost of using the
-- /slow/ implementation of reflection.
revealPredicate
  :: forall s a. (Typeable a, Ord a, KnownSet s a)
  => Dict (Predicate (InSet 'Regular s) a)
revealPredicate :: forall s a.
(Typeable a, Ord a, KnownSet s a) =>
Dict (Predicate (InSet 'Regular s) a)
revealPredicate = Set a
-> (forall s.
    (Typeable s, Reifies s (Set a)) =>
    Proxy s -> Dict (Predicate (InSet 'Regular s) a))
-> Dict (Predicate (InSet 'Regular s) a)
forall a r.
Typeable a =>
a -> (forall s. (Typeable s, Reifies s a) => Proxy s -> r) -> r
reifyTypeable (Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s))
  \(Proxy s
_ :: Proxy s') ->
    Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s') Set a
-> Dict (Predicate (InSet 'Regular s) a)
-> Dict (Predicate (InSet 'Regular s) a)
forall a b. a -> b -> b
`seq`
    --  ^ Work around https://github.com/ekmett/reflection/issues/54
      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 'Regular s) a)
forall (a :: Constraint). a => Dict a
Dict

-- | @'Element' s a@ is a value of type @a@ that has been verified to be an
-- element of @s@.
--
-- Thus, @'Element' s a@ is a \"refinement\" type of @a@, 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 @a@ value can be obtained with 'unrefine'. An @a@ can be
-- validated into an @'Element' s a@ with 'member'.
type Element s = Refined (InSet 'Regular s)

unsafeCastElement :: forall s a. Coercion a (Element s a)
unsafeCastElement :: forall s a. Coercion a (Element s a)
unsafeCastElement = Coercion a (Refined (InSet 'Regular s) a)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined

unsafeElement :: a -> Element s a
unsafeElement :: forall a s. a -> Element s a
unsafeElement = Coercion a (Element s a) -> a -> Element s a
forall a b. Coercion a b -> a -> b
coerceWith Coercion a (Element s a)
forall s a. Coercion a (Element s a)
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 'fromSet' ... of
--   'SomeSet' \@s _ -> doSomethingWith \@s
--
-- case 'fromSet' ... of
--   'SomeSet' (_ :: 'Proxy#' s) -> doSomethingWith \@s
-- @
data SomeSet a where
  SomeSet :: forall s a. KnownSet s a => Proxy# s -> SomeSet a

-- | 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.:
--
-- @
-- 'withSet' ('fromSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s
-- @
withSet
  :: forall a r. SomeSet a -> (forall s. KnownSet s a => Proxy s -> r) -> r
withSet :: forall a r.
SomeSet a -> (forall s. KnownSet s a => Proxy s -> r) -> r
withSet (SomeSet (Proxy# s
_ :: Proxy# s)) forall s. KnownSet s a => Proxy s -> r
k = Proxy s -> r
forall s. KnownSet s a => 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

-- | Construct a set from a regular 'Data.Set.Set'.
fromSet :: forall a. Set.Set a -> SomeSet a
fromSet :: forall a. Set a -> SomeSet a
fromSet Set a
s = Set a
-> (forall s. Reifies s (Set a) => Proxy s -> SomeSet a)
-> SomeSet a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Set a
s \(Proxy s
_ :: Proxy s) -> forall s a. KnownSet s a => Proxy# s -> SomeSet a
SomeSet @s Proxy# 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 SomeSetWith p a where
  SomeSetWith :: forall s a p. KnownSet s a => !(p s) -> SomeSetWith p a

-- | 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@).
withSetWith
  :: forall a r p. SomeSetWith p a -> (forall s. KnownSet s a => p s -> r) -> r
withSetWith :: forall a r (p :: * -> *).
SomeSetWith p a -> (forall s. KnownSet s a => p s -> r) -> r
withSetWith (SomeSetWith p s
p) forall s. KnownSet s a => p s -> r
k = p s -> r
forall s. KnownSet s a => 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 Some2SetWith p a where
  Some2SetWith
    :: forall s t a p. (KnownSet s a, KnownSet t a)
    => !(p s t) -> Some2SetWith p a

-- | 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@).
with2SetWith
  :: forall a r p. Some2SetWith p a
  -> (forall s t. (KnownSet s a, KnownSet t a) => p s t -> r)
  -> r
with2SetWith :: forall a r (p :: * -> * -> *).
Some2SetWith p a
-> (forall s t. (KnownSet s a, KnownSet t a) => p s t -> r) -> r
with2SetWith (Some2SetWith p s t
p) forall s t. (KnownSet s a, KnownSet t a) => p s t -> r
k = p s t -> r
forall s t. (KnownSet s a, KnownSet t a) => p s t -> r
k p s t
p

-- | An empty set.
empty :: forall a. SomeSetWith (EmptyProof 'Regular) a
empty :: forall a. SomeSetWith (EmptyProof 'Regular) a
empty = Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> SomeSetWith (EmptyProof 'Regular) a)
-> SomeSetWith (EmptyProof 'Regular) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Set a
forall a. Set a
Set.empty \(Proxy s
_ :: Proxy r)
  -> forall s a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r (EmptyProof 'Regular s -> SomeSetWith (EmptyProof 'Regular) a)
-> EmptyProof 'Regular s -> SomeSetWith (EmptyProof 'Regular) a
forall a b. (a -> b) -> a -> b
$ (forall s. InSet 'Regular s :-> InSet 'Regular s)
-> EmptyProof 'Regular s
forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular s) x
forall s. InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset

-- | Create a set with a single element.
singleton :: forall a. a -> SomeSetWith (SingletonProof 'Regular a) a
singleton :: forall a. a -> SomeSetWith (SingletonProof 'Regular a) a
singleton a
x = Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> SomeSetWith (SingletonProof 'Regular a) a)
-> SomeSetWith (SingletonProof 'Regular a) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (a -> Set a
forall a. a -> Set a
Set.singleton a
x) \(Proxy s
_ :: Proxy r)
  -> forall s a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r (SingletonProof 'Regular a s
 -> SomeSetWith (SingletonProof 'Regular a) a)
-> SingletonProof 'Regular a s
-> SomeSetWith (SingletonProof 'Regular a) a
forall a b. (a -> b) -> a -> b
$ Refined (InSet 'Regular s) a -> SingletonProof 'Regular a s
forall (f :: Flavor) a r.
Refined (InSet f r) a -> SingletonProof f a r
SingletonProof (Refined (InSet 'Regular s) a -> SingletonProof 'Regular a s)
-> Refined (InSet 'Regular s) a -> SingletonProof 'Regular a s
forall a b. (a -> b) -> a -> b
$ a -> Refined (InSet 'Regular s) a
forall a s. a -> Element s a
unsafeElement a
x

-- | Create a set from the elements of an arbitrary traversable.
fromTraversable
  :: forall t a. (Traversable t, Ord a)
  => t a -> SomeSetWith (FromTraversableProof 'Regular t a) a
fromTraversable :: forall (t :: * -> *) a.
(Traversable t, Ord a) =>
t a -> SomeSetWith (FromTraversableProof 'Regular t a) a
fromTraversable t a
xs = Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> SomeSetWith (FromTraversableProof 'Regular t a) a)
-> SomeSetWith (FromTraversableProof 'Regular t a) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Set a
set \(Proxy s
_ :: Proxy r)
  -> forall s a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r (FromTraversableProof 'Regular t a s
 -> SomeSetWith (FromTraversableProof 'Regular t a) a)
-> FromTraversableProof 'Regular t a s
-> SomeSetWith (FromTraversableProof 'Regular t a) a
forall a b. (a -> b) -> a -> b
$ t (Refined (InSet 'Regular s) a)
-> FromTraversableProof 'Regular t a s
forall (f :: Flavor) (t :: * -> *) a r.
t (Refined (InSet f r) a) -> FromTraversableProof f t a r
FromTraversableProof
    (t (Refined (InSet 'Regular s) a)
 -> FromTraversableProof 'Regular t a s)
-> t (Refined (InSet 'Regular s) a)
-> FromTraversableProof 'Regular t a s
forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce @(t (Element _ a)) @(t (Element r a)) t (Element Any a)
proof
  where
    (Set a
set, t (Element Any a)
proof) = (Set a -> a -> (Set a, Element Any a))
-> Set a -> t a -> (Set a, t (Element Any a))
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
      (\Set a
s a
x -> let !s' :: Set a
s' = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
x Set a
s in (Set a
s', a -> Element Any a
forall a s. a -> Element s a
unsafeElement a
x))
      Set a
forall a. Set a
Set.empty
      t a
xs

-- | Insert an element in a set.
insert
  :: forall s a. (Ord a, KnownSet s a)
  => a -> SomeSetWith (InsertProof 'Regular a s) a
insert :: forall s a.
(Ord a, KnownSet s a) =>
a -> SomeSetWith (InsertProof 'Regular a s) a
insert a
x = Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> SomeSetWith (InsertProof 'Regular a s) a)
-> SomeSetWith (InsertProof 'Regular a s) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
x (Set a -> Set a) -> Set a -> Set a
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
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 a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r (InsertProof 'Regular a s s
 -> SomeSetWith (InsertProof 'Regular a s) a)
-> InsertProof 'Regular a s s
-> SomeSetWith (InsertProof 'Regular a s) a
forall a b. (a -> b) -> a -> b
$ Refined (InSet 'Regular s) a
-> (InSet 'Regular s :-> InSet 'Regular s)
-> InsertProof 'Regular a 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 (a -> Refined (InSet 'Regular s) a
forall a s. a -> Element s a
unsafeElement a
x) Refined (InSet 'Regular s) x -> Refined (InSet 'Regular s) x
InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset

-- | Delete an element from a set.
delete
  :: forall s a. (Ord a, KnownSet s a)
  => a -> SomeSetWith (SupersetProof 'Regular s) a
delete :: forall s a.
(Ord a, KnownSet s a) =>
a -> SomeSetWith (SupersetProof 'Regular s) a
delete a
x = Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> SomeSetWith (SupersetProof 'Regular s) a)
-> SomeSetWith (SupersetProof 'Regular s) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.delete a
x (Set a -> Set a) -> Set a -> Set a
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
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 a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @s (SupersetProof 'Regular s s
 -> SomeSetWith (SupersetProof 'Regular s) a)
-> SupersetProof 'Regular s s
-> SomeSetWith (SupersetProof 'Regular s) a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular s :-> InSet 'Regular s)
-> SupersetProof 'Regular s s
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular s) x
InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset

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

-- | Find the largest element smaller than the given one.
lookupLT :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)
lookupLT :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)
lookupLT a
x = Coercion a (Element s a)
-> (Coercible a (Element s a) => Maybe (Element s a))
-> Maybe (Element s a)
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s a. Coercion a (Element s a)
unsafeCastElement @s @a) ((Coercible a (Element s a) => Maybe (Element s a))
 -> Maybe (Element s a))
-> (Coercible a (Element s a) => Maybe (Element s a))
-> Maybe (Element s a)
forall a b. (a -> b) -> a -> b
$ Maybe a -> Maybe (Element s a)
forall a b. Coercible a b => a -> b
coerce
  (Maybe a -> Maybe (Element s a)) -> Maybe a -> Maybe (Element s a)
forall a b. (a -> b) -> a -> b
$ a -> Set a -> Maybe a
forall a. Ord a => a -> Set a -> Maybe a
Set.lookupLT a
x (Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s)

-- | Find the smallest element greater than the given one.
lookupGT :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)
lookupGT :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)
lookupGT a
x = Coercion a (Element s a)
-> (Coercible a (Element s a) => Maybe (Element s a))
-> Maybe (Element s a)
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s a. Coercion a (Element s a)
unsafeCastElement @s @a) ((Coercible a (Element s a) => Maybe (Element s a))
 -> Maybe (Element s a))
-> (Coercible a (Element s a) => Maybe (Element s a))
-> Maybe (Element s a)
forall a b. (a -> b) -> a -> b
$ Maybe a -> Maybe (Element s a)
forall a b. Coercible a b => a -> b
coerce
  (Maybe a -> Maybe (Element s a)) -> Maybe a -> Maybe (Element s a)
forall a b. (a -> b) -> a -> b
$ a -> Set a -> Maybe a
forall a. Ord a => a -> Set a -> Maybe a
Set.lookupGT a
x (Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s)

-- | Find the largest element smaller or equal to the given one.
lookupLE :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)
lookupLE :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)
lookupLE a
x = Coercion a (Element s a)
-> (Coercible a (Element s a) => Maybe (Element s a))
-> Maybe (Element s a)
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s a. Coercion a (Element s a)
unsafeCastElement @s @a) ((Coercible a (Element s a) => Maybe (Element s a))
 -> Maybe (Element s a))
-> (Coercible a (Element s a) => Maybe (Element s a))
-> Maybe (Element s a)
forall a b. (a -> b) -> a -> b
$ Maybe a -> Maybe (Element s a)
forall a b. Coercible a b => a -> b
coerce
  (Maybe a -> Maybe (Element s a)) -> Maybe a -> Maybe (Element s a)
forall a b. (a -> b) -> a -> b
$ a -> Set a -> Maybe a
forall a. Ord a => a -> Set a -> Maybe a
Set.lookupLE a
x (Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s)

-- | Find the smallest element greater or equal to the given one.
lookupGE :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)
lookupGE :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)
lookupGE a
x = Coercion a (Element s a)
-> (Coercible a (Element s a) => Maybe (Element s a))
-> Maybe (Element s a)
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s a. Coercion a (Element s a)
unsafeCastElement @s @a) ((Coercible a (Element s a) => Maybe (Element s a))
 -> Maybe (Element s a))
-> (Coercible a (Element s a) => Maybe (Element s a))
-> Maybe (Element s a)
forall a b. (a -> b) -> a -> b
$ Maybe a -> Maybe (Element s a)
forall a b. Coercible a b => a -> b
coerce
  (Maybe a -> Maybe (Element s a)) -> Maybe a -> Maybe (Element s a)
forall a b. (a -> b) -> a -> b
$ a -> Set a -> Maybe a
forall a. Ord a => a -> Set a -> Maybe a
Set.lookupGE a
x (Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s)

-- | If the set is empty, return the proof that it is.
null :: forall s a. KnownSet s a => Maybe (EmptyProof 'Regular s)
null :: forall s a. KnownSet s a => Maybe (EmptyProof 'Regular s)
null
  | Set a -> Bool
forall a. Set a -> Bool
Set.null (Set a -> Bool) -> Set a -> Bool
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s = EmptyProof 'Regular s -> Maybe (EmptyProof 'Regular s)
forall a. a -> Maybe a
Just (EmptyProof 'Regular s -> Maybe (EmptyProof 'Regular s))
-> EmptyProof 'Regular s -> Maybe (EmptyProof 'Regular s)
forall a b. (a -> b) -> a -> b
$ (forall s. InSet 'Regular s :-> InSet 'Regular s)
-> EmptyProof 'Regular s
forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular s) x
forall s. InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset
  | Bool
otherwise = Maybe (EmptyProof 'Regular s)
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 a. (Ord a, KnownSet s a, KnownSet t a)
  => Maybe (SubsetProof 'Regular s t)
isSubsetOf :: forall s t a.
(Ord a, KnownSet s a, KnownSet t a) =>
Maybe (SubsetProof 'Regular s t)
isSubsetOf
  | Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Proxy t -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> Set a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t)
  = SubsetProof 'Regular s t -> Maybe (SubsetProof 'Regular s t)
forall a. a -> Maybe a
Just (SubsetProof 'Regular s t -> Maybe (SubsetProof 'Regular s t))
-> SubsetProof 'Regular s t -> Maybe (SubsetProof 'Regular s t)
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular s :-> InSet 'Regular t) -> SubsetProof 'Regular s t
forall (f :: Flavor) s r.
(InSet f s :-> InSet f r) -> SubsetProof f s r
SubsetProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular t) x
InSet 'Regular s :-> InSet 'Regular t
forall p q x. Refined p x -> Refined q x
unsafeSubset
  | Bool
otherwise = Maybe (SubsetProof 'Regular s t)
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 a. (Ord a, KnownSet s a, KnownSet t a)
  => Maybe (DisjointProof 'Regular s t)
disjoint :: forall s t a.
(Ord a, KnownSet s a, KnownSet t a) =>
Maybe (DisjointProof 'Regular s t)
disjoint
#if MIN_VERSION_containers(0, 5, 11)
  | Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint (Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) (Proxy t -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> Set a
reflect (Proxy t -> Set a) -> Proxy t -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t)
#else
  | Set.null $ Set.intersection (reflect $ Proxy @s) (reflect $ Proxy @t)
#endif
  = DisjointProof 'Regular s t -> Maybe (DisjointProof 'Regular s t)
forall a. a -> Maybe a
Just (DisjointProof 'Regular s t -> Maybe (DisjointProof 'Regular s t))
-> DisjointProof 'Regular s t -> Maybe (DisjointProof 'Regular s t)
forall a b. (a -> b) -> a -> b
$ (forall t.
 (InSet 'Regular t :-> InSet 'Regular s)
 -> (InSet 'Regular t :-> InSet 'Regular t)
 -> forall u x.
    Refined (InSet 'Regular t) x -> Refined (InSet 'Regular u) x)
-> DisjointProof 'Regular 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 'Regular t :-> InSet 'Regular s
f InSet 'Regular t :-> InSet 'Regular t
g -> (InSet 'Regular t :-> InSet 'Regular s)
-> (InSet 'Regular t :-> InSet 'Regular t)
-> InSet 'Regular t :-> InSet 'Regular u
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Regular t) x -> Refined (InSet 'Regular s) x
InSet 'Regular t :-> InSet 'Regular s
f Refined (InSet 'Regular t) x -> Refined (InSet 'Regular t) x
InSet 'Regular t :-> InSet 'Regular t
g
  | Bool
otherwise = Maybe (DisjointProof 'Regular s t)
forall a. Maybe a
Nothing

-- | The union of two sets.
union
  :: forall s t a. (Ord a, KnownSet s a, KnownSet t a)
  => SomeSetWith (UnionProof 'Regular s t) a
union :: forall s t a.
(Ord a, KnownSet s a, KnownSet t a) =>
SomeSetWith (UnionProof 'Regular s t) a
union = Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> SomeSetWith (UnionProof 'Regular s t) a)
-> SomeSetWith (UnionProof 'Regular s t) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Proxy t -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> Set a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))
  \(Proxy s
_ :: Proxy r) -> forall s a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r (UnionProof 'Regular s t s
 -> SomeSetWith (UnionProof 'Regular s t) a)
-> UnionProof 'Regular s t s
-> SomeSetWith (UnionProof 'Regular s t) a
forall a b. (a -> b) -> a -> b
$ ((InSet 'Regular s || InSet 'Regular t) :-> InSet 'Regular s)
-> (forall u.
    (InSet 'Regular s :-> InSet 'Regular u)
    -> (InSet 'Regular t :-> InSet 'Regular u)
    -> InSet 'Regular s :-> InSet 'Regular u)
-> UnionProof 'Regular 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 'Regular s || InSet 'Regular t) x
-> Refined (InSet 'Regular s) x
(InSet 'Regular s || InSet 'Regular t) :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Regular s :-> InSet 'Regular u)
-> (InSet 'Regular t :-> InSet 'Regular u)
-> Refined (InSet 'Regular s) x
-> Refined (InSet 'Regular u) x
(InSet 'Regular s :-> InSet 'Regular u)
-> (InSet 'Regular t :-> InSet 'Regular u)
-> InSet 'Regular s :-> InSet 'Regular u
forall u.
(InSet 'Regular s :-> InSet 'Regular u)
-> (InSet 'Regular t :-> InSet 'Regular u)
-> InSet 'Regular s :-> InSet 'Regular u
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 a. (Ord a, KnownSet s a, KnownSet t a)
  => SomeSetWith (DifferenceProof 'Regular s t) a
difference :: forall s t a.
(Ord a, KnownSet s a, KnownSet t a) =>
SomeSetWith (DifferenceProof 'Regular s t) a
difference = Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> SomeSetWith (DifferenceProof 'Regular s t) a)
-> SomeSetWith (DifferenceProof 'Regular s t) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Proxy t -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> Set a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))
  \(Proxy s
_ :: Proxy r) -> forall s a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r
    (DifferenceProof 'Regular s t s
 -> SomeSetWith (DifferenceProof 'Regular s t) a)
-> DifferenceProof 'Regular s t s
-> SomeSetWith (DifferenceProof 'Regular s t) a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular s :-> InSet 'Regular s)
-> (forall u.
    (InSet 'Regular u :-> InSet 'Regular s)
    -> (InSet 'Regular u :-> InSet 'Regular t)
    -> forall v x.
       Refined (InSet 'Regular u) x -> Refined (InSet 'Regular v) x)
-> (InSet 'Regular s :-> (InSet 'Regular t || InSet 'Regular s))
-> DifferenceProof 'Regular 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 'Regular s) x -> Refined (InSet 'Regular s) x
InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset (\InSet 'Regular u :-> InSet 'Regular s
f InSet 'Regular u :-> InSet 'Regular t
g -> (InSet 'Regular u :-> InSet 'Regular s)
-> (InSet 'Regular u :-> InSet 'Regular t)
-> InSet 'Regular u :-> InSet 'Regular v
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Regular u) x -> Refined (InSet 'Regular s) x
InSet 'Regular u :-> InSet 'Regular s
f Refined (InSet 'Regular u) x -> Refined (InSet 'Regular t) x
InSet 'Regular u :-> InSet 'Regular t
g) Refined (InSet 'Regular s) x
-> Refined (InSet 'Regular t || InSet 'Regular s) x
InSet 'Regular s :-> (InSet 'Regular t || InSet 'Regular s)
forall p q x. Refined p x -> Refined q x
unsafeSubset

-- | Intersection of two sets.
intersection
  :: forall s t a. (Ord a, KnownSet s a, KnownSet t a)
  => SomeSetWith (IntersectionProof 'Regular s t) a
intersection :: forall s t a.
(Ord a, KnownSet s a, KnownSet t a) =>
SomeSetWith (IntersectionProof 'Regular s t) a
intersection = Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> SomeSetWith (IntersectionProof 'Regular s t) a)
-> SomeSetWith (IntersectionProof 'Regular s t) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Proxy t -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> Set a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))
  \(Proxy s
_ :: Proxy r) -> forall s a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r
    (IntersectionProof 'Regular s t s
 -> SomeSetWith (IntersectionProof 'Regular s t) a)
-> IntersectionProof 'Regular s t s
-> SomeSetWith (IntersectionProof 'Regular s t) a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular s :-> (InSet 'Regular s && InSet 'Regular t))
-> (forall u.
    (InSet 'Regular u :-> InSet 'Regular s)
    -> (InSet 'Regular u :-> InSet 'Regular t)
    -> InSet 'Regular u :-> InSet 'Regular s)
-> IntersectionProof 'Regular 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 'Regular s) x
-> Refined (InSet 'Regular s && InSet 'Regular t) x
InSet 'Regular s :-> (InSet 'Regular s && InSet 'Regular t)
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Regular u :-> InSet 'Regular s)
-> (InSet 'Regular u :-> InSet 'Regular t)
-> Refined (InSet 'Regular u) x
-> Refined (InSet 'Regular s) x
(InSet 'Regular u :-> InSet 'Regular s)
-> (InSet 'Regular u :-> InSet 'Regular t)
-> InSet 'Regular u :-> InSet 'Regular s
forall u.
(InSet 'Regular u :-> InSet 'Regular s)
-> (InSet 'Regular u :-> InSet 'Regular t)
-> InSet 'Regular u :-> InSet 'Regular s
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2

-- | Cartesian product of two sets. The elements are all pairs @(x, y)@ for each
-- @x@ from @s@ and for each @y@ from @t@.
cartesianProduct
  :: forall s t a b. (KnownSet s a, KnownSet t b)
  => SomeSetWith (ProductProof 'Regular s t) (a, b)
cartesianProduct :: forall s t a b.
(KnownSet s a, KnownSet t b) =>
SomeSetWith (ProductProof 'Regular s t) (a, b)
cartesianProduct = Set (a, b)
-> (forall s.
    Reifies s (Set (a, b)) =>
    Proxy s -> SomeSetWith (ProductProof 'Regular s t) (a, b))
-> SomeSetWith (ProductProof 'Regular s t) (a, b)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify
#if MIN_VERSION_containers(0, 5, 11)
  (Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) Set a -> Set b -> Set (a, b)
forall a b. Set a -> Set b -> Set (a, b)
`Set.cartesianProduct` Proxy t -> Set b
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> Set b
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))
#else
  (Set.fromDistinctAscList $ (,) <$> Set.toAscList (reflect $ Proxy @s)
    <*> Set.toAscList (reflect $ Proxy @t))
#endif
  \(Proxy s
_ :: Proxy r) -> forall s a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r (ProductProof 'Regular s t s
 -> SomeSetWith (ProductProof 'Regular s t) (a, b))
-> ProductProof 'Regular s t s
-> SomeSetWith (ProductProof 'Regular s t) (a, b)
forall a b. (a -> b) -> a -> b
$ (forall a b.
 Coercion
   (Refined (InSet 'Regular s) a, Refined (InSet 'Regular t) b)
   (Refined (InSet 'Regular s) (a, b)))
-> ProductProof 'Regular s t s
forall (f :: Flavor) s t r.
(forall a b.
 Coercion
   (Refined (InSet f s) a, Refined (InSet f t) b)
   (Refined (InSet f r) (a, b)))
-> ProductProof f s t r
ProductProof let
      proof :: forall x y. Coercion
        (Refined (InSet 'Regular s) x, Refined (InSet 'Regular t) y)
        (Refined (InSet 'Regular r) (x, y))
      !proof :: forall a b.
Coercion
  (Refined (InSet 'Regular s) a, Refined (InSet 'Regular t) b)
  (Refined (InSet 'Regular s) (a, b))
proof
        | Coercion x (Refined (InSet 'Regular s) x)
Coercion <- forall x p. Coercion x (Refined p x)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @x @(InSet 'Regular s)
        , Coercion y (Refined (InSet 'Regular t) y)
Coercion <- forall x p. Coercion x (Refined p x)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @y @(InSet 'Regular t)
        = Coercion
  (Refined (InSet 'Regular s) x, Refined (InSet 'Regular t) y) (x, y)
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion Coercion
  (Refined (InSet 'Regular s) x, Refined (InSet 'Regular t) y) (x, y)
-> Coercion (x, y) (Refined (InSet 'Regular s) (x, y))
-> Coercion
     (Refined (InSet 'Regular s) x, Refined (InSet 'Regular t) y)
     (Refined (InSet 'Regular s) (x, y))
forall {k} (a :: k) (b :: k) (c :: k).
Coercion a b -> Coercion b c -> Coercion a c
`trans`
          forall x p. Coercion x (Refined p x)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @(x, y) @(InSet 'Regular r)
    in Coercion
  (Refined (InSet 'Regular s) a, Refined (InSet 'Regular t) b)
  (Refined (InSet 'Regular s) (a, b))
forall a b.
Coercion
  (Refined (InSet 'Regular s) a, Refined (InSet 'Regular t) b)
  (Refined (InSet 'Regular s) (a, b))
proof

-- | Disjoint union of two sets. Includes @'Left' x@ for each @x@ from @s@, and
-- @'Right' y@ for each @y@ from @t@.
disjointUnion
  :: forall s t a b. (KnownSet s a, KnownSet t b)
  => SomeSetWith (CoproductProof 'Regular s t) (Either a b)
disjointUnion :: forall s t a b.
(KnownSet s a, KnownSet t b) =>
SomeSetWith (CoproductProof 'Regular s t) (Either a b)
disjointUnion = Set (Either a b)
-> (forall s.
    Reifies s (Set (Either a b)) =>
    Proxy s -> SomeSetWith (CoproductProof 'Regular s t) (Either a b))
-> SomeSetWith (CoproductProof 'Regular s t) (Either a b)
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify
#if MIN_VERSION_containers(0, 5, 11)
  (Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) Set a -> Set b -> Set (Either a b)
forall a b. Set a -> Set b -> Set (Either a b)
`Set.disjointUnion` Proxy t -> Set b
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> Set b
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))
#else
  (Set.fromDistinctAscList $ (Left <$> Set.toAscList (reflect $ Proxy @s))
    ++ (Right <$> Set.toAscList (reflect $ Proxy @t)))
#endif
  \(Proxy s
_ :: Proxy r) -> forall s a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r (CoproductProof 'Regular s t s
 -> SomeSetWith (CoproductProof 'Regular s t) (Either a b))
-> CoproductProof 'Regular s t s
-> SomeSetWith (CoproductProof 'Regular s t) (Either a b)
forall a b. (a -> b) -> a -> b
$ (forall a b.
 Coercion
   (Either
      (Refined (InSet 'Regular s) a) (Refined (InSet 'Regular t) b))
   (Refined (InSet 'Regular s) (Either a b)))
-> CoproductProof 'Regular s t s
forall (f :: Flavor) s t r.
(forall a b.
 Coercion
   (Either (Refined (InSet f s) a) (Refined (InSet f t) b))
   (Refined (InSet f r) (Either a b)))
-> CoproductProof f s t r
CoproductProof let
      proof :: forall x y. Coercion
        (Either (Refined (InSet 'Regular s) x) (Refined (InSet 'Regular t) y))
        (Refined (InSet 'Regular r) (Either x y))
      !proof :: forall a b.
Coercion
  (Either
     (Refined (InSet 'Regular s) a) (Refined (InSet 'Regular t) b))
  (Refined (InSet 'Regular s) (Either a b))
proof
        | Coercion x (Refined (InSet 'Regular s) x)
Coercion <- forall x p. Coercion x (Refined p x)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @x @(InSet 'Regular s)
        , Coercion y (Refined (InSet 'Regular t) y)
Coercion <- forall x p. Coercion x (Refined p x)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @y @(InSet 'Regular t)
        = Coercion
  (Either
     (Refined (InSet 'Regular s) x) (Refined (InSet 'Regular t) y))
  (Either x y)
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion Coercion
  (Either
     (Refined (InSet 'Regular s) x) (Refined (InSet 'Regular t) y))
  (Either x y)
-> Coercion (Either x y) (Refined (InSet 'Regular s) (Either x y))
-> Coercion
     (Either
        (Refined (InSet 'Regular s) x) (Refined (InSet 'Regular t) y))
     (Refined (InSet 'Regular s) (Either x y))
forall {k} (a :: k) (b :: k) (c :: k).
Coercion a b -> Coercion b c -> Coercion a c
`trans`
          forall x p. Coercion x (Refined p x)
forall {k} x (p :: k). Coercion x (Refined p x)
reallyUnsafeUnderlyingRefined @(Either x y) @(InSet 'Regular r)
    in Coercion
  (Either
     (Refined (InSet 'Regular s) a) (Refined (InSet 'Regular t) b))
  (Refined (InSet 'Regular s) (Either a b))
forall a b.
Coercion
  (Either
     (Refined (InSet 'Regular s) a) (Refined (InSet 'Regular t) b))
  (Refined (InSet 'Regular s) (Either a b))
proof

-- | Return a subset of elements that satisfy the given predicate.
filter
  :: forall s a. KnownSet s a
  => (Element s a -> Bool) -> SomeSetWith (SupersetProof 'Regular s) a
filter :: forall s a.
KnownSet s a =>
(Element s a -> Bool) -> SomeSetWith (SupersetProof 'Regular s) a
filter Element s a -> Bool
p = Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> SomeSetWith (SupersetProof 'Regular s) a)
-> SomeSetWith (SupersetProof 'Regular s) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify ((a -> Bool) -> Set a -> Set a
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Element s a -> Bool
p (Element s a -> Bool) -> (a -> Element s a) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  a -> Element s a
forall a s. a -> Element s a
unsafeElement) (Set a -> Set a) -> Set a -> Set a
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
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 a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r (SupersetProof 'Regular s s
 -> SomeSetWith (SupersetProof 'Regular s) a)
-> SupersetProof 'Regular s s
-> SomeSetWith (SupersetProof 'Regular s) a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular s :-> InSet 'Regular s)
-> SupersetProof 'Regular s s
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular s) x
InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset

-- | Partition a set into two disjoint subsets: those that satisfy the
-- predicate, and those that don't.
partition
  :: forall s a. KnownSet s a
  => (Element s a -> Bool) -> Some2SetWith (PartitionProof 'Regular s a) a
partition :: forall s a.
KnownSet s a =>
(Element s a -> Bool)
-> Some2SetWith (PartitionProof 'Regular s a) a
partition Element s a -> Bool
p = case (a -> Bool) -> Set a -> (Set a, Set a)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (Element s a -> Bool
p (Element s a -> Bool) -> (a -> Element s a) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Element s a
forall a s. a -> Element s a
unsafeElement) (Set a -> (Set a, Set a)) -> Set a -> (Set a, Set a)
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s of
  (Set a
r, Set a
q) -> Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> Some2SetWith (PartitionProof 'Regular s a) a)
-> Some2SetWith (PartitionProof 'Regular s a) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Set a
r \(Proxy s
_ :: Proxy r) -> Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> Some2SetWith (PartitionProof 'Regular s a) a)
-> Some2SetWith (PartitionProof 'Regular s a) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Set a
q \(Proxy s
_ :: Proxy q)
    -> forall s t a (p :: * -> * -> *).
(KnownSet s a, KnownSet t a) =>
p s t -> Some2SetWith p a
Some2SetWith @s @r (PartitionProof 'Regular s a s s
 -> Some2SetWith (PartitionProof 'Regular s a) a)
-> PartitionProof 'Regular s a s s
-> Some2SetWith (PartitionProof 'Regular s a) a
forall a b. (a -> b) -> a -> b
$ (Element s a
 -> Either (Element s a) (Refined (InSet 'Regular s) a))
-> ((InSet 'Regular s || InSet 'Regular s) :-> InSet 'Regular s)
-> (forall t.
    (InSet 'Regular s :-> InSet 'Regular t)
    -> (InSet 'Regular s :-> InSet 'Regular t)
    -> InSet 'Regular s :-> InSet 'Regular t)
-> (forall t.
    (InSet 'Regular t :-> InSet 'Regular s)
    -> (InSet 'Regular t :-> InSet 'Regular s)
    -> forall u x.
       Refined (InSet 'Regular t) x -> Refined (InSet 'Regular u) x)
-> PartitionProof 'Regular s a 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 a
x -> if Element s a -> Bool
p Element s a
x
          then Element s a -> Either (Element s a) (Refined (InSet 'Regular s) a)
forall a b. a -> Either a b
Left (Element s a
 -> Either (Element s a) (Refined (InSet 'Regular s) a))
-> Element s a
-> Either (Element s a) (Refined (InSet 'Regular s) a)
forall a b. (a -> b) -> a -> b
$ a -> Element s a
forall a s. a -> Element s a
unsafeElement (a -> Element s a) -> a -> Element s a
forall a b. (a -> b) -> a -> b
$ Element s a -> a
forall {k} (p :: k) x. Refined p x -> x
unrefine Element s a
x
          else Refined (InSet 'Regular s) a
-> Either (Element s a) (Refined (InSet 'Regular s) a)
forall a b. b -> Either a b
Right (Refined (InSet 'Regular s) a
 -> Either (Element s a) (Refined (InSet 'Regular s) a))
-> Refined (InSet 'Regular s) a
-> Either (Element s a) (Refined (InSet 'Regular s) a)
forall a b. (a -> b) -> a -> b
$ a -> Refined (InSet 'Regular s) a
forall a s. a -> Element s a
unsafeElement (a -> Refined (InSet 'Regular s) a)
-> a -> Refined (InSet 'Regular s) a
forall a b. (a -> b) -> a -> b
$ Element s a -> a
forall {k} (p :: k) x. Refined p x -> x
unrefine Element s a
x
      Refined (InSet 'Regular s || InSet 'Regular s) x
-> Refined (InSet 'Regular s) x
(InSet 'Regular s || InSet 'Regular s) :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Regular s :-> InSet 'Regular t)
-> (InSet 'Regular s :-> InSet 'Regular t)
-> Refined (InSet 'Regular s) x
-> Refined (InSet 'Regular t) x
(InSet 'Regular s :-> InSet 'Regular t)
-> (InSet 'Regular s :-> InSet 'Regular t)
-> InSet 'Regular s :-> InSet 'Regular t
forall t.
(InSet 'Regular s :-> InSet 'Regular t)
-> (InSet 'Regular s :-> InSet 'Regular t)
-> InSet 'Regular s :-> InSet 'Regular t
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 \InSet 'Regular t :-> InSet 'Regular s
f InSet 'Regular t :-> InSet 'Regular s
g -> (InSet 'Regular t :-> InSet 'Regular s)
-> (InSet 'Regular t :-> InSet 'Regular s)
-> InSet 'Regular t :-> InSet 'Regular u
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Regular t) x -> Refined (InSet 'Regular s) x
InSet 'Regular t :-> InSet 'Regular s
f Refined (InSet 'Regular t) x -> Refined (InSet 'Regular s) x
InSet 'Regular t :-> InSet 'Regular 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 a. KnownSet s a
  => (Element s a -> Bool) -> Some2SetWith (PartialPartitionProof 'Regular s) a
spanAntitone :: forall s a.
KnownSet s a =>
(Element s a -> Bool)
-> Some2SetWith (PartialPartitionProof 'Regular s) a
spanAntitone Element s a -> Bool
p =
#if MIN_VERSION_containers(0, 5, 8)
  case (a -> Bool) -> Set a -> (Set a, Set a)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.spanAntitone (Element s a -> Bool
p (Element s a -> Bool) -> (a -> Element s a) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Element s a
forall a s. a -> Element s a
unsafeElement) (Set a -> (Set a, Set a)) -> Set a -> (Set a, Set a)
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s of
    (Set a
r, Set a
q)
#else
  case List.span (p . unsafeElement)
    $ Set.toAscList $ reflect $ Proxy @s of
    (rs, qs)
      | let r = Set.fromDistinctAscList rs
      , let q = Set.fromDistinctAscList qs
#endif
      -> Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> Some2SetWith (PartialPartitionProof 'Regular s) a)
-> Some2SetWith (PartialPartitionProof 'Regular s) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Set a
r \(Proxy s
_ :: Proxy r) -> Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> Some2SetWith (PartialPartitionProof 'Regular s) a)
-> Some2SetWith (PartialPartitionProof 'Regular s) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Set a
q \(Proxy s
_ :: Proxy q)
        -> forall s t a (p :: * -> * -> *).
(KnownSet s a, KnownSet t a) =>
p s t -> Some2SetWith p a
Some2SetWith @r @q (PartialPartitionProof 'Regular s s s
 -> Some2SetWith (PartialPartitionProof 'Regular s) a)
-> PartialPartitionProof 'Regular s s s
-> Some2SetWith (PartialPartitionProof 'Regular s) a
forall a b. (a -> b) -> a -> b
$ ((InSet 'Regular s || InSet 'Regular s) :-> InSet 'Regular s)
-> (forall t.
    (InSet 'Regular s :-> InSet 'Regular t)
    -> (InSet 'Regular s :-> InSet 'Regular t)
    -> InSet 'Regular s :-> InSet 'Regular t)
-> (forall t.
    (InSet 'Regular t :-> InSet 'Regular s)
    -> (InSet 'Regular t :-> InSet 'Regular s)
    -> forall u x.
       Refined (InSet 'Regular t) x -> Refined (InSet 'Regular u) x)
-> PartialPartitionProof 'Regular 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 'Regular s || InSet 'Regular s) x
-> Refined (InSet 'Regular s) x
(InSet 'Regular s || InSet 'Regular s) :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Regular s :-> InSet 'Regular t)
-> (InSet 'Regular s :-> InSet 'Regular t)
-> Refined (InSet 'Regular s) x
-> Refined (InSet 'Regular t) x
(InSet 'Regular s :-> InSet 'Regular t)
-> (InSet 'Regular s :-> InSet 'Regular t)
-> InSet 'Regular s :-> InSet 'Regular t
forall t.
(InSet 'Regular s :-> InSet 'Regular t)
-> (InSet 'Regular s :-> InSet 'Regular t)
-> InSet 'Regular s :-> InSet 'Regular t
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 \InSet 'Regular t :-> InSet 'Regular s
f InSet 'Regular t :-> InSet 'Regular s
g -> (InSet 'Regular t :-> InSet 'Regular s)
-> (InSet 'Regular t :-> InSet 'Regular s)
-> InSet 'Regular t :-> InSet 'Regular u
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Regular t) x -> Refined (InSet 'Regular s) x
InSet 'Regular t :-> InSet 'Regular s
f Refined (InSet 'Regular t) x -> Refined (InSet 'Regular s) x
InSet 'Regular t :-> InSet 'Regular 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 a. (Ord a, KnownSet s a)
  => a -> Some2SetWith (SplitProof 'Regular s (Element s a)) a
splitMember :: forall s a.
(Ord a, KnownSet s a) =>
a -> Some2SetWith (SplitProof 'Regular s (Element s a)) a
splitMember a
x = case a -> Set a -> (Set a, Bool, Set a)
forall a. Ord a => a -> Set a -> (Set a, Bool, Set a)
Set.splitMember a
x (Set a -> (Set a, Bool, Set a)) -> Set a -> (Set a, Bool, Set a)
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s of
  (Set a
r, Bool
m, Set a
q) -> Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> Some2SetWith (SplitProof 'Regular s (Element s a)) a)
-> Some2SetWith (SplitProof 'Regular s (Element s a)) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Set a
r \(Proxy s
_ :: Proxy r) -> Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> Some2SetWith (SplitProof 'Regular s (Element s a)) a)
-> Some2SetWith (SplitProof 'Regular s (Element s a)) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Set a
q \(Proxy s
_ :: Proxy q)
    -> forall s t a (p :: * -> * -> *).
(KnownSet s a, KnownSet t a) =>
p s t -> Some2SetWith p a
Some2SetWith @r @q (SplitProof 'Regular s (Element s a) s s
 -> Some2SetWith (SplitProof 'Regular s (Element s a)) a)
-> SplitProof 'Regular s (Element s a) s s
-> Some2SetWith (SplitProof 'Regular s (Element s a)) a
forall a b. (a -> b) -> a -> b
$ Maybe (Element s a)
-> ((InSet 'Regular s || InSet 'Regular s) :-> InSet 'Regular s)
-> (forall t.
    (InSet 'Regular t :-> InSet 'Regular s)
    -> (InSet 'Regular t :-> InSet 'Regular s)
    -> forall u x.
       Refined (InSet 'Regular t) x -> Refined (InSet 'Regular u) x)
-> SplitProof 'Regular s (Element s a) 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 a -> Maybe (Element s a)
forall a. a -> Maybe a
Just (a -> Element s a
forall a s. a -> Element s a
unsafeElement a
x) else Maybe (Element s a)
forall a. Maybe a
Nothing)
      Refined (InSet 'Regular s || InSet 'Regular s) x
-> Refined (InSet 'Regular s) x
(InSet 'Regular s || InSet 'Regular s) :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset \InSet 'Regular t :-> InSet 'Regular s
f InSet 'Regular t :-> InSet 'Regular s
g -> (InSet 'Regular t :-> InSet 'Regular s)
-> (InSet 'Regular t :-> InSet 'Regular s)
-> InSet 'Regular t :-> InSet 'Regular u
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Regular t) x -> Refined (InSet 'Regular s) x
InSet 'Regular t :-> InSet 'Regular s
f Refined (InSet 'Regular t) x -> Refined (InSet 'Regular s) x
InSet 'Regular t :-> InSet 'Regular 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 a b. (Ord b, KnownSet s a)
  => (Element s a -> b) -> SomeSetWith (MapProof 'Regular s a b) b
map :: forall s a b.
(Ord b, KnownSet s a) =>
(Element s a -> b) -> SomeSetWith (MapProof 'Regular s a b) b
map Element s a -> b
f = Set b
-> (forall s.
    Reifies s (Set b) =>
    Proxy s -> SomeSetWith (MapProof 'Regular s a b) b)
-> SomeSetWith (MapProof 'Regular s a b) b
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Map b (Element s a) -> Set b
forall k a. Map k a -> Set k
Map.keysSet Map b (Element s a)
m) \(Proxy s
_ :: Proxy r) -> forall s a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r
  (MapProof 'Regular s a b s
 -> SomeSetWith (MapProof 'Regular s a b) b)
-> MapProof 'Regular s a b s
-> SomeSetWith (MapProof 'Regular s a b) b
forall a b. (a -> b) -> a -> b
$ (Element s a -> Refined (InSet 'Regular s) b)
-> (Refined (InSet 'Regular s) b -> Element s a)
-> MapProof 'Regular s a b 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 (b -> Refined (InSet 'Regular s) b
forall a s. a -> Element s a
unsafeElement (b -> Refined (InSet 'Regular s) b)
-> (Element s a -> b)
-> Element s a
-> Refined (InSet 'Regular s) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Element s a -> b
f) \Refined (InSet 'Regular s) b
y -> case b -> Map b (Element s a) -> Maybe (Element s a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Refined (InSet 'Regular s) b -> b
forall {k} (p :: k) x. Refined p x -> x
unrefine Refined (InSet 'Regular s) b
y) Map b (Element s a)
m of
    Maybe (Element s a)
Nothing -> [Char] -> Element s a
forall a. HasCallStack => [Char] -> a
error [Char]
"map: bug: Data.Set.Refined has been subverted"
    Just Element s a
x -> Element s a
x
  where
    !m :: Map b (Element s a)
m = [(b, Element s a)] -> Map b (Element s a)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
      [ (b
y, a -> Element s a
forall a s. a -> Element s a
unsafeElement a
x)
      | a
x <- Set a -> [a]
forall a. Set a -> [a]
Set.toList (Set a -> [a]) -> Set a -> [a]
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s
      , let !y :: b
y = Element s a -> b
f (Element s a -> b) -> Element s a -> b
forall a b. (a -> b) -> a -> b
$ a -> Element s a
forall a s. a -> Element s a
unsafeElement a
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 a m. (KnownSet s a, Monoid m) => (Element s a -> m) -> m
foldMap :: forall s a m. (KnownSet s a, Monoid m) => (Element s a -> m) -> m
foldMap Element s a -> m
f = (a -> m) -> Set a -> m
forall m a. Monoid m => (a -> m) -> Set a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap (Element s a -> m
f (Element s a -> m) -> (a -> Element s a) -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Element s a
forall a s. a -> Element s a
unsafeElement) (Set a -> m) -> Set a -> m
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s

-- | Right associative fold with a lazy accumulator.
foldr :: forall s a b. KnownSet s a => (Element s a -> b -> b) -> b -> b
foldr :: forall s a b. KnownSet s a => (Element s a -> b -> b) -> b -> b
foldr Element s a -> b -> b
f b
z = (a -> b -> b) -> b -> Set a -> b
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr (Element s a -> b -> b
f (Element s a -> b -> b) -> (a -> Element s a) -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Element s a
forall a s. a -> Element s a
unsafeElement) b
z (Set a -> b) -> Set a -> b
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s

-- | Left associative fold with a lazy accumulator.
foldl :: forall s a b. KnownSet s a => (b -> Element s a -> b) -> b -> b
foldl :: forall s a b. KnownSet s a => (b -> Element s a -> b) -> b -> b
foldl b -> Element s a -> b
f b
z = (b -> a -> b) -> b -> Set a -> b
forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl (((Element s a -> b) -> (a -> Element s a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Element s a
forall a s. a -> Element s a
unsafeElement) ((Element s a -> b) -> a -> b)
-> (b -> Element s a -> b) -> b -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Element s a -> b
f) b
z (Set a -> b) -> Set a -> b
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s

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

-- | Left associative fold with a strict accumulator.
foldl' :: forall s a b. KnownSet s a => (b -> Element s a -> b) -> b -> b
foldl' :: forall s a b. KnownSet s a => (b -> Element s a -> b) -> b -> b
foldl' b -> Element s a -> b
f b
z = (b -> a -> b) -> b -> Set a -> b
forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' (((Element s a -> b) -> (a -> Element s a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Element s a
forall a s. a -> Element s a
unsafeElement) ((Element s a -> b) -> a -> b)
-> (b -> Element s a -> b) -> b -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Element s a -> b
f) b
z (Set a -> b) -> Set a -> b
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
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 a. KnownSet s a
  => Either
    (EmptyProof 'Regular s)
    (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
minView :: forall s a.
KnownSet s a =>
Either
  (EmptyProof 'Regular s)
  (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
minView = case Set a -> Maybe (a, Set a)
forall a. Set a -> Maybe (a, Set a)
Set.minView (Set a -> Maybe (a, Set a)) -> Set a -> Maybe (a, Set a)
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s of
  Maybe (a, Set a)
Nothing -> EmptyProof 'Regular s
-> Either
     (EmptyProof 'Regular s)
     (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
forall a b. a -> Either a b
Left (EmptyProof 'Regular s
 -> Either
      (EmptyProof 'Regular s)
      (Element s a, SomeSetWith (SupersetProof 'Regular s) a))
-> EmptyProof 'Regular s
-> Either
     (EmptyProof 'Regular s)
     (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
forall a b. (a -> b) -> a -> b
$ (forall s. InSet 'Regular s :-> InSet 'Regular s)
-> EmptyProof 'Regular s
forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular s) x
forall s. InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset
  Just (a
x, Set a
xs) -> (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
-> Either
     (EmptyProof 'Regular s)
     (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
forall a b. b -> Either a b
Right ((Element s a, SomeSetWith (SupersetProof 'Regular s) a)
 -> Either
      (EmptyProof 'Regular s)
      (Element s a, SomeSetWith (SupersetProof 'Regular s) a))
-> (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
-> Either
     (EmptyProof 'Regular s)
     (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
forall a b. (a -> b) -> a -> b
$ (a -> Element s a
forall a s. a -> Element s a
unsafeElement a
x,) (SomeSetWith (SupersetProof 'Regular s) a
 -> (Element s a, SomeSetWith (SupersetProof 'Regular s) a))
-> SomeSetWith (SupersetProof 'Regular s) a
-> (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
forall a b. (a -> b) -> a -> b
$ Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> SomeSetWith (SupersetProof 'Regular s) a)
-> SomeSetWith (SupersetProof 'Regular s) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Set a
xs \(Proxy s
_ :: Proxy r)
    -> forall s a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r (SupersetProof 'Regular s s
 -> SomeSetWith (SupersetProof 'Regular s) a)
-> SupersetProof 'Regular s s
-> SomeSetWith (SupersetProof 'Regular s) a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular s :-> InSet 'Regular s)
-> SupersetProof 'Regular s s
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular s) x
InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
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 a. KnownSet s a
  => Either
    (EmptyProof 'Regular s)
    (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
maxView :: forall s a.
KnownSet s a =>
Either
  (EmptyProof 'Regular s)
  (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
maxView = case Set a -> Maybe (a, Set a)
forall a. Set a -> Maybe (a, Set a)
Set.maxView (Set a -> Maybe (a, Set a)) -> Set a -> Maybe (a, Set a)
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s of
  Maybe (a, Set a)
Nothing -> EmptyProof 'Regular s
-> Either
     (EmptyProof 'Regular s)
     (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
forall a b. a -> Either a b
Left (EmptyProof 'Regular s
 -> Either
      (EmptyProof 'Regular s)
      (Element s a, SomeSetWith (SupersetProof 'Regular s) a))
-> EmptyProof 'Regular s
-> Either
     (EmptyProof 'Regular s)
     (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
forall a b. (a -> b) -> a -> b
$ (forall s. InSet 'Regular s :-> InSet 'Regular s)
-> EmptyProof 'Regular s
forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular s) x
forall s. InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset
  Just (a
x, Set a
xs) -> (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
-> Either
     (EmptyProof 'Regular s)
     (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
forall a b. b -> Either a b
Right ((Element s a, SomeSetWith (SupersetProof 'Regular s) a)
 -> Either
      (EmptyProof 'Regular s)
      (Element s a, SomeSetWith (SupersetProof 'Regular s) a))
-> (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
-> Either
     (EmptyProof 'Regular s)
     (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
forall a b. (a -> b) -> a -> b
$ (a -> Element s a
forall a s. a -> Element s a
unsafeElement a
x,) (SomeSetWith (SupersetProof 'Regular s) a
 -> (Element s a, SomeSetWith (SupersetProof 'Regular s) a))
-> SomeSetWith (SupersetProof 'Regular s) a
-> (Element s a, SomeSetWith (SupersetProof 'Regular s) a)
forall a b. (a -> b) -> a -> b
$ Set a
-> (forall s.
    Reifies s (Set a) =>
    Proxy s -> SomeSetWith (SupersetProof 'Regular s) a)
-> SomeSetWith (SupersetProof 'Regular s) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Set a
xs \(Proxy s
_ :: Proxy r)
    -> forall s a (p :: * -> *). KnownSet s a => p s -> SomeSetWith p a
SomeSetWith @r (SupersetProof 'Regular s s
 -> SomeSetWith (SupersetProof 'Regular s) a)
-> SupersetProof 'Regular s s
-> SomeSetWith (SupersetProof 'Regular s) a
forall a b. (a -> b) -> a -> b
$ (InSet 'Regular s :-> InSet 'Regular s)
-> SupersetProof 'Regular s s
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Regular s) x -> Refined (InSet 'Regular s) x
InSet 'Regular s :-> InSet 'Regular s
forall p q x. Refined p x -> Refined q x
unsafeSubset

-- | List of elements in the set in ascending order.
toList :: forall s a. KnownSet s a => [Element s a]
toList :: forall s a. KnownSet s a => [Element s a]
toList = Coercion a (Element s a)
-> (Coercible a (Element s a) => [Element s a]) -> [Element s a]
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s a. Coercion a (Element s a)
unsafeCastElement @s @a) ((Coercible a (Element s a) => [Element s a]) -> [Element s a])
-> (Coercible a (Element s a) => [Element s a]) -> [Element s a]
forall a b. (a -> b) -> a -> b
$ [a] -> [Element s a]
forall a b. Coercible a b => a -> b
coerce
  ([a] -> [Element s a]) -> [a] -> [Element s a]
forall a b. (a -> b) -> a -> b
$ Set a -> [a]
forall a. Set a -> [a]
Set.toAscList (Set a -> [a]) -> Set a -> [a]
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s

-- | List of elements in the set in descending order.
toDescList :: forall s a. KnownSet s a => [Element s a]
toDescList :: forall s a. KnownSet s a => [Element s a]
toDescList = Coercion a (Element s a)
-> (Coercible a (Element s a) => [Element s a]) -> [Element s a]
forall {k} (a :: k) (b :: k) r.
Coercion a b -> (Coercible a b => r) -> r
gcoerceWith (forall s a. Coercion a (Element s a)
unsafeCastElement @s @a) ((Coercible a (Element s a) => [Element s a]) -> [Element s a])
-> (Coercible a (Element s a) => [Element s a]) -> [Element s a]
forall a b. (a -> b) -> a -> b
$ [a] -> [Element s a]
forall a b. Coercible a b => a -> b
coerce
  ([a] -> [Element s a]) -> [a] -> [Element s a]
forall a b. (a -> b) -> a -> b
$ Set a -> [a]
forall a. Set a -> [a]
Set.toDescList (Set a -> [a]) -> Set a -> [a]
forall a b. (a -> b) -> a -> b
$ Proxy s -> Set a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> Set a
reflect (Proxy s -> Set a) -> Proxy s -> Set a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s

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

-- | Convert a 'Set' into a 'HashSet', retaining its set of elements, which can
-- be converted with 'castFlavor'.
asHashSet :: forall s a. (Hashable a, KnownSet s a) => HashSet s a
asHashSet :: forall s a. (Hashable a, KnownSet s a) => HashSet s a
asHashSet = HashSet s a
forall s a. (Hashable a, KnownSet s a) => HashSet s a
set2HashSet

-- | 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. Element s x -> Element t x)
  -> (forall x. Element t x -> Element s x)
  -> Coercion (Element s a) (Element t a)
castElement :: forall s t a.
(forall x. Element s x -> Element t x)
-> (forall x. Element t x -> Element s x)
-> Coercion (Element s a) (Element t a)
castElement = (InSet 'Regular s :-> InSet 'Regular t)
-> (InSet 'Regular t :-> InSet 'Regular s)
-> Coercion
     (Refined (InSet 'Regular s) a) (Refined (InSet 'Regular t) a)
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' ''Regular' s s r
--   -> 'Coercion' ('Set' r a) ('Set' s a)
-- castIntersection ( v'IntersectionProof' p1 p2)
--   = 'cast' $ 'castElement' ('andLeft' . p1) (p2 'id' 'id')
-- @
cast
  :: forall s t a. (forall x. Coercion (Element s x) (Element t x))
  -> Coercion (Set s a) (Set t a)
cast :: forall s t a.
(forall x. Coercion (Element s x) (Element t x))
-> Coercion (Set s a) (Set t a)
cast Coercion (Element s Any) (Element t Any)
forall x. Coercion (Element s x) (Element 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 (Set s a) (Set t a)
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
#else
  = repr $ unsafeCoerce Refl
#endif