{-# LANGUAGE DeriveGeneric #-}

-- entry point of the LSP server

module Server
  ( run
  ) where

import qualified Agda
import           Control.Concurrent             ( writeChan )
import           Control.Monad.Reader           ( MonadIO(liftIO)
                                                , void
                                                )
import           Data.Aeson                     ( FromJSON
                                                , ToJSON
                                                )
import qualified Data.Aeson                    as JSON
import           Data.Text                      ( pack )
import           GHC.IO.IOMode                  ( IOMode(ReadWriteMode) )
import           Language.LSP.Server     hiding ( Options )
import           Language.LSP.Types      hiding ( Options(..)
                                                , TextDocumentSyncClientCapabilities(..)
                                                )
import           Monad
import qualified Network.Simple.TCP            as TCP
import           Network.Socket                 ( socketToHandle )
import qualified Switchboard
import           Switchboard                    ( Switchboard )

import qualified Server.Handler                as Handler

import qualified Language.LSP.Server           as LSP
import           Options


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

run :: Options -> IO Int
run :: Options -> IO Int
run Options
options = do
  case Options -> Maybe Int
optViaTCP Options
options of
    Just Int
port -> do
      forall (f :: * -> *) a. Functor f => f a -> f ()
void
        forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadIO m =>
HostPreference -> String -> ((Socket, SockAddr) -> IO ()) -> m a
TCP.serve (String -> HostPreference
TCP.Host String
"127.0.0.1") (forall a. Show a => a -> String
show Int
port)
        forall a b. (a -> b) -> a -> b
$ \(Socket
sock, SockAddr
_remoteAddr) -> do
            -- writeChan (envLogChan env) "[Server] connection established"
            Handle
handle <- Socket -> IOMode -> IO Handle
socketToHandle Socket
sock IOMode
ReadWriteMode
            Int
_      <- forall config.
Handle -> Handle -> ServerDefinition config -> IO Int
runServerWithHandles Handle
handle Handle
handle (Options -> ServerDefinition Config
serverDefn Options
options)
            forall (m :: * -> *) a. Monad m => a -> m a
return ()
      -- Switchboard.destroy switchboard
      forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
    Maybe Int
Nothing -> do
      forall config. ServerDefinition config -> IO Int
runServer (Options -> ServerDefinition Config
serverDefn Options
options)
 where
  serverDefn :: Options -> ServerDefinition Config
  serverDefn :: Options -> ServerDefinition Config
serverDefn Options
options = ServerDefinition
    { defaultConfig :: Config
defaultConfig         = Config
initConfig
    , onConfigurationChange :: Config -> Value -> Either Text Config
onConfigurationChange = \Config
old Value
newRaw -> case forall a. FromJSON a => Value -> Result a
JSON.fromJSON Value
newRaw of
      JSON.Error String
s -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String -> Text
pack forall a b. (a -> b) -> a -> b
$ String
"Cannot parse server configuration: " forall a. Semigroup a => a -> a -> a
<> String
s
      JSON.Success Config
new -> forall a b. b -> Either a b
Right Config
new
    , doInitialize :: LanguageContextEnv Config
-> Message 'Initialize
-> IO (Either ResponseError (LanguageContextEnv Config, Env))
doInitialize          = \LanguageContextEnv Config
ctxEnv Message 'Initialize
_req -> do
                                Env
env <- forall config (m :: * -> *) a.
LanguageContextEnv config -> LspT config m a -> m a
runLspT LanguageContextEnv Config
ctxEnv (forall (m :: * -> *).
(MonadIO m, MonadLsp Config m) =>
Options -> m Env
createInitEnv Options
options)
                                Switchboard
switchboard <- Env -> IO Switchboard
Switchboard.new Env
env
                                Switchboard -> LanguageContextEnv Config -> IO ()
Switchboard.setupLanguageContextEnv Switchboard
switchboard LanguageContextEnv Config
ctxEnv
                                forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (LanguageContextEnv Config
ctxEnv, Env
env)
    , staticHandlers :: Handlers (ServerM (LspM Config))
staticHandlers        = Handlers (ServerM (LspM Config))
handlers
    , interpretHandler :: (LanguageContextEnv Config, Env) -> ServerM (LspM Config) <~> IO
interpretHandler      = \(LanguageContextEnv Config
ctxEnv, Env
env) ->
                                forall {k} (m :: k -> *) (n :: k -> *).
(forall (a :: k). m a -> n a)
-> (forall (a :: k). n a -> m a) -> m <~> n
Iso (forall config (m :: * -> *) a.
LanguageContextEnv config -> LspT config m a -> m a
runLspT LanguageContextEnv Config
ctxEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Env -> ServerM m a -> m a
runServerM Env
env) forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
    , options :: Options
options               = Options
lspOptions
    }

  lspOptions :: LSP.Options
  lspOptions :: Options
lspOptions = Options
defaultOptions { textDocumentSync :: Maybe TextDocumentSyncOptions
textDocumentSync = forall a. a -> Maybe a
Just TextDocumentSyncOptions
syncOptions }

  -- these `TextDocumentSyncOptions` are essential for receiving notifications from the client
  syncOptions :: TextDocumentSyncOptions
  syncOptions :: TextDocumentSyncOptions
syncOptions = TextDocumentSyncOptions { $sel:_openClose:TextDocumentSyncOptions :: Maybe Bool
_openClose = forall a. a -> Maybe a
Just Bool
True -- receive open and close notifications from the client
                                        , $sel:_change:TextDocumentSyncOptions :: Maybe TextDocumentSyncKind
_change = forall a. a -> Maybe a
Just TextDocumentSyncKind
changeOptions -- receive change notifications from the client
                                        , $sel:_willSave:TextDocumentSyncOptions :: Maybe Bool
_willSave = forall a. a -> Maybe a
Just Bool
False -- receive willSave notifications from the client
                                        , $sel:_willSaveWaitUntil:TextDocumentSyncOptions :: Maybe Bool
_willSaveWaitUntil = forall a. a -> Maybe a
Just Bool
False -- receive willSave notifications from the client
                                        , $sel:_save:TextDocumentSyncOptions :: Maybe (Bool |? SaveOptions)
_save = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. b -> a |? b
InR SaveOptions
saveOptions
                                        }

  changeOptions :: TextDocumentSyncKind
  changeOptions :: TextDocumentSyncKind
changeOptions = TextDocumentSyncKind
TdSyncIncremental

  -- includes the document content on save, so that we don't have to read it from the disk
  saveOptions :: SaveOptions
  saveOptions :: SaveOptions
saveOptions = Maybe Bool -> SaveOptions
SaveOptions (forall a. a -> Maybe a
Just Bool
True)

-- handlers of the LSP server
handlers :: Handlers (ServerM (LspM Config))
handlers :: Handlers (ServerM (LspM Config))
handlers = forall a. Monoid a => [a] -> a
mconcat
  [ -- custom methods, not part of LSP
    forall (m :: Method 'FromClient 'Request) (f :: * -> *).
SMethod m -> Handler f m -> Handlers f
requestHandler (forall {f :: From} {t :: MethodType}. Text -> SMethod 'CustomMethod
SCustomMethod Text
"agda") forall a b. (a -> b) -> a -> b
$ \RequestMessage 'CustomMethod
req Either ResponseError Value -> ReaderT Env (LspM Config) ()
responder -> do
    let RequestMessage Text
_ LspId 'CustomMethod
_i SMethod 'CustomMethod
_ MessageParams 'CustomMethod
params = RequestMessage 'CustomMethod
req
    Value
response <- forall (m :: * -> *). MonadIO m => Value -> ServerM m Value
Agda.sendCommand MessageParams 'CustomMethod
params
    Either ResponseError Value -> ReaderT Env (LspM Config) ()
responder forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Value
response
  ,
        -- hover provider
    forall (m :: Method 'FromClient 'Request) (f :: * -> *).
SMethod m -> Handler f m -> Handlers f
requestHandler SMethod 'TextDocumentHover
STextDocumentHover forall a b. (a -> b) -> a -> b
$ \RequestMessage 'TextDocumentHover
req Either ResponseError (Maybe Hover) -> ReaderT Env (LspM Config) ()
responder -> do
    let
      RequestMessage Text
_ LspId 'TextDocumentHover
_ SMethod 'TextDocumentHover
_ (HoverParams (TextDocumentIdentifier Uri
uri) Position
pos Maybe ProgressToken
_workDone)
        = RequestMessage 'TextDocumentHover
req
    Maybe Hover
result <- Uri -> Position -> ServerM (LspM Config) (Maybe Hover)
Handler.onHover Uri
uri Position
pos
    Either ResponseError (Maybe Hover) -> ReaderT Env (LspM Config) ()
responder forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Maybe Hover
result
  -- -- syntax highlighting 
  -- , requestHandler STextDocumentSemanticTokensFull $ \req responder -> do
  --   result <- Handler.onHighlight (req ^. (params . textDocument . uri))
  --   responder result
  ]