rzk 0.6.0 → 0.6.1
raw patch · 5 files changed
+54/−19 lines, 5 files
Files
- ChangeLog.md +6/−0
- rzk.cabal +1/−1
- src/Language/Rzk/Syntax.hs +23/−3
- src/Language/Rzk/VSCode/Handlers.hs +17/−10
- src/Language/Rzk/VSCode/Lsp.hs +7/−5
ChangeLog.md view
@@ -6,6 +6,12 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.6.1 — 2023-09-24++This version contains a minor fix:++- Catch exceptions in the parser, fixing LSP for files where layout resolver fails (see [#99](https://github.com/rzk-lang/rzk/pull/99)).+ ## v0.6.0 — 2023-09-23 This version introduces a proper LSP server with basic support for incremental typechecking
rzk.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: rzk-version: 0.6.0+version: 0.6.1 synopsis: An experimental proof assistant for synthetic ∞-categories description: Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme> category: Dependent Types
src/Language/Rzk/Syntax.hs view
@@ -1,8 +1,10 @@-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-} module Language.Rzk.Syntax ( module Language.Rzk.Syntax.Abs, + parseModuleSafe, parseModule, parseModuleRzk, parseModuleFile,@@ -10,8 +12,13 @@ printTree, tryExtractMarkdownCodeBlocks, extractMarkdownCodeBlocks,+ tryOrDisplayException,+ tryOrDisplayExceptionIO, ) where +import Control.Exception (Exception (..), SomeException,+ evaluate, try)+ import Data.Char (isSpace) import qualified Data.List as List @@ -22,6 +29,18 @@ import Language.Rzk.Syntax.Lex (tokens) import Language.Rzk.Syntax.Par (pModule, pTerm) +tryOrDisplayException :: Either String a -> IO (Either String a)+tryOrDisplayException = tryOrDisplayExceptionIO . evaluate++tryOrDisplayExceptionIO :: IO (Either String a) -> IO (Either String a)+tryOrDisplayExceptionIO x =+ try x >>= \case+ Left (ex :: SomeException) -> return (Left (displayException ex))+ Right result -> return result++parseModuleSafe :: String -> IO (Either String Module)+parseModuleSafe = tryOrDisplayException . parseModule+ parseModule :: String -> Either String Module parseModule = pModule . resolveLayout True . tokens . tryExtractMarkdownCodeBlocks "rzk" @@ -30,7 +49,8 @@ parseModuleFile :: FilePath -> IO (Either String Module) parseModuleFile path = do- parseModule <$> readFile path+ source <- readFile path+ parseModuleSafe source parseTerm :: String -> Either String Term parseTerm = pTerm . tokens
src/Language/Rzk/VSCode/Handlers.hs view
@@ -1,8 +1,10 @@-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-} module Language.Rzk.VSCode.Handlers where +import Control.Exception (SomeException, evaluate, try) import Control.Monad.Cont (MonadIO (liftIO), forM_) import Data.List (sort, (\\)) import qualified Data.Text as T@@ -60,6 +62,9 @@ let rzkYamlPath = rootPath </> "rzk.yaml" eitherConfig <- liftIO $ Yaml.decodeFileEither @ProjectConfig rzkYamlPath case eitherConfig of+ Left err -> do+ sendNotification SMethod_WindowShowMessage (ShowMessageParams MessageType_Warning (T.pack $ "Invalid or missing rzk.yaml: " ++ Yaml.prettyPrintParseException err))+ Right config -> do rawPaths <- liftIO $ globDir (map compile (include config)) rootPath let paths = concatMap sort rawPaths@@ -69,13 +74,17 @@ modifiedFiles = paths \\ cachedPaths (parseErrors, parsedModules) <- liftIO $ collectErrors <$> parseFiles modifiedFiles- (typeErrors, _checkedModules) <- case defaultTypeCheck (typecheckModulesWithLocationIncremental cachedModules parsedModules) of- Left err -> return ([err], []) -- sort of impossible- Right (checkedModules, errors) -> do- -- cache well-typed modules- cacheTypecheckedModules checkedModules- return (errors, checkedModules)+ tcResults <- liftIO $ try $ evaluate $+ defaultTypeCheck (typecheckModulesWithLocationIncremental cachedModules parsedModules) + (typeErrors, _checkedModules) <- case tcResults of+ Left (_ex :: SomeException) -> return ([], []) -- FIXME: publish diagnostics about an exception during typechecking!+ Right (Left err) -> return ([err], []) -- sort of impossible+ Right (Right (checkedModules, errors)) -> do+ -- cache well-typed modules+ cacheTypecheckedModules checkedModules+ return (errors, checkedModules)+ -- Reset all published diags -- TODO: remove this after properly grouping by path below, after which there can be an empty list of errors forM_ paths $ \path -> do@@ -92,8 +101,6 @@ let errPath = filepathOfTypeError err errDiagnostic = diagnosticOfTypeError err publishDiagnostics maxDiagnosticCount (filePathToNormalizedUri errPath) Nothing (partitionBySource [errDiagnostic])- Left err -> do- sendNotification SMethod_WindowShowMessage (ShowMessageParams MessageType_Warning (T.pack $ "Invalid or missing rzk.yaml: " ++ Yaml.prettyPrintParseException err)) where filepathOfTypeError :: TypeErrorInScopedContext var -> FilePath filepathOfTypeError (PlainTypeError err) =
src/Language/Rzk/VSCode/Lsp.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeApplications #-} module Language.Rzk.VSCode.Lsp where @@ -16,7 +17,7 @@ import Language.LSP.Server import Language.LSP.VFS (virtualFileText) -import Language.Rzk.Syntax (parseModule)+import Language.Rzk.Syntax (parseModuleSafe) import Language.Rzk.VSCode.Env import Language.Rzk.VSCode.Handlers import Language.Rzk.VSCode.Tokenize (tokenizeModule)@@ -60,12 +61,13 @@ , requestHandler SMethod_TextDocumentSemanticTokensFull $ \req responder -> do let doc = req ^. params . textDocument . uri . to toNormalizedUri mdoc <- getVirtualFile doc- let possibleTokens = case virtualFileText <$> mdoc of- Nothing -> Left "Failed to get file content"- Just sourceCode -> tokenizeModule <$> parseModule (T.unpack sourceCode)+ possibleTokens <- case virtualFileText <$> mdoc of+ Nothing -> return (Left "Failed to get file content")+ Just sourceCode -> fmap (fmap tokenizeModule) $ liftIO $+ parseModuleSafe (T.unpack sourceCode) case possibleTokens of Left _err -> do- -- Failed to open the file or to tokenize+ -- Exception occurred when parsing the module return () Right tokens -> do let encoded = encodeTokens defaultSemanticTokensLegend $ relativizeTokens tokens