{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | A strict version of the 'Maybe' type. -- -- Import qualified, as in -- @ -- import qualified Agda.Utils.Maybe.Strict as Strict -- @ -- -- Copyright : (c) 2006-2007 Roman Leshchinskiy -- (c) 2013 Simon Meier -- License : BSD-style (see the file LICENSE) -- -- Copyright : (c) 2014 Andreas Abel module Agda.Utils.Maybe.Strict ( module Data.Strict.Maybe , module Agda.Utils.Maybe.Strict ) where -- The following code is copied from -- http://hackage.haskell.org/package/strict-base-types-0.3.0/docs/src/Data-Maybe-Strict.html import Prelude hiding (Maybe (..), maybe, null) import qualified Prelude as Lazy import Control.Applicative (pure, (<$>)) import Control.DeepSeq (NFData (..)) import Data.Binary (Binary (..)) import Data.Data (Data (..)) import Data.Monoid (Monoid, mempty, mappend) import Data.Semigroup (Semigroup, (<>)) import Data.Foldable (Foldable (..)) import Data.Traversable (Traversable (..)) import Data.Strict.Maybe (Maybe (Nothing, Just), fromJust, fromMaybe, isJust, isNothing, maybe) import GHC.Generics (Generic (..)) import Agda.Utils.Null toStrict :: Lazy.Maybe a -> Maybe a toStrict Lazy.Nothing = Nothing toStrict (Lazy.Just x) = Just x toLazy :: Maybe a -> Lazy.Maybe a toLazy Nothing = Lazy.Nothing toLazy (Just x) = Lazy.Just x deriving instance Data a => Data (Maybe a) deriving instance Generic (Maybe a) instance Null (Maybe a) where empty = Nothing null = isNothing -- The monoid instance was fixed in strict-base-types 0.5.0. See -- Issue 1805. instance Semigroup a => Semigroup (Maybe a) where Nothing <> m = m m <> Nothing = m Just x1 <> Just x2 = Just (x1 <> x2) instance Semigroup a => Monoid (Maybe a) where mempty = Nothing mappend = (<>) instance Foldable Maybe where foldMap _ Nothing = mempty foldMap f (Just x) = f x instance Traversable Maybe where traverse _ Nothing = pure Nothing traverse f (Just x) = Just <$> f x instance NFData a => NFData (Maybe a) where rnf = rnf . toLazy instance Binary a => Binary (Maybe a) where put = put . toLazy get = toStrict <$> get -- | Analogous to 'Lazy.listToMaybe' in "Data.Maybe". listToMaybe :: [a] -> Maybe a listToMaybe [] = Nothing listToMaybe (a:_) = Just a -- | Analogous to 'Lazy.maybeToList' in "Data.Maybe". maybeToList :: Maybe a -> [a] maybeToList Nothing = [] maybeToList (Just x) = [x] -- | Analogous to 'Lazy.catMaybes' in "Data.Maybe". catMaybes :: [Maybe a] -> [a] catMaybes ls = [x | Just x <- ls] -- | Analogous to 'Lazy.mapMaybe' in "Data.Maybe". mapMaybe :: (a -> Maybe b) -> [a] -> [b] mapMaybe _ [] = [] mapMaybe f (x:xs) = case f x of Nothing -> rs Just r -> r:rs where rs = mapMaybe f xs -- The remaining code is a copy of Agda.Utils.Maybe -- * Collection operations. -- | @unionWith@ for collections of size <= 1. unionMaybeWith :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a unionMaybeWith f Nothing mb = mb unionMaybeWith f ma Nothing = ma unionMaybeWith f (Just a) (Just b) = Just $ f a b -- | Unzipping a list of length <= 1. unzipMaybe :: Maybe (a,b) -> (Maybe a, Maybe b) unzipMaybe Nothing = (Nothing, Nothing) unzipMaybe (Just (a,b)) = (Just a, Just b) -- | Filtering a singleton list. -- -- @filterMaybe p a = 'listToMaybe' ('filter' p [a])@ filterMaybe :: (a -> Bool) -> a -> Maybe a filterMaybe p a | p a = Just a | otherwise = Nothing -- * Conditionals and loops. -- | Version of 'mapMaybe' with different argument ordering. forMaybe :: [a] -> (a -> Maybe b) -> [b] forMaybe = flip mapMaybe -- | Version of 'maybe' with different argument ordering. -- Often, we want to case on a 'Maybe', do something interesting -- in the 'Just' case, but only a default action in the 'Nothing' -- case. Then, the argument ordering of @caseMaybe@ is preferable. -- -- @caseMaybe m err f = flip (maybe err) m f@ caseMaybe :: Maybe a -> b -> (a -> b) -> b caseMaybe m err f = maybe err f m -- * Monads and Maybe. -- | Monadic version of 'maybe'. maybeM :: Monad m => m b -> (a -> m b) -> m (Maybe a) -> m b maybeM n j mm = maybe n j =<< mm -- | Monadic version of 'fromMaybe'. fromMaybeM :: Monad m => m a -> m (Maybe a) -> m a fromMaybeM m mm = maybeM m return mm -- | Monadic version of 'caseMaybe'. -- That is, 'maybeM' with a different argument ordering. caseMaybeM :: Monad m => m (Maybe a) -> m b -> (a -> m b) -> m b caseMaybeM mm err f = maybeM err f mm -- | 'caseMaybeM' with flipped branches. ifJustM :: Monad m => m (Maybe a) -> (a -> m b) -> m b -> m b ifJustM mm = flip (caseMaybeM mm) -- | A more telling name for 'Traversable.forM' for the 'Maybe' collection type. -- Or: 'caseMaybe' without the 'Nothing' case. whenJust :: Monad m => Maybe a -> (a -> m ()) -> m () whenJust m k = caseMaybe m (return ()) k -- | 'caseMaybeM' without the 'Nothing' case. whenJustM :: Monad m => m (Maybe a) -> (a -> m ()) -> m () whenJustM c m = c >>= (`whenJust` m)