Agda-2.5.4: src/full/Agda/Utils/Maybe/Strict.hs
{-# 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)