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 -> String -> TCM () -> TCM ()
repl InteractionOutputCallback
callback String
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
        String -> IO ()
putStr String
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 String
s   -> IO () -> CommandM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO ()
putStrLn String
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
      String
r <- IO String
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
$! String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
r     -- force to read the full input line
      case (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
r of
        String
""          -> IO Command
readCommand
        (Char
'-':Char
'-':String
_) -> IO Command
readCommand
        String
_           -> case [(IOTCM, String)] -> Maybe (IOTCM, String)
forall a. [a] -> Maybe a
listToMaybe ([(IOTCM, String)] -> Maybe (IOTCM, String))
-> [(IOTCM, String)] -> Maybe (IOTCM, String)
forall a b. (a -> b) -> a -> b
$ ReadS IOTCM
forall a. Read a => ReadS a
reads String
r of
          Just (IOTCM
x, String
"")  -> 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
_, String
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
$ String -> Command
forall a. String -> Command' a
Error (String -> Command) -> String -> Command
forall a b. (a -> b) -> a -> b
$ String
"not consumed: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rem
          Maybe (IOTCM, String)
_             -> 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
$ String -> Command
forall a. String -> Command' a
Error (String -> Command) -> String -> Command
forall a b. (a -> b) -> a -> b
$ String
"cannot read: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
r