{-# LANGUAGE CPP #-}
-- | This module implements a way of tracking the contents of a
-- 'Data.HashSet.HashSet' at the type level, and provides utilities for
-- manipulating such sets.
--
-- The contents of a set are associated with a type parameter, e.g. @s@, so that
-- whenever you see the same type parameter, you know you are working with the
-- same set. The type @s@ itself has no internal structure, rather it is merely
-- a skolem type variable (rank-2 polymorphism 'Control.Monad.ST.runST' trick)
-- introduced by "Data.Reflection".
--
-- = Warning
-- This module together with "Data.HashSet" rely on 'Eq' and 'Hashable'
-- instances being lawful: that '==' is an equivalence relation, and that
-- 'Data.Hashable.hashWithSalt' is defined on the quotient by this equivalence
-- relation; at least for the subset of values that are actually encountered at
-- runtime. If this assumption is violated, this module may not be able to
-- uphold its invariants and may throw errors. In particular beware of NaN in
-- 'Float' and 'Double', and, if using @hashable < 1.3@, beware of @0@ and @-0@.
module Data.HashSet.Refined
  (
  -- * Set type
    KnownHashSet
  , HashSet
  -- * Refinement type
  , InSet(..)
  , Flavor(Hashed)
  , Element
  , revealPredicate
  -- * Existentials and common proofs
  , SomeHashSet(..)
  , withHashSet
  , SomeHashSetWith(..)
  , withHashSetWith
  , Some2HashSetWith(..)
  , with2HashSetWith
  , (:->)
  , SupersetProof(..)
  , EmptyProof(..)
  -- * Construction
  , empty
  , singleton
  , SingletonProof(..)
  , fromHashSet
  , fromTraversable
  , FromTraversableProof(..)
  -- * Insertion
  , insert
  , InsertProof(..)
  -- * Deletion
  , delete
  -- * Query
  , member
  , null
  , isSubsetOf
  , SubsetProof(..)
  , disjoint
  , DisjointProof(..)
  -- * Combine
  , union
  , UnionProof(..)
  , difference
  , DifferenceProof(..)
  , intersection
  , IntersectionProof(..)
  -- * Filter
  , filter
  , partition
  , PartitionProof(..)
  -- * Map
  , map
  , MapProof(..)
  -- * Folds
  , foldMap
  , foldr
  , foldl
  , foldr'
  , foldl'
  -- * Conversion
  , toList
  , asSet
  , asIntSet
  -- * Casts
  , castElement
  , cast
  , castFlavor
  ) where

import           Data.Coerce
import           Data.Constraint (Dict(..))
import           Data.Container.Refined.Conversion
import           Data.Container.Refined.Hashable
import           Data.Container.Refined.Proofs
import           Data.Container.Refined.Unsafe
import qualified Data.Foldable as Foldable
import qualified Data.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


-- | To use "Refined" machinery that uses the 'Predicate' typeclass you will
-- need to pattern match on this 'Dict'.
--
-- The reason is that in the default /fast/ implementation of reflection, we
-- don't have @'Typeable' s@, which "Refined" wants for pretty-printing
-- exceptions. We /can/ provide @'Typeable' s@, but at the cost of using the
-- /slow/ implementation of reflection.
revealPredicate
  :: forall s a. (Typeable a, 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`
    --  ^ Work around https://github.com/ekmett/reflection/issues/54
      case (Any :~: Any) -> s :~: s
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: s :~: s' of
        s :~: s
Refl -> Dict (Predicate (InSet 'Hashed s) a)
forall (a :: Constraint). a => Dict a
Dict

-- | @'Element' s a@ is a value of type @a@ that has been verified to be an
-- element of @s@.
--
-- Thus, @'Element' s a@ is a \"refinement\" type of @a@, and this library
-- integrates with an implementation of refimenement types in "Refined", so
-- the machinery from there can be used to manipulate 'Element's (however see
-- 'revealPredicate').
--
-- The underlying @a@ value can be obtained with 'unrefine'. An @a@ can be
-- validated into an @'Element' s a@ with 'member'.
type Element s = Refined (InSet '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

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

-- | Apply an unknown set to a continuation that can accept any set. This gives
-- you a way to refer to the set (the parameter @s@), e.g.:
--
-- @
-- 'withHashSet' ('fromHashSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s
-- @
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

-- | Construct a set from a regular 'Data.HashSet.HashSet'.
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#

-- | An existential wrapper for an as-yet-unknown set, together with a proof of
-- some fact @p@ about the set. Pattern matching on it gives you a way to refer
-- to the set (the parameter @s@). Most functions will return a set in this way,
-- together with a proof that somehow relates the set to the function's inputs.
data SomeHashSetWith p a where
  SomeHashSetWith
    :: forall s a p. KnownHashSet s a => !(p s) -> SomeHashSetWith p a

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

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

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

-- | An empty set.
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

-- | Create a set with a single element.
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

-- | Create a set from the elements of an arbitrary traversable.
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 an element in a set.
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 an element from a set.
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

-- | If an element is in the set, return the proof that it is.
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

-- | If the set is empty, return the proof that it is.
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

-- | If @s@ is a subset of @t@ (or is equal to), return a proof of that.
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

-- | If @s@ and @t@ are disjoint (i.e. their intersection is empty), return a
-- proof of that.
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

-- | The union of two sets.
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

-- unions :: ?

-- | HashSet with elements of @s@ that are not in @t@.
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 of two sets.
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

-- | Return a subset of elements that satisfy the given predicate.
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 a set into two disjoint subsets: those that satisfy the
-- predicate, and those that don't.
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

-- | Apply the given function to each element of the set and collect the
-- results. Note that the resulting set can be smaller.
map
  :: forall s a b. (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
      ]

-- | Map each element of @s@ into a monoid (with proof that it was an element),
-- and combine the results using 'Data.Monoid.<>'.
foldMap :: forall s a m. (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

-- | Right associative fold with a lazy accumulator.
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

-- | Left associative fold with a lazy accumulator.
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

-- | Right associative fold with a strict accumulator.
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

-- | Left associative fold with a strict accumulator.
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

-- | List of elements in the set.
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


-- | Convert an 'IntSet' into a 'Set', retaining its set of elements, which can
-- be converted with 'castFlavor'.
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

-- | Convert an 'IntSet' into a 'HashSet', retaining its set of elements, which
-- can be converted with 'castFlavor'.
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

-- | If elements of @s@ can be weakened to elements of @t@ and vice versa, then
-- @s@ and @t@ actually stand for the same set and @'Element' s@ can be safely
-- interconverted with @'Element' t@.
--
-- The requirement that the weakenings are natural transformations ensures that
-- they don't actually alter the elements. To build these you can compose
-- ':->''s from proofs returned by functions in this module, or "Refined"
-- functions like 'andLeft' or 'leftOr'.
castElement
  :: forall s t a. (forall x. Element s x -> Element t x)
  -> (forall x. Element t x -> Element s x)
  -> Coercion (Element s a) (Element t a)
castElement :: forall s t a.
(forall x. Element s x -> Element t x)
-> (forall x. Element t x -> Element s x)
-> Coercion (Element s a) (Element t a)
castElement = (InSet '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

-- | If elements can be interconverted (e.g. as proved by 'castElement'), then
-- the sets can be interconverted too. For example we can establish that the
-- intersection of a set with itself is interconvertible with that set:
--
-- @
-- castIntersection
--   :: t'IntersectionProof' ''Data.HashSet.Refined.Hashed' s s r
--   -> 'Coercion' ('HashSet' r a) ('HashSet' s a)
-- castIntersection ( v'IntersectionProof' p1 p2)
--   = 'cast' $ 'castElement' ('andLeft' . p1) (p2 'id' 'id')
-- @
cast
  :: forall s t a. (forall x. Coercion (Element s x) (Element t x))
  -> Coercion (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