AgdaTop.hs

{-# 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.Interaction.Command ( CommandM )

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 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 -- Done.
        Command _ -> return False
        Error s   -> do
          exit <- optExitOnError <$> 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 = do
    done <- 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
        ""          -> readCommand
        ('-':'-':_) -> readCommand
        _           -> case parseIOTCM r of
          Right cmd -> return $ Command cmd
          Left err  -> return $ Error err