-- | Extend 'Data.Maybe' by common operations for the 'Maybe' type. -- -- Note: since this module is usually imported unqualified, -- we do not use short names, but all names contain 'Maybe', -- 'Just', or 'Nothing. module Agda.Utils.Maybe ( module Agda.Utils.Maybe , module Data.Maybe ) where import Control.Monad.Trans.Maybe import Data.Maybe -- * Conversion. -- | Retain object when tag is 'True'. boolToMaybe :: Bool -> a -> Maybe a boolToMaybe b x = if b then Just x else Nothing -- * Collection operations. -- UNUSED Liang-Ting Chen 05-07-2019 -- Andreas, 2020-02-17: -- Yeah, but a useful function to have in the library nevertheless. -- | @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 -- | @unionsWith@ for collections of size <= 1. unionsMaybeWith :: (a -> a -> a) -> [Maybe a] -> Maybe a unionsMaybeWith f ms = case catMaybes ms of [] -> Nothing as -> Just $ foldl1 f as -- | 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 d f = flip (maybe d) m f@ caseMaybe :: Maybe a -> b -> (a -> b) -> b caseMaybe m d f = maybe d f m -- | 'caseMaybe' with flipped branches. ifJust :: Maybe a -> (a -> b) -> b -> b ifJust m f d = maybe d 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 d f = maybeM d 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 -- | 'caseMaybe' without the 'Just' case. whenNothing :: Monad m => Maybe a -> m () -> m () whenNothing m d = caseMaybe m d (\_ -> return ()) -- | 'caseMaybeM' without the 'Nothing' case. whenJustM :: Monad m => m (Maybe a) -> (a -> m ()) -> m () whenJustM c m = c >>= (`whenJust` m) -- | 'caseMaybeM' without the 'Just' case. whenNothingM :: Monad m => m (Maybe a) -> m () -> m () whenNothingM mm d = mm >>= (`whenNothing` d) -- | Lazy version of @allJust <.> sequence@. -- (@allJust = mapM@ for the @Maybe@ monad.) -- Only executes monadic effect while @isJust@. allJustM :: Monad m => [m (Maybe a)] -> m (Maybe [a]) allJustM = runMaybeT . mapM MaybeT -- allJustM [] = return $ Just [] -- allJustM (mm : mms) = caseMaybeM mm (return Nothing) $ \ a -> -- fmap (a:) <$> allJust mms