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

    CommandQueue
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

    CommandM () -> CommandM ()
handleCommand_ (TCM () -> CommandM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
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 -> TCMT IO ((), 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 a. a -> TCMT IO a
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 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
      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 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
          Bool
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 Bool
exit
            then IO Bool -> StateT CommandState TCM Bool
forall a. IO a -> StateT CommandState TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (AgdaError -> IO Bool
forall a. AgdaError -> IO a
exitAgdaWith AgdaError
CommandError)
            else do
              IO () -> CommandM ()
forall a. IO a -> StateT CommandState TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ([Char] -> IO ()
putStrLn [Char]
s)
              Bool -> StateT CommandState TCM Bool
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    TCM () -> CommandM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
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 a. a -> IO a
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 a. a -> IO a
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 a. [a] -> 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 [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