    {-# OPTIONS_GHC -fno-warn-orphans #-}

    -- | Overloaded @null@ and @empty@ for collections and sequences.

    module Agda.Utils.Null where

    import Prelude hiding (null)

    import Control.Monad
    import Control.Monad.Reader
    import Control.Monad.State

    import qualified Data.ByteString.Char8 as ByteStringChar8
    import qualified Data.ByteString.Lazy as ByteStringLazy

    import Data.HashMap.Strict (HashMap)
    import qualified Data.HashMap.Strict as HashMap
    import Data.HashSet (HashSet)
    import qualified Data.HashSet as HashSet
    import Data.IntMap (IntMap)
    import qualified Data.IntMap as IntMap
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet
    import qualified Data.List as List
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Sequence (Seq)
    import qualified Data.Sequence as Seq
    import Data.Set (Set)
    import qualified Data.Set as Set

    import Data.Text (Text)
    import qualified Data.Text as Text

    import Text.PrettyPrint (Doc, isEmpty)

    import Agda.Utils.Bag (Bag)
    import qualified Agda.Utils.Bag as Bag

    import Agda.Utils.Impossible

    class Null a where
      empty :: a
      null  :: a -> Bool
      -- ^ Satisfying @null empty == True@.

      default null :: Eq a => a -> Bool
      null = (a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    forall a. Null a => a
    empty)

    instance Null () where
      empty :: ()
    empty  = ()
      null :: () -> Bool
    null ()
    _ = Bool
    True

    instance (Null a, Null b) => Null (a,b) where
      empty :: (a, b)
    empty      = (a
    forall a. Null a => a
    empty, b
    forall a. Null a => a
    empty)
      null :: (a, b) -> Bool
    null (a
    a,b
    b) = a -> Bool
    forall a. Null a => a -> Bool
    null a
    a Bool -> Bool -> Bool
    && b -> Bool
    forall a. Null a => a -> Bool
    null b
    b

    instance (Null a, Null b, Null c) => Null (a,b,c) where
      empty :: (a, b, c)
    empty        = (a
    forall a. Null a => a
    empty, b
    forall a. Null a => a
    empty, c
    forall a. Null a => a
    empty)
      null :: (a, b, c) -> Bool
    null (a
    a,b
    b,c
    c) = a -> Bool
    forall a. Null a => a -> Bool
    null a
    a Bool -> Bool -> Bool
    && b -> Bool
    forall a. Null a => a -> Bool
    null b
    b Bool -> Bool -> Bool
    && c -> Bool
    forall a. Null a => a -> Bool
    null c
    c

    instance (Null a, Null b, Null c, Null d) => Null (a,b,c,d) where
      empty :: (a, b, c, d)
    empty          = (a
    forall a. Null a => a
    empty, b
    forall a. Null a => a
    empty, c
    forall a. Null a => a
    empty, d
    forall a. Null a => a
    empty)
      null :: (a, b, c, d) -> Bool
    null (a
    a,b
    b,c
    c,d
    d) = a -> Bool
    forall a. Null a => a -> Bool
    null a
    a Bool -> Bool -> Bool
    && b -> Bool
    forall a. Null a => a -> Bool
    null b
    b Bool -> Bool -> Bool
    && c -> Bool
    forall a. Null a => a -> Bool
    null c
    c Bool -> Bool -> Bool
    && d -> Bool
    forall a. Null a => a -> Bool
    null d
    d

    instance Null ByteStringChar8.ByteString where
      empty :: ByteString
    empty = ByteString
    ByteStringChar8.empty
      null :: ByteString -> Bool
    null  = ByteString -> Bool
    ByteStringChar8.null

    instance Null ByteStringLazy.ByteString where
      empty :: ByteString
    empty = ByteString
    ByteStringLazy.empty
      null :: ByteString -> Bool
    null  = ByteString -> Bool
    ByteStringLazy.null

    instance Null Text where
      empty :: Text
    empty = Text
    Text.empty
      null :: Text -> Bool
    null  = Text -> Bool
    Text.null

    instance Null [a] where
      empty :: [a]
    empty = []
      null :: [a] -> Bool
    null  = [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    List.null

    instance Null (Bag a) where
      empty :: Bag a
    empty = Bag a
    forall a. Bag a
    Bag.empty
      null :: Bag a -> Bool
    null  = Bag a -> Bool
    forall a. Bag a -> Bool
    Bag.null

    instance Null (IntMap a) where
      empty :: IntMap a
    empty = IntMap a
    forall a. IntMap a
    IntMap.empty
      null :: IntMap a -> Bool
    null  = IntMap a -> Bool
    forall a. IntMap a -> Bool
    IntMap.null

    instance Null IntSet where
      empty :: IntSet
    empty = IntSet
    IntSet.empty
      null :: IntSet -> Bool
    null  = IntSet -> Bool
    IntSet.null

    instance Null (Map k a) where
      empty :: Map k a
    empty = Map k a
    forall k a. Map k a
    Map.empty
      null :: Map k a -> Bool
    null  = Map k a -> Bool
    forall k a. Map k a -> Bool
    Map.null

    instance Null (HashMap k a) where
      empty :: HashMap k a
    empty = HashMap k a
    forall k a. HashMap k a
    HashMap.empty
      null :: HashMap k a -> Bool
    null  = HashMap k a -> Bool
    forall k a. HashMap k a -> Bool
    HashMap.null

    instance Null (HashSet a) where
      empty :: HashSet a
    empty = HashSet a
    forall a. HashSet a
    HashSet.empty
      null :: HashSet a -> Bool
    null  = HashSet a -> Bool
    forall a. HashSet a -> Bool
    HashSet.null

    instance Null (Seq a) where
      empty :: Seq a
    empty = Seq a
    forall a. Seq a
    Seq.empty
      null :: Seq a -> Bool
    null  = Seq a -> Bool
    forall a. Seq a -> Bool
    Seq.null

    instance Null (Set a) where
      empty :: Set a
    empty = Set a
    forall a. Set a
    Set.empty
      null :: Set a -> Bool
    null  = Set a -> Bool
    forall a. Set a -> Bool
    Set.null

    -- | A 'Maybe' is 'null' when it corresponds to the empty list.
    instance Null (Maybe a) where
      empty :: Maybe a
    empty = Maybe a
    forall a. Maybe a
    Nothing
      null :: Maybe a -> Bool
    null Maybe a
    Nothing  = Bool
    True
      null (Just a
    a) = Bool
    False

    instance Null Doc where
      empty :: Doc
    empty = Doc
    forall a. Monoid a => a
    mempty
      null :: Doc -> Bool
    null  = Doc -> Bool
    isEmpty

    instance (Null (m a), Monad m) => Null (ReaderT r m a) where
      empty :: ReaderT r m a
    empty = m a -> ReaderT r m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift m a
    forall a. Null a => a
    empty
      null :: ReaderT r m a -> Bool
    null  = ReaderT r m a -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance (Null (m a), Monad m) => Null (StateT r m a) where
      empty :: StateT r m a
    empty = m a -> StateT r m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift m a
    forall a. Null a => a
    empty
      null :: StateT r m a -> Bool
    null  = StateT r m a -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- * Testing for null.

    ifNull :: (Null a) => a -> b -> (a -> b) -> b
    ifNull :: forall a b. Null a => a -> b -> (a -> b) -> b
    ifNull a
    a b
    b a -> b
    k = if a -> Bool
    forall a. Null a => a -> Bool
    null a
    a then b
    b else a -> b
    k a
    a

    ifNotNull :: (Null a) => a -> (a -> b) -> b -> b
    ifNotNull :: forall a b. Null a => a -> (a -> b) -> b -> b
    ifNotNull a
    a a -> b
    k b
    b = a -> b -> (a -> b) -> b
    forall a b. Null a => a -> b -> (a -> b) -> b
    ifNull a
    a b
    b a -> b
    k

    ifNullM :: (Monad m, Null a) => m a -> m b -> (a -> m b) -> m b
    ifNullM :: forall (m :: * -> *) a b.
    (Monad m, Null a) =>
    m a -> m b -> (a -> m b) -> m b
    ifNullM m a
    ma m b
    mb a -> m b
    k = m a
    ma m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ a
    a -> a -> m b -> (a -> m b) -> m b
    forall a b. Null a => a -> b -> (a -> b) -> b
    ifNull a
    a m b
    mb a -> m b
    k

    ifNotNullM :: (Monad m, Null a) => m a -> (a -> m b) -> m b -> m b
    ifNotNullM :: forall (m :: * -> *) a b.
    (Monad m, Null a) =>
    m a -> (a -> m b) -> m b -> m b
    ifNotNullM m a
    ma a -> m b
    k m b
    mb = m a -> m b -> (a -> m b) -> m b
    forall (m :: * -> *) a b.
    (Monad m, Null a) =>
    m a -> m b -> (a -> m b) -> m b
    ifNullM m a
    ma m b
    mb a -> m b
    k

    whenNull :: (Monad m, Null a) => a -> m () -> m ()
    whenNull :: forall (m :: * -> *) a. (Monad m, Null a) => a -> m () -> m ()
    whenNull = Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Bool -> m () -> m ()) -> (a -> Bool) -> a -> m () -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Bool
    forall a. Null a => a -> Bool
    null

    unlessNull :: (Monad m, Null a) => a -> (a -> m ()) -> m ()
    unlessNull :: forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull a
    a a -> m ()
    k = Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (a -> Bool
    forall a. Null a => a -> Bool
    null a
    a) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ a -> m ()
    k a
    a

    whenNullM :: (Monad m, Null a) => m a -> m () -> m ()
    whenNullM :: forall (m :: * -> *) a. (Monad m, Null a) => m a -> m () -> m ()
    whenNullM m a
    ma m ()
    k = m a
    ma m a -> (a -> m ()) -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (a -> m () -> m ()
    forall (m :: * -> *) a. (Monad m, Null a) => a -> m () -> m ()
    `whenNull` m ()
    k)

    unlessNullM :: (Monad m, Null a) => m a -> (a -> m ()) -> m ()
    unlessNullM :: forall (m :: * -> *) a.
    (Monad m, Null a) =>
    m a -> (a -> m ()) -> m ()
    unlessNullM m a
    ma a -> m ()
    k = m a
    ma m a -> (a -> m ()) -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (a -> (a -> m ()) -> m ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    `unlessNull` a -> m ()
    k)