    {-# LANGUAGE CPP #-}

    -- | Auxiliary functions for the IO monad.

    module Agda.Utils.IO where

    import Control.Exception
    import Control.Monad.Except
    import Control.Monad.State
    import Control.Monad.Writer

    import Agda.Utils.List (dropFrom)
    import Agda.Utils.String (rtrim)

    -- | Catch 'Exception's in an extension of the 'IO' monad.
    --
    class CatchIO m where
      catchIO :: Exception e => m a -> (e -> m a) -> m a

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

    -- | Upon exception, the error is lost.

    instance CatchIO m => CatchIO (ExceptT e m) where
      catchIO :: forall e a.
    Exception e =>
    ExceptT e m a -> (e -> ExceptT e m a) -> ExceptT e m a
    catchIO ExceptT e m a
    m e -> ExceptT e m a
    h = m (Either e a) -> ExceptT e m a
    forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
    ExceptT (m (Either e a) -> ExceptT e m a)
    -> m (Either e a) -> ExceptT e m a
    forall a b. (a -> b) -> a -> b
    $ ExceptT e m a -> m (Either e a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT ExceptT e m a
    m m (Either e a) -> (e -> m (Either e a)) -> m (Either e a)
    forall e a. Exception e => m a -> (e -> m a) -> m a
    forall (m :: * -> *) e a.
    (CatchIO m, Exception e) =>
    m a -> (e -> m a) -> m a
    `catchIO` \ e
    e -> ExceptT e m a -> m (Either e a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (e -> ExceptT e m a
    h e
    e)

    -- | Upon exception, the written output is lost.
    --
    instance CatchIO m => CatchIO (WriterT w m) where
      catchIO :: forall e a.
    Exception e =>
    WriterT w m a -> (e -> WriterT w m a) -> WriterT w m a
    catchIO WriterT w m a
    m e -> 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) -> (e -> m (a, w)) -> m (a, w)
    forall e a. Exception e => m a -> (e -> m a) -> m a
    forall (m :: * -> *) e a.
    (CatchIO m, Exception e) =>
    m a -> (e -> m a) -> m a
    `catchIO` \ e
    e -> WriterT w m a -> m (a, w)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT (e -> WriterT w m a
    h e
    e)

    -- | Upon exception, the state is reset.
    --
    instance CatchIO m => CatchIO (StateT s m) where
      catchIO :: forall e a.
    Exception e =>
    StateT s m a -> (e -> StateT s m a) -> StateT s m a
    catchIO StateT s m a
    m e -> StateT s m a
    h = (s -> m (a, s)) -> StateT s m a
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StateT ((s -> m (a, s)) -> StateT s m a)
    -> (s -> m (a, s)) -> StateT s m a
    forall a b. (a -> b) -> a -> b
    $ \s
    s -> StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT StateT s m a
    m s
    s m (a, s) -> (e -> m (a, s)) -> m (a, s)
    forall e a. Exception e => m a -> (e -> m a) -> m a
    forall (m :: * -> *) e a.
    (CatchIO m, Exception e) =>
    m a -> (e -> m a) -> m a
    `catchIO` \ e
    e -> StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (e -> StateT s m a
    h e
    e) s
    s

    -- | Print an 'IOException' without the call stack.
    --
    showIOException :: Exception e => e -> String
    showIOException :: forall e. Exception e => e -> String
    showIOException =
      String -> String
    rtrim
    #if MIN_VERSION_base(4,20,0)
      -- Andreas, 2024-07-05, issue #7299.
      -- Ugly hack to drop call stack (introduced in GHC 9.10) from IOException.
      -- If you have a better solution, please update this.
      (String -> String) -> (e -> String) -> e -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 Char -> String -> String
    forall a. Eq a => List1 a -> [a] -> [a]
    dropFrom List1 Char
    "HasCallStack"
    #endif
      (String -> String) -> (e -> String) -> e -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . e -> String
    forall e. Exception e => e -> String
    displayException