    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 Data.Maybe
    import System.IO

    import Agda.Interaction.Base
    import Agda.Interaction.Response as R
    import Agda.Interaction.InteractionTop
    import Agda.Interaction.Options
    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 (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

        CommandQueue
    commands <- IO CommandQueue -> TCMT IO CommandQueue
    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

        CommandM () -> CommandM ()
    handleCommand_ (TCM () -> CommandM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM ()
    setup) CommandM () -> CommandState -> TCM ()
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    `evalStateT` CommandQueue -> CommandState
    initCommandState CommandQueue
    commands

        CommandLineOptions
    opts <- TCMT IO CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
        ((), CommandState)
    _ <- CommandM ()
    interact' CommandM () -> CommandState -> TCM ((), CommandState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    `runStateT`
               (CommandQueue -> CommandState
    initCommandState CommandQueue
    commands)
                 { optionsOnReload :: CommandLineOptions
    optionsOnReload = CommandLineOptions
    opts{ optAbsoluteIncludePaths :: [AbsolutePath]
    optAbsoluteIncludePaths = [] } }
        () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      where
      interact' :: CommandM ()
      interact' :: CommandM ()
    interact' = do
        CommandM ()
    forall (m :: * -> *). MonadBench m => m ()
    Bench.reset
        Bool
    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 (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
          Command' (Maybe ())
    r <- (IOTCM -> CommandM ()) -> CommandM (Command' (Maybe ()))
    forall a. (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
    maybeAbort IOTCM -> CommandM ()
    runInteraction
          case Command' (Maybe ())
    r of
            Command' (Maybe ())
    Done      -> Bool -> StateT CommandState TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True -- Done.
            Error [Char]
    s   -> IO () -> CommandM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ([Char] -> IO ()
    putStrLn [Char]
    s) CommandM ()
    -> StateT CommandState TCM Bool -> StateT CommandState TCM Bool
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Bool -> StateT CommandState TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
            Command Maybe ()
    _ -> Bool -> StateT CommandState TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

        TCM () -> CommandM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCM ()
    forall (tcm :: * -> *). MonadTCM tcm => tcm ()
    Bench.print
        Bool -> CommandM () -> CommandM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    done CommandM ()
    interact'

      -- Reads the next command from stdin.

      readCommand :: IO Command
      readCommand :: IO Command
    readCommand = do
        Bool
    done <- IO Bool
    isEOF
        if Bool
    done then
          Command -> IO Command
    forall (m :: * -> *) a. Monad m => a -> m a
    return Command
    forall a. Command' a
    Done
        else do
          [Char]
    r <- IO [Char]
    getLine
          Int
    _ <- Int -> IO Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> IO Int) -> Int -> IO Int
    forall a b. (a -> b) -> a -> b
    $! [Char] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Char]
    r     -- force to read the full input line
          case (Char -> Bool) -> [Char] -> [Char]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile Char -> Bool
    isSpace [Char]
    r of
            [Char]
    ""          -> IO Command
    readCommand
            (Char
    '-':Char
    '-':[Char]
    _) -> IO Command
    readCommand
            [Char]
    _           -> case [(IOTCM, [Char])] -> Maybe (IOTCM, [Char])
    forall a. [a] -> Maybe a
    listToMaybe ([(IOTCM, [Char])] -> Maybe (IOTCM, [Char]))
    -> [(IOTCM, [Char])] -> Maybe (IOTCM, [Char])
    forall a b. (a -> b) -> a -> b
    $ ReadS IOTCM
    forall a. Read a => ReadS a
    reads [Char]
    r of
              Just (IOTCM
    x, [Char]
    "")  -> Command -> IO Command
    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
    x
              Just (IOTCM
    _, [Char]
    rem) -> Command -> IO Command
    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] -> Command) -> [Char] -> Command
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "not consumed: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    rem
              Maybe (IOTCM, [Char])
    _             -> Command -> IO Command
    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] -> Command) -> [Char] -> Command
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "cannot read: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    r