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
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ IO Command -> IO CommandQueue
initialiseCommandQueue IO Command
readCommand

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

    CommandLineOptions
opts <- forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
    ((), CommandState)
_ <- CommandM ()
interact' 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 = [] } }
    forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
  interact' :: CommandM ()
  interact' :: CommandM ()
interact' = do
    forall (m :: * -> *). MonadBench m => m ()
Bench.reset
    Bool
done <- forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [] forall a b. (a -> b) -> a -> b
$ do

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

    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (tcm :: * -> *). MonadTCM tcm => tcm ()
Bench.print
    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
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Command' a
Done
    else do
      [Char]
r <- IO [Char]
getLine
      Int
_ <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
r     -- force to read the full input line
      case 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Command' a
Command IOTCM
cmd
          Left [Char]
err  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> Command' a
Error [Char]
err