{-# LANGUAGE CPP #-}
module Agda.Utils.Monad
( module Agda.Utils.Monad
, when, unless, MonadPlus(..)
, (<$>), (<*>)
, (<$)
)
where
import Prelude hiding (concat)
import Control.Monad hiding (mapM, forM)
import Control.Monad.State
import Control.Monad.Writer
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.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
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' =
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
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, 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'
mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM f xs = catMaybes <$> Trav.mapM f xs
forMaybeM :: Monad m => [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))
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 (liftM 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
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