{-# OPTIONS_GHC -Wno-missing-methods #-}
{-# LANGUAGE DeriveGeneric #-}

module Agda
  ( start
  , runAgda
  , sendCommand
  , getCommandLineOptions
  ) where

import           Agda.Compiler.Backend          ( parseBackendOptions )
import           Agda.Compiler.Builtin          ( builtinBackends )
import           Agda.Convert                   ( fromResponse )
import           Agda.Interaction.Base          ( Command
                                                , Command'(Command, Done, Error)
                                                , CommandM
                                                , CommandState(optionsOnReload)
                                                , IOTCM
                                                , initCommandState
                                                )
import           Agda.Interaction.InteractionTop
                                                ( initialiseCommandQueue
                                                , maybeAbort
                                                , runInteraction
                                                )
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.VersionCommit             ( versionWithCommitInfo )
import           Control.Exception              ( SomeException
                                                , catch
                                                )
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)
                                                )

getAgdaVersion :: String
getAgdaVersion :: String
getAgdaVersion = String
versionWithCommitInfo

start :: ServerM IO ()
start :: ServerM IO ()
start = do
  Env
env <- forall r (m :: * -> *). MonadReader r m => m r
ask

  forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog Text
"[Agda] interaction start"

  Either String ()
result <- forall (m :: * -> *) a.
MonadIO m =>
ServerM TCM a -> ServerM m (Either String a)
runAgda forall a b. (a -> b) -> a -> b
$ do
    -- decides how to output Response
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ InteractionOutputCallback -> TCM ()
setInteractionOutputCallback forall a b. (a -> b) -> a -> b
$ \Response
response -> do
      Response
reaction <- Response -> TCM Response
fromResponse Response
response
      forall (m :: * -> *).
(Monad m, MonadIO m) =>
Env -> Response -> TCMT m ()
sendResponse Env
env Response
reaction

    -- keep reading command
    CommandQueue
commands <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ IO Command -> IO CommandQueue
initialiseCommandQueue (Env -> IO Command
readCommand Env
env)

    -- get command line options 
    CommandLineOptions
options  <- forall (m :: * -> *).
(HasOptions m, MonadIO m) =>
ServerM m CommandLineOptions
getCommandLineOptions

    -- start the loop
    let commandState :: CommandState
commandState = (CommandQueue -> CommandState
initCommandState CommandQueue
commands)
          { optionsOnReload :: CommandLineOptions
optionsOnReload = CommandLineOptions
options { optAbsoluteIncludePaths :: [AbsolutePath]
optAbsoluteIncludePaths = [] }
          }

    ((), CommandState)
_ <- forall (m :: * -> *) a (n :: * -> *) b r.
(m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT (forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` CommandState
commandState) (Env -> ServerM CommandM ()
loop Env
env)

    forall (m :: * -> *) a. Monad m => a -> m a
return ()
  -- TODO: we should examine the result
  case Either String ()
result of
    Left  String
_err -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Right ()
_val -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
 where
  loop :: Env -> ServerM CommandM ()
  loop :: Env -> ServerM CommandM ()
loop Env
env = 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
      Command' (Maybe ())
r <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
maybeAbort IOTCM -> StateT CommandState TCM ()
runInteraction
      case Command' (Maybe ())
r of
        Command' (Maybe ())
Done    -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- Done.
        Error String
s -> do
          forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog (Text
"Error " forall a. Semigroup a => a -> a -> a
<> String -> Text
pack String
s)
          forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        Command Maybe ()
_ -> do
          forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog Text
"[Response] Finished sending, waiting for them to complete"
          forall (m :: * -> *). (Monad m, MonadIO m) => ServerM m ()
waitUntilResponsesSent
          forall (m :: * -> *). (Monad m, MonadIO m) => ServerM m ()
signalCommandFinish
          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 (Env -> ServerM CommandM ()
loop Env
env)

  -- Reads the next command from the Channel
  readCommand :: Env -> IO Command
  readCommand :: Env -> IO Command
readCommand Env
env = forall a. a -> Command' a
Command forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Monad m, MonadIO m) => Env -> m IOTCM
consumeCommand Env
env

--------------------------------------------------------------------------------

-- | Convert "CommandReq" to "CommandRes"

sendCommand :: MonadIO m => Value -> ServerM m Value
sendCommand :: forall (m :: * -> *). MonadIO m => Value -> ServerM m Value
sendCommand Value
value = do
    -- JSON Value => Request => Response
  case forall a. FromJSON a => Value -> Result a
fromJSON Value
value of
    JSON.Error String
msg ->
      forall (m :: * -> *) a. Monad m => a -> m a
return
        forall a b. (a -> b) -> a -> b
$  forall a. ToJSON a => a -> Value
toJSON
        forall a b. (a -> b) -> a -> b
$  Maybe CommandErr -> CommandRes
CmdRes
        forall a b. (a -> b) -> a -> b
$  forall a. a -> Maybe a
Just
        forall a b. (a -> b) -> a -> b
$  String -> CommandErr
CmdErrCannotDecodeJSON
        forall a b. (a -> b) -> a -> b
$  forall a. Show a => a -> String
show String
msg
        forall a. [a] -> [a] -> [a]
++ String
"\n"
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
value
    JSON.Success CommandReq
request -> forall a. ToJSON a => a -> Value
toJSON forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadIO m =>
CommandReq -> ServerM m CommandRes
handleCommandReq CommandReq
request


handleCommandReq :: MonadIO m => CommandReq -> ServerM m CommandRes
handleCommandReq :: forall (m :: * -> *).
MonadIO m =>
CommandReq -> ServerM m CommandRes
handleCommandReq CommandReq
CmdReqSYN    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> CommandRes
CmdResACK String
Agda.getAgdaVersion
handleCommandReq (CmdReq String
cmd) = do
  case String -> Either String IOTCM
parseIOTCM String
cmd of
    Left String
err -> do
      forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog forall a b. (a -> b) -> a -> b
$ Text
"[Error] CmdErrCannotParseCommand:\n" forall a. Semigroup a => a -> a -> a
<> String -> Text
pack String
err
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Maybe CommandErr -> CommandRes
CmdRes (forall a. a -> Maybe a
Just (String -> CommandErr
CmdErrCannotParseCommand String
err))
    Right IOTCM
iotcm -> do
      forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog forall a b. (a -> b) -> a -> b
$ Text
"[Request] " forall a. Semigroup a => a -> a -> a
<> String -> Text
pack (forall a. Show a => a -> String
show String
cmd)
      forall (m :: * -> *). (Monad m, MonadIO m) => IOTCM -> ServerM m ()
provideCommand IOTCM
iotcm
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Maybe CommandErr -> CommandRes
CmdRes forall a. Maybe a
Nothing

parseIOTCM :: String -> Either String IOTCM
parseIOTCM :: String -> Either String IOTCM
parseIOTCM String
raw = case forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ forall a. Read a => ReadS a
reads String
raw of
  Just (IOTCM
x, String
""     ) -> forall a b. b -> Either a b
Right IOTCM
x
  Just (IOTCM
_, String
remnent) -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String
"not consumed: " forall a. [a] -> [a] -> [a]
++ String
remnent
  Maybe (IOTCM, String)
_                 -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String
"cannot read: " forall a. [a] -> [a] -> [a]
++ String
raw

--------------------------------------------------------------------------------

getCommandLineOptions
  :: (HasOptions m, MonadIO m) => ServerM m CommandLineOptions
getCommandLineOptions :: forall (m :: * -> *).
(HasOptions m, MonadIO m) =>
ServerM m CommandLineOptions
getCommandLineOptions = do
  -- command line options from ARGV 
  [String]
argv   <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Options -> [String]
optRawAgdaOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Options
envOptions)
  -- command line options from agda-mode
  [String]
config <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Config -> [String]
configRawAgdaOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Config
envConfig)
  -- concatenate both 
  let merged :: [String]
merged = [String]
argv forall a. Semigroup a => a -> a -> a
<> [String]
config

  Either String CommandLineOptions
result <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ do
    ([Backend]
bs, CommandLineOptions
opts) <- forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) opts.
Monad m =>
OptM opts -> m (Either String opts)
runOptM forall a b. (a -> b) -> a -> b
$ [Backend]
-> [String]
-> CommandLineOptions
-> OptM ([Backend], CommandLineOptions)
parseBackendOptions [Backend]
builtinBackends
                                                          [String]
merged
                                                          CommandLineOptions
defaultOptions
    forall (m :: * -> *) a. Monad m => a -> m a
return CommandLineOptions
opts
  case Either String CommandLineOptions
result of
    -- something bad happened, use the default options instead 
    Left  String
_    -> forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
    Right CommandLineOptions
opts -> forall (m :: * -> *) a. Monad m => a -> m a
return CommandLineOptions
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 :: forall (m :: * -> *) a.
MonadIO m =>
ServerM TCM a -> ServerM m (Either String a)
runAgda ServerM TCM a
p = do
  Env
env <- forall r (m :: * -> *). MonadReader r m => m r
ask
  let p' :: TCM a
p' = forall (m :: * -> *) a. Env -> ServerM m a -> m a
runServerM Env
env ServerM TCM a
p
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
    forall a b. (a -> b) -> a -> b
$       forall (m :: * -> *) a. MonadIO m => TCMT m a -> m a
runTCMTop'
              (                 (forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM a
p')
              forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError`      forall a. TCErr -> TCM (Either String a)
handleTCErr
              forall (m :: * -> *) a.
CatchImpossible m =>
m a -> (Impossible -> m a) -> m a
`catchImpossible` forall a. Impossible -> TCM (Either String a)
handleImpossible
              )
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` forall a. SomeException -> IO (Either String a)
catchException
 where
  handleTCErr :: TCErr -> TCM (Either String a)
  handleTCErr :: forall a. TCErr -> TCM (Either String a)
handleTCErr TCErr
err = do
    [String]
s2s <- [TCWarning] -> TCMT IO [String]
prettyTCWarnings' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr TCErr
err
    String
s1  <- forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
prettyError TCErr
err
    let ss :: [String]
ss       = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) forall a b. (a -> b) -> a -> b
$ [String]
s2s forall a. [a] -> [a] -> [a]
++ [String
s1]
    let errorMsg :: String
errorMsg = [String] -> String
unlines [String]
ss
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left String
errorMsg)

  handleImpossible :: Impossible -> TCM (Either String a)
  handleImpossible :: forall a. Impossible -> TCM (Either String a)
handleImpossible = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show

  catchException :: SomeException -> IO (Either String a)
  catchException :: forall a. SomeException -> IO (Either String a)
catchException SomeException
e = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show SomeException
e

--------------------------------------------------------------------------------

data CommandReq
  = CmdReqSYN -- ^ For client to initiate a 2-way handshake
  | CmdReq String
  deriving (forall x. Rep CommandReq x -> CommandReq
forall x. CommandReq -> Rep CommandReq x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CommandReq x -> CommandReq
$cfrom :: forall x. CommandReq -> Rep CommandReq x
Generic)

instance FromJSON CommandReq

data CommandRes
  = CmdResACK -- ^ For server to complete a 2-way handshake
      String   -- ^ Version number of Agda
  | CmdRes -- ^ Response for 'CmdReq'
      (Maybe CommandErr) -- ^ 'Nothing' to indicate success
  deriving (forall x. Rep CommandRes x -> CommandRes
forall x. CommandRes -> Rep CommandRes x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CommandRes x -> CommandRes
$cfrom :: forall x. CommandRes -> Rep CommandRes x
Generic)

instance ToJSON CommandRes

data CommandErr
  = CmdErrCannotDecodeJSON String
  | CmdErrCannotParseCommand String
  deriving (forall x. Rep CommandErr x -> CommandErr
forall x. CommandErr -> Rep CommandErr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CommandErr x -> CommandErr
$cfrom :: forall x. CommandErr -> Rep CommandErr x
Generic)

instance ToJSON CommandErr