diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -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: diff --git a/rzk.cabal b/rzk.cabal --- a/rzk.cabal +++ b/rzk.cabal @@ -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 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 diff --git a/src/Language/Rzk/Syntax.hs b/src/Language/Rzk/Syntax.hs --- a/src/Language/Rzk/Syntax.hs +++ b/src/Language/Rzk/Syntax.hs @@ -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 diff --git a/src/Language/Rzk/VSCode/Handlers.hs b/src/Language/Rzk/VSCode/Handlers.hs --- a/src/Language/Rzk/VSCode/Handlers.hs +++ b/src/Language/Rzk/VSCode/Handlers.hs @@ -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 diff --git a/src/Language/Rzk/VSCode/Lsp.hs b/src/Language/Rzk/VSCode/Lsp.hs --- a/src/Language/Rzk/VSCode/Lsp.hs +++ b/src/Language/Rzk/VSCode/Lsp.hs @@ -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. diff --git a/src/Rzk/Format.hs b/src/Rzk/Format.hs --- a/src/Rzk/Format.hs +++ b/src/Rzk/Format.hs @@ -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)) diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs --- a/src/Rzk/TypeCheck.hs +++ b/src/Rzk/TypeCheck.hs @@ -47,7 +47,7 @@ , declValue :: Maybe (TermT var) , declIsAssumption :: Bool , declUsedVars :: [var] - } + } deriving Eq type Decl' = Decl VarIdent diff --git a/test/Rzk/FormatSpec.hs b/test/Rzk/FormatSpec.hs new file mode 100644 --- /dev/null +++ b/test/Rzk/FormatSpec.hs @@ -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 diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -1,2 +1,1 @@ -main :: IO () -main = putStrLn "Test suite not yet implemented" +{-# OPTIONS_GHC -F -pgmF hspec-discover #-}