-- | Auxiliary functions for the IO monad.

module Agda.Utils.IO where

import Control.Exception
import Control.Monad.Writer

-- | Catch 'IOException's.
--
class CatchIO m where
  catchIO :: m a -> (IOException -> m a) -> m a

-- | Alias of 'catch' for the IO monad.
--
instance CatchIO IO where
  catchIO :: IO a -> (IOException -> IO a) -> IO a
catchIO = IO a -> (IOException -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch

-- | Upon exception, the written output is lost.
--
instance CatchIO m => CatchIO (WriterT w m) where
  catchIO :: WriterT w m a -> (IOException -> WriterT w m a) -> WriterT w m a
catchIO WriterT w m a
m IOException -> WriterT w m a
h = m (a, w) -> WriterT w m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (m (a, w) -> WriterT w m a) -> m (a, w) -> WriterT w m a
forall a b. (a -> b) -> a -> b
$ WriterT w m a -> m (a, w)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT WriterT w m a
m m (a, w) -> (IOException -> m (a, w)) -> m (a, w)
forall (m :: * -> *) a.
CatchIO m =>
m a -> (IOException -> m a) -> m a
`catchIO` \ IOException
e -> WriterT w m a -> m (a, w)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (IOException -> WriterT w m a
h IOException
e)