{-# 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 Data.ByteString.Char8 qualified as ByteStringChar8
import Data.ByteString.Lazy qualified as ByteStringLazy

import Data.EnumMap (EnumMap)
import Data.EnumMap qualified as EnumMap
import Data.EnumSet (EnumSet)
import Data.EnumSet qualified as EnumSet
import Data.HashMap.Strict (HashMap)
import Data.HashMap.Strict qualified as HashMap
import Data.HashSet (HashSet)
import Data.HashSet qualified as HashSet
import Data.IntMap (IntMap)
import Data.IntMap qualified as IntMap
import Data.IntSet (IntSet)
import Data.IntSet qualified as IntSet
import Data.List qualified as List
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Sequence (Seq)
import Data.Sequence qualified as Seq
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Word (Word32, Word64)

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

import Text.PrettyPrint.Annotated (Doc, isEmpty)

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

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  = ()
  {-# INLINE empty #-}
  null :: () -> Bool
null ()
_ = Bool
True
  {-# INLINE null #-}

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
  {-# INLINE empty #-}
  null :: ByteString -> Bool
null  = ByteString -> Bool
ByteStringChar8.null
  {-# INLINE null #-}

instance Null ByteStringLazy.ByteString where
  empty :: ByteString
empty = ByteString
ByteStringLazy.empty
  {-# INLINE empty #-}
  null :: ByteString -> Bool
null  = ByteString -> Bool
ByteStringLazy.null
  {-# INLINE null #-}

instance Null Text where
  empty :: Text
empty = Text
Text.empty
  {-# INLINE empty #-}
  null :: Text -> Bool
null  = Text -> Bool
Text.null
  {-# INLINE null #-}

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

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

instance Null (EnumMap k a) where
  empty :: EnumMap k a
empty = EnumMap k a
forall k a. EnumMap k a
EnumMap.empty
  {-# INLINE empty #-}
  null :: EnumMap k a -> Bool
null  = EnumMap k a -> Bool
forall k a. EnumMap k a -> Bool
EnumMap.null
  {-# INLINE null #-}

instance Null (EnumSet a) where
  empty :: EnumSet a
empty = EnumSet a
forall a. EnumSet a
EnumSet.empty
  {-# INLINE empty #-}
  null :: EnumSet a -> Bool
null  = EnumSet a -> Bool
forall a. EnumSet a -> Bool
EnumSet.null
  {-# INLINE null #-}

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

instance Null IntSet where
  empty :: IntSet
empty = IntSet
IntSet.empty
  {-# INLINE empty #-}
  null :: IntSet -> Bool
null  = IntSet -> Bool
IntSet.null
  {-# INLINE null #-}

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

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

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

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

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

instance Null VarSet where
  empty :: VarSet
empty = VarSet
VarSet.empty
  {-# INLINE empty #-}
  null :: VarSet -> Bool
null = VarSet -> Bool
VarSet.null
  {-# INLINE 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
  {-# INLINE empty #-}
  null :: Maybe a -> Bool
null  = Maybe a -> Bool
forall a. Maybe a -> Bool
isNothing
  {-# INLINE null #-}

instance Null Word32 where
  empty :: Word32
empty = Word32
0
  {-# INLINE empty #-}

instance Null Word64 where
  empty :: Word64
empty = Word64
0
  {-# INLINE empty #-}

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

instance Null (Doc a) where
  empty :: Doc a
empty = Doc a
forall a. Monoid a => a
mempty
  {-# INLINE empty #-}
  null :: Doc a -> Bool
null  = Doc a -> Bool
forall a. Doc a -> Bool
isEmpty
  {-# NOINLINE null #-}

-- | 'Either' is seen as error monad.
instance Null a => Null (Either e a) where
  empty :: Either e a
empty = a -> Either e a
forall a b. b -> Either a b
Right a
forall a. Null a => a
empty
  {-# INLINE empty #-}
  null :: Either e a -> Bool
null  = (e -> Bool) -> (a -> Bool) -> Either e a -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Bool -> e -> Bool
forall a b. a -> b -> a
const Bool
False) a -> Bool
forall a. Null a => a -> Bool
null
  {-# NOINLINE null #-}

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
  {-# INLINE 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
  {-# INLINE null #-}

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
  {-# INLINE empty #-}
  null :: IO a -> Bool
null  = IO a -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
  {-# NOINLINE null #-}

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
  {-# INLINE empty #-}
  null :: ExceptT e m a -> Bool
null  = ExceptT e m a -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
  {-# NOINLINE null #-}

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
  {-# INLINE empty #-}
  null :: MaybeT m a -> Bool
null  = MaybeT m a -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
  {-# NOINLINE null #-}

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
  {-# INLINE empty #-}
  null :: ReaderT r m a -> Bool
null  = ReaderT r m a -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
  {-# NOINLINE null #-}

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
  {-# INLINE empty #-}
  null :: StateT s m a -> Bool
null  = StateT s m a -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
  {-# NOINLINE null #-}

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
  {-# INLINE empty #-}
  null :: WriterT w m a -> Bool
null  = WriterT w m a -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
  {-# NOINLINE null #-}

-- * 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