{-# OPTIONS_GHC -Wno-missing-methods #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveGeneric #-}
module Agda
( start
, runAgda
, sendCommand
, getCommandLineOptions
, CommandReq(..)
, CommandRes(..)
) where
import Prelude hiding ( null )
import Agda.Compiler.Backend ( parseBackendOptions )
import Agda.Compiler.Builtin ( builtinBackends )
import Agda.Convert ( fromResponse )
import Agda.Interaction.Base ( Command
, Command'(Command, Done, Error)
#if MIN_VERSION_Agda(2,7,0)
#else
, CommandM
#endif
, CommandState(optionsOnReload)
, IOTCM
, initCommandState
, parseIOTCM
)
#if MIN_VERSION_Agda(2,8,0)
import Agda.Interaction.Command ( CommandM )
#endif
import Agda.Syntax.Common.Pretty ( render, vcat )
import Agda.Interaction.InteractionTop
( initialiseCommandQueue
, maybeAbort
, runInteraction
#if MIN_VERSION_Agda(2,8,0)
#elif MIN_VERSION_Agda(2,7,0)
, CommandM
#endif
)
import Agda.Interaction.Options ( CommandLineOptions
( optAbsoluteIncludePaths
)
, defaultOptions
, runOptM
)
import Agda.TypeChecking.Errors ( getAllWarningsOfTCErr
, prettyError
, prettyTCWarnings'
)
import Agda.TypeChecking.Monad ( HasOptions
, TCErr
, commandLineOptions
, runTCMTop'
)
import Agda.TypeChecking.Monad.Base ( TCM )
import qualified Agda.TypeChecking.Monad.Benchmark
as Bench
import Agda.TypeChecking.Monad.State ( setInteractionOutputCallback )
import Agda.Utils.FileName ( absolute )
import Agda.Utils.Impossible ( CatchImpossible
( catchImpossible
)
, Impossible
)
import Agda.Utils.Null ( null )
import Agda.VersionCommit ( versionWithCommitInfo )
import Control.Exception ( SomeException
, catch
)
import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Data.Aeson ( FromJSON
, ToJSON(toJSON)
, Value
, fromJSON
)
import qualified Data.Aeson as JSON
import Data.Maybe ( listToMaybe )
import Data.Text ( pack )
import GHC.Generics ( Generic )
import Language.LSP.Server ( getConfig )
import Monad
import Options ( Config(configRawAgdaOptions)
, Options(optRawAgdaOptions, optRawResponses)
, versionNumber
)
import qualified Agda.IR as IR
import Agda.Interaction.JSON ( encode, encodeTCM )
import Agda.Interaction.JSONTop ()
getAgdaVersion :: String
getAgdaVersion = versionWithCommitInfo
start :: ServerM IO ()
start = do
env <- ask
writeLog "[Agda] interaction start"
result <- runAgda $ do
-- decides how to output Response
lift $ setInteractionOutputCallback $ \response -> do
resp <- if optRawResponses (envOptions env)
then do
value <- (pure . encodeTCM) response
resp' <- fmap IR.ResponseJSONRaw value
return resp'
else fromResponse response
sendResponse env resp
-- keep reading command
commands <- liftIO $ initialiseCommandQueue (readCommand env)
-- get command line options
options <- getCommandLineOptions
-- start the loop
let commandState = (initCommandState commands)
{ optionsOnReload = options { optAbsoluteIncludePaths = [] }
}
_ <- mapReaderT (`runStateT` commandState) (loop env)
return ()
-- TODO: we should examine the result
case result of
Left _err -> return ()
Right _val -> return ()
where
loop :: Env -> ServerM CommandM ()
loop env = do
Bench.reset
done <- Bench.billTo [] $ do
r <- lift $ maybeAbort runInteraction
case r of
Done -> return True -- Done.
Error s -> do
writeLog ("Error " <> pack s)
return False
Command _ -> do
writeLog "[Response] Finished sending, waiting for them to complete"
waitUntilResponsesSent
signalCommandFinish
return False
lift Bench.print
unless done (loop env)
-- Reads the next command from the Channel
readCommand :: Env -> IO Command
readCommand env = Command <$> consumeCommand env
--------------------------------------------------------------------------------
-- | Convert "CommandReq" to "CommandRes"
sendCommand :: MonadIO m => Value -> ServerM m Value
sendCommand value = do
-- JSON Value => Request => Response
case fromJSON value of
JSON.Error msg ->
return
$ toJSON
$ CmdRes
$ Just
$ CmdErrCannotDecodeJSON
$ show msg
++ "\n"
++ show value
JSON.Success request -> toJSON <$> handleCommandReq request
handleCommandReq :: MonadIO m => CommandReq -> ServerM m CommandRes
handleCommandReq CmdReqSYN = return $ CmdResACK Agda.getAgdaVersion versionNumber
handleCommandReq (CmdReq cmd) = do
case parseIOTCM cmd of
Left err -> do
writeLog $ "[Error] CmdErrCannotParseCommand:\n" <> pack err
return $ CmdRes (Just (CmdErrCannotParseCommand err))
Right iotcm -> do
writeLog $ "[Request] " <> pack (show cmd)
provideCommand iotcm
return $ CmdRes Nothing
--------------------------------------------------------------------------------
getCommandLineOptions
:: (HasOptions m, MonadIO m) => ServerM m CommandLineOptions
getCommandLineOptions = do
-- command line options from ARGV
argv <- asks (optRawAgdaOptions . envOptions)
-- command line options from agda-mode
config <- asks (configRawAgdaOptions . envConfig)
-- concatenate both
let merged = argv <> config
result <- runExceptT $ do
let p = parseBackendOptions builtinBackends merged defaultOptions
let (r, _warns) = runOptM p
(bs, opts) <- ExceptT $ pure r
return opts
case result of
-- something bad happened, use the default options instead
Left _ -> commandLineOptions
Right opts -> return opts
-- | Run a TCM action in IO and throw away all of the errors
-- TODO: handle the caught errors
runAgda :: MonadIO m => ServerM TCM a -> ServerM m (Either String a)
runAgda p = do
env <- ask
let p' = runServerM env p
liftIO
$ runTCMTop'
( (Right <$> p')
`catchError` handleTCErr
`catchImpossible` handleImpossible
)
`catch` catchException
where
handleTCErr :: TCErr -> TCM (Either String a)
handleTCErr err = do
s2s <- prettyTCWarnings' =<< getAllWarningsOfTCErr err
s1 <- prettyError err
let ss = filter (not . null) $ s2s ++ [s1]
let errorMsg = render $ vcat ss
return (Left errorMsg)
handleImpossible :: Impossible -> TCM (Either String a)
handleImpossible = return . Left . show
catchException :: SomeException -> IO (Either String a)
catchException e = return $ Left $ show e
--------------------------------------------------------------------------------
data CommandReq
= CmdReqSYN -- ^ For client to initiate a 2-way handshake
| CmdReq String
deriving (Generic)
instance ToJSON CommandReq
instance FromJSON CommandReq
data CommandRes
= CmdResACK -- ^ For server to complete a 2-way handshake
String -- ^ Version number of Agda
Int -- ^ Version number of the language server
| CmdRes -- ^ Response for 'CmdReq'
(Maybe CommandErr) -- ^ 'Nothing' to indicate success
deriving (Generic)
instance ToJSON CommandRes
data CommandErr
= CmdErrCannotDecodeJSON String
| CmdErrCannotParseCommand String
deriving (Generic)
instance ToJSON CommandErr