module Agda.Utils.Maybe
( module Agda.Utils.Maybe
, module Data.Maybe
) where
import Control.Monad
import Control.Monad.Trans.Maybe
import Data.Maybe
import Data.Functor
boolToMaybe :: Bool -> a -> Maybe a
boolToMaybe b x = if b then Just x else Nothing
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
unzipMaybe :: Maybe (a,b) -> (Maybe a, Maybe b)
unzipMaybe Nothing = (Nothing, Nothing)
unzipMaybe (Just (a,b)) = (Just a, Just b)
filterMaybe :: (a -> Bool) -> a -> Maybe a
filterMaybe p a
| p a = Just a
| otherwise = Nothing
forMaybe :: [a] -> (a -> Maybe b) -> [b]
forMaybe = flip mapMaybe
caseMaybe :: Maybe a -> b -> (a -> b) -> b
caseMaybe m d f = maybe d f m
ifJust :: Maybe a -> (a -> b) -> b -> b
ifJust m f d = maybe d f m
maybeM :: Monad m => m b -> (a -> m b) -> m (Maybe a) -> m b
maybeM n j mm = maybe n j =<< mm
fromMaybeM :: Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m mm = maybeM m return mm
caseMaybeM :: Monad m => m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM mm d f = maybeM d f mm
ifJustM :: Monad m => m (Maybe a) -> (a -> m b) -> m b -> m b
ifJustM mm = flip (caseMaybeM mm)
whenJust :: Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust m k = caseMaybe m (return ()) k
whenNothing :: Monad m => Maybe a -> m () -> m ()
whenNothing m d = caseMaybe m d (\_ -> return ())
whenJustM :: Monad m => m (Maybe a) -> (a -> m ()) -> m ()
whenJustM c m = c >>= (`whenJust` m)
whenNothingM :: Monad m => m (Maybe a) -> m () -> m ()
whenNothingM mm d = mm >>= (`whenNothing` d)
allJustM :: Monad m => [m (Maybe a)] -> m (Maybe [a])
allJustM = runMaybeT . mapM MaybeT