module Agda.Utils.Monad
( module Agda.Utils.Monad
, when, unless, MonadPlus(..)
, (<$>), (<*>)
, (<$)
)
where
import Control.Applicative (liftA2)
import Control.Monad hiding (mapM, forM)
import qualified Control.Monad.Fail as Fail
import Control.Monad.Identity ( Identity )
import Control.Monad.State
import Data.Traversable as Trav hiding (for, sequence)
import Data.Foldable as Fold
import Data.Maybe
import Agda.Utils.Either
import Agda.Utils.Except
( Error(strMsg)
, MonadError(catchError, throwError)
)
import Agda.Utils.Null (ifNotNullM)
import Agda.Utils.Impossible
(==<<) :: Monad m => (a -> b -> m c) -> (m a, m b) -> m c
k ==<< (ma, mb) = ma >>= \ a -> k a =<< mb
whenM :: Monad m => m Bool -> m () -> m ()
whenM c m = c >>= (`when` m)
unlessM :: Monad m => m Bool -> m () -> m ()
unlessM c m = c >>= (`unless` m)
guardM :: (Monad m, MonadPlus m) => m Bool -> m ()
guardM c = guard =<< c
ifM :: Monad m => m Bool -> m a -> m a -> m a
ifM c m m' = c >>= \b -> if b then m else m'
ifNotM :: Monad m => m Bool -> m a -> m a -> m a
ifNotM c = flip $ ifM c
and2M :: Monad m => m Bool -> m Bool -> m Bool
and2M ma mb = ifM ma mb (return False)
andM :: (Foldable f, Monad m) => f (m Bool) -> m Bool
andM = Fold.foldl and2M (return True)
allM :: (Functor f, Foldable f, Monad m) => f a -> (a -> m Bool) -> m Bool
allM xs f = andM $ fmap f xs
or2M :: Monad m => m Bool -> m Bool -> m Bool
or2M ma = ifM ma (return True)
orM :: (Foldable f, Monad m) => f (m Bool) -> m Bool
orM = Fold.foldl or2M (return False)
anyM :: (Functor f, Foldable f, Monad m) => f a -> (a -> m Bool) -> m Bool
anyM xs f = orM $ fmap f xs
altM1 :: Monad m => (a -> m (Either err b)) -> [a] -> m (Either err b)
altM1 f [] = __IMPOSSIBLE__
altM1 f [a] = f a
altM1 f (a : as) = either (const $ altM1 f as) (return . Right) =<< f a
orEitherM :: (Monoid e, Monad m, Functor m) => [m (Either e b)] -> m (Either e b)
orEitherM [] = return $ Left mempty
orEitherM (m : ms) = caseEitherM m (\e -> mapLeft (e `mappend`) <$> orEitherM ms)
(return . Right)
mapM' :: (Foldable t, Applicative m, Monoid b) => (a -> m b) -> t a -> m b
mapM' f = Fold.foldl (\ mb a -> liftA2 mappend mb (f a)) (pure mempty)
forM' :: (Foldable t, Applicative m, Monoid b) => t a -> (a -> m b) -> m b
forM' = flip mapM'
mapMM :: (Traversable t, Monad m) => (a -> m b) -> m (t a) -> m (t b)
mapMM f mxs = Trav.mapM f =<< mxs
forMM :: (Traversable t, Monad m) => m (t a) -> (a -> m b) -> m (t b)
forMM = flip mapMM
mapMM_ :: (Foldable t, Monad m) => (a -> m ()) -> m (t a) -> m ()
mapMM_ f mxs = Fold.mapM_ f =<< mxs
forMM_ :: (Foldable t, Monad m) => m (t a) -> (a -> m ()) -> m ()
forMM_ = flip mapMM_
mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM f xs = catMaybes <$> Trav.mapM f xs
mapMaybeMM :: Monad m => (a -> m (Maybe b)) -> m [a] -> m [b]
mapMaybeMM f m = mapMaybeM f =<< m
forMaybeM :: Monad m => [a] -> (a -> m (Maybe b)) -> m [b]
forMaybeM = flip mapMaybeM
forMaybeMM :: Monad m => m [a] -> (a -> m (Maybe b)) -> m [b]
forMaybeMM = flip mapMaybeMM
dropWhileM :: Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileM p [] = return []
dropWhileM p (x : xs) = ifM (p x) (dropWhileM p xs) (return (x : xs))
dropWhileEndM :: Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileEndM p [] = return []
dropWhileEndM p (x : xs) = ifNotNullM (dropWhileEndM p xs) (return . (x:)) $
ifM (p x) (return []) (return [x])
partitionM :: (Functor m, Applicative m) => (a -> m Bool) -> [a] -> m ([a],[a])
partitionM f [] =
pure ([], [])
partitionM f (x:xs) =
(\ b (l, r) -> if b then (x:l, r) else (l, x:r)) <$> f x <*> partitionM f xs
fromMaybeMP :: MonadPlus m => Maybe a -> m a
fromMaybeMP = maybe mzero return
catMaybesMP :: MonadPlus m => m (Maybe a) -> m a
catMaybesMP = (>>= fromMaybeMP)
finally :: MonadError e m => m a -> m () -> m a
first `finally` after = do
r <- catchError (fmap Right first) (return . Left)
after
case r of
Left e -> throwError e
Right r -> return r
tryMaybe :: (MonadError e m, Functor m) => m a -> m (Maybe a)
tryMaybe m = (Just <$> m) `catchError` \ _ -> return Nothing
tryCatch :: (MonadError e m, Functor m) => m () -> m (Maybe e)
tryCatch m = (Nothing <$ m) `catchError` \ err -> return $ Just err
bracket_ :: Monad m
=> m a
-> (a -> m ())
-> m b
-> m b
bracket_ acquire release compute = do
resource <- acquire
result <- compute
release resource
return result
localState :: MonadState s m => m a -> m a
localState = bracket_ get put
readM :: (Error e, MonadError e m, Read a) => String -> m a
readM s = case reads s of
[(x,"")] -> return x
_ ->
throwError $ strMsg $ "readM: parse error string " ++ s