module Agda.Utils.Monad
    ( module Agda.Utils.Monad
    , when, unless, MonadPlus(..)
    , (<$>), (<*>)
    , (<$)
    )
    where

import Control.Applicative    ( liftA2 )
import Control.Monad          ( MonadPlus(..), guard, unless, when )
import Control.Monad.Except   ( MonadError(catchError, throwError) )
import Control.Monad.Identity ( runIdentity )
import Control.Monad.State    ( MonadState(get, put) )
import Control.Monad.Writer   ( Writer, WriterT, mapWriterT )

import Data.Bifunctor         ( first, second )
import Data.Bool              ( bool )
import Data.Traversable as Trav hiding (for, sequence)
import Data.Foldable as Fold
import Data.Maybe
import Data.Monoid

import Agda.Utils.Applicative
import Agda.Utils.Either
import Agda.Utils.Null (empty, ifNotNullM)

import Agda.Utils.Impossible

---------------------------------------------------------------------------

-- | Binary bind.
(==<<) :: Monad m => (a -> b -> m c) -> (m a, m b) -> m c
a -> b -> m c
k ==<< :: forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> m c) -> (m a, m b) -> m c
==<< (m a
ma, m b
mb) = m a
ma forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ a
a -> a -> b -> m c
k a
a forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m b
mb

-- Conditionals and monads ------------------------------------------------

whenM :: Monad m => m Bool -> m () -> m ()
whenM :: forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM m Bool
c m ()
m = m Bool
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
`when` m ()
m)

unlessM :: Monad m => m Bool -> m () -> m ()
unlessM :: forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM m Bool
c m ()
m = m Bool
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
`unless` m ()
m)

-- | Monadic guard.
guardM :: (Monad m, MonadPlus m) => m Bool -> m ()
guardM :: forall (m :: * -> *). (Monad m, MonadPlus m) => m Bool -> m ()
guardM m Bool
c = forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Bool
c

-- | Monadic if-then-else.
ifM :: Monad m => m Bool -> m a -> m a -> m a
ifM :: forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
c m a
m m a
m' = m Bool
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Bool
b -> if Bool
b then m a
m else m a
m'

-- | @ifNotM mc = ifM (not <$> mc)@
ifNotM :: Monad m => m Bool -> m a -> m a -> m a
ifNotM :: forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM m Bool
c = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
c

-- | Lazy monadic conjunction.
and2M :: Monad m => m Bool -> m Bool -> m Bool
and2M :: forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
and2M m Bool
ma m Bool
mb = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
ma m Bool
mb (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)

andM :: (Foldable f, Monad m) => f (m Bool) -> m Bool
andM :: forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl' forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
and2M (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)

allM :: (Foldable f, Monad m) => f a -> (a -> m Bool) -> m Bool
allM :: forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
allM f a
xs a -> m Bool
f = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl' (\m Bool
b -> forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
and2M m Bool
b forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m Bool
f) (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True) f a
xs

-- | Lazy monadic disjunction.
or2M :: Monad m => m Bool -> m Bool -> m Bool
or2M :: forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
or2M m Bool
ma = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
ma (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)

orM :: (Foldable f, Monad m) => f (m Bool) -> m Bool
orM :: forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
orM = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl' forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
or2M (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)

anyM :: (Foldable f, Monad m) => f a -> (a -> m Bool) -> m Bool
anyM :: forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
anyM f a
xs a -> m Bool
f = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl' (\m Bool
b -> forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
or2M m Bool
b forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m Bool
f) (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) f a
xs

-- | Lazy monadic disjunction with @Either@  truth values.
--   Returns the last error message if all fail.
altM1 :: Monad m => (a -> m (Either err b)) -> [a] -> m (Either err b)
altM1 :: forall (m :: * -> *) a err b.
Monad m =>
(a -> m (Either err b)) -> [a] -> m (Either err b)
altM1 a -> m (Either err b)
f []       = forall a. HasCallStack => a
__IMPOSSIBLE__
altM1 a -> m (Either err b)
f [a
a]      = a -> m (Either err b)
f a
a
altM1 a -> m (Either err b)
f (a
a : [a]
as) = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a err b.
Monad m =>
(a -> m (Either err b)) -> [a] -> m (Either err b)
altM1 a -> m (Either err b)
f [a]
as) (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> m (Either err b)
f a
a

-- | Lazy monadic disjunction with accumulation of errors in a monoid.
--   Errors are discarded if we succeed.
orEitherM :: (Monoid e, Monad m, Functor m) => [m (Either e b)] -> m (Either e b)
orEitherM :: forall e (m :: * -> *) b.
(Monoid e, Monad m, Functor m) =>
[m (Either e b)] -> m (Either e b)
orEitherM []       = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a. Monoid a => a
mempty
orEitherM (m (Either e b)
m : [m (Either e b)]
ms) = forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM m (Either e b)
m (\e
e -> forall a c b. (a -> c) -> Either a b -> Either c b
mapLeft (e
e forall a. Monoid a => a -> a -> a
`mappend`) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e (m :: * -> *) b.
(Monoid e, Monad m, Functor m) =>
[m (Either e b)] -> m (Either e b)
orEitherM [m (Either e b)]
ms)
                                   (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right)

-- Loops gathering results in a Monoid ------------------------------------

-- | Generalized version of @traverse_ :: Applicative m => (a -> m ()) -> [a] -> m ()@
--   Executes effects and collects results in left-to-right order.
--   Works best with left-associative monoids.
--
--   Note that there is an alternative
--
--     @mapM' f t = foldr mappend mempty <$> mapM f t@
--
--   that collects results in right-to-left order
--   (effects still left-to-right).
--   It might be preferable for right associative monoids.
mapM' :: (Foldable t, Applicative m, Monoid b) => (a -> m b) -> t a -> m b
mapM' :: forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
(a -> m b) -> t a -> m b
mapM' a -> m b
f = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl (\ m b
mb a
a -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall a. Monoid a => a -> a -> a
mappend m b
mb (a -> m b
f a
a)) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty)

-- | Generalized version of @for_ :: Applicative m => [a] -> (a -> m ()) -> m ()@
forM' :: (Foldable t, Applicative m, Monoid b) => t a -> (a -> m b) -> m b
forM' :: forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
t a -> (a -> m b) -> m b
forM' = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Applicative m, Monoid b) =>
(a -> m b) -> t a -> m b
mapM'

-- Variations of Traversable

mapMM :: (Traversable t, Monad m) => (a -> m b) -> m (t a) -> m (t b)
mapMM :: forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> m (t a) -> m (t b)
mapMM a -> m b
f m (t a)
mxs = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
Trav.mapM a -> m b
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (t a)
mxs

forMM :: (Traversable t, Monad m) => m (t a) -> (a -> m b) -> m (t b)
forMM :: forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
m (t a) -> (a -> m b) -> m (t b)
forMM = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> m (t a) -> m (t b)
mapMM

-- Variations of Foldable

mapMM_ :: (Foldable t, Monad m) => (a -> m ()) -> m (t a) -> m ()
mapMM_ :: forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
(a -> m ()) -> m (t a) -> m ()
mapMM_ a -> m ()
f m (t a)
mxs = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Fold.mapM_ a -> m ()
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (t a)
mxs

forMM_ :: (Foldable t, Monad m) => m (t a) -> (a -> m ()) -> m ()
forMM_ :: forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
m (t a) -> (a -> m ()) -> m ()
forMM_ = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
(a -> m ()) -> m (t a) -> m ()
mapMM_

-- Continuation monad -----------------------------------------------------

-- Andreas, 2017-04-11, issue #2543
-- The terribly useful thread function is now UNUSED.  [Sadistic laughter :)]
--
-- type Cont r a = (a -> r) -> r
--
-- -- | 'Control.Monad.mapM' for the continuation monad. Terribly useful.
-- 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)

-- Lists and monads -------------------------------------------------------

-- | A monadic version of @'mapMaybe' :: (a -> Maybe b) -> [a] -> [b]@.
mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM a -> m (Maybe b)
f [a]
xs = forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
Trav.mapM a -> m (Maybe b)
f [a]
xs

-- | A version of @'mapMaybeM'@ with a computation for the input list.
mapMaybeMM :: Monad m => (a -> m (Maybe b)) -> m [a] -> m [b]
mapMaybeMM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> m [a] -> m [b]
mapMaybeMM a -> m (Maybe b)
f m [a]
m = forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM a -> m (Maybe b)
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m [a]
m

-- | The @for@ version of 'mapMaybeM'.
forMaybeM :: Monad m => [a] -> (a -> m (Maybe b)) -> m [b]
forMaybeM :: forall (m :: * -> *) a b.
Monad m =>
[a] -> (a -> m (Maybe b)) -> m [b]
forMaybeM = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM

-- | The @for@ version of 'mapMaybeMM'.
forMaybeMM :: Monad m => m [a] -> (a -> m (Maybe b)) -> m [b]
forMaybeMM :: forall (m :: * -> *) a b.
Monad m =>
m [a] -> (a -> m (Maybe b)) -> m [b]
forMaybeMM = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> m [a] -> m [b]
mapMaybeMM

-- | A monadic version of @'dropWhile' :: (a -> Bool) -> [a] -> [a]@.
dropWhileM :: Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileM :: forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileM a -> m Bool
p []       = forall (m :: * -> *) a. Monad m => a -> m a
return []
dropWhileM a -> m Bool
p (a
x : [a]
xs) = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (a -> m Bool
p a
x) (forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileM a -> m Bool
p [a]
xs) (forall (m :: * -> *) a. Monad m => a -> m a
return (a
x forall a. a -> [a] -> [a]
: [a]
xs))

-- | A monadic version of @'dropWhileEnd' :: (a -> Bool) -> [a] -> m [a]@.
--   Effects happen starting at the end of the list until @p@ becomes false.
dropWhileEndM :: Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileEndM :: forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileEndM a -> m Bool
p []       = forall (m :: * -> *) a. Monad m => a -> m a
return []
dropWhileEndM a -> m Bool
p (a
x : [a]
xs) = forall (m :: * -> *) a b.
(Monad m, Null a) =>
m a -> (a -> m b) -> m b -> m b
ifNotNullM (forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileEndM a -> m Bool
p [a]
xs) (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
xforall a. a -> [a] -> [a]
:)) forall a b. (a -> b) -> a -> b
$ {-else-}
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (a -> m Bool
p a
x) (forall (m :: * -> *) a. Monad m => a -> m a
return []) (forall (m :: * -> *) a. Monad m => a -> m a
return [a
x])

-- | A ``monadic'' version of @'partition' :: (a -> Bool) -> [a] -> ([a],[a])
partitionM :: (Functor m, Applicative m) => (a -> m Bool) -> [a] -> m ([a], [a])
partitionM :: forall (m :: * -> *) a.
(Functor m, Applicative m) =>
(a -> m Bool) -> [a] -> m ([a], [a])
partitionM a -> m Bool
f =
  forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ a
x m ([a], [a])
mlr -> forall a. a -> a -> Bool -> a
bool (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (a
xforall a. a -> [a] -> [a]
:)) (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (a
xforall a. a -> [a] -> [a]
:)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m Bool
f a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m ([a], [a])
mlr)
        (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Null a => a
empty)

-- MonadPlus -----------------------------------------------------------------

-- | Translates 'Maybe' to 'MonadPlus'.
fromMaybeMP :: MonadPlus m => Maybe a -> m a
fromMaybeMP :: forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP = forall (f :: * -> *) (t :: * -> *) a.
(Alternative f, Foldable t) =>
t a -> f a
foldA

-- | Generalises the 'catMaybes' function from lists to an arbitrary
-- 'MonadPlus'.
catMaybesMP :: MonadPlus m => m (Maybe a) -> m a
catMaybesMP :: forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP = forall (m :: * -> *) (t :: * -> *) a.
(MonadPlus m, Foldable t) =>
m (t a) -> m a
scatterMP

-- | Branch over elements of a monadic 'Foldable' data structure.
scatterMP :: (MonadPlus m, Foldable t) => m (t a) -> m a
scatterMP :: forall (m :: * -> *) (t :: * -> *) a.
(MonadPlus m, Foldable t) =>
m (t a) -> m a
scatterMP = (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: * -> *) (t :: * -> *) a.
(Alternative f, Foldable t) =>
t a -> f a
foldA)


-- Error monad ------------------------------------------------------------

-- | Finally for the 'Error' class. Errors in the finally part take
-- precedence over prior errors.

finally :: MonadError e m => m a -> m () -> m a
m a
first finally :: forall e (m :: * -> *) a. MonadError e m => m a -> m () -> m a
`finally` m ()
after = do
  Either e a
r <- forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right m a
first) (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left)
  m ()
after
  case Either e a
r of
    Left e
e  -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e
    Right a
r -> forall (m :: * -> *) a. Monad m => a -> m a
return a
r

-- | Try a computation, return 'Nothing' if an 'Error' occurs.

tryMaybe :: (MonadError e m, Functor m) => m a -> m (Maybe a)
tryMaybe :: forall e (m :: * -> *) a.
(MonadError e m, Functor m) =>
m a -> m (Maybe a)
tryMaybe m a
m = (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
m) forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ e
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

-- | Run a command, catch the exception and return it.

tryCatch :: (MonadError e m, Functor m) => m () -> m (Maybe e)
tryCatch :: forall e (m :: * -> *).
(MonadError e m, Functor m) =>
m () -> m (Maybe e)
tryCatch m ()
m = (forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ m ()
m) forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ e
err -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just e
err

-- | Like 'guard', but raise given error when condition fails.

guardWithError :: MonadError e m => e -> Bool -> m ()
guardWithError :: forall e (m :: * -> *). MonadError e m => e -> Bool -> m ()
guardWithError e
e Bool
b = if Bool
b then forall (m :: * -> *) a. Monad m => a -> m a
return () else forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e

-- State monad ------------------------------------------------------------

-- | Bracket without failure.  Typically used to preserve state.
bracket_ :: Monad m
         => m a         -- ^ Acquires resource. Run first.
         -> (a -> m ())  -- ^ Releases resource. Run last.
         -> m b         -- ^ Computes result. Run in-between.
         -> m b
bracket_ :: forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ m a
acquire a -> m ()
release m b
compute = do
  a
resource <- m a
acquire
  b
result <- m b
compute
  a -> m ()
release a
resource
  forall (m :: * -> *) a. Monad m => a -> m a
return b
result

-- | Restore state after computation.
localState :: MonadState s m => m a -> m a
localState :: forall s (m :: * -> *) a. MonadState s m => m a -> m a
localState = forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ forall s (m :: * -> *). MonadState s m => m s
get forall s (m :: * -> *). MonadState s m => s -> m ()
put

-- Writer monad -----------------------------------------------------------

embedWriter :: (Monoid w, Monad m) => Writer w a -> WriterT w m a
embedWriter :: forall w (m :: * -> *) a.
(Monoid w, Monad m) =>
Writer w a -> WriterT w m a
embedWriter = forall (m :: * -> *) a w (n :: * -> *) b w'.
(m (a, w) -> n (b, w')) -> WriterT w m a -> WriterT w' n b
mapWriterT (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Identity a -> a
runIdentity)