{-# 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 = versionWithCommitInfo

start :: ServerM IO ()
start = do
  env <- ask

  writeLog "[Agda] interaction start"

  result <- runAgda $ do
    -- decides how to output Response
    lift $ setInteractionOutputCallback $ \response -> do
      reaction <- fromResponse response
      sendResponse env reaction

    -- 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
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

parseIOTCM :: String -> Either String IOTCM
parseIOTCM raw = case listToMaybe $ reads raw of
  Just (x, ""     ) -> Right x
  Just (_, remnent) -> Left $ "not consumed: " ++ remnent
  _                 -> Left $ "cannot read: " ++ raw

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

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
    (bs, opts) <- ExceptT $ runOptM $ parseBackendOptions builtinBackends
                                                          merged
                                                          defaultOptions
    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 = unlines 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 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 (Generic)

instance ToJSON CommandRes

data CommandErr
  = CmdErrCannotDecodeJSON String
  | CmdErrCannotParseCommand String
  deriving (Generic)

instance ToJSON CommandErr