-- | Non-empty sets.
--
--   Provides type @Set1@ of non-empty sets.
--
--   Import:
--   @
--
--     import           Agda.Utils.Set1 (Set1)
--     import qualified Agda.Utils.Set1 as Set1
--
--   @

module Agda.Utils.Set1
  ( module Agda.Utils.Set1
  , module Set1
  ) where

import Data.Set (Set, empty)
import Data.Set.NonEmpty as Set1

type Set1 = Set1.NESet

ifNull :: Set a -> b -> (Set1 a -> b) -> b
ifNull :: forall a b. Set a -> b -> (Set1 a -> b) -> b
ifNull Set a
s b
b Set1 a -> b
f = b -> (Set1 a -> b) -> Set a -> b
forall r a. r -> (NESet a -> r) -> Set a -> r
Set1.withNonEmpty b
b Set1 a -> b
f Set a
s

-- | Lossless 'toSet'.  Opposite of 'nonEmptySet'.

toSet' :: Maybe (Set1 a) -> Set a
toSet' :: forall a. Maybe (Set1 a) -> Set a
toSet' = Set a -> (Set1 a -> Set a) -> Maybe (Set1 a) -> Set a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set a
forall a. Set a
empty Set1 a -> Set a
forall a. NESet a -> Set a
toSet

-- | A more general type would be @Null m => Set a -> (Set1 a -> m) -> m@
--   but this type is problematic as we do not have a general
--   @instance Applicative m => Null (m ())@.
--
unlessNull :: Applicative m => Set a -> (Set1 a -> m ()) -> m ()
unlessNull :: forall (m :: * -> *) a.
Applicative m =>
Set a -> (Set1 a -> m ()) -> m ()
unlessNull = ((Set1 a -> m ()) -> Set a -> m ())
-> Set a -> (Set1 a -> m ()) -> m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Set1 a -> m ()) -> Set a -> m ())
 -> Set a -> (Set1 a -> m ()) -> m ())
-> ((Set1 a -> m ()) -> Set a -> m ())
-> Set a
-> (Set1 a -> m ())
-> m ()
forall a b. (a -> b) -> a -> b
$ m () -> (Set1 a -> m ()) -> Set a -> m ()
forall r a. r -> (NESet a -> r) -> Set a -> r
Set1.withNonEmpty (m () -> (Set1 a -> m ()) -> Set a -> m ())
-> m () -> (Set1 a -> m ()) -> Set a -> m ()
forall a b. (a -> b) -> a -> b
$ () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
{-# INLINE unlessNull #-}

unlessNullM :: Monad m => m (Set a) -> (Set1 a -> m ()) -> m ()
unlessNullM :: forall (m :: * -> *) a.
Monad m =>
m (Set a) -> (Set1 a -> m ()) -> m ()
unlessNullM m (Set a)
m Set1 a -> m ()
k = m (Set a)
m m (Set a) -> (Set a -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Set a -> (Set1 a -> m ()) -> m ()
forall (m :: * -> *) a.
Applicative m =>
Set a -> (Set1 a -> m ()) -> m ()
`unlessNull` Set1 a -> m ()
k)
{-# INLINE unlessNullM #-}