{-# 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 Data.ByteString.Char8 (ByteString)
import qualified Data.ByteString.Char8 as ByteString

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 ByteString where
  empty :: ByteString
empty = ByteString
ByteString.empty
  null :: ByteString -> Bool
null  = ByteString -> Bool
ByteString.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)