{-# OPTIONS_GHC -Wunused-imports #-}

module Mikan.Interaction.AgdaTop
    ( repl
    ) where

import Control.Monad                ( unless )
import Control.Monad.IO.Class       ( MonadIO(..) )
import Control.Monad.Except         ( tryError )
import Control.Monad.State          ( evalStateT )
import Control.Monad.Trans          ( lift )

import Data.Char

import System.IO

import Mikan.Interaction.Base
import Mikan.Interaction.ExitCode
import Mikan.Interaction.Response as R
import Mikan.Interaction.InteractionTop
import Mikan.Interaction.Options
import Mikan.Interaction.Command ( CommandM )

import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Monad.Benchmark qualified 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
    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

    TCM () -> TCMT IO (Either TCErr ())
forall e (m :: * -> *) a. MonadError e m => m a -> m (Either e a)
tryError TCM ()
setup TCMT IO (Either TCErr ()) -> (Either TCErr () -> TCM ()) -> TCM ()
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left TCErr
err -> do
        InteractionOutputCallback
callback InteractionOutputCallback -> InteractionOutputCallback
forall a b. (a -> b) -> a -> b
$ DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> Response_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
-> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_DisplayInfo (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
 -> Response_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> Response_boot TCErr TCWarning WarningsAndNonFatalErrors
forall a b. (a -> b) -> a -> b
$ Info_Error_boot TCErr TCWarning
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
Info_Error_boot tcErr tcWarning
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Error (Info_Error_boot TCErr TCWarning
 -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> Info_Error_boot TCErr TCWarning
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall a b. (a -> b) -> a -> b
$ TCErr -> Info_Error_boot TCErr TCWarning
forall tcErr tcWarning. tcErr -> Info_Error_boot tcErr tcWarning
Info_GenericError TCErr
err
        InteractionOutputCallback
callback InteractionOutputCallback -> InteractionOutputCallback
forall a b. (a -> b) -> a -> b
$ Status -> Response_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
Status -> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_Status (Status -> Response_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> Status
-> Response_boot TCErr TCWarning WarningsAndNonFatalErrors
forall a b. (a -> b) -> a -> b
$ Status
          { sChecked :: Bool
sChecked = Bool
False
          -- We couldn't initialize the command line options, so
          -- we've just got to pick reasonable defaults here.
          , sShowImplicitArguments :: Bool
sShowImplicitArguments = Bool
False
          , sShowIrrelevantArguments :: Bool
sShowIrrelevantArguments = Bool
False
          }
        -- We can't consult --interaction-exit-on-error,
        -- so the most reasonable thing to do is just bail out.
        -- We use 'CommandError' here so that editor tooling
        -- can know that it should interpret the output
        -- as interaction commands.
        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
$ AgdaError -> IO ()
forall a. AgdaError -> IO a
exitAgdaWith AgdaError
CommandError
      Right () -> do
        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
        opts <- commandLineOptions
        evalStateT interact' (initCommandState (opts { optAbsoluteIncludePaths = [] }) commands)
  where
  interact' :: CommandM ()
  interact' :: StateT CommandState TCM ()
interact' = do
    StateT CommandState TCM ()
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 () -> StateT CommandState TCM ()
forall a. IO a -> StateT CommandState TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT CommandState TCM ())
-> IO () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> IO ()
putStr [Char]
prompt
        Handle -> IO ()
hFlush Handle
stdout
      r <- (IOTCM -> StateT CommandState TCM ())
-> CommandM (Command' (Maybe ()))
forall a. (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
maybeAbort IOTCM -> StateT CommandState TCM ()
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 -- Done.
        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'

  -- Reads the next command from stdin.
  readCommand :: IO Command
  readCommand :: IO Command
readCommand = do
    done <- IO Bool
isEOF
    if done then
      return Done
    else do
      r <- getLine
      _ <- return $! length r     -- force to read the full input line
      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