diff --git a/gcl.cabal b/gcl.cabal index 350b1548..1c04bba7 100644 --- a/gcl.cabal +++ b/gcl.cabal @@ -61,10 +61,10 @@ library Server.Handler.AutoCompletion Server.Handler.CustomMethod Server.Handler.CustomMethod2 - Server.Handler.CustomMethod3 Server.Handler.Diagnostic Server.Handler.GoToDefn Server.Handler.Hover + Server.Handlers2 Server.Highlighting Server.Hover Server.IntervalMap @@ -214,10 +214,10 @@ test-suite gcl-test Server.Handler.AutoCompletion Server.Handler.CustomMethod Server.Handler.CustomMethod2 - Server.Handler.CustomMethod3 Server.Handler.Diagnostic Server.Handler.GoToDefn Server.Handler.Hover + Server.Handlers2 Server.Highlighting Server.Hover Server.IntervalMap diff --git a/src/Server/Handler/CustomMethod.hs b/src/Server/Handler/CustomMethod.hs index a787b6fa..291c6fc0 100644 --- a/src/Server/Handler/CustomMethod.hs +++ b/src/Server/Handler/CustomMethod.hs @@ -43,9 +43,10 @@ handleRefine range = do mute True setLastSelection range source <- getSource + -- find the spec and its content in the source (spec, payloadLines) <- refine source range - -- remove the Spec + -- add indentation to the content let indentedPayload = case payloadLines of [] -> "" [x] -> x @@ -53,9 +54,12 @@ handleRefine range = do let indentation = Text.replicate (posCol (rangeStart (specRange spec)) - 1) " " in Text.unlines $ x : map (indentation <>) xs + + -- remove the brackets of the spec and leave only the content source' <- editText (specRange spec) indentedPayload - parsed <- parse source' + -- reload + parsed <- parse source' converted <- convert parsed typeChecked <- typeCheck converted mute False diff --git a/src/Server/Handler/CustomMethod2.hs b/src/Server/Handler/CustomMethod2.hs index caf875dd..80ecf0ca 100644 --- a/src/Server/Handler/CustomMethod2.hs +++ b/src/Server/Handler/CustomMethod2.hs @@ -25,7 +25,6 @@ import qualified Syntax.Parser as Parser import qualified Syntax.Abstract as A import qualified Data.Text as Text import Error (Error(..)) -import Syntax.Concrete (ToAbstract(..)) import Control.Monad.Except (runExcept) import Pretty (toText) import Data.Loc (posCol) @@ -51,7 +50,7 @@ handler params responder = do handleRequest _request@(Req filePath reqKind) = do case reqKind of ReqReload -> handleReload filePath respondResult respondError - ReqHelloWorld range -> replaceWithHelloworld' range respondError + ReqHelloWorld range -> handleHelloWorld range respondResult respondError _ -> return $ error "Not yet implemented" where respondError :: Error -> ServerM () @@ -72,6 +71,9 @@ getSource filepath = fmap LSP.virtualFileText logText :: Text -> ServerM () logText = Server.Monad.logText +bumpVersion :: ServerM Int +bumpVersion = Server.Monad.bumpVersion + sendDiagnostics :: FilePath -> [LSP.Diagnostic] -> ServerM () sendDiagnostics = Server.Monad.sendDiagnosticsLSP @@ -103,10 +105,28 @@ editText range textToReplace onSuccess = do _newText = textToReplace } --- ServerM program - example 1 -- +-- Hello World -- -replaceWithHelloworld :: FilePath -> Range -> (Error -> ServerM ()) -> ServerM () -replaceWithHelloworld filepath range onError = do +handleHelloWorld :: Range -> ServerM () -> (Error -> ServerM ()) -> ServerM () +handleHelloWorld range onFinish onError = do + let filepath :: FilePath = rangeFile range + replaceWithHelloworld filepath range (do + let helloWorldRange = rangeAfterReplacedWithHelloWorld range + diagnosticOnHelloWorld = makeDiagnostic Nothing helloWorldRange "Hello, World?" "This is a warning" + sendDiagnostics [diagnosticOnHelloWorld] + version <- bumpVersion + onFinish [ + ResDisplay version [ + Section Blue [ + Header "Hello, world" Nothing + , Paragraph $ fromString "LSP server successfully responded." + ] + ] + ] + ) onError + +replaceWithHelloworld :: FilePath -> Range -> ServerM () -> (Error -> ServerM ()) -> ServerM () +replaceWithHelloworld filepath range onFinish onError = do maybeSource <- getSource filepath case maybeSource of Nothing -> onError (CannotReadFile filepath) @@ -114,7 +134,7 @@ replaceWithHelloworld filepath range onError = do logText "before replacement" logText source logText "\n" - editText range "Hello, World!" $ do + editText range "Hello, World!\n" $ do maybeSource' <- getSource filepath case maybeSource' of Nothing -> onError (CannotReadFile filepath) @@ -122,34 +142,52 @@ replaceWithHelloworld filepath range onError = do logText "after replacement" logText source' logText "\n" + onFinish -replaceWithHelloworld' :: Range -> (Error -> ServerM ()) -> ServerM () -replaceWithHelloworld' range onError = do - let filepath :: FilePath = rangeFile range - replaceWithHelloworld filepath range onError +rangeAfterReplacedWithHelloWorld :: Range -> Range +rangeAfterReplacedWithHelloWorld = + Range (rangeStart range) (addToCoff 13 $ rangeEnd range) + where + addToCoff :: Int -> Pos -> Pos + addToCoff offset pos = Pos (posFile pos) (posLine pos) (posCol pos) (posCoff pos + offset) -- Reload -- handleReload :: FilePath -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () handleReload filepath onFinsih onError = do + -- load source maybeSource <- getSource filepath case maybeSource of Nothing -> onError (CannotReadFile filepath) Just source -> + -- parse source into concrete syntax case parse filepath source of Left err -> onError err - Right concrete -> convert filepath concrete (\abstract -> do + Right concrete -> + -- dig holes and convert to abstract syntax + toAbstract filepath concrete (\abstract -> do -- type check case typeCheck abstract of Left err -> onError err Right scopeTree -> + -- calculate proof obligations, specs and other hints case WP.sweep abstract of Left err -> onError (StructError err) - Right (pos, specs, warings, redexes, counter) -> do - -- TODO convert sweep result to data or rendering - -- respond and send diagnostics - return () + Right (pos, specs, warnings, redexes, counter) -> do + -- send warnings as diagnostics + let diagnostics = concatMap collect warnings + sendDiagnostics diagnostics + + -- send all hints as reponses for client to render + let (A.Program _ _ globalProperties _ _) = abstract + version' <- bumpVersion + let response :: [ResKind] = + hintsToResponseBody + version' + Nothing + (globalProperties, List.sort pos, sortOn locOf specs, warnings, redexes, counter) + onFinsih response ) onError parse :: FilePath -> Text -> Either Error C.Program @@ -158,9 +196,9 @@ parse filepath source = Left err -> Left (ParseError err) Right program -> Right program -convert :: FilePath -> C.Program -> (A.Program -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () -convert filepath concrete onFinish onError = do - case runExcept $ toAbstract concrete of +toAbstract :: FilePath -> C.Program -> (A.Program -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () +toAbstract filepath concrete onFinish onError = do + case runExcept $ C.toAbstract concrete of Left rangeToDigHole -> do _ <- digHole rangeToDigHole do maybeSource <- getSource filepath @@ -185,96 +223,61 @@ typeCheck abstract = do Left e -> Left (TypeError e) Right (_, scopeTree) -> return scopeTree --- -- | Converts abstract syntax to POs and other stuff --- -- persists the result --- sweep :: TypeCheckResult -> PipelineM SweepResult --- sweep result = do --- let abstract@(A.Program _ _ globalProps _ _) = --- convertedProgram (typeCheckedPreviousStage result) --- swept <- case WP.sweep abstract of --- Left e -> throwError [StructError e] --- Right (pos, specs, warings, redexes, counter) -> return $ SweepResult --- { sweptPreviousStage = result --- , sweptPOs = List.sort pos --- , sweptSpecs = sortOn locOf specs --- , sweptProps = globalProps --- , sweptWarnings = warings --- , sweptRedexes = redexes --- , sweptCounter = counter --- } --- save (Swept swept) -- save the current progress --- return swept - --------------------------------------------------------------------------------- --- | Monad for handling the pipeline --- --- Side effects: --- Reader: FilePath --- State: PipelineState --- Exception: [Error] --- --- Also, PipelineM is also a free monad of Instruction --- which allows us to "compile" a PipelineM program into a series of Instructions --- We can then decide to run these compiled Instructions in the real world --- or simulate them for testing - --- toReponse :: ([PO], [Spec], [StructWarning], IntMap (Int, A.Expr), Int) -> [ResKind] --- toReponse (proofObligations, specs, warnings, redexes, counter) = - --- toDiagnostics :: ([PO], [Spec], [StructWarning], IntMap (Int, A.Expr), Int) -> [LSP.Diagnostic] --- toDiagnostics = - --- generateResponseAndDiagnostics :: SweepResult -> PipelineM [ResKind] --- generateResponseAndDiagnostics result = do --- let (SweepResult _ pos specs globalProps warnings _redexes _) = result - --- -- get Specs around the mouse selection --- lastSelection <- getLastSelection --- let overlappedSpecs = case lastSelection of --- Nothing -> specs --- Just selection -> filter (withinRange selection) specs --- -- get POs around the mouse selection (including their corresponding Proofs) - --- let withinPOrange sel po = case poAnchorLoc po of --- Nothing -> withinRange sel po --- Just anchor -> withinRange sel po || withinRange sel anchor - --- let overlappedPOs = case lastSelection of --- Nothing -> pos --- Just selection -> filter (withinPOrange selection) pos --- -- render stuff --- let warningsSections = --- if null warnings then [] else map renderSection warnings --- let globalPropsSections = if null globalProps --- then [] --- else map --- (\expr -> Section --- Plain --- [Header "Property" (fromLoc (locOf expr)), Code (render expr)] --- ) --- globalProps --- let specsSections = --- if null overlappedSpecs then [] else map renderSection overlappedSpecs --- let poSections = --- if null overlappedPOs then [] else map renderSection overlappedPOs --- let sections = mconcat --- [warningsSections, specsSections, poSections, globalPropsSections] - --- version <- bumpVersion --- let encodeSpec spec = --- ( specID spec --- , toText $ render (specPreCond spec) --- , toText $ render (specPostCond spec) --- , specRange spec --- ) - --- let rangesOfPOs = mapMaybe (fromLoc . locOf) pos --- let responses = --- [ ResDisplay version sections --- , ResUpdateSpecs (map encodeSpec specs) --- , ResMarkPOs rangesOfPOs --- ] --- let diagnostics = concatMap collect warnings --- sendDiagnostics diagnostics - --- return responses +hintsToResponseBody :: Int -> Maybe Range -> ([Expr], [PO], [Spec], [StructWarning], IntMap (Int, A.Expr), Int) -> [ResKind] +hintsToResponseBody version rangeToInspect _hints@(globalProperties, proofObligations, specs, warnings, redexes, counter) = + [ ResMarkPOs rangesOfPOs + , ResUpdateSpecs (map encodeSpec specs) + , ResDisplay version sections + ] + where + rangesOfPOs :: [Range] + rangesOfPOs = mapMaybe (fromLoc . locOf) pos + encodeSpec :: Spec -> (Int, Text, Text, Range) + encodeSpec spec = + ( specID spec + , toText $ render (specPreCond spec) + , toText $ render (specPostCond spec) + , specRange spec + ) + sections :: [Section] + sections = mconcat + [ warningsSections + , specsSections + , poSections + , globalPropertiesSections + ] + where + warningsSections :: [Section] + warningSections = map renderSection warnings + specsSections :: [Section] + specsSections = map renderSection specsWithinCurrentSelection + where + specsWithinCurrentSelection :: [Spec] + specsWithinCurrentSelection = case rangeToInspect of + Nothing -> specs + Just selectedRange -> filter (withinRange selectedRange) specs + poSections :: [Section] + poSections = map renderSection posWithCurrentSelection + where + posWithCurrentSelection :: [PO] + posWithCurrentSelection = case rangeToInspect of + Nothing -> pos + Just selectedRange -> filter (selectedRange `covers`) pos + where + covers :: Range -> PO -> Bool + covers range po = case poAnchorLoc po of + Nothing -> withinRange sel po + Just anchor -> withinRange sel po || withinRange sel anchor + globalPropertiesSections :: [Section] + globalPropertiesSections = map + (\expr -> Section + Plain + [Header "Property" (fromLoc (locOf expr)), Code (render expr)] + ) + globalProperties + +-- Refine -- + +handleRefine :: Range -> Text -> ServerM () +handleRefine specRange filledText = do + _ \ No newline at end of file diff --git a/src/Server/Handler/CustomMethod3.hs b/src/Server/Handler/CustomMethod3.hs deleted file mode 100644 index a9c81189..00000000 --- a/src/Server/Handler/CustomMethod3.hs +++ /dev/null @@ -1,187 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE OverloadedStrings #-} - - -import qualified Data.Aeson as JSON -import Server.CustomMethod -import qualified Language.LSP.Server as LSP -import Control.Monad.Trans.Reader (ReaderT (runReaderT), asks) -import Control.Monad.Trans.Except (ExceptT, runExceptT, runExcept) -import Error (Error (CannotReadFile, ParseError)) -import Data.Loc.Range (Range, rangeFile, rangeStart) -import Data.Text (Text) -import qualified Language.LSP.VFS as LSP -import qualified Language.LSP.Types as LSP -import qualified Server.SrcLoc as SrcLoc -import qualified Syntax.Parser as Parser -import qualified Syntax.Concrete as C -import qualified Syntax.Abstract as A -import qualified Data.Text as Text -import Control.Monad.Trans (lift, liftIO) -import Control.Concurrent.Chan (writeChan, Chan) -import qualified Language.LSP.Diagnostics as LSP -import Data.IORef (IORef, readIORef, writeIORef) -import Control.Monad.Except (throwError) -import Syntax.Concrete (ToAbstract(..)) -import Pretty.Util (toText) -import Data.Loc (posCol) -import Language.LSP.VFS (VirtualFile(VirtualFile)) - -data GlobalEnv = GlobalEnv - { -- Channel for printing log - globalChan :: Chan Text - , - -- Counter for generating fresh numbers - globalCounter :: IORef Int - } - -type ServerM = LSP.LspT () (ReaderT GlobalEnv (ExceptT Error IO)) - -runServerM :: ServerM a -> GlobalEnv -> LSP.LanguageContextEnv () -> IO (Either Error a) -runServerM program env ctxEnv = runExceptT $ runReaderT (LSP.runLspT ctxEnv program) env - -handler :: JSON.Value -> (Response -> ServerM ()) -> ServerM () -handler params responder = do - -- JSON Value => Request => Response - case JSON.fromJSON params of - JSON.Error msg -> do - -- logText - -- $ " --> CustomMethod: CannotDecodeRequest " - -- <> Text.pack (show msg) - -- <> " " - -- <> Text.pack (show params) - responder $ CannotDecodeRequest $ show msg ++ "\n" ++ show params - JSON.Success request -> handleRequest request - where - -- convert Request to Response and Diagnostics - handleRequest :: Request -> ServerM () - handleRequest _request@(Req filePath reqKind) = do - case reqKind of - ReqReload -> handleReload filePath - ReqRefine range -> handleRefine filePath range - ReqHelloWorld range -> replaceWithHelloworld' range - _ -> return $ error "Not yet implemented" - -handleRefine :: FilePath -> Range -> ServerM () -handleRefine filePath range = _ - --- Basic Instructions for our ServerM programs -- - -getSource :: FilePath -> ServerM Text -getSource filepath = do - -- let y = LSP.toNormalizedUri (LSP.filePathToUri filepath) - -- let z :: ServerM (Maybe VirtualFile) = LSP.getVirtualFile y - -- let x = LSP.getVirtualFile (LSP.toNormalizedUri (LSP.filePathToUri filepath)) - _ - -- result <- fmap LSP.virtualFileText - -- <$> LSP.getVirtualFile (LSP.toNormalizedUri (LSP.filePathToUri filepath)) - -- case result of - -- Nothing -> throwError (CannotReadFile filepath) - -- Just source -> executeOneStep filepath continuation (next source) - -- case maybeVirtualFile of - -- Nothing -> throwError (CannotReadFile filepath) - -- Just virtualFile -> return $ LSP.virtualFileText virtualFile - -logText :: Text -> ServerM () -logText s = do - chan <- lift $ asks globalChan - liftIO $ writeChan chan s - -sendDiagnostics :: FilePath -> [LSP.Diagnostic] -> ServerM () -sendDiagnostics filepath diagnostics = do - version <- bumpVersion - -- LSP.publishDiagnostics 100 - -- (LSP.toNormalizedUri (LSP.filePathToUri filepath)) - -- (Just version) - -- (LSP.partitionBySource diagnostics) - -bumpVersion :: ServerM Int -bumpVersion = do - ref <- lift $ asks globalCounter - n <- liftIO $ readIORef ref - liftIO $ writeIORef ref (succ n) - return n - -editText :: Range -> Text -> ServerM () -> ServerM () -editText range textToReplace onSuccess = do - let requestParams :: LSP.ApplyWorkspaceEditParams - = LSP.ApplyWorkspaceEditParams { - _label = Just "Resolve Spec", - _edit = LSP.WorkspaceEdit { - _changes = Nothing, - _documentChanges = Just (LSP.List [LSP.InL textDocumentEdit]), - _changeAnnotations = Nothing - } - } - _ <- LSP.sendRequest LSP.SWorkspaceApplyEdit requestParams (const onSuccess) - return () - - where - filepath :: FilePath - filepath = rangeFile range - textDocumentEdit :: LSP.TextDocumentEdit - textDocumentEdit = LSP.TextDocumentEdit { - _textDocument = LSP.VersionedTextDocumentIdentifier (LSP.filePathToUri filepath) (Just 0), - _edits = LSP.List [LSP.InL textEdit] - } - textEdit :: LSP.TextEdit - textEdit = LSP.TextEdit { - _range = SrcLoc.toLSPRange range, - _newText = textToReplace - } - --- ServerM program - example 1 -- - -replaceWithHelloworld :: FilePath -> Range -> ServerM () -replaceWithHelloworld filepath range = do - source <- getSource filepath - logText "before replacement" - logText source - logText "\n" - editText range "Hello, World!" $ do - source' <- getSource filepath - logText "after replacement" - logText source' - logText "\n" - -replaceWithHelloworld' :: Range -> ServerM () -replaceWithHelloworld' range = do - let filepath :: FilePath = rangeFile range - replaceWithHelloworld filepath range - - --- Reload -- - -handleReload :: FilePath -> ServerM () -handleReload filepath = do - source <- getSource filepath - concrete <- parse filepath source - convert filepath concrete (\abstract -> do - -- type check - return () - ) - -parse :: FilePath -> Text -> ServerM C.Program -parse filepath source = - case Parser.scanAndParse Parser.program filepath source of - Left err -> throwError (ParseError err) - Right program -> return program - -convert :: FilePath -> C.Program -> (A.Program -> ServerM ()) -> ServerM () -convert filepath concrete onFinish = do - case runExcept $ toAbstract concrete of - Left rangeToDigHole -> do - digHole rangeToDigHole do - sourceAfterHoleDigging <- getSource filepath - concreteAfterHoleDigging <- parse filepath sourceAfterHoleDigging - convert filepath concreteAfterHoleDigging onFinish - Right abstract -> onFinish abstract - where - digHole :: Range -> ServerM () -> ServerM () - digHole range _onFinish = do - logText $ " < DigHole " <> toText range - let indent = Text.replicate (posCol (rangeStart range) - 1) " " - let holeText = "[!\n" <> indent <> "\n" <> indent <> "!]" - editText range holeText _onFinish \ No newline at end of file diff --git a/src/Server/Handler/GoToDefn.hs b/src/Server/Handler/GoToDefn.hs index 87aafe62..1e271e09 100644 --- a/src/Server/Handler/GoToDefn.hs +++ b/src/Server/Handler/GoToDefn.hs @@ -9,16 +9,17 @@ module Server.Handler.GoToDefn import Data.Maybe ( maybeToList ) import Error ( Error ) import Language.LSP.Types hiding ( Range ) +import qualified Language.LSP.Types as LSP import Server.Monad hiding ( logText ) import Server.Pipeline import qualified Server.SrcLoc as SrcLoc import qualified Server.IntervalMap as IntervalMap -ignoreErrors :: ([Error], Maybe [LocationLink]) -> [LocationLink] +ignoreErrors :: ([Error], Maybe [LSP.LocationLink]) -> [LSP.LocationLink] ignoreErrors (_, Nothing) = [] ignoreErrors (_, Just xs) = xs -handler :: Uri -> Position -> ([LocationLink] -> ServerM ()) -> ServerM () +handler :: Uri -> Position -> ([LSP.LocationLink] -> ServerM ()) -> ServerM () handler uri position responder = do case uriToFilePath uri of Nothing -> return () @@ -45,3 +46,21 @@ handler uri position responder = do return $ maybeToList $ case tokenMap of Nothing -> Nothing Just xs -> IntervalMap.lookup pos xs + +handler' :: Uri -> Position -> ([LSP.LocationLink] -> ServerM ()) -> ServerM () +handler' uri position responder = do + case uriToFilePath uri of + Nothing -> return () + Just filePath -> do + logText "<-- Goto Definition" + source <- getSource filePath + + let table = SrcLoc.makeToOffset source + let positions' = SrcLoc.fromLSPPosition table filepath position + + loadedProgram <- dumpProgram filePath + + case IntervalMap.lookup positions' (scopingInfo loadedProgram) of + Nothing -> return () + Just locationLinks -> responder locationLinks + diff --git a/src/Server/Handlers2.hs b/src/Server/Handlers2.hs new file mode 100644 index 00000000..a7a08a3d --- /dev/null +++ b/src/Server/Handlers2.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DisambiguateRecordFields #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PolyKinds #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} +{-# HLINT ignore "Use lambda-case" #-} + +module Server.Handler + ( handlers + ) where + +import Control.Lens ( (^.) ) +import qualified Data.Aeson as JSON +import Language.LSP.Server ( Handlers + , notificationHandler + , requestHandler + ) +import Server.Monad hiding (logText) +import Server.Pipeline + +import Error ( Error ) +import qualified Language.LSP.Types as J +import qualified Language.LSP.Types.Lens as J +import qualified Server.Handler.AutoCompletion as AutoCompletion +import qualified Server.Handler.CustomMethod as CustomMethod +import qualified Server.Handler.CustomMethod2 as CustomMethod' +import qualified Server.Handler.GoToDefn as GoToDefn +import qualified Server.Handler.Hover as Hover + +-- handlers of the LSP server +handlers :: Handlers ServerM +handlers = mconcat + [ notificationHandler J.SInitialized $ \_not -> do + pure () + , + -- autocompletion + requestHandler J.STextDocumentCompletion $ \req responder -> do + let completionContext = req ^. J.params . J.context + let position = req ^. J.params . J.position + AutoCompletion.handler position completionContext >>= responder . Right + , -- custom methods + requestHandler (J.SCustomMethod "guabao2") $ \req responder -> do + let params = req ^. J.params + CustomMethod'.handler params (responder . Right . JSON.toJSON) + , -- Goto Definition + requestHandler J.STextDocumentDefinition $ \req responder -> do + let uri = req ^. (J.params . J.textDocument . J.uri) + let pos = req ^. (J.params . J.position) + GoToDefn.handler uri pos (responder . Right . J.InR . J.InR . J.List) + , -- Hover + requestHandler J.STextDocumentHover $ \req responder -> do + let uri = req ^. (J.params . J.textDocument . J.uri) + let pos = req ^. (J.params . J.position) + Hover.handler uri pos (responder . Right) + , requestHandler J.STextDocumentSemanticTokensFull $ \req responder -> do + let uri = req ^. (J.params . J.textDocument . J.uri) + interpret uri (responder . ignoreErrors) $ do + logText "\n ---> Syntax Highlighting" + let legend = J.SemanticTokensLegend + (J.List J.knownSemanticTokenTypes) + (J.List J.knownSemanticTokenModifiers) + stage <- load + let + highlightings = case stage of + Raw _ -> [] + Parsed result -> parsedHighlighings result + Converted result -> + parsedHighlighings (convertedPreviousStage result) + TypeChecked result -> parsedHighlighings + (convertedPreviousStage (typeCheckedPreviousStage result)) + Swept result -> parsedHighlighings + (convertedPreviousStage + (typeCheckedPreviousStage (sweptPreviousStage result)) + ) + let tokens = J.makeSemanticTokens legend highlightings + case tokens of + Left t -> return $ Left $ J.ResponseError J.InternalError t Nothing + Right tokens' -> return $ Right $ Just tokens' + ] + +ignoreErrors + :: ([Error], Maybe (Either J.ResponseError (Maybe J.SemanticTokens))) + -> Either J.ResponseError (Maybe J.SemanticTokens) +ignoreErrors (_, Nothing) = Left $ J.ResponseError J.InternalError "?" Nothing +ignoreErrors (_, Just xs) = xs diff --git a/src/Server/Monad.hs b/src/Server/Monad.hs index 319d8f02..273dc0db 100644 --- a/src/Server/Monad.hs +++ b/src/Server/Monad.hs @@ -139,6 +139,20 @@ data GlobalEnv = GlobalEnv -- Counter for generating fresh numbers globalCounter :: IORef Int , globalCurrentStage :: IORef (Map FilePath PipelineState) + -- NEW: book keeping abstract syntax and hints + , loadedPrograms :: IORef (Map FilePath LoadedProgram) + } + +data LoadedProgram = LoadedProgram + { highlightingInfos :: [J.SemanticTokenAbsolute] + , abstractProgram :: A.Program + , scopingInfo :: IntervalMap J.LocationLink + , typeCheckingInfo :: IntervalMap (J.Hover, Type) + , pos :: [PO] + , specs :: [Spec] + , warnings :: [StructWarning] + , redexes :: IntMap (Int, A.Expr) + , variableCounter :: Int } -- | Constructs an initial global state @@ -149,6 +163,7 @@ initGlobalEnv = -- <*> newIORef Map.empty <*> newIORef 0 <*> newIORef Map.empty + <*> newIORef Map.empty -------------------------------------------------------------------------------- @@ -196,6 +211,22 @@ getState filepath = do Nothing -> return $ initState filepath Just state -> return state + +-------------------------------------------------------------------------------- + +cacheProgram :: FilePath -> LoadedProgram -> ServerM () +cacheProgram filepath state = do + ref <- lift $ asks loadedPrograms + liftIO $ modifyIORef' ref (Map.insert filepath state) + +dumpProgram :: FilePath -> ServerM LoadedProgram +dumpProgram filepath = do + ref <- lift $ asks loadedPrograms + mapping <- liftIO $ readIORef ref + case Map.lookup filepath mapping of + Nothing -> return $ initState filepath + Just state -> return state + -------------------------------------------------------------------------------- convertErrorsToResponsesAndDiagnostics