{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
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 Data.Maybe ( isNothing )
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.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
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 (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
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
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 (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__
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