rzk 0.7.2 → 0.7.3
raw patch · 9 files changed
+196/−41 lines, 9 filesdep +hspecdep +hspec-discover
Dependencies added: hspec, hspec-discover
Files
- ChangeLog.md +11/−0
- rzk.cabal +4/−1
- src/Language/Rzk/Syntax.hs +22/−4
- src/Language/Rzk/VSCode/Handlers.hs +12/−4
- src/Language/Rzk/VSCode/Lsp.hs +54/−2
- src/Rzk/Format.hs +42/−27
- src/Rzk/TypeCheck.hs +1/−1
- test/Rzk/FormatSpec.hs +49/−0
- test/Spec.hs +1/−2
ChangeLog.md view
@@ -6,6 +6,17 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.7.3 — 2023-12-16++Fixes:+- Fix overlapping edits in the formatter, hopefully making it idempotent (see [#160](https://github.com/rzk-lang/rzk/pull/160));+- Fix formatter crashing the language server (see [#161](https://github.com/rzk-lang/rzk/pull/161));+- Avoid unnecessary typechecking when semantics of a file has not changed (see [#159](https://github.com/rzk-lang/rzk/pull/159));+- Stop typechecking after the first parse error (avoid invalid cache) (see [`68ab0b4`](https://github.com/rzk-lang/rzk/commit/68ab0b4dd3d627756e10adb55cb16845b08d09d9));++Other:+- Add unit tests for the formatter (see [#157](https://github.com/rzk-lang/rzk/pull/157));+ ## v0.7.2 — 2023-12-12 Fixes:
rzk.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: rzk-version: 0.7.2+version: 0.7.3 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@@ -159,6 +159,7 @@ type: exitcode-stdio-1.0 main-is: Spec.hs other-modules:+ Rzk.FormatSpec Paths_rzk hs-source-dirs: test@@ -175,6 +176,8 @@ , bifunctors >=5.5.3 , bytestring >=0.10.8.2 , directory >=1.2.7.0+ , hspec+ , hspec-discover , mtl >=2.2.2 , rzk , template-haskell >=2.14.0.0
src/Language/Rzk/Syntax.hs view
@@ -9,6 +9,7 @@ parseModuleRzk, parseModuleFile, parseTerm,+ resolveLayout, Print.Print(..), printTree, tryExtractMarkdownCodeBlocks, extractMarkdownCodeBlocks,@@ -23,11 +24,12 @@ import qualified Data.List as List import Language.Rzk.Syntax.Abs+import qualified Language.Rzk.Syntax.Layout as Layout import qualified Language.Rzk.Syntax.Print as Print -import Language.Rzk.Syntax.Layout (resolveLayout)-import Language.Rzk.Syntax.Lex (tokens)+import Language.Rzk.Syntax.Lex (tokens, Token) import Language.Rzk.Syntax.Par (pModule, pTerm)+import GHC.IO (unsafePerformIO) tryOrDisplayException :: Either String a -> IO (Either String a) tryOrDisplayException = tryOrDisplayExceptionIO . evaluate@@ -42,10 +44,10 @@ parseModuleSafe = tryOrDisplayException . parseModule parseModule :: String -> Either String Module-parseModule = pModule . resolveLayout True . tokens . tryExtractMarkdownCodeBlocks "rzk"+parseModule = pModule . Layout.resolveLayout True . tokens . tryExtractMarkdownCodeBlocks "rzk" parseModuleRzk :: String -> Either String Module-parseModuleRzk = pModule . resolveLayout True . tokens+parseModuleRzk = pModule . Layout.resolveLayout True . tokens parseModuleFile :: FilePath -> IO (Either String Module) parseModuleFile path = do@@ -121,6 +123,22 @@ | otherwise = NonCode where (prefix, suffix) = List.splitAt 3 line++-- * Making BNFC resolveLayout safer++-- | Replace layout syntax with explicit layout tokens.+resolveLayout+ :: Bool -- ^ Whether to use top-level layout.+ -> [Token] -- ^ Token stream before layout resolution.+ -> Either String [Token] -- ^ Token stream after layout resolution.+resolveLayout isTopLevel toks = unsafePerformIO $ do+ -- NOTE: we use (length . show) as poor man's Control.DeepSeq.force+ -- NOTE: this is required to force all resolveLayout error's to come out+ try (evaluate (length (show resolvedToks))) >>= \case+ Left (err :: SomeException) -> return (Left (displayException err))+ Right _ -> return (Right resolvedToks)+ where+ resolvedToks = Layout.resolveLayout isTopLevel toks -- * Overriding BNFC pretty-printer
src/Language/Rzk/VSCode/Handlers.hs view
@@ -61,7 +61,7 @@ collectErrors [] = ([], []) collectErrors ((path, result) : paths) = case result of- Left err -> ((path, err) : errors, modules)+ Left err -> ((path, err) : errors, []) Right module_ -> (errors, (path, module_) : modules) where (errors, modules) = collectErrors paths@@ -106,8 +106,14 @@ 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+ Left (ex :: SomeException) -> do+ -- Just a warning to be logged in the "Output" panel and not shown to the user as an error message+ -- because exceptions are expected when the file has invalid syntax+ logWarning ("Encountered an exception while typechecking:\n" ++ show ex)+ return ([], [])+ Right (Left err) -> do+ logError ("An impossible error happened! Please report a bug:\n" ++ ppTypeErrorInScopedContext' BottomUp err)+ return ([err], []) -- sort of impossible Right (Right (checkedModules, errors)) -> do -- cache well-typed modules logInfo (show (length checkedModules) ++ " modules successfully typechecked")@@ -233,7 +239,9 @@ mdoc <- getVirtualFile doc possibleEdits <- case virtualFileText <$> mdoc of Nothing -> return (Left "Failed to get file contents")- Just sourceCode -> return (Right $ map formattingEditToTextEdit $ formatTextEdits (filter (/= '\r') $ T.unpack sourceCode))+ Just sourceCode -> do+ let edits = formatTextEdits (filter (/= '\r') $ T.unpack sourceCode)+ return (Right $ map formattingEditToTextEdit edits) case possibleEdits of Left err -> res $ Left $ ResponseError (InR ErrorCodes_InternalError) err Nothing Right edits -> do
src/Language/Rzk/VSCode/Lsp.hs view
@@ -1,5 +1,7 @@ {-# LANGUAGE DuplicateRecordFields #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeApplications #-} module Language.Rzk.VSCode.Lsp where @@ -17,19 +19,66 @@ import Language.LSP.Server import Language.LSP.VFS (virtualFileText) +import Control.Exception (SomeException, evaluate, try)+import Control.Monad.Except (ExceptT (ExceptT),+ MonadError (throwError),+ modifyError, runExceptT) import Data.Aeson (Result (Error, Success), fromJSON)-import Language.Rzk.Syntax (parseModuleSafe)+import Language.Rzk.Syntax (parseModuleFile,+ parseModuleSafe) import Language.Rzk.VSCode.Config (ServerConfig (..)) import Language.Rzk.VSCode.Env import Language.Rzk.VSCode.Handlers import Language.Rzk.VSCode.Logging import Language.Rzk.VSCode.Tokenize (tokenizeModule)+import Rzk.TypeCheck (defaultTypeCheck,+ typecheckModulesWithLocationIncremental) -- | The maximum number of diagnostic messages to send to the client maxDiagnosticCount :: Int maxDiagnosticCount = 100 +data IsChanged+ = HasChanged+ | NotChanged++-- | Detects if the given path has changes in its declaration compared to what's in the cache+isChanged :: RzkTypecheckCache -> FilePath -> LSP IsChanged+isChanged cache path = toIsChanged $ do+ cachedDecls <- maybeToEitherLSP $ lookup path cache+ module' <- toExceptTLifted $ parseModuleFile path+ e <- toExceptTLifted $ try @SomeException $ evaluate $+ defaultTypeCheck (typecheckModulesWithLocationIncremental (takeWhile ((/= path) . fst) cache) [(path, module')])+ (checkedModules, _errors) <- toExceptT $ return e+ decls' <- maybeToEitherLSP $ lookup path checkedModules+ return $ if decls' == cachedDecls+ then NotChanged+ else HasChanged+ where+ toExceptT = modifyError (const ()) . ExceptT+ toExceptTLifted = toExceptT . liftIO+ maybeToEitherLSP = \case+ Nothing -> throwError ()+ Just x -> return x+ toIsChanged m = runExceptT m >>= \case+ Left _ -> return HasChanged -- in case of error consider the file has changed+ Right x -> return x++hasNotChanged :: RzkTypecheckCache -> FilePath -> LSP Bool+hasNotChanged cache path = isChanged cache path >>= \case+ HasChanged -> return False+ NotChanged -> return True++-- | Monadic 'dropWhile'+dropWhileM :: (Monad m) => (a -> m Bool) -> [a] -> m [a]+dropWhileM _ [] = return []+dropWhileM p (x:xs) = do+ q <- p x+ if q+ then dropWhileM p xs+ else return (x:xs)+ handlers :: Handlers LSP handlers = mconcat@@ -46,7 +95,10 @@ then do logDebug "rzk.yaml modified. Clearing module cache" resetCacheForAllFiles- else resetCacheForFiles modifiedPaths+ else do+ cache <- getCachedTypecheckedModules+ actualModified <- dropWhileM (hasNotChanged cache) modifiedPaths+ resetCacheForFiles actualModified typecheckFromConfigFile , notificationHandler SMethod_TextDocumentDidSave $ \_msg -> do -- TODO: check if the file is included in the config's `include` list.
src/Rzk/Format.hs view
@@ -5,8 +5,10 @@ The formatter is designed in a way that can be consumed both by the CLI and the LSP server. -}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wno-orphans #-} module Rzk.Format ( FormattingEdit (FormattingEdit),@@ -15,20 +17,21 @@ isWellFormatted, isWellFormattedFile, ) where -import Control.Monad ((<$!>))-import Data.List (elemIndex, foldl', sort)+import Data.List (elemIndex, sort) -import Language.Rzk.Syntax (tryExtractMarkdownCodeBlocks)-import Language.Rzk.Syntax.Layout (resolveLayout)-import Language.Rzk.Syntax.Lex (Posn (Pn),- Tok (TK, T_VarIdentToken),- TokSymbol (TokSymbol), Token (PT),- tokens)+import qualified Data.Text as T+import qualified Data.Text.IO as T +import Language.Rzk.Syntax (tryExtractMarkdownCodeBlocks,+ resolveLayout)+import Language.Rzk.Syntax.Lex (Posn (Pn), Tok (..),+ TokSymbol (TokSymbol),+ Token (PT), tokens)+ -- | All indices are 1-based (as received from the lexer) -- Note: LSP uses 0-based indices data FormattingEdit = FormattingEdit Int Int Int Int String- deriving (Eq, Ord)+ deriving (Eq, Ord, Show) -- TODO: more patterns, e.g. for identifiers and literals pattern Symbol :: String -> Tok@@ -47,19 +50,22 @@ { parensDepth :: Int -- ^ The level of parentheses nesting , definingName :: Bool -- ^ After #define, in name or assumptions (to detect the : for the type) , lambdaArrow :: Bool -- ^ After a lambda '\', in the parameters (to leave its -> on the same line)+ , allTokens :: [Token] -- ^ The full array of tokens after resolving the layout } -- TODO: replace all tabs with 1 space before processing formatTextEdits :: String -> [FormattingEdit]-formatTextEdits contents = go initialState toks+formatTextEdits contents =+ case resolveLayout True (tokens rzkBlocks) of+ Left _err -> [] -- TODO: log error (in a CLI and LSP friendly way)+ Right allToks -> go (initialState {allTokens = allToks}) allToks where- initialState = FormatState { parensDepth = 0, definingName = False, lambdaArrow = False }+ initialState = FormatState { parensDepth = 0, definingName = False, lambdaArrow = False, allTokens = [] } incParensDepth s = s { parensDepth = parensDepth s + 1 }- decParensDepth s = s { parensDepth = parensDepth s - 1 }+ decParensDepth s = s { parensDepth = 0 `max` (parensDepth s - 1) } rzkBlocks = tryExtractMarkdownCodeBlocks "rzk" contents -- TODO: replace tabs with spaces contentLines line = lines rzkBlocks !! (line - 1) -- Sorry- toks = resolveLayout True (tokens rzkBlocks)- lineTokensBefore line col = filter isBefore toks+ lineTokensBefore toks line col = filter isBefore toks where isBefore (PT (Pn _ l c) _) = l == line && c < col isBefore _ = False@@ -124,7 +130,7 @@ where spaceCol = col + 1 lineContent = contentLines line- precededBySingleCharOnly = all isPunctuation (lineTokensBefore line col)+ precededBySingleCharOnly = all isPunctuation (lineTokensBefore (allTokens s) line col) singleCharUnicodeTokens = filter (\(_, unicode) -> length unicode == 1) unicodeTokens punctuations = concat [ map fst singleCharUnicodeTokens -- ASCII sequences will be converted soon@@ -232,21 +238,26 @@ spacesNextLine = length $ takeWhile (== ' ') nextLine edits = spaceEdits ++ unicodeEdits spaceEdits- | tk `elem` ["->", "→", ",", "*", "×", "="] = map snd $ filter fst+ | tk `elem` ["->", "→", ",", "*", "×", "="] = concatMap snd $ filter fst -- Ensure exactly one space before (unless first char in line, or about to move to next line) [ (not isFirstNonSpaceChar && spacesBefore /= 1 && not isLastNonSpaceChar,- FormattingEdit line (col - spacesBefore) line col " ")+ [FormattingEdit line (col - spacesBefore) line col " "]) -- Ensure exactly one space after (unless last char in line) , (not isLastNonSpaceChar && spacesAfter /= 1,- FormattingEdit line (col + length tk) line (col + length tk + spacesAfter) " ")+ [FormattingEdit line (col + length tk) line (col + length tk + spacesAfter) " "]) -- If last char in line, move it to next line (except for lambda arrow) , (isLastNonSpaceChar && not (lambdaArrow s),- FormattingEdit line (col - spacesBefore) (line + 1) (spacesNextLine + 1) $- "\n" ++ replicate (2 `max` (spacesNextLine - (spacesNextLine `min` 2))) ' ' ++ tk ++ " ")+ -- This is split into 2 edits to avoid possible overlap with unicode replacement+ -- 1. Add a new line (with relevant spaces) before the token+ [ FormattingEdit line (col - spacesBefore) line col $+ "\n" ++ replicate (2 `max` (spacesNextLine - (spacesNextLine `min` 2))) ' '+ -- 2. Replace the new line and spaces after the token with a single space+ , FormattingEdit line (col + length tk) (line + 1) (spacesNextLine + 1) " "+ ]) -- If lambda -> is first char in line, move it to the previous line , (isFirstNonSpaceChar && isArrow && lambdaArrow s,- FormattingEdit (line - 1) (length prevLine + 1) line (col + length tk + spacesAfter) $- " " ++ tk ++ "\n" ++ replicate spacesBefore ' ')+ [FormattingEdit (line - 1) (length prevLine + 1) line (col + length tk + spacesAfter) $+ " " ++ tk ++ "\n" ++ replicate spacesBefore ' ']) ] | otherwise = [] unicodeEdits@@ -275,7 +286,7 @@ Nothing -> length t' applyTextEdits :: [FormattingEdit] -> String -> String-applyTextEdits edits contents = foldl' (flip applyTextEdit) contents (reverse $ sort edits)+applyTextEdits edits contents = foldr applyTextEdit contents (sort edits) -- | Format Rzk code, returning the formatted version. format :: String -> String@@ -283,7 +294,9 @@ -- | Format Rzk code from a file formatFile :: FilePath -> IO String-formatFile path = format <$!> readFile path -- strict because possibility of writing to same file+formatFile path = do+ contents <- T.readFile path+ return (format (T.unpack contents)) -- | Format the file and write the result back to the file. formatFileWrite :: FilePath -> IO ()@@ -296,4 +309,6 @@ -- | Same as 'isWellFormatted', but reads the source code from a file. isWellFormattedFile :: FilePath -> IO Bool-isWellFormattedFile path = isWellFormatted <$> readFile path+isWellFormattedFile path = do+ contents <- T.readFile path+ return (isWellFormatted (T.unpack contents))
src/Rzk/TypeCheck.hs view
@@ -47,7 +47,7 @@ , declValue :: Maybe (TermT var) , declIsAssumption :: Bool , declUsedVars :: [var]- }+ } deriving Eq type Decl' = Decl VarIdent
+ test/Rzk/FormatSpec.hs view
@@ -0,0 +1,49 @@+{-|+Module : FormatterSpec+Description : Tests related to the formatter module+-}+module Rzk.FormatSpec where++import Test.Hspec++import Rzk.Format (format, isWellFormatted)++formatsTo :: FilePath -> FilePath -> Expectation+formatsTo beforePath afterPath = do+ beforeSrc <- readFile ("test/files/" ++ beforePath)+ afterSrc <- readFile ("test/files/" ++ afterPath)+ format beforeSrc `shouldBe` afterSrc+ isWellFormatted afterSrc `shouldBe` True -- idempotency++formats :: FilePath -> Expectation+formats path = (path ++ "-bad.rzk") `formatsTo` (path ++ "-good.rzk")+++spec :: Spec+spec = do+ describe "Formatter" $ do+ it "Puts definition assumptions, conclusion, and construction on separate lines" $ do+ -- formats "definition-structure"+ pendingWith "Doesn't currently place assumptions on a new line"++ it "Replaces common ASCII sequences with their unicode equivalent" $ do+ formats "unicode"++ it "Formats Rzk blocks in Literate Rzk Markdown" $ do+ "literate-bad.rzk.md" `formatsTo` "literate-good.rzk.md"++ it "Preserves comments" $ do+ formats "comments"++ it "Moves trailing binary operators to next line (except lambda arrow)" $ do+ formats "bin-ops"++ it "Adds relevant spaces to structure constructions like a tree" $ do+ formats "tree-structure"++ it "Doesn't fail on empty inputs" $ do+ formats "empty"++ it "Fixes indentation" pending++ it "Wraps long lines" pending
test/Spec.hs view
@@ -1,2 +1,1 @@-main :: IO ()-main = putStrLn "Test suite not yet implemented"+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}