{-# LANGUAGE CPP #-}
module Data.HashSet.Refined
(
KnownHashSet
, HashSet
, InSet(..)
, Flavor(Hashed)
, Element
, revealPredicate
, SomeHashSet(..)
, withHashSet
, SomeHashSetWith(..)
, withHashSetWith
, Some2HashSetWith(..)
, with2HashSetWith
, (:->)
, SupersetProof(..)
, EmptyProof(..)
, empty
, singleton
, SingletonProof(..)
, fromHashSet
, fromTraversable
, FromTraversableProof(..)
, insert
, InsertProof(..)
, delete
, member
, null
, isSubsetOf
, SubsetProof(..)
, disjoint
, DisjointProof(..)
, union
, UnionProof(..)
, difference
, DifferenceProof(..)
, intersection
, IntersectionProof(..)
, filter
, partition
, PartitionProof(..)
, map
, MapProof(..)
, foldMap
, foldr
, foldl
, foldr'
, foldl'
, toList
, asSet
, asIntSet
, 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.HashMap.Lazy as HashMap
import qualified Data.HashSet as HashSet
import Data.Proxy
import Data.Reflection
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
revealPredicate
:: forall s a. (Typeable a, Hashable a, KnownHashSet s a)
=> Dict (Predicate (InSet 'Hashed s) a)
revealPredicate :: forall s a.
(Typeable a, Hashable a, KnownHashSet s a) =>
Dict (Predicate (InSet 'Hashed s) a)
revealPredicate = HashSet a
-> (forall s.
(Typeable s, Reifies s (HashSet a)) =>
Proxy s -> Dict (Predicate (InSet 'Hashed s) a))
-> Dict (Predicate (InSet 'Hashed s) a)
forall a r.
Typeable a =>
a -> (forall s. (Typeable s, Reifies s a) => Proxy s -> r) -> r
reifyTypeable (Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s))
\(Proxy s
_ :: Proxy s') ->
Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s') HashSet a
-> Dict (Predicate (InSet 'Hashed s) a)
-> Dict (Predicate (InSet 'Hashed 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 'Hashed s) a)
forall (a :: Constraint). a => Dict a
Dict
type Element s = Refined (InSet 'Hashed s)
unsafeCastElement :: forall s a. Coercion a (Element s a)
unsafeCastElement :: forall s a. Coercion a (Element s a)
unsafeCastElement = Coercion a (Refined (InSet 'Hashed 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 SomeHashSet a where
SomeHashSet :: forall s a. KnownHashSet s a => Proxy# s -> SomeHashSet a
withHashSet
:: forall a r. SomeHashSet a
-> (forall s. KnownHashSet s a => Proxy s -> r)
-> r
withHashSet :: forall a r.
SomeHashSet a -> (forall s. KnownHashSet s a => Proxy s -> r) -> r
withHashSet (SomeHashSet (Proxy# s
_ :: Proxy# s)) forall s. KnownHashSet s a => Proxy s -> r
k = Proxy s -> r
forall s. KnownHashSet 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
fromHashSet :: forall a. HashSet.HashSet a -> SomeHashSet a
fromHashSet :: forall a. HashSet a -> SomeHashSet a
fromHashSet HashSet a
s = HashSet a
-> (forall s. Reifies s (HashSet a) => Proxy s -> SomeHashSet a)
-> SomeHashSet a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify HashSet a
s \(Proxy s
_ :: Proxy s) -> forall s a. KnownHashSet s a => Proxy# s -> SomeHashSet a
SomeHashSet @s Proxy# s
forall {k} (a :: k). Proxy# a
proxy#
data SomeHashSetWith p a where
SomeHashSetWith
:: forall s a p. KnownHashSet s a => !(p s) -> SomeHashSetWith p a
withHashSetWith
:: forall a r p. SomeHashSetWith p a
-> (forall s. KnownHashSet s a => p s -> r)
-> r
withHashSetWith :: forall a r (p :: * -> *).
SomeHashSetWith p a
-> (forall s. KnownHashSet s a => p s -> r) -> r
withHashSetWith (SomeHashSetWith p s
p) forall s. KnownHashSet s a => p s -> r
k = p s -> r
forall s. KnownHashSet s a => p s -> r
k p s
p
data Some2HashSetWith p a where
Some2HashSetWith
:: forall s t a p. (KnownHashSet s a, KnownHashSet t a)
=> !(p s t) -> Some2HashSetWith p a
with2HashSetWith
:: forall a r p. Some2HashSetWith p a
-> (forall s t. (KnownHashSet s a, KnownHashSet t a) => p s t -> r)
-> r
with2HashSetWith :: forall a r (p :: * -> * -> *).
Some2HashSetWith p a
-> (forall s t. (KnownHashSet s a, KnownHashSet t a) => p s t -> r)
-> r
with2HashSetWith (Some2HashSetWith p s t
p) forall s t. (KnownHashSet s a, KnownHashSet t a) => p s t -> r
k = p s t -> r
forall s t. (KnownHashSet s a, KnownHashSet t a) => p s t -> r
k p s t
p
empty :: forall a. SomeHashSetWith (EmptyProof 'Hashed) a
empty :: forall a. SomeHashSetWith (EmptyProof 'Hashed) a
empty = HashSet a
-> (forall s.
Reifies s (HashSet a) =>
Proxy s -> SomeHashSetWith (EmptyProof 'Hashed) a)
-> SomeHashSetWith (EmptyProof 'Hashed) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify HashSet a
forall a. HashSet a
HashSet.empty \(Proxy s
_ :: Proxy r)
-> forall s a (p :: * -> *).
KnownHashSet s a =>
p s -> SomeHashSetWith p a
SomeHashSetWith @r (EmptyProof 'Hashed s -> SomeHashSetWith (EmptyProof 'Hashed) a)
-> EmptyProof 'Hashed s -> SomeHashSetWith (EmptyProof 'Hashed) a
forall a b. (a -> b) -> a -> b
$ (forall s. InSet 'Hashed s :-> InSet 'Hashed s)
-> EmptyProof 'Hashed s
forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof Refined (InSet 'Hashed s) x -> Refined (InSet 'Hashed s) x
forall s. InSet 'Hashed s :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset
singleton
:: forall a. Hashable a => a -> SomeHashSetWith (SingletonProof 'Hashed a) a
singleton :: forall a.
Hashable a =>
a -> SomeHashSetWith (SingletonProof 'Hashed a) a
singleton a
x = HashSet a
-> (forall s.
Reifies s (HashSet a) =>
Proxy s -> SomeHashSetWith (SingletonProof 'Hashed a) a)
-> SomeHashSetWith (SingletonProof 'Hashed a) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (a -> HashSet a
forall a. Hashable a => a -> HashSet a
HashSet.singleton a
x) \(Proxy s
_ :: Proxy r)
-> forall s a (p :: * -> *).
KnownHashSet s a =>
p s -> SomeHashSetWith p a
SomeHashSetWith @r (SingletonProof 'Hashed a s
-> SomeHashSetWith (SingletonProof 'Hashed a) a)
-> SingletonProof 'Hashed a s
-> SomeHashSetWith (SingletonProof 'Hashed a) a
forall a b. (a -> b) -> a -> b
$ Refined (InSet 'Hashed s) a -> SingletonProof 'Hashed a s
forall (f :: Flavor) a r.
Refined (InSet f r) a -> SingletonProof f a r
SingletonProof (Refined (InSet 'Hashed s) a -> SingletonProof 'Hashed a s)
-> Refined (InSet 'Hashed s) a -> SingletonProof 'Hashed a s
forall a b. (a -> b) -> a -> b
$ a -> Refined (InSet 'Hashed s) a
forall a s. a -> Element s a
unsafeElement a
x
fromTraversable
:: forall t a. (Traversable t, Hashable a)
=> t a -> SomeHashSetWith (FromTraversableProof 'Hashed t a) a
fromTraversable :: forall (t :: * -> *) a.
(Traversable t, Hashable a) =>
t a -> SomeHashSetWith (FromTraversableProof 'Hashed t a) a
fromTraversable t a
xs = HashSet a
-> (forall s.
Reifies s (HashSet a) =>
Proxy s -> SomeHashSetWith (FromTraversableProof 'Hashed t a) a)
-> SomeHashSetWith (FromTraversableProof 'Hashed t a) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify HashSet a
set \(Proxy s
_ :: Proxy r)
-> forall s a (p :: * -> *).
KnownHashSet s a =>
p s -> SomeHashSetWith p a
SomeHashSetWith @r (FromTraversableProof 'Hashed t a s
-> SomeHashSetWith (FromTraversableProof 'Hashed t a) a)
-> FromTraversableProof 'Hashed t a s
-> SomeHashSetWith (FromTraversableProof 'Hashed t a) a
forall a b. (a -> b) -> a -> b
$ t (Refined (InSet 'Hashed s) a)
-> FromTraversableProof 'Hashed t a s
forall (f :: Flavor) (t :: * -> *) a r.
t (Refined (InSet f r) a) -> FromTraversableProof f t a r
FromTraversableProof
(t (Refined (InSet 'Hashed s) a)
-> FromTraversableProof 'Hashed t a s)
-> t (Refined (InSet 'Hashed s) a)
-> FromTraversableProof 'Hashed 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
(HashSet a
set, t (Element Any a)
proof) = (HashSet a -> a -> (HashSet a, Element Any a))
-> HashSet a -> t a -> (HashSet a, t (Element Any a))
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
(\HashSet a
s a
x -> let !s' :: HashSet a
s' = a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert a
x HashSet a
s in (HashSet a
s', a -> Element Any a
forall a s. a -> Element s a
unsafeElement a
x))
HashSet a
forall a. HashSet a
HashSet.empty
t a
xs
insert
:: forall s a. (Hashable a, KnownHashSet s a)
=> a -> SomeHashSetWith (InsertProof 'Hashed a s) a
insert :: forall s a.
(Hashable a, KnownHashSet s a) =>
a -> SomeHashSetWith (InsertProof 'Hashed a s) a
insert a
x = HashSet a
-> (forall s.
Reifies s (HashSet a) =>
Proxy s -> SomeHashSetWith (InsertProof 'Hashed a s) a)
-> SomeHashSetWith (InsertProof 'Hashed a s) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert a
x (HashSet a -> HashSet a) -> HashSet a -> HashSet a
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet 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 :: * -> *).
KnownHashSet s a =>
p s -> SomeHashSetWith p a
SomeHashSetWith @r (InsertProof 'Hashed a s s
-> SomeHashSetWith (InsertProof 'Hashed a s) a)
-> InsertProof 'Hashed a s s
-> SomeHashSetWith (InsertProof 'Hashed a s) a
forall a b. (a -> b) -> a -> b
$ Refined (InSet 'Hashed s) a
-> (InSet 'Hashed s :-> InSet 'Hashed s)
-> InsertProof 'Hashed 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 'Hashed s) a
forall a s. a -> Element s a
unsafeElement a
x) Refined (InSet 'Hashed s) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed s :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset
delete
:: forall s a. (Hashable a, KnownHashSet s a)
=> a -> SomeHashSetWith (SupersetProof 'Hashed s) a
delete :: forall s a.
(Hashable a, KnownHashSet s a) =>
a -> SomeHashSetWith (SupersetProof 'Hashed s) a
delete a
x = HashSet a
-> (forall s.
Reifies s (HashSet a) =>
Proxy s -> SomeHashSetWith (SupersetProof 'Hashed s) a)
-> SomeHashSetWith (SupersetProof 'Hashed s) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.delete a
x (HashSet a -> HashSet a) -> HashSet a -> HashSet a
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet 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 :: * -> *).
KnownHashSet s a =>
p s -> SomeHashSetWith p a
SomeHashSetWith @s (SupersetProof 'Hashed s s
-> SomeHashSetWith (SupersetProof 'Hashed s) a)
-> SupersetProof 'Hashed s s
-> SomeHashSetWith (SupersetProof 'Hashed s) a
forall a b. (a -> b) -> a -> b
$ (InSet 'Hashed s :-> InSet 'Hashed s) -> SupersetProof 'Hashed s s
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Hashed s) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed s :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset
member :: forall s a. (Hashable a, KnownHashSet s a) => a -> Maybe (Element s a)
member :: forall s a.
(Hashable a, KnownHashSet s a) =>
a -> Maybe (Element s a)
member a
x
| a
x a -> HashSet a -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HashSet.member` Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet 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
null :: forall s a. KnownHashSet s a => Maybe (EmptyProof 'Hashed s)
null :: forall s a. KnownHashSet s a => Maybe (EmptyProof 'Hashed s)
null
| HashSet a -> Bool
forall a. HashSet a -> Bool
HashSet.null (HashSet a -> Bool) -> HashSet a -> Bool
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s = EmptyProof 'Hashed s -> Maybe (EmptyProof 'Hashed s)
forall a. a -> Maybe a
Just (EmptyProof 'Hashed s -> Maybe (EmptyProof 'Hashed s))
-> EmptyProof 'Hashed s -> Maybe (EmptyProof 'Hashed s)
forall a b. (a -> b) -> a -> b
$ (forall s. InSet 'Hashed s :-> InSet 'Hashed s)
-> EmptyProof 'Hashed s
forall (f :: Flavor) r.
(forall s. InSet f r :-> InSet f s) -> EmptyProof f r
EmptyProof Refined (InSet 'Hashed s) x -> Refined (InSet 'Hashed s) x
forall s. InSet 'Hashed s :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset
| Bool
otherwise = Maybe (EmptyProof 'Hashed s)
forall a. Maybe a
Nothing
isSubsetOf
:: forall s t a. (Hashable a, KnownHashSet s a, KnownHashSet t a)
=> Maybe (SubsetProof 'Hashed s t)
isSubsetOf :: forall s t a.
(Hashable a, KnownHashSet s a, KnownHashSet t a) =>
Maybe (SubsetProof 'Hashed s t)
isSubsetOf
#if MIN_VERSION_unordered_containers(0, 2, 12)
| Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) HashSet a -> HashSet a -> Bool
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> Bool
`HashSet.isSubsetOf` Proxy t -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> HashSet a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t)
#else
| all (`HashSet.member` reflect (Proxy @t)) (reflect (Proxy @s))
#endif
= SubsetProof 'Hashed s t -> Maybe (SubsetProof 'Hashed s t)
forall a. a -> Maybe a
Just (SubsetProof 'Hashed s t -> Maybe (SubsetProof 'Hashed s t))
-> SubsetProof 'Hashed s t -> Maybe (SubsetProof 'Hashed s t)
forall a b. (a -> b) -> a -> b
$ (InSet 'Hashed s :-> InSet 'Hashed t) -> SubsetProof 'Hashed s t
forall (f :: Flavor) s r.
(InSet f s :-> InSet f r) -> SubsetProof f s r
SubsetProof Refined (InSet 'Hashed s) x -> Refined (InSet 'Hashed t) x
InSet 'Hashed s :-> InSet 'Hashed t
forall p q x. Refined p x -> Refined q x
unsafeSubset
| Bool
otherwise = Maybe (SubsetProof 'Hashed s t)
forall a. Maybe a
Nothing
disjoint
:: forall s t a. (Hashable a, KnownHashSet s a, KnownHashSet t a)
=> Maybe (DisjointProof 'Hashed s t)
disjoint :: forall s t a.
(Hashable a, KnownHashSet s a, KnownHashSet t a) =>
Maybe (DisjointProof 'Hashed s t)
disjoint
| HashSet a -> Bool
forall a. HashSet a -> Bool
HashSet.null
(HashSet a -> Bool) -> HashSet a -> Bool
forall a b. (a -> b) -> a -> b
$ HashSet a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.intersection (Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) (Proxy t -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> HashSet a
reflect (Proxy t -> HashSet a) -> Proxy t -> HashSet a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t)
= DisjointProof 'Hashed s t -> Maybe (DisjointProof 'Hashed s t)
forall a. a -> Maybe a
Just (DisjointProof 'Hashed s t -> Maybe (DisjointProof 'Hashed s t))
-> DisjointProof 'Hashed s t -> Maybe (DisjointProof 'Hashed s t)
forall a b. (a -> b) -> a -> b
$ (forall t.
(InSet 'Hashed t :-> InSet 'Hashed s)
-> (InSet 'Hashed t :-> InSet 'Hashed t)
-> forall u x.
Refined (InSet 'Hashed t) x -> Refined (InSet 'Hashed u) x)
-> DisjointProof 'Hashed 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 'Hashed t :-> InSet 'Hashed s
f InSet 'Hashed t :-> InSet 'Hashed t
g -> (InSet 'Hashed t :-> InSet 'Hashed s)
-> (InSet 'Hashed t :-> InSet 'Hashed t)
-> InSet 'Hashed t :-> InSet 'Hashed u
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Hashed t) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed t :-> InSet 'Hashed s
f Refined (InSet 'Hashed t) x -> Refined (InSet 'Hashed t) x
InSet 'Hashed t :-> InSet 'Hashed t
g
| Bool
otherwise = Maybe (DisjointProof 'Hashed s t)
forall a. Maybe a
Nothing
union
:: forall s t a. (Hashable a, KnownHashSet s a, KnownHashSet t a)
=> SomeHashSetWith (UnionProof 'Hashed s t) a
union :: forall s t a.
(Hashable a, KnownHashSet s a, KnownHashSet t a) =>
SomeHashSetWith (UnionProof 'Hashed s t) a
union = HashSet a
-> (forall s.
Reifies s (HashSet a) =>
Proxy s -> SomeHashSetWith (UnionProof 'Hashed s t) a)
-> SomeHashSetWith (UnionProof 'Hashed s t) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) HashSet a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HashSet.union` Proxy t -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> HashSet a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))
\(Proxy s
_ :: Proxy r) -> forall s a (p :: * -> *).
KnownHashSet s a =>
p s -> SomeHashSetWith p a
SomeHashSetWith @r
(UnionProof 'Hashed s t s
-> SomeHashSetWith (UnionProof 'Hashed s t) a)
-> UnionProof 'Hashed s t s
-> SomeHashSetWith (UnionProof 'Hashed s t) a
forall a b. (a -> b) -> a -> b
$ ((InSet 'Hashed s || InSet 'Hashed t) :-> InSet 'Hashed s)
-> (forall u.
(InSet 'Hashed s :-> InSet 'Hashed u)
-> (InSet 'Hashed t :-> InSet 'Hashed u)
-> InSet 'Hashed s :-> InSet 'Hashed u)
-> UnionProof 'Hashed 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 'Hashed s || InSet 'Hashed t) x
-> Refined (InSet 'Hashed s) x
(InSet 'Hashed s || InSet 'Hashed t) :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Hashed s :-> InSet 'Hashed u)
-> (InSet 'Hashed t :-> InSet 'Hashed u)
-> Refined (InSet 'Hashed s) x
-> Refined (InSet 'Hashed u) x
(InSet 'Hashed s :-> InSet 'Hashed u)
-> (InSet 'Hashed t :-> InSet 'Hashed u)
-> InSet 'Hashed s :-> InSet 'Hashed u
forall u.
(InSet 'Hashed s :-> InSet 'Hashed u)
-> (InSet 'Hashed t :-> InSet 'Hashed u)
-> InSet 'Hashed s :-> InSet 'Hashed u
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2
difference
:: forall s t a. (Hashable a, KnownHashSet s a, KnownHashSet t a)
=> SomeHashSetWith (DifferenceProof 'Hashed s t) a
difference :: forall s t a.
(Hashable a, KnownHashSet s a, KnownHashSet t a) =>
SomeHashSetWith (DifferenceProof 'Hashed s t) a
difference = HashSet a
-> (forall s.
Reifies s (HashSet a) =>
Proxy s -> SomeHashSetWith (DifferenceProof 'Hashed s t) a)
-> SomeHashSetWith (DifferenceProof 'Hashed s t) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) HashSet a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HashSet.difference` Proxy t -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> HashSet a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))
\(Proxy s
_ :: Proxy r) -> forall s a (p :: * -> *).
KnownHashSet s a =>
p s -> SomeHashSetWith p a
SomeHashSetWith @r
(DifferenceProof 'Hashed s t s
-> SomeHashSetWith (DifferenceProof 'Hashed s t) a)
-> DifferenceProof 'Hashed s t s
-> SomeHashSetWith (DifferenceProof 'Hashed s t) a
forall a b. (a -> b) -> a -> b
$ (InSet 'Hashed s :-> InSet 'Hashed s)
-> (forall u.
(InSet 'Hashed u :-> InSet 'Hashed s)
-> (InSet 'Hashed u :-> InSet 'Hashed t)
-> forall v x.
Refined (InSet 'Hashed u) x -> Refined (InSet 'Hashed v) x)
-> (InSet 'Hashed s :-> (InSet 'Hashed t || InSet 'Hashed s))
-> DifferenceProof 'Hashed 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 'Hashed s) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed s :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset (\InSet 'Hashed u :-> InSet 'Hashed s
f InSet 'Hashed u :-> InSet 'Hashed t
g -> (InSet 'Hashed u :-> InSet 'Hashed s)
-> (InSet 'Hashed u :-> InSet 'Hashed t)
-> InSet 'Hashed u :-> InSet 'Hashed v
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Hashed u) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed u :-> InSet 'Hashed s
f Refined (InSet 'Hashed u) x -> Refined (InSet 'Hashed t) x
InSet 'Hashed u :-> InSet 'Hashed t
g) Refined (InSet 'Hashed s) x
-> Refined (InSet 'Hashed t || InSet 'Hashed s) x
InSet 'Hashed s :-> (InSet 'Hashed t || InSet 'Hashed s)
forall p q x. Refined p x -> Refined q x
unsafeSubset
intersection
:: forall s t a. (Hashable a, KnownHashSet s a, KnownHashSet t a)
=> SomeHashSetWith (IntersectionProof 'Hashed s t) a
intersection :: forall s t a.
(Hashable a, KnownHashSet s a, KnownHashSet t a) =>
SomeHashSetWith (IntersectionProof 'Hashed s t) a
intersection
= HashSet a
-> (forall s.
Reifies s (HashSet a) =>
Proxy s -> SomeHashSetWith (IntersectionProof 'Hashed s t) a)
-> SomeHashSetWith (IntersectionProof 'Hashed s t) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) HashSet a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HashSet.intersection` Proxy t -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy t -> HashSet a
reflect (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))
\(Proxy s
_ :: Proxy r) -> forall s a (p :: * -> *).
KnownHashSet s a =>
p s -> SomeHashSetWith p a
SomeHashSetWith @r
(IntersectionProof 'Hashed s t s
-> SomeHashSetWith (IntersectionProof 'Hashed s t) a)
-> IntersectionProof 'Hashed s t s
-> SomeHashSetWith (IntersectionProof 'Hashed s t) a
forall a b. (a -> b) -> a -> b
$ (InSet 'Hashed s :-> (InSet 'Hashed s && InSet 'Hashed t))
-> (forall u.
(InSet 'Hashed u :-> InSet 'Hashed s)
-> (InSet 'Hashed u :-> InSet 'Hashed t)
-> InSet 'Hashed u :-> InSet 'Hashed s)
-> IntersectionProof 'Hashed 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 'Hashed s) x
-> Refined (InSet 'Hashed s && InSet 'Hashed t) x
InSet 'Hashed s :-> (InSet 'Hashed s && InSet 'Hashed t)
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Hashed u :-> InSet 'Hashed s)
-> (InSet 'Hashed u :-> InSet 'Hashed t)
-> Refined (InSet 'Hashed u) x
-> Refined (InSet 'Hashed s) x
(InSet 'Hashed u :-> InSet 'Hashed s)
-> (InSet 'Hashed u :-> InSet 'Hashed t)
-> InSet 'Hashed u :-> InSet 'Hashed s
forall u.
(InSet 'Hashed u :-> InSet 'Hashed s)
-> (InSet 'Hashed u :-> InSet 'Hashed t)
-> InSet 'Hashed u :-> InSet 'Hashed s
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2
filter
:: forall s a. KnownHashSet s a
=> (Element s a -> Bool) -> SomeHashSetWith (SupersetProof 'Hashed s) a
filter :: forall s a.
KnownHashSet s a =>
(Element s a -> Bool)
-> SomeHashSetWith (SupersetProof 'Hashed s) a
filter Element s a -> Bool
p = HashSet a
-> (forall s.
Reifies s (HashSet a) =>
Proxy s -> SomeHashSetWith (SupersetProof 'Hashed s) a)
-> SomeHashSetWith (SupersetProof 'Hashed s) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify ((a -> Bool) -> HashSet a -> HashSet a
forall a. (a -> Bool) -> HashSet a -> HashSet a
HashSet.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) (HashSet a -> HashSet a) -> HashSet a -> HashSet a
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet 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 :: * -> *).
KnownHashSet s a =>
p s -> SomeHashSetWith p a
SomeHashSetWith @r (SupersetProof 'Hashed s s
-> SomeHashSetWith (SupersetProof 'Hashed s) a)
-> SupersetProof 'Hashed s s
-> SomeHashSetWith (SupersetProof 'Hashed s) a
forall a b. (a -> b) -> a -> b
$ (InSet 'Hashed s :-> InSet 'Hashed s) -> SupersetProof 'Hashed s s
forall (f :: Flavor) s r.
(InSet f r :-> InSet f s) -> SupersetProof f s r
SupersetProof Refined (InSet 'Hashed s) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed s :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset
partition
:: forall s a. KnownHashSet s a
=> (Element s a -> Bool) -> Some2HashSetWith (PartitionProof 'Hashed s a) a
partition :: forall s a.
KnownHashSet s a =>
(Element s a -> Bool)
-> Some2HashSetWith (PartitionProof 'Hashed s a) a
partition Element s a -> Bool
p = HashSet a
-> (forall s.
Reifies s (HashSet a) =>
Proxy s -> Some2HashSetWith (PartitionProof 'Hashed s a) a)
-> Some2HashSetWith (PartitionProof 'Hashed s a) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify ((a -> Bool) -> HashSet a -> HashSet a
forall a. (a -> Bool) -> HashSet a -> HashSet a
HashSet.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) (HashSet a -> HashSet a) -> HashSet a -> HashSet a
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s)
\(Proxy s
_ :: Proxy r)
-> HashSet a
-> (forall s.
Reifies s (HashSet a) =>
Proxy s -> Some2HashSetWith (PartitionProof 'Hashed s a) a)
-> Some2HashSetWith (PartitionProof 'Hashed s a) a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify ((a -> Bool) -> HashSet a -> HashSet a
forall a. (a -> Bool) -> HashSet a -> HashSet a
HashSet.filter (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) (HashSet a -> HashSet a) -> HashSet a -> HashSet a
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s)
\(Proxy s
_ :: Proxy q)
-> forall s t a (p :: * -> * -> *).
(KnownHashSet s a, KnownHashSet t a) =>
p s t -> Some2HashSetWith p a
Some2HashSetWith @s @r (PartitionProof 'Hashed s a s s
-> Some2HashSetWith (PartitionProof 'Hashed s a) a)
-> PartitionProof 'Hashed s a s s
-> Some2HashSetWith (PartitionProof 'Hashed s a) a
forall a b. (a -> b) -> a -> b
$ (Element s a -> Either (Element s a) (Refined (InSet 'Hashed s) a))
-> ((InSet 'Hashed s || InSet 'Hashed s) :-> InSet 'Hashed s)
-> (forall t.
(InSet 'Hashed s :-> InSet 'Hashed t)
-> (InSet 'Hashed s :-> InSet 'Hashed t)
-> InSet 'Hashed s :-> InSet 'Hashed t)
-> (forall t.
(InSet 'Hashed t :-> InSet 'Hashed s)
-> (InSet 'Hashed t :-> InSet 'Hashed s)
-> forall u x.
Refined (InSet 'Hashed t) x -> Refined (InSet 'Hashed u) x)
-> PartitionProof 'Hashed 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 'Hashed s) a)
forall a b. a -> Either a b
Left (Element s a -> Either (Element s a) (Refined (InSet 'Hashed s) a))
-> Element s a
-> Either (Element s a) (Refined (InSet 'Hashed 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 'Hashed s) a
-> Either (Element s a) (Refined (InSet 'Hashed s) a)
forall a b. b -> Either a b
Right (Refined (InSet 'Hashed s) a
-> Either (Element s a) (Refined (InSet 'Hashed s) a))
-> Refined (InSet 'Hashed s) a
-> Either (Element s a) (Refined (InSet 'Hashed s) a)
forall a b. (a -> b) -> a -> b
$ a -> Refined (InSet 'Hashed s) a
forall a s. a -> Element s a
unsafeElement (a -> Refined (InSet 'Hashed s) a)
-> a -> Refined (InSet 'Hashed 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 'Hashed s || InSet 'Hashed s) x
-> Refined (InSet 'Hashed s) x
(InSet 'Hashed s || InSet 'Hashed s) :-> InSet 'Hashed s
forall p q x. Refined p x -> Refined q x
unsafeSubset (InSet 'Hashed s :-> InSet 'Hashed t)
-> (InSet 'Hashed s :-> InSet 'Hashed t)
-> Refined (InSet 'Hashed s) x
-> Refined (InSet 'Hashed t) x
(InSet 'Hashed s :-> InSet 'Hashed t)
-> (InSet 'Hashed s :-> InSet 'Hashed t)
-> InSet 'Hashed s :-> InSet 'Hashed t
forall t.
(InSet 'Hashed s :-> InSet 'Hashed t)
-> (InSet 'Hashed s :-> InSet 'Hashed t)
-> InSet 'Hashed s :-> InSet 'Hashed t
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 \InSet 'Hashed t :-> InSet 'Hashed s
f InSet 'Hashed t :-> InSet 'Hashed s
g -> (InSet 'Hashed t :-> InSet 'Hashed s)
-> (InSet 'Hashed t :-> InSet 'Hashed s)
-> InSet 'Hashed t :-> InSet 'Hashed u
forall p' q' p'' q'' p q. (p' :-> q') -> (p'' :-> q'') -> p :-> q
unsafeSubsetWith2 Refined (InSet 'Hashed t) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed t :-> InSet 'Hashed s
f Refined (InSet 'Hashed t) x -> Refined (InSet 'Hashed s) x
InSet 'Hashed t :-> InSet 'Hashed s
g
map
:: forall s a b. (Hashable b, KnownHashSet s a)
=> (Element s a -> b) -> SomeHashSetWith (MapProof 'Hashed s a b) b
map :: forall s a b.
(Hashable b, KnownHashSet s a) =>
(Element s a -> b) -> SomeHashSetWith (MapProof 'Hashed s a b) b
map Element s a -> b
f = HashSet b
-> (forall s.
Reifies s (HashSet b) =>
Proxy s -> SomeHashSetWith (MapProof 'Hashed s a b) b)
-> SomeHashSetWith (MapProof 'Hashed s a b) b
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify (HashMap b (Element s a) -> HashSet b
forall k a. HashMap k a -> HashSet k
HashMap.keysSet HashMap b (Element s a)
m)
\(Proxy s
_ :: Proxy r) -> forall s a (p :: * -> *).
KnownHashSet s a =>
p s -> SomeHashSetWith p a
SomeHashSetWith @r
(MapProof 'Hashed s a b s
-> SomeHashSetWith (MapProof 'Hashed s a b) b)
-> MapProof 'Hashed s a b s
-> SomeHashSetWith (MapProof 'Hashed s a b) b
forall a b. (a -> b) -> a -> b
$ (Element s a -> Refined (InSet 'Hashed s) b)
-> (Refined (InSet 'Hashed s) b -> Element s a)
-> MapProof 'Hashed 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 'Hashed s) b
forall a s. a -> Element s a
unsafeElement (b -> Refined (InSet 'Hashed s) b)
-> (Element s a -> b) -> Element s a -> Refined (InSet 'Hashed s) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Element s a -> b
f) \Refined (InSet 'Hashed s) b
y -> case b -> HashMap b (Element s a) -> Maybe (Element s a)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup (Refined (InSet 'Hashed s) b -> b
forall {k} (p :: k) x. Refined p x -> x
unrefine Refined (InSet 'Hashed s) b
y) HashMap 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.HashSet.Refined has been subverted"
Just Element s a
x -> Element s a
x
where
!m :: HashMap b (Element s a)
m = [(b, Element s a)] -> HashMap b (Element s a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList
[ (b
y, a -> Element s a
forall a s. a -> Element s a
unsafeElement a
x)
| a
x <- HashSet a -> [a]
forall a. HashSet a -> [a]
HashSet.toList (HashSet a -> [a]) -> HashSet a -> [a]
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet 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. (KnownHashSet s a, Monoid m) => (Element s a -> m) -> m
foldMap :: forall s a m.
(KnownHashSet s a, Monoid m) =>
(Element s a -> m) -> m
foldMap Element s a -> m
f = (a -> m) -> HashSet a -> m
forall m a. Monoid m => (a -> m) -> HashSet 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) (HashSet a -> m) -> HashSet a -> m
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet 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. KnownHashSet s a => (Element s a -> b -> b) -> b -> b
foldr :: forall s a b. KnownHashSet s a => (Element s a -> b -> b) -> b -> b
foldr Element s a -> b -> b
f b
z = (a -> b -> b) -> b -> HashSet a -> b
forall b a. (b -> a -> a) -> a -> HashSet b -> a
HashSet.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 (HashSet a -> b) -> HashSet a -> b
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet 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. KnownHashSet s a => (b -> Element s a -> b) -> b -> b
foldl :: forall s a b. KnownHashSet s a => (b -> Element s a -> b) -> b -> b
foldl b -> Element s a -> b
f b
z = (b -> a -> b) -> b -> HashSet a -> b
forall b a. (b -> a -> b) -> b -> HashSet a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Foldable.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 (HashSet a -> b) -> HashSet a -> b
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet 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. KnownHashSet s a => (Element s a -> b -> b) -> b -> b
foldr' :: forall s a b. KnownHashSet s a => (Element s a -> b -> b) -> b -> b
foldr' Element s a -> b -> b
f b
z = (a -> b -> b) -> b -> HashSet a -> b
forall b a. (b -> a -> a) -> a -> HashSet b -> a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Foldable.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 (HashSet a -> b) -> HashSet a -> b
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet 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. KnownHashSet s a => (b -> Element s a -> b) -> b -> b
foldl' :: forall s a b. KnownHashSet s a => (b -> Element s a -> b) -> b -> b
foldl' b -> Element s a -> b
f b
z = (b -> a -> b) -> b -> HashSet a -> b
forall b a. (b -> a -> b) -> b -> HashSet a -> b
HashSet.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 (HashSet a -> b) -> HashSet a -> b
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s
toList :: forall s a. KnownHashSet s a => [Element s a]
toList :: forall s a. KnownHashSet 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
$ HashSet a -> [a]
forall a. HashSet a -> [a]
HashSet.toList (HashSet a -> [a]) -> HashSet a -> [a]
forall a b. (a -> b) -> a -> b
$ Proxy s -> HashSet a
forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
forall (proxy :: * -> *). proxy s -> HashSet a
reflect (Proxy s -> HashSet a) -> Proxy s -> HashSet a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s
asSet :: forall s a. (Ord a, KnownHashSet s a) => Set s a
asSet :: forall s a. (Ord a, KnownHashSet s a) => Set s a
asSet = Set s a
forall s a. (Ord a, KnownHashSet s a) => Set s a
hashSet2Set
asIntSet :: forall s. KnownHashSet s Int => IntSet s
asIntSet :: forall s. KnownHashSet s Int => IntSet s
asIntSet = IntSet s
forall s. KnownHashSet s Int => IntSet s
hashSet2IntSet
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 'Hashed s :-> InSet 'Hashed t)
-> (InSet 'Hashed t :-> InSet 'Hashed s)
-> Coercion
(Refined (InSet 'Hashed s) a) (Refined (InSet 'Hashed 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 (HashSet s a) (HashSet t a)
cast :: forall s t a.
(forall x. Coercion (Element s x) (Element t x))
-> Coercion (HashSet s a) (HashSet 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 (HashSet s a) (HashSet t a)
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
#else
= repr $ unsafeCoerce Refl
#endif