{-# LANGUAGE CPP #-}

-- | Auxiliary functions for the IO monad.

module Agda.Utils.IO where

import Control.Exception
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 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