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