{-# 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
      IO Any -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void
        (IO Any -> IO ()) -> IO Any -> IO ()
forall a b. (a -> b) -> a -> b
$ HostPreference
-> ServiceName -> ((Socket, SockAddr) -> IO ()) -> IO Any
forall (m :: * -> *) a.
MonadIO m =>
HostPreference
-> ServiceName -> ((Socket, SockAddr) -> IO ()) -> m a
TCP.serve (ServiceName -> HostPreference
TCP.Host ServiceName
"127.0.0.1") (Int -> ServiceName
forall a. Show a => a -> ServiceName
show Int
port)
        (((Socket, SockAddr) -> IO ()) -> IO Any)
-> ((Socket, SockAddr) -> IO ()) -> IO Any
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
_      <- Handle -> Handle -> ServerDefinition Config -> IO Int
forall config.
Handle -> Handle -> ServerDefinition config -> IO Int
runServerWithHandles Handle
handle Handle
handle (Options -> ServerDefinition Config
serverDefn Options
options)
            () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      -- Switchboard.destroy switchboard
      Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
    Maybe Int
Nothing -> do
      ServerDefinition Config -> IO Int
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 :: forall config (m :: * -> *) a.
config
-> (config -> Value -> Either Text config)
-> (LanguageContextEnv config
    -> Message 'Initialize -> IO (Either ResponseError a))
-> Handlers m
-> (a -> m <~> IO)
-> Options
-> ServerDefinition config
ServerDefinition
    { defaultConfig :: Config
defaultConfig         = Config
initConfig
    , onConfigurationChange :: Config -> Value -> Either Text Config
onConfigurationChange = \Config
old Value
newRaw -> case Value -> Result Config
forall a. FromJSON a => Value -> Result a
JSON.fromJSON Value
newRaw of
      JSON.Error ServiceName
s -> Text -> Either Text Config
forall a b. a -> Either a b
Left (Text -> Either Text Config) -> Text -> Either Text Config
forall a b. (a -> b) -> a -> b
$ ServiceName -> Text
pack (ServiceName -> Text) -> ServiceName -> Text
forall a b. (a -> b) -> a -> b
$ ServiceName
"Cannot parse server configuration: " ServiceName -> ServiceName -> ServiceName
forall a. Semigroup a => a -> a -> a
<> ServiceName
s
      JSON.Success Config
new -> Config -> Either Text Config
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 <- LanguageContextEnv Config -> LspT Config IO Env -> IO Env
forall config (m :: * -> *) a.
LanguageContextEnv config -> LspT config m a -> m a
runLspT LanguageContextEnv Config
ctxEnv (Options -> LspT Config IO Env
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
                                Either ResponseError (LanguageContextEnv Config, Env)
-> IO (Either ResponseError (LanguageContextEnv Config, Env))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ResponseError (LanguageContextEnv Config, Env)
 -> IO (Either ResponseError (LanguageContextEnv Config, Env)))
-> Either ResponseError (LanguageContextEnv Config, Env)
-> IO (Either ResponseError (LanguageContextEnv Config, Env))
forall a b. (a -> b) -> a -> b
$ (LanguageContextEnv Config, Env)
-> Either ResponseError (LanguageContextEnv Config, Env)
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 a. ServerM (LspM Config) a -> IO a)
-> (forall a. IO a -> ServerM (LspM Config) a)
-> ServerM (LspM Config) <~> IO
forall k (m :: k -> *) (n :: k -> *).
(forall (a :: k). m a -> n a)
-> (forall (a :: k). n a -> m a) -> m <~> n
Iso (LanguageContextEnv Config -> LspT Config IO a -> IO a
forall config (m :: * -> *) a.
LanguageContextEnv config -> LspT config m a -> m a
runLspT LanguageContextEnv Config
ctxEnv (LspT Config IO a -> IO a)
-> (ServerM (LspM Config) a -> LspT Config IO a)
-> ServerM (LspM Config) a
-> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ServerM (LspM Config) a -> LspT Config IO a
forall (m :: * -> *) a. Env -> ServerM m a -> m a
runServerM Env
env) forall a. IO a -> ServerM (LspM Config) a
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 = TextDocumentSyncOptions -> Maybe TextDocumentSyncOptions
forall a. a -> Maybe a
Just TextDocumentSyncOptions
syncOptions }

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

-- handlers of the LSP server
handlers :: Handlers (ServerM (LspM Config))
handlers :: Handlers (ServerM (LspM Config))
handlers = [Handlers (ServerM (LspM Config))]
-> Handlers (ServerM (LspM Config))
forall a. Monoid a => [a] -> a
mconcat
  [ -- custom methods, not part of LSP
    SMethod 'CustomMethod
-> Handler (ServerM (LspM Config)) 'CustomMethod
-> Handlers (ServerM (LspM Config))
forall (m :: Method 'FromClient 'Request) (f :: * -> *).
SMethod m -> Handler f m -> Handlers f
requestHandler (Text -> SMethod 'CustomMethod
forall (f :: From) (t :: MethodType). Text -> SMethod 'CustomMethod
SCustomMethod Text
"agda") (Handler (ServerM (LspM Config)) 'CustomMethod
 -> Handlers (ServerM (LspM Config)))
-> Handler (ServerM (LspM Config)) 'CustomMethod
-> Handlers (ServerM (LspM Config))
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 <- Value -> ServerM (LspM Config) Value
forall (m :: * -> *). MonadIO m => Value -> ServerM m Value
Agda.sendCommand Value
MessageParams 'CustomMethod
params
    Either ResponseError Value -> ReaderT Env (LspM Config) ()
responder (Either ResponseError Value -> ReaderT Env (LspM Config) ())
-> Either ResponseError Value -> ReaderT Env (LspM Config) ()
forall a b. (a -> b) -> a -> b
$ Value -> Either ResponseError Value
forall a b. b -> Either a b
Right Value
response
  ,
        -- hover provider
    SMethod 'TextDocumentHover
-> Handler (ServerM (LspM Config)) 'TextDocumentHover
-> Handlers (ServerM (LspM Config))
forall (m :: Method 'FromClient 'Request) (f :: * -> *).
SMethod m -> Handler f m -> Handlers f
requestHandler SMethod 'TextDocumentHover
STextDocumentHover (Handler (ServerM (LspM Config)) 'TextDocumentHover
 -> Handlers (ServerM (LspM Config)))
-> Handler (ServerM (LspM Config)) 'TextDocumentHover
-> Handlers (ServerM (LspM Config))
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) pos _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 (Either ResponseError (Maybe Hover)
 -> ReaderT Env (LspM Config) ())
-> Either ResponseError (Maybe Hover)
-> ReaderT Env (LspM Config) ()
forall a b. (a -> b) -> a -> b
$ Maybe Hover -> Either ResponseError (Maybe Hover)
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
  ]