module Agda.Interaction.AgdaTop
( repl
) where
import Control.Monad.State
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 :: InteractionOutputCallback -> String -> TCM () -> TCM ()
repl callback prompt setup = do
liftIO $ do
hSetBuffering stdout LineBuffering
hSetBuffering stdin LineBuffering
hSetEncoding stdout utf8
hSetEncoding stdin utf8
setInteractionOutputCallback callback
commands <- liftIO $ initialiseCommandQueue readCommand
handleCommand_ (lift setup) `evalStateT` initCommandState commands
opts <- commandLineOptions
_ <- interact' `runStateT`
(initCommandState commands)
{ optionsOnReload = opts{ optAbsoluteIncludePaths = [] } }
return ()
where
interact' :: CommandM ()
interact' = do
Bench.reset
done <- Bench.billTo [] $ do
liftIO $ do
putStr prompt
hFlush stdout
r <- maybeAbort runInteraction
case r of
Done -> return True
Error s -> liftIO (putStrLn s) >> return False
Command _ -> return False
lift Bench.print
unless done interact'
readCommand :: IO Command
readCommand = do
done <- isEOF
if done then
return Done
else do
r <- getLine
_ <- return $! length r
case dropWhile isSpace r of
"" -> readCommand
('-':'-':_) -> readCommand
_ -> case listToMaybe $ reads r of
Just (x, "") -> return $ Command x
Just (_, rem) -> return $ Error $ "not consumed: " ++ rem
_ -> return $ Error $ "cannot read: " ++ r