Skip to content

Update dependency on lsp-types and lsp libraries #261

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
dorchard merged 1 commit into from
Oct 21, 2025
Merged

Update dependency on lsp-types and lsp libraries #261

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
78 changes: 44 additions & 34 deletions server/app/Language/Granule/Server.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE TypeOperators #-}

module Language.Granule.Server where

Expand All @@ -29,9 +30,10 @@ import qualified Data.Text.IO as T

import Language.LSP.Diagnostics
import Language.LSP.Server
import Language.LSP.Types
import Language.LSP.Protocol.Types
import Language.LSP.Protocol.Message
import Language.LSP.VFS
import qualified Language.LSP.Types.Lens as L
import qualified Language.LSP.Protocol.Lens as L

import Language.Granule.Checker.Monad
import Language.Granule.Syntax.Def
Expand All @@ -43,6 +45,8 @@ import qualified Language.Granule.Checker.Checker as Checker
import qualified Language.Granule.Interpreter as Interpreter
import qualified Language.Granule.Syntax.Parser as Parser

type TextDocumentVersion = Int32 |? Null

data LsState = LsState { currentDefns :: M.Map String (Def () ()),
currentADTs :: M.Map String DataDecl }

Expand Down Expand Up @@ -171,19 +175,21 @@ parserDiagnostic doc version message = do
let diags =
[ Diagnostic
(getParseErrorRange message)
(Just DsError)
(Just DiagnosticSeverity_Error)
Nothing
Nothing
(Just "grls")
(T.pack $ message ++ "\n")
Nothing
(Just (List []))
Nothing
Nothing
]
publishDiagnostics 1 doc version (partitionBySource diags)
publishDiagnostics 1 doc (nullToMaybe version) (partitionBySource diags)

checkerDiagnostics :: (?globals :: Globals) => NormalizedUri -> TextDocumentVersion -> NonEmpty CheckerError -> LspS ()
checkerDiagnostics doc version l = do
let diags = toList $ checkerErrorToDiagnostic doc version <$> l
publishDiagnostics (Prelude.length diags) doc version (partitionBySource diags)
publishDiagnostics (Prelude.length diags) doc (nullToMaybe version) (partitionBySource diags)

checkerErrorToDiagnostic :: (?globals :: Globals) => NormalizedUri -> TextDocumentVersion -> CheckerError -> Diagnostic
checkerErrorToDiagnostic doc version e =
Expand All @@ -193,25 +199,27 @@ checkerErrorToDiagnostic doc version e =
message = title e ++ ":\n" ++ msg e
in Diagnostic
(Range (Position (startLine-1) (startCol-1)) (Position (endLine-1) endCol))
(Just DsError)
(Just DiagnosticSeverity_Error)
Nothing
Nothing
(Just "grls")
(T.pack $ message ++ "\n")
Nothing
(Just (List []))
Nothing
Nothing

objectToSymbol :: (?globals :: Globals) => (a -> Span) -> (a -> Id) -> a -> SymbolInformation
objectToSymbol objSpan objId obj = let loc = objSpan obj in SymbolInformation
(T.pack $ pretty $ objId obj)
(SkUnknown 0)
SymbolKind_Variable
(Nothing)
(Nothing)
(Nothing)
(Location
(filePathToUri $ filename loc)
(Range
(let (x, y) = startPos loc in Position (fromIntegral x-1) (fromIntegral y-1))
(let (x, y) = endPos loc in Position (fromIntegral x-1) (fromIntegral y-1))))
(Nothing)

posInSpan :: Position -> Span -> Bool
posInSpan (Position l c) s = let
Expand Down Expand Up @@ -241,28 +249,28 @@ getWordFromString (x:xs) n acc = if x == ' ' then getWordFromString xs (n-1) []

handlers :: (?globals :: Globals) => Handlers LspS
handlers = mconcat
[ notificationHandler SInitialized $ \msg -> do
[ notificationHandler SMethod_Initialized $ \msg -> do
return ()
, notificationHandler STextDocumentDidClose $ \msg -> do
, notificationHandler SMethod_TextDocumentDidClose $ \msg -> do
return ()
, notificationHandler SCancelRequest $ \msg -> do
, notificationHandler SMethod_CancelRequest $ \msg -> do
return ()
, notificationHandler STextDocumentDidSave $ \msg -> do
, notificationHandler SMethod_TextDocumentDidSave $ \msg -> do
let doc = msg ^. L.params . L.textDocument . L.uri
content = fromMaybe "?" $ msg ^. L.params . L.text
validateGranuleCode (toNormalizedUri doc) Nothing content
, notificationHandler STextDocumentDidOpen $ \msg -> do
validateGranuleCode (toNormalizedUri doc) (maybeToNull Nothing) content
, notificationHandler SMethod_TextDocumentDidOpen $ \msg -> do
let doc = msg ^. L.params . L.textDocument . L.uri
content = msg ^. L.params . L.textDocument . L.text
validateGranuleCode (toNormalizedUri doc) Nothing content
, notificationHandler STextDocumentDidChange $ \msg -> do
validateGranuleCode (toNormalizedUri doc) (maybeToNull Nothing) content
, notificationHandler SMethod_TextDocumentDidChange $ \msg -> do
let doc = msg ^. L.params . L.textDocument . L.uri . to toNormalizedUri
mdoc <- getVirtualFile doc
case mdoc of
Just vf@(VirtualFile _ version _rope) -> do
validateGranuleCode doc (Just (fromIntegral version)) (virtualFileText vf)
validateGranuleCode doc (maybeToNull (Just (fromIntegral version))) (virtualFileText vf)
_ -> debugS $ "No virtual file found for: " <> (T.pack (show msg))
, requestHandler SWorkspaceSymbol $ \req responder -> do
, requestHandler SMethod_WorkspaceSymbol $ \req responder -> do
let query = T.unpack $ req ^. L.params . L.query
defns <- getDefns
let possibleDefn = M.lookup query defns
Expand All @@ -276,11 +284,11 @@ handlers = mconcat
constrIds = M.fromList $ map (\x -> (pretty $ dataConstrId x, x)) constrs
possibleConstr = M.lookup query constrIds
case possibleConstr of
Nothing -> responder $ Right $ List []
Just c -> responder $ Right $ List [objectToSymbol dataConstrSpan dataConstrId c]
Just d -> responder $ Right $ List [objectToSymbol dataDeclSpan dataDeclId d]
Just d -> responder $ Right $ List [objectToSymbol defSpan defId d]
, requestHandler STextDocumentDefinition $ \req responder -> do
Nothing -> responder $ Right $ InR $ InR Null
Just c -> responder $ Right $ InL [objectToSymbol dataConstrSpan dataConstrId c]
Just d -> responder $ Right $ InL [objectToSymbol dataDeclSpan dataDeclId d]
Just d -> responder $ Right $ InL [objectToSymbol defSpan defId d]
, requestHandler SMethod_TextDocumentDefinition $ \req responder -> do
let params = req ^. L.params
pos = params ^. L.position
doc = params ^. L.textDocument . L.uri . to toNormalizedUri
Expand All @@ -289,7 +297,7 @@ handlers = mconcat
Just vf@(VirtualFile _ version _rope) -> do
let t = virtualFileText vf
query = getWordAtPosition t pos
validateGranuleCode doc (Just (fromIntegral version)) t
validateGranuleCode doc (maybeToNull (Just (fromIntegral version))) t
case query of
Nothing -> debugS $ "This should be impossible!"
Just q -> do
Expand All @@ -305,10 +313,10 @@ handlers = mconcat
constrIds = M.fromList $ map (\x -> (pretty $ dataConstrId x, x)) constrs
possibleConstr = M.lookup q constrIds
case possibleConstr of
Nothing -> responder $ Right $ InR $ InL $ List []
Just c -> responder $ Right $ InR $ InL $ List [spanToLocation $ dataConstrSpan c]
Just d -> responder $ Right $ InR $ InL $ List [spanToLocation $ dataDeclSpan d]
Just d -> responder $ Right $ InR $ InL $ List [spanToLocation $ defSpan d]
Nothing -> responder $ Right $ InR $ InR Null
Just c -> responder $ Right $ InL $ Definition $ InL $ spanToLocation $ dataConstrSpan c
Just d -> responder $ Right $ InL $ Definition $ InL $ spanToLocation $ dataDeclSpan d
Just d -> responder $ Right $ InL $ Definition $ InL $ spanToLocation $ defSpan d
_ -> debugS $ "No virtual file found for: " <> (T.pack (show doc))
]

Expand All @@ -317,15 +325,17 @@ main = do
globals <- Interpreter.getGrConfig >>= (return . Interpreter.grGlobals . snd)
state <- newLsStateVar
runServer $ ServerDefinition
{ onConfigurationChange = const $ const $ Right ()
{ onConfigChange = \_ -> pure ()
, defaultConfig = ()
, doInitialize = const . pure . Right
, staticHandlers = (let ?globals = globals in handlers)
, parseConfig = \_ _ -> Left "Not supported"
, configSection = T.pack "granule"
, staticHandlers = let ?globals = globals in (\_ -> handlers)
, interpretHandler = \env -> Iso (\lsps -> runLspS lsps state env) liftIO
, options =
defaultOptions
{
textDocumentSync =
optTextDocumentSync =
Just
( TextDocumentSyncOptions
(Just True)
Expand All @@ -337,4 +347,4 @@ main = do
}
}
where
syncKind = TdSyncFull
syncKind = TextDocumentSyncKind_Full
4 changes: 4 additions & 0 deletions stack.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,10 @@ packages:
extra-deps:
- text-replace-0.1.0.3
- syz-0.2.0.0
- lsp-types-2.3.0.1
- lsp-2.7.0.1
- mod-0.2.0.1
- row-types-1.0.1.2
- git: https://github.com/jackohughes/haskell-src-exts
commit: 5c2647fa0746bdac046897f5a6b7e4f5ef3afa79

Expand Down
Loading