From e0cbc2c8f9a2172a1a8425039e8c2005394f533f Mon Sep 17 00:00:00 2001 From: Vince Date: Tue, 20 Feb 2024 16:29:06 +0800 Subject: [PATCH] new handler: inspect and insert proof template --- src/Server/CustomMethod.hs | 10 +- src/Server/Handler2/CustomMethod.hs | 258 ++---------------- .../Handler2/CustomMethod/HelloWorld.hs | 58 ++++ .../CustomMethod/InsertProofTemplate.hs | 48 ++++ src/Server/Handler2/CustomMethod/Inspect.hs | 18 ++ src/Server/Handler2/CustomMethod/Refine.hs | 47 ++++ src/Server/Handler2/CustomMethod/Reload.hs | 119 ++++++++ src/Server/Handler2/CustomMethod/Utils.hs | 72 +++++ .../TextDocumentSemanticTokensFull.hs | 16 +- src/Server/Handler2/Utils.hs | 2 +- 10 files changed, 405 insertions(+), 243 deletions(-) create mode 100644 src/Server/Handler2/CustomMethod/HelloWorld.hs create mode 100644 src/Server/Handler2/CustomMethod/InsertProofTemplate.hs create mode 100644 src/Server/Handler2/CustomMethod/Inspect.hs create mode 100644 src/Server/Handler2/CustomMethod/Refine.hs create mode 100644 src/Server/Handler2/CustomMethod/Reload.hs create mode 100644 src/Server/Handler2/CustomMethod/Utils.hs diff --git a/src/Server/CustomMethod.hs b/src/Server/CustomMethod.hs index 6ce31bf6..152950f9 100644 --- a/src/Server/CustomMethod.hs +++ b/src/Server/CustomMethod.hs @@ -69,7 +69,8 @@ data ReqKind -- new | ReqHelloWorld Range | ReqReload - deriving (Generic) + | ReqRefine2 Range Text + | ReqInsertProofTemplate Range Text instance FromJSON ReqKind @@ -79,8 +80,13 @@ instance Show ReqKind where show (ReqInsertAnchor hash ) = "InsertAnchor " <> show hash show (ReqSubstitute i ) = "Substitute " <> show i show ReqDebug = "Debug" - show (ReqHelloWorld range) = "HelloWorld" <> show (ShortRange range) + show (ReqHelloWorld range) = "HelloWorld " <> show (ShortRange range) show ReqReload = "Reload" + show (ReqRefine2 range text) = "Refine2 " <> show (ShortRange range) + <> " " <> show text + show (ReqInsertProofTemplate range hash) + = "InsertProofTemplate " <> show (ShortRange range) + <> " " <> show hash data Request = Req FilePath ReqKind deriving Generic diff --git a/src/Server/Handler2/CustomMethod.hs b/src/Server/Handler2/CustomMethod.hs index 42ce66ce..3b6407d9 100644 --- a/src/Server/Handler2/CustomMethod.hs +++ b/src/Server/Handler2/CustomMethod.hs @@ -8,47 +8,29 @@ module Server.Handler2.CustomMethod where import qualified Data.Aeson.Types as JSON import Server.CustomMethod (Response (..), Request (..), ReqKind (..), ResKind (..)) -import Server.Monad (ServerM, convertErrorsToResponsesAndDiagnostics, LoadedProgram (..)) - -import Data.Loc.Range (Range (..), rangeFile, rangeStart, rangeEnd, withinRange, fromLoc) -import Data.Text (Text) - -import qualified GCL.WP as WP -import qualified Syntax.Concrete as C -import qualified Syntax.Parser as Parser -import qualified Syntax.Abstract as A -import qualified Data.Text as Text +import Server.Monad (ServerM) +import qualified Server.Monad (convertErrorsToResponsesAndDiagnostics) import Error (Error(..)) -import Control.Monad.Except (runExcept) -import Pretty (toText) -import Data.Loc hiding ( fromLoc ) -import GCL.Type (ScopeTreeZipper) -import qualified GCL.Type as TypeChecking -import qualified Data.List as List -import Syntax.Abstract (Expr) -import GCL.WP.Type (StructWarning) -import GCL.Predicate (PO (..), Spec (..)) -import Data.IntMap (IntMap) -import Render (Section (..), Deco (..), Block (..), Render (..), RenderSection (..)) -import Server.Handler.Diagnostic (makeDiagnostic, Collect (collect)) -import Data.String (fromString) -import Data.List (sortOn) -import Data.Maybe (mapMaybe) + import Server.Handler2.Utils -import Server.Highlighting (collectHighlighting) -import Server.Hover (collectHoverInfo) -import Server.GoToDefn (collectLocationLinks) +import qualified Server.Handler2.CustomMethod.Reload as Reload (handler) +import qualified Server.Handler2.CustomMethod.Inspect as Inspect (handler) +import qualified Server.Handler2.CustomMethod.Refine as Refine (slowHandler) +import qualified Server.Handler2.CustomMethod.InsertProofTemplate + as InsertProofTemplate (slowHandler) +import qualified Server.Handler2.CustomMethod.HelloWorld as HelloWorld (handler) + 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) + logText + $ " --> CustomMethod: CannotDecodeRequest " + <> Text.pack (show msg) + <> " " + <> Text.pack (show params) responder $ CannotDecodeRequest $ show msg ++ "\n" ++ show params JSON.Success request -> handleRequest request where @@ -56,212 +38,18 @@ handler params responder = do handleRequest :: Request -> ServerM () handleRequest _request@(Req filePath reqKind) = do case reqKind of - ReqReload -> handleReload filePath respondResult respondError - ReqHelloWorld range -> handleHelloWorld range respondResult respondError - _ -> return $ error "Not yet implemented" + ReqReload -> Reload.handler filePath respondResult respondError + ReqInspect range -> Inspect.handler range respondResult respondError + ReqRefine' range text -> Refine.slowHandler range text respondResult respondError + ReqInsertProofTemplate range hash -> InsertProofTemplate.slowHandler filePath range hash respondResult respondError + ReqHelloWorld range -> HelloWorld.handler range respondResult respondError + _ -> respondError (Others "Not implemented yet.") where respondError :: Error -> ServerM () respondError err = do - (responsesFromError, diagnosticsFromError) <- Server.Monad.convertErrorsToResponsesAndDiagnostics [err] + (responsesFromError, diagnosticsFromError) + <- Server.Monad.convertErrorsToResponsesAndDiagnostics [err] sendDiagnostics filePath diagnosticsFromError responder (Res filePath responsesFromError) - respondResult :: [ResKind] -> ServerM () respondResult results = responder (Res filePath results) - --- Hello World -- - -handleHelloWorld :: Range -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () -handleHelloWorld range onFinish onError = do - let filepath :: FilePath = rangeFile range - replaceWithHelloworld filepath range (do - let helloWorldRange = rangeAfterReplacedWithHelloWorld range - let diagnosticOnHelloWorld = makeDiagnostic Nothing helloWorldRange "Hello, World?" "This is a warning" - _ <- sendDiagnostics filepath [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) - Just source -> do - logText "before replacement" - logText source - logText "\n" - editText range "Hello, World!\n" $ do - maybeSource' <- getSource filepath - case maybeSource' of - Nothing -> onError (CannotReadFile filepath) - Just source' -> do - logText "after replacement" - logText source' - logText "\n" - onFinish - -rangeAfterReplacedWithHelloWorld :: Range -> Range -rangeAfterReplacedWithHelloWorld range = - 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 -- - -reload :: FilePath -> (LoadedProgram -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () -reload filepath onFinish 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 -> - -- 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, warnings, redexes, counter) -> do - -- cache all results - loadedProgram <- cacheProgram filepath LoadedProgram - { _highlightingInfos = collectHighlighting concrete - , _abstractProgram = abstract - , _scopingInfo = collectLocationLinks abstract - , _typeCheckingInfo = collectHoverInfo abstract scopeTree - , _proofObligations = List.sort pos - , _specifiations = sortOn locOf specs - , _warnings = warnings - , _redexes = redexes - , _variableCounter = counter - } - onFinish loadedProgram - ) onError - -handleReload :: FilePath -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () -handleReload filepath onFinsih onError = do - reload filepath (\loadedProgram -> do - -- send warnings as diagnostics - let warnings = _warnings loadedProgram - let diagnostics = concatMap collect warnings - sendDiagnostics filepath diagnostics - - -- send all hints as reponses for client to render - version' <- bumpVersion - let response = loadedProgramToReponse loadedProgram version' Nothing - onFinsih response - ) onError - -parse :: FilePath -> Text -> Either Error C.Program -parse filepath source = - case Parser.scanAndParse Parser.program filepath source of - Left err -> Left (ParseError err) - Right program -> Right program - -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 - case maybeSource of - Nothing -> onError (CannotReadFile filepath) - Just source' -> case parse filepath source' of - Left err -> onError err - Right concrete' -> toAbstract filepath concrete' onFinish onError - return () - 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 - -typeCheck :: A.Program -> Either Error (ScopeTreeZipper A.Type) -typeCheck abstract = do - case TypeChecking.runTypeCheck abstract of - Left e -> Left (TypeError e) - Right (_, scopeTree) -> return scopeTree - -loadedProgramToReponse :: LoadedProgram -> Int -> Maybe Range -> [ResKind] -loadedProgramToReponse loadedProgram@(LoadedProgram _ abstract@(A.Abstract _ globalProperties _) _ _ proofObligations specs warnings _ _) - version rangeToInspect - = _ - -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) proofObligations - 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] - warningsSections = 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 -> proofObligations - Just selectedRange -> filter (selectedRange `covers`) proofObligations - where - covers :: Range -> PO -> Bool - covers range po = case poAnchorLoc po of - Nothing -> withinRange range po - Just anchor -> withinRange range po || withinRange range 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 - -- TODO: refine - return () \ No newline at end of file diff --git a/src/Server/Handler2/CustomMethod/HelloWorld.hs b/src/Server/Handler2/CustomMethod/HelloWorld.hs new file mode 100644 index 00000000..24dc01e3 --- /dev/null +++ b/src/Server/Handler2/CustomMethod/HelloWorld.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Server.Handler2.CustomMethod.HelloWorld (handler) where + +import Data.String (fromString) +import Data.Loc.Range (Range (..), rangeFile, rangeStart, rangeEnd) + +import Render (Section (..), Deco (..), Block (..)) +import Error (Error(..)) + +import Server.Monad (ServerM) +import Server.Handler2.Utils + + +handler :: Range -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () +handler range onFinish onError = do + let filepath :: FilePath = rangeFile range + replaceWithHelloworld filepath range (do + let helloWorldRange = rangeAfterReplacedWithHelloWorld range + let diagnosticOnHelloWorld = makeDiagnostic Nothing helloWorldRange "Hello, World?" "This is a warning" + _ <- sendDiagnostics filepath [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) + Just source -> do + logText "before replacement" + logText source + logText "\n" + editText range "Hello, World!\n" $ do + maybeSource' <- getSource filepath + case maybeSource' of + Nothing -> onError (CannotReadFile filepath) + Just source' -> do + logText "after replacement" + logText source' + logText "\n" + onFinish + +rangeAfterReplacedWithHelloWorld :: Range -> Range +rangeAfterReplacedWithHelloWorld range = + 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) diff --git a/src/Server/Handler2/CustomMethod/InsertProofTemplate.hs b/src/Server/Handler2/CustomMethod/InsertProofTemplate.hs new file mode 100644 index 00000000..22a2f797 --- /dev/null +++ b/src/Server/Handler2/CustomMethod/InsertProofTemplate.hs @@ -0,0 +1,48 @@ + +module Server.Handler2.CustomMethod.InsertProofTemplate (slowHandler) where + +import Data.Text (Text) +import qualified Data.Text as Text +import qualified Data.List as List + +import Data.Loc.Range (Range (..), rangeFile) +import Render.Predicate (exprOfPred) +import GCL.Predicate (PO(..)) +import Pretty (docToText) + +import Server.Monad (ServerM, LoadedProgram(..)) +import Server.Handler2.Utils +import Server.Handler2.CustomMethod.Utils +import Server.Handler2.CustomMethod.Reload as Reload + +slowHandler :: FilePath -> Range -> Text -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () +slowHandler sourceFilePath rangeToInsertProof proofObligationHash onFinish onError = do + -- reload source + reload sourceFilePath (\loadedProgram -> do + -- find proof obligation by hash + let proofObligations :: [PO] = _proofObligations loadedProgram + case findProofObligationByHash proofObligations proofObligationHash of + Nothing -> onError (Others "Proof obligation not found.") + Just proofObligation -> do + -- insert proof template + let proofTemplate :: Text = makeProofTemplate proofObligation + editText rangeToInsertProof ("\n\n" <> template) do + -- reload, send diagnostics and respond hint updates + Reload.handler filepath onFinsih onError + ) onError + where + findProofObligationByHash :: [PO] -> Text -> Maybe PO + findProofObligationByHash proofObligations hash = + List.find (\po -> poAnchorHash po == hash) proofObligations + makeProofTemplate :: PO -> Text + makeProofTemplate proofObligation = + "{- #" <> poAnchorHash proofObligation <> "\n" + <> preExpr <> "\n" + <> "⇒" <> "\n" + <> postExpr <> "\n" + <> Text.pack (replicate len '=') + <> "\n\n-}\n" + where + preExpr = docToText $ pretty $ exprOfPred $ poPre proofObligation + postExpr = docToText $ pretty $ exprOfPred $ poPost proofObligation + len = max (max (Text.length preExpr) (Text.length postExpr) - 2) 5 diff --git a/src/Server/Handler2/CustomMethod/Inspect.hs b/src/Server/Handler2/CustomMethod/Inspect.hs new file mode 100644 index 00000000..e4aa8795 --- /dev/null +++ b/src/Server/Handler2/CustomMethod/Inspect.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Server.Handler2.CustomMethod.Inspect (handler) where + +import Data.Loc.Range (Range (..), rangeFile) + +import Server.Handler2.Utils (dumpProgram) +import Server.Handler2.CustomMethod.Utils (sendDiagnosticsAndMakeResponseFromLoadedProgram) + +handler :: Range -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () +handler rangeToInspect onFinish onError = do + let filePath :: FilePath = rangeFile range + maybeLoadedProgram <- dumpProgram filePath + case maybeLoadedProgram of + Nothing -> onError (Others "Please reload before inspect.") + Just loadedProgam -> do + response <- sendDiagnosticsAndMakeResponseFromLoadedProgram loadedProgam rangeToInspect + onFinish response + diff --git a/src/Server/Handler2/CustomMethod/Refine.hs b/src/Server/Handler2/CustomMethod/Refine.hs new file mode 100644 index 00000000..79608576 --- /dev/null +++ b/src/Server/Handler2/CustomMethod/Refine.hs @@ -0,0 +1,47 @@ + +module Server.Handler2.CustomMethod.Refine (slowHandler) where + +import Data.Loc.Range (Range (..), rangeFile) + +import Server.Monad (ServerM) +import Server.Handler2.Utils +import Server.Handler2.CustomMethod.Utils +import Server.Handler2.CustomMethod.Reload as Reload + +slowHandler :: Range -> Text -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () +slowHandler specRange filledText onFinish onError = do + -- remove brackets + editText specRange filledText do + -- reload source + Reload.handler filepath onFinsih onError + +-- 檢查 text typecheck 過了的話 +-- 更新 loadedProgram (concrete/ abstract/ pos/ specs ...etc) +-- (會比重新load有效率嗎？laziness? +-- 用新的loadedProgram更新view + +handler :: Range -> Text -> ServerM () +handler specRange filledText = do + let filepath :: FilePath = rangeFile specRange + maybeLoadedProgram <- dumpProgram filepath + case maybeLoadedProgram of + Nothing -> _ + Just loadedProgram -> do + let (refinedProgram, newRangeToFocus) = refine loadedProgram specRange filledText + _ <- cacheProgram filePath refinedProgram + response <- sendDiagnosticsAndMakeResponseFromLoadedProgram loadedProgam newRangeToFocus + onFinish response + +refine :: LoadedProgram -> Range -> Text -> (LoadedProgram, Maybe Range) +refine loadedProgram specRange filledText = + LoadedProgram + { _highlightingInfos = _ + , _abstractProgram = _ + , _scopingInfo = _ + , _typeCheckingInfo = _ + , _proofObligations = _ + , _specifiations = _ + , _warnings = _ + , _redexes = _ + , _variableCounter = _ + } \ No newline at end of file diff --git a/src/Server/Handler2/CustomMethod/Reload.hs b/src/Server/Handler2/CustomMethod/Reload.hs new file mode 100644 index 00000000..6ca045fc --- /dev/null +++ b/src/Server/Handler2/CustomMethod/Reload.hs @@ -0,0 +1,119 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE BlockArguments #-} +module Server.Handler2.CustomMethod.Reload (handler) where + +import qualified Data.Aeson.Types as JSON + + +import Data.Loc.Range (Range (..), rangeStart, withinRange, fromLoc) +import Data.Text (Text) + +import qualified GCL.WP as WP +import qualified Syntax.Concrete as C +import qualified Syntax.Parser as Parser +import qualified Syntax.Abstract as A +import qualified Data.Text as Text +import Error (Error(..)) +import Control.Monad.Except (runExcept) +import Pretty (toText) +import Data.Loc hiding ( fromLoc ) +import GCL.Type (ScopeTreeZipper) +import qualified GCL.Type as TypeChecking +import qualified Data.List as List +import Syntax.Abstract (Expr) +import GCL.WP.Type (StructWarning) +import GCL.Predicate (PO (..), Spec (..)) +import Data.IntMap (IntMap) +import Render (Render (..), RenderSection (..)) +import Data.String (fromString) +import Data.List (sortOn) +import Data.Maybe (mapMaybe) + +import Server.CustomMethod (Response (..), Request (..), ReqKind (..), ResKind (..)) +import Server.Monad (ServerM, LoadedProgram (..)) +import Server.Handler.Diagnostic (makeDiagnostic, Collect (collect)) +import Server.Highlighting (collectHighlighting) +import Server.Hover (collectHoverInfo) +import Server.GoToDefn (collectLocationLinks) + +import Server.Handler2.Utils +import Server.Handler2.CustomMethod.Utils (sendDiagnosticsAndMakeResponseFromLoadedProgram) + + +handler :: FilePath -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () +handler filepath onFinsih onError = do + reload filepath (\loadedProgram -> do + response <- sendDiagnosticsAndMakeResponseFromLoadedProgram loadedProgram Nothing + onFinsih response + ) onError + +reload :: FilePath -> (LoadedProgram -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () +reload filepath onFinish 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 -> + -- 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, warnings, redexes, counter) -> do + -- cache all results + loadedProgram <- cacheProgram filepath LoadedProgram + { _highlightingInfos = collectHighlighting concrete + , _abstractProgram = abstract + , _scopingInfo = collectLocationLinks abstract + , _typeCheckingInfo = collectHoverInfo abstract scopeTree + , _proofObligations = List.sort pos + , _specifiations = sortOn locOf specs + , _warnings = warnings + , _redexes = redexes + , _variableCounter = counter + } + onFinish loadedProgram + ) onError + +parse :: FilePath -> Text -> Either Error C.Program +parse filepath source = + case Parser.scanAndParse Parser.program filepath source of + Left err -> Left (ParseError err) + Right program -> Right program + +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 + case maybeSource of + Nothing -> onError (CannotReadFile filepath) + Just source' -> case parse filepath source' of + Left err -> onError err + Right concrete' -> toAbstract filepath concrete' onFinish onError + return () + 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 + +typeCheck :: A.Program -> Either Error (ScopeTreeZipper A.Type) +typeCheck abstract = do + case TypeChecking.runTypeCheck abstract of + Left e -> Left (TypeError e) + Right (_, scopeTree) -> return scopeTree + diff --git a/src/Server/Handler2/CustomMethod/Utils.hs b/src/Server/Handler2/CustomMethod/Utils.hs new file mode 100644 index 00000000..49fb9b90 --- /dev/null +++ b/src/Server/Handler2/CustomMethod/Utils.hs @@ -0,0 +1,72 @@ + +module Server.Handler2.CustomMethod.Utils where + +sendDiagnosticsAndMakeResponseFromLoadedProgram :: LoadedProgram -> Maybe Range -> ServerM () +sendDiagnosticsAndMakeResponseFromLoadedProgram loadedProgram rangeToFocus = do + -- destructure and get needed data + let (LoadedProgram + _ (A.Program _ _ globalProperties _) + _ _ proofObligations specs warnings _ _ + ) = loadedProgram + + -- send warnings as diagnostics + let diagnostics = concatMap collect warnings + sendDiagnostics filepath diagnostics + + -- send reponse for client to render hints + version' <- bumpVersion + let response = makeResponseFromHints version' rangeToFocus (globalProperties, proofObligations, specs, warnings) + return response + +makeResponseFromHints :: Int -> Maybe Range -> ([Expr], [PO], [Spec], [StructWarning]) -> [ResKind] +makeResponseFromHints version rangeToInspect _hints@(globalProperties, proofObligations, specs, warnings) = + [ ResMarkPOs rangesOfProofObligations + , ResUpdateSpecs (map encodeSpec specs) + , ResDisplay version sections + ] + where + rangesOfProofObligations :: [Range] + rangesOfProofObligations = mapMaybe (fromLoc . locOf) proofObligations + 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 + , proofObligationSections + , globalPropertiesSections + ] + where + warningsSections :: [Section] + warningsSections = map renderSection warnings + specsSections :: [Section] + specsSections = map renderSection specsToDisplay + where + specsToDisplay :: [Spec] + specsToDisplay = case rangeToInspect of + Nothing -> specs + Just selectedRange -> filter (withinRange selectedRange) specs + proofObligationSections :: [Section] + proofObligationSections = map renderSection proofObligationsToDisplay + where + proofObligationsToDisplay :: [PO] + proofObligationsToDisplay = case rangeToInspect of + Nothing -> proofObligations + Just selectedRange -> filter (selectedRange `covers`) proofObligations + where + covers :: Range -> PO -> Bool + covers range po = case poAnchorLoc po of + Nothing -> withinRange range po + Just anchor -> withinRange range po || withinRange range anchor + globalPropertiesSections :: [Section] + globalPropertiesSections = map + (\expr -> Section + Plain + [Header "Property" (fromLoc (locOf expr)), Code (render expr)] + ) + globalProperties diff --git a/src/Server/Handler2/TextDocumentSemanticTokensFull.hs b/src/Server/Handler2/TextDocumentSemanticTokensFull.hs index ba2178be..b1bd56d5 100644 --- a/src/Server/Handler2/TextDocumentSemanticTokensFull.hs +++ b/src/Server/Handler2/TextDocumentSemanticTokensFull.hs @@ -7,9 +7,8 @@ import Server.Handler2.Utils handler :: LSP.Uri -> (Either LSP.ResponseError (Maybe LSP.SemanticTokens) -> ServerM ()) -> ServerM () handler fileUri responder = do - case LSP.uriToFilePath fileUri of - Nothing -> return () + Nothing -> respondError (LSP.ResponseError LSP.InvalidParams "Invalid uri" Nothing) Just filePath -> do logText "\n ---> Syntax Highlighting" let legend = LSP.SemanticTokensLegend @@ -17,8 +16,15 @@ handler fileUri responder = do (LSP.List LSP.knownSemanticTokenModifiers) maybeLoadedProgram <- dumpProgram filePath case maybeLoadedProgram of - Nothing -> responder (Left $ LSP.ResponseError LSP.ServerNotInitialized "Please reload before requesting semantic tokens." Nothing) + Nothing -> respondError (LSP.ResponseError LSP.ServerNotInitialized "Please reload before requesting for semantic tokens." Nothing) Just loadedProgram -> do case LSP.makeSemanticTokens legend $ _highlightingInfos loadedProgram of - Left errorMessage -> responder (Left $ LSP.ResponseError LSP.InternalError errorMessage Nothing) - Right semanticTokens -> responder (Right $ Just semanticTokens) \ No newline at end of file + Left errorMessage -> do + respondError (LSP.ResponseError LSP.InternalError errorMessage Nothing) + Right semanticTokens -> do + respondResult semanticTokens + where + respondResult :: Maybe LSP.SemanticTokens -> ServerM () + respondResult result = responder (Right result) + respondError :: Error -> ServerM () + respondError err = responder (Left err) \ No newline at end of file diff --git a/src/Server/Handler2/Utils.hs b/src/Server/Handler2/Utils.hs index 71db1304..cc808a2a 100644 --- a/src/Server/Handler2/Utils.hs +++ b/src/Server/Handler2/Utils.hs @@ -44,7 +44,7 @@ editText range textToReplace onSuccess = do _changeAnnotations = Nothing } } - _ <- LSP.sendRequest LSP.SWorkspaceApplyEdit requestParams (const onSuccess) + _requestId <- LSP.sendRequest LSP.SWorkspaceApplyEdit requestParams (\_ -> onSuccess) return () where