    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# 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          ( when, unless )
    import Control.Monad.Except   ( ExceptT )
    import Control.Monad.Identity ( Identity(..) )
    import Control.Monad.Reader   ( ReaderT )
    import Control.Monad.State    ( StateT  )
    import Control.Monad.Writer   ( WriterT )
    import Control.Monad.Trans    ( lift    )
    import Control.Monad.Trans.Maybe

    import Data.Maybe             ( isNothing )

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

    import Data.EnumMap (EnumMap)
    import qualified Data.EnumMap as EnumMap
    import Data.EnumSet (EnumSet)
    import qualified Data.EnumSet as EnumSet
    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.Annotated (Doc, isEmpty)

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

    import Agda.Utils.Unsafe (unsafeComparePointers)
    import Agda.Utils.Impossible

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

      -- | The default implementation of 'null' compares with 'empty',
      --   first trying pointer equality, then falling back to 'Eq' equality.
      default null :: Eq a => a -> Bool
      null a
    a = a -> a -> Bool
    forall a. a -> a -> Bool
    unsafeComparePointers a
    a a
    forall a. Null a => a
    empty Bool -> Bool -> Bool
    || a
    a 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 a. [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 (EnumMap k a) where
      empty :: EnumMap k a
    empty = EnumMap k a
    forall k a. EnumMap k a
    EnumMap.empty
      null :: EnumMap k a -> Bool
    null  = EnumMap k a -> Bool
    forall k a. EnumMap k a -> Bool
    EnumMap.null

    instance Null (EnumSet a) where
      empty :: EnumSet a
    empty = EnumSet a
    forall a. EnumSet a
    EnumSet.empty
      null :: EnumSet a -> Bool
    null  = EnumSet a -> Bool
    forall a. EnumSet a -> Bool
    EnumSet.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 -> Bool
    forall a. Maybe a -> Bool
    isNothing

    -- | Viewing 'Bool' as @'Maybe' ()@, a boolean is 'null' when it is false.
    instance Null Bool where
      empty :: Bool
    empty = Bool
    False
      null :: Bool -> Bool
    null  = Bool -> Bool
    not

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

    instance Null a => Null (Identity a) where
      empty :: Identity a
    empty = a -> Identity a
    forall a. a -> Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    forall a. Null a => a
    empty
      null :: Identity a -> Bool
    null  = a -> Bool
    forall a. Null a => a -> Bool
    null (a -> Bool) -> (Identity a -> a) -> Identity a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Identity a -> a
    forall a. Identity a -> a
    runIdentity

    instance Null a => Null (IO a) where
      empty :: IO a
    empty = a -> IO a
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    forall a. Null a => a
    empty
      null :: IO a -> Bool
    null  = IO a -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance (Null (m a), Monad m) => Null (ExceptT e m a) where
      empty :: ExceptT e m a
    empty = m a -> ExceptT e m a
    forall (m :: * -> *) a. Monad m => m a -> ExceptT e 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 :: ExceptT e m a -> Bool
    null  = ExceptT e m a -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance (Null (m a), Monad m) => Null (MaybeT m a) where
      empty :: MaybeT m a
    empty = m a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => m a -> MaybeT 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 :: MaybeT m a -> Bool
    null  = MaybeT m a -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    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 (m :: * -> *) a. Monad m => 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 s m a) where
      empty :: StateT s m a
    empty = m a -> StateT s m a
    forall (m :: * -> *) a. Monad m => m a -> StateT s 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 s m a -> Bool
    null  = StateT s m a -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance (Null (m a), Monad m, Monoid w) => Null (WriterT w m a) where
      empty :: WriterT w m a
    empty = m a -> WriterT w m a
    forall (m :: * -> *) a. Monad m => m a -> WriterT w 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 :: WriterT w m a -> Bool
    null  = WriterT w 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 a b. 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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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)

    applyUnlessNull :: (Null a) => a -> (a -> b -> b) -> (b -> b)
    applyUnlessNull :: forall a b. Null a => a -> (a -> b -> b) -> b -> b
    applyUnlessNull a
    a a -> b -> b
    f = if a -> Bool
    forall a. Null a => a -> Bool
    null a
    a then b -> b
    forall a. a -> a
    id else a -> b -> b
    f a
    a

    -- | Disjunction (interpreting @null _@ as @False@).
    catchNull :: Null a => a -> a -> a
    catchNull :: forall a. Null a => a -> a -> a
    catchNull a
    a a
    b = if a -> Bool
    forall a. Null a => a -> Bool
    null a
    a then a
    b else a
    a