{-# LANGUAGE CPP #-}
module Data.Set.Refined
(
KnownSet
, Set
, InSet(..)
, Flavor(Regular)
, Element
, revealPredicate
, SomeSet(..)
, withSet
, SomeSetWith(..)
, withSetWith
, Some2SetWith(..)
, with2SetWith
, (:->)
, SupersetProof(..)
, EmptyProof(..)
, empty
, singleton
, SingletonProof(..)
, fromSet
, fromTraversable
, FromTraversableProof(..)
, insert
, InsertProof(..)
, delete
, member
, lookupLT
, lookupGT
, lookupLE
, lookupGE
, null
, isSubsetOf
, SubsetProof(..)
, disjoint
, DisjointProof(..)
, union
, UnionProof(..)
, difference
, DifferenceProof(..)
, intersection
, IntersectionProof(..)
, cartesianProduct
, ProductProof(..)
, disjointUnion
, CoproductProof(..)
, filter
, partition
, PartitionProof(..)
, spanAntitone
, PartialPartitionProof(..)
, splitMember
, SplitProof(..)
, map
, MapProof(..)
, foldMap
, foldr
, foldl
, foldr'
, foldl'
, minView
, maxView
, toList
, toDescList
, asIntSet
, asHashSet
, 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
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`
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
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
data SomeSet a where
SomeSet :: forall s a. KnownSet s a => Proxy# s -> SomeSet a
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
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#
data SomeSetWith p a where
SomeSetWith :: forall s a p. KnownSet s a => !(p s) -> SomeSetWith p a
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
data Some2SetWith p a where
Some2SetWith
:: forall s t a p. (KnownSet s a, KnownSet t a)
=> !(p s t) -> Some2SetWith p a
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
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
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
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
:: 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
:: 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
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
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)
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)
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)
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)
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
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
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
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
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
:: 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
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
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
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
:: 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
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
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
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
]
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
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
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
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
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
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
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
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
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
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
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
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
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