module Agda.Utils.Monad
( module Agda.Utils.Monad
, when, unless, MonadPlus(..)
, (<$>), (<*>)
, (<$)
#if MIN_VERSION_mtl(2,2,0)
, Control.Monad.State.modify'
#endif
)
where
import Prelude hiding (concat)
import Control.Monad hiding (mapM, forM)
import Control.Monad.State
import Control.Monad.Writer
import Control.Applicative
import Data.Traversable as Trav hiding (for, sequence)
import Data.Foldable as Fold
import Data.Maybe
import Agda.Utils.Except
( Error(strMsg)
, MonadError(catchError, throwError)
)
import Agda.Utils.List
#include "undefined.h"
import Agda.Utils.Impossible
(==<<) :: Monad m => (a -> b -> m c) -> (m a, m b) -> m c
k ==<< (ma, mb) = ma >>= \ a -> k a =<< mb
when_ :: Monad m => Bool -> m a -> m ()
when_ b m = when b $ m >> return ()
unless_ :: Monad m => Bool -> m a -> m ()
unless_ b m = unless b $ m >> return ()
whenM :: Monad m => m Bool -> m a -> m ()
whenM c m = c >>= (`when_` m)
unlessM :: Monad m => m Bool -> m a -> m ()
unlessM c m = c >>= (`unless_` m)
ifM :: Monad m => m Bool -> m a -> m a -> m a
ifM c m m' =
do b <- c
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 mb = ifM ma (return True) mb
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
mapM' :: (Foldable t, Monad m, Monoid b) => (a -> m b) -> t a -> m b
mapM' f = Fold.foldl (\ mb a -> liftM2 mappend mb (f a)) (return mempty)
forM' :: (Foldable t, Monad m, Monoid b) => t a -> (a -> m b) -> m b
forM' = flip mapM'
type Cont r a = (a -> r) -> r
thread :: (a -> Cont r b) -> [a] -> Cont r [b]
thread f [] ret = ret []
thread f (x:xs) ret =
f x $ \y -> thread f xs $ \ys -> ret (y:ys)
zipWithM' :: Monad m => (a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM' f xs ys = sequence (zipWith' f xs ys)
mapMaybeM
#if __GLASGOW_HASKELL__ <= 708
:: (Functor m, Monad m)
#else
:: Monad m
#endif
=> (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM f xs = catMaybes <$> Trav.mapM f xs
forMaybeM
#if __GLASGOW_HASKELL__ <= 708
:: (Functor m, Monad m)
#else
:: Monad m
#endif
=> [a] -> (a -> m (Maybe b)) -> m [b]
forMaybeM = flip mapMaybeM
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))
finally :: MonadError e m => m a -> m b -> m a
first `finally` after = do
r <- catchError (liftM Right first) (return . Left)
_ <- after
case r of
Left e -> throwError e
Right r -> return r
bracket_ :: Monad m
=> m a
-> (a -> m c)
-> 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
#if !MIN_VERSION_mtl(2,2,0)
modify' :: MonadState s m => (s -> s) -> m ()
modify' f = do
x <- get
put $! f x
#endif
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