module Agda.Utils.Monad
( module Agda.Utils.Monad
, module Control.Monad
, (<$>), (<*>)
, (<$)
)
where
import Prelude hiding (concat)
import Control.Monad hiding (mapM, forM)
import Control.Monad.Error
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.List
#include "../undefined.h"
import Agda.Utils.Impossible
when_ :: Monad m => Bool -> m a -> m ()
when_ b m = when b $ do m >> return ()
unless_ :: Monad m => Bool -> m a -> m ()
unless_ b m = unless b $ do 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 :: Monad m => [m Bool] -> m Bool
andM = Fold.foldl and2M (return True)
or2M :: Monad m => m Bool -> m Bool -> m Bool
or2M ma mb = ifM ma (return True) mb
orM :: Monad m => [m Bool] -> m Bool
orM = Fold.foldl or2M (return False)
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 :: (Monad m, Functor m) => (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM f xs = catMaybes <$> Trav.mapM f xs
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))
instance Error () where
noMsg = ()
finally :: (Error e, 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 :: (Error e, MonadError e m)
=> m a
-> (a -> m c)
-> (a -> m b)
-> m b
bracket acquire release compute = do
resource <- acquire
compute resource `finally` release resource
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
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