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 :: 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
Error [Char]
s -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ([Char] -> IO ()
putStrLn [Char]
s) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Command Maybe ()
_ -> 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'
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
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 forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ forall a. Read a => ReadS a
reads [Char]
r of
Just (IOTCM
x, [Char]
"") -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Command' a
Command IOTCM
x
Just (IOTCM
_, [Char]
rem) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> Command' a
Error forall a b. (a -> b) -> a -> b
$ [Char]
"not consumed: " forall a. [a] -> [a] -> [a]
++ [Char]
rem
Maybe (IOTCM, [Char])
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> Command' a
Error forall a b. (a -> b) -> a -> b
$ [Char]
"cannot read: " forall a. [a] -> [a] -> [a]
++ [Char]
r