1{-# OPTIONS_GHC -fno-warn-orphans #-} 2 3 4-- | Overloaded @null@ and @empty@ for collections and sequences. 5 6module Agda.Utils.Null where 7 8import Prelude hiding (null) 9 10import Control.Monad 11import Control.Monad.Reader 12import Control.Monad.State 13 14import Data.ByteString.Char8 (ByteString) 15import qualified Data.ByteString.Char8 as ByteString 16 17import Data.HashMap.Strict (HashMap) 18import qualified Data.HashMap.Strict as HashMap 19import Data.HashSet (HashSet) 20import qualified Data.HashSet as HashSet 21import Data.IntMap (IntMap) 22import qualified Data.IntMap as IntMap 23import Data.IntSet (IntSet) 24import qualified Data.IntSet as IntSet 25import qualified Data.List as List 26import Data.Map (Map) 27import qualified Data.Map as Map 28 29import Data.Sequence (Seq) 30import qualified Data.Sequence as Seq 31import Data.Set (Set) 32import qualified Data.Set as Set 33 34import Text.PrettyPrint (Doc, isEmpty) 35 36import Agda.Utils.Bag (Bag) 37import qualified Agda.Utils.Bag as Bag 38 39import Agda.Utils.Impossible 40 41class Null a where 42 empty :: a 43 null :: a -> Bool 44 -- ^ Satisfying @null empty == True@. 45 46 default null :: Eq a => a -> Bool 47 null = (== empty) 48 49instance Null () where 50 empty = () 51 null _ = True 52 53instance (Null a, Null b) => Null (a,b) where 54 empty = (empty, empty) 55 null (a,b) = null a && null b 56 57instance (Null a, Null b, Null c) => Null (a,b,c) where 58 empty = (empty, empty, empty) 59 null (a,b,c) = null a && null b && null c 60 61instance (Null a, Null b, Null c, Null d) => Null (a,b,c,d) where 62 empty = (empty, empty, empty, empty) 63 null (a,b,c,d) = null a && null b && null c && null d 64 65instance Null ByteString where 66 empty = ByteString.empty 67 null = ByteString.null 68 69instance Null [a] where 70 empty = [] 71 null = List.null 72 73instance Null (Bag a) where 74 empty = Bag.empty 75 null = Bag.null 76 77instance Null (IntMap a) where 78 empty = IntMap.empty 79 null = IntMap.null 80 81instance Null IntSet where 82 empty = IntSet.empty 83 null = IntSet.null 84 85instance Null (Map k a) where 86 empty = Map.empty 87 null = Map.null 88 89instance Null (HashMap k a) where 90 empty = HashMap.empty 91 null = HashMap.null 92 93instance Null (HashSet a) where 94 empty = HashSet.empty 95 null = HashSet.null 96 97instance Null (Seq a) where 98 empty = Seq.empty 99 null = Seq.null 100 101instance Null (Set a) where 102 empty = Set.empty 103 null = Set.null 104 105-- | A 'Maybe' is 'null' when it corresponds to the empty list. 106instance Null (Maybe a) where 107 empty = Nothing 108 null Nothing = True 109 null (Just a) = False 110 111instance Null Doc where 112 empty = mempty 113 null = isEmpty 114 115instance (Null (m a), Monad m) => Null (ReaderT r m a) where 116 empty = lift empty 117 null = __IMPOSSIBLE__ 118 119instance (Null (m a), Monad m) => Null (StateT r m a) where 120 empty = lift empty 121 null = __IMPOSSIBLE__ 122 123-- * Testing for null. 124 125ifNull :: (Null a) => a -> b -> (a -> b) -> b 126ifNull a b k = if null a then b else k a 127 128ifNotNull :: (Null a) => a -> (a -> b) -> b -> b 129ifNotNull a k b = ifNull a b k 130 131ifNullM :: (Monad m, Null a) => m a -> m b -> (a -> m b) -> m b 132ifNullM ma mb k = ma >>= \ a -> ifNull a mb k 133 134ifNotNullM :: (Monad m, Null a) => m a -> (a -> m b) -> m b -> m b 135ifNotNullM ma k mb = ifNullM ma mb k 136 137whenNull :: (Monad m, Null a) => a -> m () -> m () 138whenNull = when . null 139 140unlessNull :: (Monad m, Null a) => a -> (a -> m ()) -> m () 141unlessNull a k = unless (null a) $ k a 142 143whenNullM :: (Monad m, Null a) => m a -> m () -> m () 144whenNullM ma k = ma >>= (`whenNull` k) 145 146unlessNullM :: (Monad m, Null a) => m a -> (a -> m ()) -> m () 147unlessNullM ma k = ma >>= (`unlessNull` k) 148