    {-# OPTIONS_GHC -Wunused-imports #-}

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

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

    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

    import Agda.TypeChecking.Monad
      ( HasOptions
      , MonadFileId
      , MonadTCEnv
      , MonadTCM
      , MonadTCState
      , ReadTCState
      , TCErr
      , TCM, TCMT(..)
      , mapTCMT
      )

    -- | 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
    $cfmap :: forall a b. (a -> b) -> IM a -> IM b
    fmap :: forall a b. (a -> b) -> IM a -> IM b
    $c<$ :: forall a b. a -> IM b -> IM a
    <$ :: forall a b. a -> IM b -> IM a
    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
    $cpure :: forall a. a -> IM a
    pure :: forall a. a -> IM a
    $c<*> :: forall a b. IM (a -> b) -> IM a -> IM b
    <*> :: forall a b. IM (a -> b) -> IM a -> IM b
    $cliftA2 :: forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c
    liftA2 :: forall a b c. (a -> b -> c) -> IM a -> IM b -> IM c
    $c*> :: forall a b. IM a -> IM b -> IM b
    *> :: forall a b. IM a -> IM b -> IM b
    $c<* :: forall a b. IM a -> IM b -> IM a
    <* :: forall a b. IM a -> IM b -> 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
    $c>>= :: forall a b. IM a -> (a -> IM b) -> IM b
    >>= :: forall a b. IM a -> (a -> IM b) -> IM b
    $c>> :: forall a b. IM a -> IM b -> IM b
    >> :: forall a b. IM a -> IM b -> IM b
    $creturn :: forall a. a -> IM a
    return :: forall a. a -> IM a
    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
    $cliftIO :: forall a. IO a -> IM a
    liftIO :: 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
    $cpragmaOptions :: IM PragmaOptions
    pragmaOptions :: IM PragmaOptions
    $ccommandLineOptions :: IM CommandLineOptions
    commandLineOptions :: IM CommandLineOptions
    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
    $caskTC :: IM TCEnv
    askTC :: IM TCEnv
    $clocalTC :: forall a. (TCEnv -> TCEnv) -> IM a -> IM a
    localTC :: forall a. (TCEnv -> TCEnv) -> IM a -> IM a
    MonadTCEnv, Monad IM
    IM TCState
    Monad IM =>
    IM TCState
    -> (forall a b. Lens' TCState a -> (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' TCState a -> (a -> a) -> IM b -> IM b
    forall (m :: * -> *).
    Monad m =>
    m TCState
    -> (forall a b. Lens' TCState a -> (a -> a) -> m b -> m b)
    -> (forall a. (TCState -> TCState) -> m a -> m a)
    -> ReadTCState m
    $cgetTCState :: IM TCState
    getTCState :: IM TCState
    $clocallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> IM b -> IM b
    locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> IM b -> IM b
    $cwithTCState :: forall a. (TCState -> TCState) -> IM a -> IM a
    withTCState :: forall a. (TCState -> TCState) -> IM a -> IM a
    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
    $cgetTC :: IM TCState
    getTC :: IM TCState
    $cputTC :: TCState -> IM ()
    putTC :: TCState -> IM ()
    $cmodifyTC :: (TCState -> TCState) -> IM ()
    modifyTC :: (TCState -> TCState) -> IM ()
    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
    $cliftTCM :: forall a. TCM a -> IM a
    liftTCM :: forall a. TCM a -> IM a
    MonadTCM
      , Monad IM
    Monad IM =>
    (FileId -> IM File) -> (File -> IM FileId) -> MonadFileId IM
    File -> IM FileId
    FileId -> IM File
    forall (m :: * -> *).
    Monad m =>
    (FileId -> m File) -> (File -> m FileId) -> MonadFileId m
    $cfileFromId :: FileId -> IM File
    fileFromId :: FileId -> IM File
    $cidFromFile :: File -> IM FileId
    idFromFile :: File -> IM FileId
    MonadFileId
      )

    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 a. 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. (HasCallStack, 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 e a.
    (HasCallStack, Exception e) =>
    InputT IO a -> (e -> InputT IO a) -> InputT IO a
    forall (m :: * -> *) e a.
    (MonadCatch m, HasCallStack, 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 (m :: * -> *) a. Monad m => m a -> TCMT m a
    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)