{-# 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.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