    {-# OPTIONS_GHC -fwarn-orphans #-}
    {-# LANGUAGE CPP               #-}

    module Agda.Interaction.Monad
      ( IM
      , runIM
      , readline
      ) where

    import Agda.TypeChecking.Monad
      ( HasOptions
      , MonadTCEnv
      , MonadTCM
      , MonadTCState
      , ReadTCState
      , TCErr
      , TCM, TCMT(..)
      , mapTCMT
      )
    import Control.Exception (throwIO)
    import Control.Monad.Except (MonadError (..))
    import Control.Monad.Trans (MonadIO, lift, liftIO)
    import qualified System.Console.Haskeline as Haskeline

    -- MonadException is replaced by MonadCatch in haskeline 0.8
    #if MIN_VERSION_haskeline(0,8,0)
    import qualified Control.Monad.Catch as Haskeline (catch)
    #endif

    -- | Interaction monad.
    newtype IM a = IM {forall a. IM a -> TCMT (InputT IO) a
    unIM :: TCMT (Haskeline.InputT IO) a}
      deriving
      ( (forall a b. (a -> b) -> IM a -> IM b)
    -> (forall a b. a -> IM b -> IM a) -> Functor IM
    forall a b. a -> IM b -> IM a
    forall a b. (a -> b) -> IM a -> IM b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> IM b -> IM a
    $c<$ :: forall a b. a -> IM b -> IM a
    fmap :: forall a b. (a -> b) -> IM a -> IM b
    $cfmap :: forall a b. (a -> b) -> IM a -> IM b
    Functor, Functor IM
    Functor IM
    -> (forall a. a -> IM a)
    -> (forall a b. IM (a -> b) -> IM a -> IM b)
    -> (forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c)
    -> (forall a b. IM a -> IM b -> IM b)
    -> (forall a b. IM a -> IM b -> IM a)
    -> Applicative IM
    forall a. a -> IM a
    forall a b. IM a -> IM b -> IM a
    forall a b. IM a -> IM b -> IM b
    forall a b. IM (a -> b) -> IM a -> IM b
    forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c
    forall (f :: * -> *).
    Functor f
    -> (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    <* :: forall a b. IM a -> IM b -> IM a
    $c<* :: forall a b. IM a -> IM b -> IM a
    *> :: forall a b. IM a -> IM b -> IM b
    $c*> :: forall a b. IM a -> IM b -> IM b
    liftA2 :: forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c
    $cliftA2 :: forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c
    <*> :: forall a b. IM (a -> b) -> IM a -> IM b
    $c<*> :: forall a b. IM (a -> b) -> IM a -> IM b
    pure :: forall a. a -> IM a
    $cpure :: forall a. a -> IM a
    Applicative, Applicative IM
    Applicative IM
    -> (forall a b. IM a -> (a -> IM b) -> IM b)
    -> (forall a b. IM a -> IM b -> IM b)
    -> (forall a. a -> IM a)
    -> Monad IM
    forall a. a -> IM a
    forall a b. IM a -> IM b -> IM b
    forall a b. IM a -> (a -> IM b) -> IM b
    forall (m :: * -> *).
    Applicative m
    -> (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    return :: forall a. a -> IM a
    $creturn :: forall a. a -> IM a
    >> :: forall a b. IM a -> IM b -> IM b
    $c>> :: forall a b. IM a -> IM b -> IM b
    >>= :: forall a b. IM a -> (a -> IM b) -> IM b
    $c>>= :: forall a b. IM a -> (a -> IM b) -> IM b
    Monad, Monad IM
    Monad IM -> (forall a. IO a -> IM a) -> MonadIO IM
    forall a. IO a -> IM a
    forall (m :: * -> *).
    Monad m -> (forall a. IO a -> m a) -> MonadIO m
    liftIO :: forall a. IO a -> IM a
    $cliftIO :: forall a. IO a -> IM a
    MonadIO
      , Monad IM
    Functor IM
    Applicative IM
    IM PragmaOptions
    IM CommandLineOptions
    Functor IM
    -> Applicative IM
    -> Monad IM
    -> IM PragmaOptions
    -> IM CommandLineOptions
    -> HasOptions IM
    forall (m :: * -> *).
    Functor m
    -> Applicative m
    -> Monad m
    -> m PragmaOptions
    -> m CommandLineOptions
    -> HasOptions m
    commandLineOptions :: IM CommandLineOptions
    $ccommandLineOptions :: IM CommandLineOptions
    pragmaOptions :: IM PragmaOptions
    $cpragmaOptions :: IM PragmaOptions
    HasOptions, Monad IM
    IM TCEnv
    Monad IM
    -> IM TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> IM a -> IM a)
    -> MonadTCEnv IM
    forall a. (TCEnv -> TCEnv) -> IM a -> IM a
    forall (m :: * -> *).
    Monad m
    -> m TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
    -> MonadTCEnv m
    localTC :: forall a. (TCEnv -> TCEnv) -> IM a -> IM a
    $clocalTC :: forall a. (TCEnv -> TCEnv) -> IM a -> IM a
    askTC :: IM TCEnv
    $caskTC :: IM TCEnv
    MonadTCEnv, Monad IM
    IM TCState
    Monad IM
    -> IM TCState
    -> (forall a b. Lens' a TCState -> (a -> a) -> IM b -> IM b)
    -> (forall a. (TCState -> TCState) -> IM a -> IM a)
    -> ReadTCState IM
    forall a. (TCState -> TCState) -> IM a -> IM a
    forall a b. Lens' a TCState -> (a -> a) -> IM b -> IM b
    forall (m :: * -> *).
    Monad m
    -> m TCState
    -> (forall a b. Lens' a TCState -> (a -> a) -> m b -> m b)
    -> (forall a. (TCState -> TCState) -> m a -> m a)
    -> ReadTCState m
    withTCState :: forall a. (TCState -> TCState) -> IM a -> IM a
    $cwithTCState :: forall a. (TCState -> TCState) -> IM a -> IM a
    locallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> IM b -> IM b
    $clocallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> IM b -> IM b
    getTCState :: IM TCState
    $cgetTCState :: IM TCState
    ReadTCState, Monad IM
    IM TCState
    Monad IM
    -> IM TCState
    -> (TCState -> IM ())
    -> ((TCState -> TCState) -> IM ())
    -> MonadTCState IM
    TCState -> IM ()
    (TCState -> TCState) -> IM ()
    forall (m :: * -> *).
    Monad m
    -> m TCState
    -> (TCState -> m ())
    -> ((TCState -> TCState) -> m ())
    -> MonadTCState m
    modifyTC :: (TCState -> TCState) -> IM ()
    $cmodifyTC :: (TCState -> TCState) -> IM ()
    putTC :: TCState -> IM ()
    $cputTC :: TCState -> IM ()
    getTC :: IM TCState
    $cgetTC :: IM TCState
    MonadTCState, Applicative IM
    MonadIO IM
    HasOptions IM
    MonadTCState IM
    MonadTCEnv IM
    Applicative IM
    -> MonadIO IM
    -> MonadTCEnv IM
    -> MonadTCState IM
    -> HasOptions IM
    -> (forall a. TCM a -> IM a)
    -> MonadTCM IM
    forall a. TCM a -> IM a
    forall (tcm :: * -> *).
    Applicative tcm
    -> MonadIO tcm
    -> MonadTCEnv tcm
    -> MonadTCState tcm
    -> HasOptions tcm
    -> (forall a. TCM a -> tcm a)
    -> MonadTCM tcm
    liftTCM :: forall a. TCM a -> IM a
    $cliftTCM :: forall a. TCM a -> IM a
    MonadTCM )

    runIM :: IM a -> TCM a
    runIM :: forall a. IM a -> TCM a
    runIM = (forall a1. InputT IO a1 -> IO a1)
    -> TCMT (InputT IO) a -> TCMT IO a
    forall (m :: * -> *) (n :: * -> *) a.
    (forall a1. m a1 -> n a1) -> TCMT m a -> TCMT n a
    mapTCMT (Settings IO -> InputT IO a1 -> IO a1
    forall (m :: * -> *) a.
    (MonadIO m, MonadMask m) =>
    Settings m -> InputT m a -> m a
    Haskeline.runInputT Settings IO
    forall (m :: * -> *). MonadIO m => Settings m
    Haskeline.defaultSettings) (TCMT (InputT IO) a -> TCMT IO a)
    -> (IM a -> TCMT (InputT IO) a) -> IM a -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IM a -> TCMT (InputT IO) a
    forall a. IM a -> TCMT (InputT IO) a
    unIM

    instance MonadError TCErr IM where
      throwError :: forall a. TCErr -> IM a
    throwError                = IO a -> IM a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO a -> IM a) -> (TCErr -> IO a) -> TCErr -> IM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCErr -> IO a
    forall e a. Exception e => e -> IO a
    throwIO
      catchError :: forall a. IM a -> (TCErr -> IM a) -> IM a
    catchError (IM (TCM IORef TCState -> TCEnv -> InputT IO a
    m)) TCErr -> IM a
    h = TCMT (InputT IO) a -> IM a
    forall a. TCMT (InputT IO) a -> IM a
    IM (TCMT (InputT IO) a -> IM a)
    -> ((IORef TCState -> TCEnv -> InputT IO a) -> TCMT (InputT IO) a)
    -> (IORef TCState -> TCEnv -> InputT IO a)
    -> IM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (IORef TCState -> TCEnv -> InputT IO a) -> TCMT (InputT IO) a
    forall (m :: * -> *) a. (IORef TCState -> TCEnv -> m a) -> TCMT m a
    TCM ((IORef TCState -> TCEnv -> InputT IO a) -> IM a)
    -> (IORef TCState -> TCEnv -> InputT IO a) -> IM a
    forall a b. (a -> b) -> a -> b
    $ \IORef TCState
    s TCEnv
    e ->
        IORef TCState -> TCEnv -> InputT IO a
    m IORef TCState
    s TCEnv
    e InputT IO a -> (TCErr -> InputT IO a) -> InputT IO a
    forall (m :: * -> *) e a.
    (MonadCatch m, Exception e) =>
    m a -> (e -> m a) -> m a
    `Haskeline.catch` \TCErr
    err -> TCMT (InputT IO) a -> IORef TCState -> TCEnv -> InputT IO a
    forall (m :: * -> *) a. TCMT m a -> IORef TCState -> TCEnv -> m a
    unTCM (IM a -> TCMT (InputT IO) a
    forall a. IM a -> TCMT (InputT IO) a
    unIM (TCErr -> IM a
    h TCErr
    err)) IORef TCState
    s TCEnv
    e

    -- | Line reader. The line reader history is not stored between
    -- sessions.
    readline :: String -> IM (Maybe String)
    readline :: String -> IM (Maybe String)
    readline String
    s = TCMT (InputT IO) (Maybe String) -> IM (Maybe String)
    forall a. TCMT (InputT IO) a -> IM a
    IM (TCMT (InputT IO) (Maybe String) -> IM (Maybe String))
    -> TCMT (InputT IO) (Maybe String) -> IM (Maybe String)
    forall a b. (a -> b) -> a -> b
    $ InputT IO (Maybe String) -> TCMT (InputT IO) (Maybe String)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (String -> InputT IO (Maybe String)
    forall (m :: * -> *).
    (MonadIO m, MonadMask m) =>
    String -> InputT m (Maybe String)
    Haskeline.getInputLine String
    s)