{-# 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 :: 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
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'
readCommand :: IO Command
readCommand :: IO Command
readCommand = do
done <- IO Bool
isEOF
if done then
return Done
else do
r <- getLine
_ <- return $! length r
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