    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.Interaction.AgdaTop
        ( repl
        ) where

    import Control.Monad                ( unless )
    import Control.Monad.IO.Class       ( MonadIO(..) )
    import Control.Monad.State          ( evalStateT, runStateT )
    import Control.Monad.Trans          ( lift )

    import Data.Char

    import System.IO

    import Agda.Interaction.Base
    import Agda.Interaction.ExitCode
    import Agda.Interaction.Response as R
    import Agda.Interaction.InteractionTop
    import Agda.Interaction.Options
    import Agda.Interaction.Command ( CommandM )

    import Agda.TypeChecking.Monad
    import qualified Agda.TypeChecking.Monad.Benchmark as Bench

    ----------------------------------

    -- | 'repl' is a fake ghci interpreter for both the Emacs the JSON frontend
    repl :: InteractionOutputCallback -> String -> TCM () -> TCM ()
    repl :: InteractionOutputCallback -> [Char] -> TCM () -> TCM ()
    repl InteractionOutputCallback
    callback [Char]
    prompt TCM ()
    setup = do
        IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          Handle -> BufferMode -> IO ()
    hSetBuffering Handle
    stdout BufferMode
    LineBuffering
          Handle -> BufferMode -> IO ()
    hSetBuffering Handle
    stdin  BufferMode
    LineBuffering
          Handle -> TextEncoding -> IO ()
    hSetEncoding  Handle
    stdout TextEncoding
    utf8
          Handle -> TextEncoding -> IO ()
    hSetEncoding  Handle
    stdin  TextEncoding
    utf8

        InteractionOutputCallback -> TCM ()
    setInteractionOutputCallback InteractionOutputCallback
    callback

        commands <- IO CommandQueue -> TCMT IO CommandQueue
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO CommandQueue -> TCMT IO CommandQueue)
    -> IO CommandQueue -> TCMT IO CommandQueue
    forall a b. (a -> b) -> a -> b
    $ IO Command -> IO CommandQueue
    initialiseCommandQueue IO Command
    readCommand

        handleCommand_ (lift setup) `evalStateT` initCommandState commands

        opts <- commandLineOptions
        _ <- interact' `runStateT`
               (initCommandState commands)
                 { optionsOnReload = opts{ optAbsoluteIncludePaths = [] } }
        return ()
      where
      interact' :: CommandM ()
      interact' :: CommandM ()
    interact' = do
        CommandM ()
    forall (m :: * -> *). MonadBench m => m ()
    Bench.reset
        done <- Account (BenchPhase (StateT CommandState TCM))
    -> StateT CommandState TCM Bool -> StateT CommandState TCM Bool
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [] (StateT CommandState TCM Bool -> StateT CommandState TCM Bool)
    -> StateT CommandState TCM Bool -> StateT CommandState TCM Bool
    forall a b. (a -> b) -> a -> b
    $ do

          IO () -> CommandM ()
    forall a. IO a -> StateT CommandState TCM a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> CommandM ()) -> IO () -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ do
            [Char] -> IO ()
    putStr [Char]
    prompt
            Handle -> IO ()
    hFlush Handle
    stdout
          r <- (IOTCM -> CommandM ()) -> CommandM (Command' (Maybe ()))
    forall a. (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
    maybeAbort IOTCM -> CommandM ()
    runInteraction
          case r of
            Command' (Maybe ())
    Done      -> Bool -> StateT CommandState TCM Bool
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True -- Done.
            Command Maybe ()
    _ -> Bool -> StateT CommandState TCM Bool
    forall a. a -> StateT CommandState TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
            Error [Char]
    s   -> do
              exit <- CommandLineOptions -> Bool
    optExitOnError (CommandLineOptions -> Bool)
    -> StateT CommandState TCM CommandLineOptions
    -> StateT CommandState TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> StateT CommandState TCM CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
              if exit
                then liftIO (exitAgdaWith CommandError)
                else do
                  liftIO (putStrLn s)
                  return False

        lift Bench.print
        unless done interact'

      -- Reads the next command from stdin.

      readCommand :: IO Command
      readCommand :: IO Command
    readCommand = do
        done <- IO Bool
    isEOF
        if done then
          return Done
        else do
          r <- getLine
          _ <- return $! length r     -- force to read the full input line
          case dropWhile isSpace r of
            [Char]
    ""          -> IO Command
    readCommand
            (Char
    '-':Char
    '-':[Char]
    _) -> IO Command
    readCommand
            [Char]
    _           -> case [Char] -> Either [Char] IOTCM
    parseIOTCM [Char]
    r of
              Right IOTCM
    cmd -> Command -> IO Command
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Command -> IO Command) -> Command -> IO Command
    forall a b. (a -> b) -> a -> b
    $ IOTCM -> Command
    forall a. a -> Command' a
    Command IOTCM
    cmd
              Left [Char]
    err  -> Command -> IO Command
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Command -> IO Command) -> Command -> IO Command
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Command
    forall a. [Char] -> Command' a
    Error [Char]
    err