diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -6,6 +6,10 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.7.0 — 2023-12-08 + + + ## v0.6.7 — 2023-10-07 - Fix build on some systems (fix `BNFC:bnfc` executable dependency, see [#125](https://github.com/rzk-lang/rzk/pull/125)) diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -1,14 +1,93 @@ -{-# LANGUAGE CPP #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE NamedFieldPuns #-} + module Main (main) where #ifndef __GHCJS__ import Main.Utf8 (withUtf8) #endif -import qualified Rzk.Main +import Control.Monad (forM, forM_, unless, when, + (>=>)) +import Data.Version (showVersion) + +#ifdef LSP +import Language.Rzk.VSCode.Lsp (runLsp) +#endif + +import Options.Generic +import System.Exit (exitFailure, exitSuccess) + +import Data.Functor ((<&>)) +import Paths_rzk (version) +import Rzk.Format (formatFile, formatFileWrite, + isWellFormattedFile) +import Rzk.TypeCheck +import Rzk.Main + +data FormatOptions = FormatOptions + { check :: Bool + , write :: Bool + } deriving (Generic, Show, ParseRecord, Read, ParseField) + +instance ParseFields FormatOptions where + parseFields _ _ _ _ = FormatOptions + <$> parseFields (Just "Check if the files are correctly formatted") (Just "check") (Just 'c') Nothing + <*> parseFields (Just "Write formatted file to disk") (Just "write") (Just 'w') Nothing + +data Command + = Typecheck [FilePath] + | Lsp + | Format FormatOptions [FilePath] + | Version + deriving (Generic, Show, ParseRecord) + main :: IO () -main = +main = do #ifndef __GHCJS__ - withUtf8 + withUtf8 $ #endif - Rzk.Main.main + getRecord "rzk: an experimental proof assistant for synthetic ∞-categories" >>= \case + Typecheck paths -> do + modules <- parseRzkFilesOrStdin paths + case defaultTypeCheck (typecheckModulesWithLocation modules) of + Left err -> do + putStrLn "An error occurred when typechecking!" + putStrLn $ unlines + [ "Type Error:" + , ppTypeErrorInScopedContext' BottomUp err + ] + exitFailure + Right _decls -> putStrLn "Everything is ok!" + + Lsp -> +#ifdef LSP + void runLsp +#else + error "rzk lsp is not supported with this build" +#endif + + Format (FormatOptions {check, write}) paths -> do + when (check && write) (error "Options --check and --write are mutually exclusive") + expandedPaths <- expandRzkPathsOrYaml paths + case expandedPaths of + [] -> error "No files found" + filePaths -> do + when (not check && not write) $ forM_ filePaths (formatFile >=> putStrLn) + when write $ forM_ filePaths formatFileWrite + when check $ do + results <- forM filePaths $ \path -> isWellFormattedFile path <&> (path,) + let notFormatted = map fst $ filter (not . snd) results + unless (null notFormatted) $ do + putStrLn "Some files are not well formatted:" + forM_ notFormatted $ \path -> putStrLn (" " <> path) + exitFailure + exitSuccess + + Version -> putStrLn (showVersion version) + 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.6.7 +version: 0.7.0 synopsis: An experimental proof assistant for synthetic ∞-categories description: Please see the README on GitHub at category: Dependent Types @@ -49,6 +49,7 @@ Language.Rzk.Syntax.Par Language.Rzk.Syntax.Print Rzk + Rzk.Format Rzk.Main Rzk.Project.Config Rzk.TypeCheck @@ -70,18 +71,18 @@ , bytestring >=0.10.8.2 , directory >=1.2.7.0 , mtl >=2.2.2 - , optparse-generic >=1.3.0 , template-haskell >=2.14.0.0 , text >=1.2.3.1 , yaml >=0.11.0.0 default-language: Haskell2010 if flag(lsp) && !impl(ghcjs) exposed-modules: + Language.Rzk.VSCode.Config Language.Rzk.VSCode.Env Language.Rzk.VSCode.Handlers + Language.Rzk.VSCode.Logging Language.Rzk.VSCode.Lsp Language.Rzk.VSCode.Tokenize - Language.Rzk.VSCode.Logging cpp-options: -DLSP build-depends: aeson >=1.4.2.0 @@ -113,7 +114,6 @@ , bytestring >=0.10.8.2 , directory >=1.2.7.0 , mtl >=2.2.2 - , optparse-generic >=1.3.0 , rzk , template-haskell >=2.14.0.0 , text >=1.2.3.1 @@ -121,7 +121,8 @@ default-language: Haskell2010 if !impl(ghcjs) build-depends: - with-utf8 >=1.0.2.4 + optparse-generic >=1.4.0 + , with-utf8 >=1.0.2.4 test-suite doctests type: exitcode-stdio-1.0 @@ -144,7 +145,6 @@ , directory >=1.2.7.0 , doctest , mtl >=2.2.2 - , optparse-generic >=1.3.0 , template-haskell , text >=1.2.3.1 , yaml >=0.11.0.0 @@ -171,7 +171,6 @@ , bytestring >=0.10.8.2 , directory >=1.2.7.0 , mtl >=2.2.2 - , optparse-generic >=1.3.0 , rzk , template-haskell >=2.14.0.0 , text >=1.2.3.1 diff --git a/src/Language/Rzk/VSCode/Config.hs b/src/Language/Rzk/VSCode/Config.hs new file mode 100644 --- /dev/null +++ b/src/Language/Rzk/VSCode/Config.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} + +module Language.Rzk.VSCode.Config ( + ServerConfig(..), +) where + +import Data.Aeson +import Data.Default.Class (Default, def) + +data ServerConfig = ServerConfig + { formatEnabled :: Bool + } deriving Show + +instance Default ServerConfig where + def = ServerConfig + { formatEnabled = True + } + +-- We need to derive the FromJSON instance manually in order to provide defaults +-- for absent fields. +instance FromJSON ServerConfig where + -- Note: "configSection" in ServerDefinition already filters by the "rzk." prefix + parseJSON = withObject "rzkSettings" $ \rzkSettings -> do + formatSettings <- rzkSettings .: "format" -- TODO: how to make this optional? + formatEnabled <- formatSettings .:? "enable" .!= formatEnabled def + return ServerConfig { .. } + +instance ToJSON ServerConfig where + toJSON (ServerConfig { .. }) = object + [ "format" .= object + [ "enable" .= formatEnabled + ] + ] diff --git a/src/Language/Rzk/VSCode/Env.hs b/src/Language/Rzk/VSCode/Env.hs --- a/src/Language/Rzk/VSCode/Env.hs +++ b/src/Language/Rzk/VSCode/Env.hs @@ -3,7 +3,8 @@ import Control.Concurrent.STM import Control.Monad.Reader import Language.LSP.Server -import Rzk.TypeCheck (Decl') +import Language.Rzk.VSCode.Config (ServerConfig) +import Rzk.TypeCheck (Decl') type RzkTypecheckCache = [(FilePath, [Decl'])] @@ -18,7 +19,7 @@ { rzkEnvTypecheckCache = typecheckCache } -type LSP = LspT () (ReaderT RzkEnv IO) +type LSP = LspT ServerConfig (ReaderT RzkEnv IO) -- | Override the cache with given typechecked modules. cacheTypecheckedModules :: RzkTypecheckCache -> LSP () 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 @@ -4,7 +4,11 @@ {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wno-orphans #-} -module Language.Rzk.VSCode.Handlers where +module Language.Rzk.VSCode.Handlers ( + typecheckFromConfigFile, + provideCompletions, + formatDocument, +) where import Control.Exception (SomeException, evaluate, try) import Control.Lens @@ -25,6 +29,7 @@ import Language.LSP.Protocol.Message import Language.LSP.Protocol.Types import Language.LSP.Server +import Language.LSP.VFS (virtualFileText) import System.FilePath (makeRelative, ()) import System.FilePath.Glob (compile, globDir) @@ -32,8 +37,11 @@ VarIdent (getVarIdent)) import Language.Rzk.Syntax (Module, VarIdent' (VarIdent), parseModuleFile, printTree) +import Language.Rzk.VSCode.Config (ServerConfig (ServerConfig, formatEnabled)) import Language.Rzk.VSCode.Env import Language.Rzk.VSCode.Logging +import Rzk.Format (FormattingEdit (..), + formatTextEdits) import Rzk.Project.Config (ProjectConfig (include)) import Rzk.TypeCheck @@ -206,3 +214,30 @@ (RzkPosition _path pos') = pos line = maybe 0 fst pos' _col = maybe 0 snd pos' + +formattingEditToTextEdit :: FormattingEdit -> TextEdit +formattingEditToTextEdit (FormattingEdit startLine startCol endLine endCol newText) = + TextEdit + (Range + (Position (fromIntegral startLine - 1) (fromIntegral startCol - 1)) + (Position (fromIntegral endLine - 1) (fromIntegral endCol - 1)) + ) + (T.pack newText) + +formatDocument :: Handler LSP 'Method_TextDocumentFormatting +formatDocument req res = do + let doc = req ^. params . textDocument . uri . to toNormalizedUri + logInfo $ "Formatting document: " <> show doc + ServerConfig {formatEnabled = fmtEnabled} <- getConfig + if fmtEnabled then do + 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)) + case possibleEdits of + Left err -> res $ Left $ ResponseError (InR ErrorCodes_InternalError) err Nothing + Right edits -> do + res $ Right $ InL edits + else do + logDebug "Formatting is disabled in config" + res $ Right $ InR Null 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 @@ -6,6 +6,7 @@ import Control.Lens (_Just, to, (^.), (^..)) import Control.Monad.IO.Class import Control.Monad.Reader +import Data.Default.Class (Default (def)) import Data.List (isSuffixOf) import qualified Data.Text as T import Language.LSP.Protocol.Lens (HasParams (params), @@ -16,7 +17,10 @@ import Language.LSP.Server import Language.LSP.VFS (virtualFileText) +import Data.Aeson (Result (Error, Success), + fromJSON) import Language.Rzk.Syntax (parseModuleSafe) +import Language.Rzk.VSCode.Config (ServerConfig (..)) import Language.Rzk.VSCode.Env import Language.Rzk.VSCode.Handlers import Language.Rzk.VSCode.Logging @@ -48,6 +52,8 @@ -- TODO: check if the file is included in the config's `include` list. -- If not (and not in `exclude`) either, issue a warning. return () -- FIXME: typecheck standalone files (if they are not a part of the project) + -- An empty hadler is needed to silence the error since it is already handled by the LSP package + , notificationHandler SMethod_WorkspaceDidChangeConfiguration $ const $ pure () -- , requestHandler SMethod_TextDocumentHover $ \req responder -> do -- TODO: Read from the list of symbols that is supposed to be cached by the typechecker -- let TRequestMessage _ _ _ (HoverParams _doc pos _workDone) = req @@ -63,7 +69,7 @@ possibleTokens <- case virtualFileText <$> mdoc of Nothing -> return (Left "Failed to get file content") Just sourceCode -> fmap (fmap tokenizeModule) $ liftIO $ - parseModuleSafe (T.unpack sourceCode) + parseModuleSafe (filter (/= '\r') $ T.unpack sourceCode) case possibleTokens of Left err -> do -- Exception occurred when parsing the module @@ -76,6 +82,7 @@ return () Right list -> responder (Right (InL SemanticTokens { _resultId = Nothing, _data_ = list })) + , requestHandler SMethod_TextDocumentFormatting formatDocument ] @@ -94,11 +101,14 @@ runServer $ ServerDefinition { configSection = "rzk" - , parseConfig = const . pure + , parseConfig = \_oldConfig newObject -> case fromJSON newObject of + -- TODO: handle partial config updates from VS Code by updating oldConfig rather than parsing from scratch + Error err -> Left $ T.pack err + Success rzkConfig -> Right rzkConfig , onConfigChange = const $ pure () , doInitialize = const . pure . Right , staticHandlers = const handlers , interpretHandler = \env -> Iso (flip runReaderT rzkEnv . runLspT env) liftIO , options = defaultOptions { optTextDocumentSync = Just syncOptions } - , defaultConfig = () + , defaultConfig = def :: ServerConfig } diff --git a/src/Rzk/Format.hs b/src/Rzk/Format.hs new file mode 100644 --- /dev/null +++ b/src/Rzk/Format.hs @@ -0,0 +1,295 @@ +{-| +Module : Formatter +Description : This module defines the formatter for rzk files. + +The formatter is designed in a way that can be consumed both by the CLI and the +LSP server. +-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} + +module Rzk.Format ( + FormattingEdit (FormattingEdit), + formatTextEdits, + format, formatFile, formatFileWrite, + isWellFormatted, isWellFormattedFile, +) where + +import Control.Monad ((<$!>)) +import Data.List (elemIndex, foldl', 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) + +-- | 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) + +-- TODO: more patterns, e.g. for identifiers and literals +pattern Symbol :: String -> Tok +pattern Symbol s <- TK (TokSymbol s _) + +pattern Token :: String -> Int -> Int -> Token +pattern Token s line col <- PT (Pn _ line col) (Symbol s) + +-- pattern TokenSym :: String -> Int -> Int -> Token +-- pattern TokenSym s line col <- PT (Pn _ line col) (Symbol s) + +pattern TokenIdent :: String -> Int -> Int -> Token +pattern TokenIdent s line col <- PT (Pn _ line col) (T_VarIdentToken s) + +data FormatState = FormatState + { 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) + } + +-- TODO: replace all tabs with 1 space before processing +formatTextEdits :: String -> [FormattingEdit] +formatTextEdits contents = go initialState toks + where + initialState = FormatState { parensDepth = 0, definingName = False, lambdaArrow = False } + incParensDepth s = s { parensDepth = parensDepth s + 1 } + decParensDepth s = s { parensDepth = parensDepth s - 1 } + rzkBlocks = tryExtractMarkdownCodeBlocks "rzk" contents -- TODO: replace tabs with spaces + contentLines line = lines rzkBlocks !! (line - 1) -- Sorry + toks = resolveLayout True (tokens rzkBlocks) + unicodeTokens = + [ ("->", "→") + , ("|->", "↦") + , ("===", "≡") + , ("<=", "≤") + , ("/\\", "∧") + , ("\\/", "∨") + , ("Sigma", "Σ") + , ("∑", "Σ") + , ("*_1", "*₁") + , ("0_2", "0₂") + , ("1_2", "1₂") + , ("*", "×") + ] + go :: FormatState -> [Token] -> [FormattingEdit] + go _ [] = [] + go s (Token "#lang" langLine langCol : Token "rzk-1" rzkLine rzkCol : tks) + -- FIXME: Tab characters break this because BNFC increases the column number to the next multiple of 8 + -- Should probably check the first field of Pn (always incremented by 1) + -- Or `tabSize` param sent along the formatting request + -- But we should probably convert tabs to spaces first before any other formatting + = edits ++ go s tks + where + edits = map snd $ filter fst + -- Remove extra spaces before #lang + [ (langCol > 1, FormattingEdit langLine 1 langLine langCol "") + -- Remove extra spaces between #lang and rzk-1 + , (rzkLine > langLine || rzkCol > langCol + 5 + 1, + FormattingEdit langLine (langCol + 5) rzkLine rzkCol " ") + ] + + go s (Token "#postulate" _ _ : tks) = go (s {definingName = True}) tks + + go s (Token "#define" defLine defCol : TokenIdent _name nameLine nameCol : tks) + = edits ++ go (s {definingName = True}) tks + where + edits = map snd $ filter fst + -- Remove any space before #define + [ (defCol > 1, FormattingEdit defLine 1 defLine defCol "") + -- Ensure exactly one space after #define + , (nameLine /= defLine || nameCol > defCol + 7 + 1, + FormattingEdit defLine (defCol + 7) nameLine nameCol " ") + ] + -- #def is an alias for #define + go s (Token "#def" line col : tks) = go s (PT (Pn 0 line col) (TK (TokSymbol "#define" 0)):tks) + -- TODO: similarly for other commands + + -- Ensure exactly one space after the first open paren of a line + go s (Token "(" line col : tks) + | precededBySingleCharOnly && spacesAfter /= 1 && not isLastNonSpaceChar + = FormattingEdit line spaceCol line (spaceCol + spacesAfter) " " + : go (incParensDepth s) tks + -- Remove extra spaces if it's not the first open paren on a new line + | not precededBySingleCharOnly && spacesAfter > 0 + = FormattingEdit line spaceCol line (spaceCol + spacesAfter) "" + : go (incParensDepth s) tks + | otherwise = go (incParensDepth s) tks + -- TODO: Split after 80 chars + where + spaceCol = col + 1 + lineContent = contentLines line + -- | This is similar to (\\) but removes all occurrences (not just the first one) + setDifference xs excludes = filter (not . (`elem` excludes)) xs + precededBySingleCharOnly = null $ foldl' setDifference (take (col - 1) lineContent) punctuations + punctuations = concat + [ map fst unicodeTokens -- ASCII sequences will be converted soon + , map snd unicodeTokens + , ["(", ":", ",", "="] + , [" ", "\t"] + ] + spacesAfter = length $ takeWhile (== ' ') (drop col lineContent) + isLastNonSpaceChar = all (== ' ') (drop col lineContent) + + -- Remove any space before the closing paren + go s (Token ")" line col : tks) + = edits ++ go (decParensDepth s) tks + where + lineContent = contentLines line + isFirstNonSpaceChar = all (== ' ') (take (col - 1) lineContent) + spacesBefore = length $ takeWhile (== ' ') (reverse $ take (col - 1) lineContent) + edits = map snd $ filter fst + [ (not isFirstNonSpaceChar && spacesBefore > 0, + FormattingEdit line (col - spacesBefore) line col "") + ] + + -- line break before : (only the top-level one) and one space after + go s (Token ":" line col : tks) + | isDefinitionTypeSeparator = typeSepEdits ++ go (s {definingName = False}) tks + | otherwise = normalEdits ++ go s tks + where + isDefinitionTypeSeparator = parensDepth s == 0 && definingName s + lineContent = contentLines line + isFirstNonSpaceChar = all (== ' ') (take (col - 1) lineContent) + isLastNonSpaceChar = all (== ' ') (drop col lineContent) + spacesBefore = length $ takeWhile (== ' ') (reverse $ take (col - 1) lineContent) + spaceCol = col + 1 + spacesAfter = length $ takeWhile (== ' ') (drop col lineContent) + typeSepEdits = map snd $ filter fst + -- Ensure line break before : (and remove any spaces before) + [ (not isFirstNonSpaceChar, FormattingEdit line (col - spacesBefore) line col "\n ") + -- Ensure 2 spaces before : (if already on a new line) + , (isFirstNonSpaceChar && spacesBefore /= 2, FormattingEdit line 1 line col " ") + -- Ensure 1 space after + , (not isLastNonSpaceChar && spacesAfter /= 1, + FormattingEdit line spaceCol line (spaceCol + spacesAfter) " ") + ] + normalEdits = map snd $ filter fst + -- 1 space before : + [ (spacesBefore /= 1, FormattingEdit line (col - spacesBefore) line col " ") + -- 1 space after + , (not isLastNonSpaceChar && spacesAfter /= 1, + FormattingEdit line spaceCol line (spaceCol + spacesAfter) " ") + ] + + -- Line break before := and one space after + go s (Token ":=" line col : tks) + = edits ++ go s tks + where + lineContent = contentLines line + isFirstNonSpaceChar = all (== ' ') (take (col - 1) lineContent) + spacesAfter = length $ takeWhile (== ' ') (drop (col + 1) lineContent) + spacesBefore = length $ takeWhile (== ' ') (reverse $ take (col - 1) lineContent) + edits = map snd $ filter fst + -- Ensure line break before `:=` + [ (not isFirstNonSpaceChar, FormattingEdit line (col - spacesBefore) line col "\n ") + -- Ensure 2 spaces before `:=` (if already on a new line) + , (isFirstNonSpaceChar && spacesBefore /= 2, + FormattingEdit line 1 line col " ") + -- Ensure exactly one space after + , (length lineContent > col + 2 && spacesAfter /= 1, + FormattingEdit line (col + 2) line (col + 2 + spacesAfter) " ") + ] + + -- One space after \ + go s (Token "\\" line col : tks) + = edits ++ go (s { lambdaArrow = True }) tks + where + lineContent = contentLines line + spacesAfter = length $ takeWhile (== ' ') (drop col lineContent) + isLastNonSpaceChar = all (== ' ') (drop col lineContent) + spaceCol = col + 1 + edits = map snd $ filter fst + [ (not isLastNonSpaceChar && spacesAfter /= 1, + FormattingEdit line spaceCol line (spaceCol + spacesAfter) " ") + ] + + -- Reset any state necessary after finishing a command + go s (Token ";" _ _ : tks) = go s tks + + -- One space (or new line) around binary operators and replace ASCII w/ unicode + go s (Token tk line col : tks) = edits ++ go s' tks + where + s' | isArrow = s { lambdaArrow = False } -- reset flag after reaching the arrow + | otherwise = s + isArrow = tk `elem` ["->", "→"] + lineContent = contentLines line + spacesBefore = length $ takeWhile (== ' ') (reverse $ take (col - 1) lineContent) + spacesAfter = length $ takeWhile (== ' ') (drop (col + length tk - 1) lineContent) + isFirstNonSpaceChar = all (== ' ') (take (col - 1) lineContent) + isLastNonSpaceChar = all (== ' ') (drop (col + length tk - 1) lineContent) + prevLine + | line > 0 = contentLines (line - 1) + | otherwise = "" + nextLine + | line + 1 < length (lines rzkBlocks) = contentLines (line + 1) + | otherwise = "" + spacesNextLine = length $ takeWhile (== ' ') nextLine + edits = spaceEdits ++ unicodeEdits + spaceEdits + | tk `elem` ["->", "→", ",", "*", "×", "="] = map 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 " ") + -- Ensure exactly one space after (unless last char in line) + , (not isLastNonSpaceChar && spacesAfter /= 1, + 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 ++ " ") + -- 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 ' ') + ] + | otherwise = [] + unicodeEdits + | Just unicodeToken <- tk `lookup` unicodeTokens = + [ FormattingEdit line col line (col + length tk) unicodeToken + ] + | otherwise = [] + + go s (_:tks) = go s tks + +-- Adapted from https://hackage.haskell.org/package/lsp-types-2.1.0.0/docs/Language-LSP-Protocol-Types.html#g:7 +applyTextEdit :: FormattingEdit -> String -> String +applyTextEdit (FormattingEdit sl sc el ec newText) oldText = + let (_, afterEnd) = splitAtPos (el-1, ec -1) oldText + (beforeStart, _) = splitAtPos (sl-1, sc-1) oldText + in mconcat [beforeStart, newText, afterEnd] + where + splitAtPos :: (Int, Int) -> String -> (String, String) + splitAtPos (l, c) t = let index = c + startLineIndex l t in splitAt index t + + startLineIndex :: Int -> String -> Int + startLineIndex 0 _ = 0 + startLineIndex line t' = + case elemIndex '\n' t' of + Just i -> i + 1 + startLineIndex (line - 1) (drop (i + 1) t') + Nothing -> length t' + +applyTextEdits :: [FormattingEdit] -> String -> String +applyTextEdits edits contents = foldl' (flip applyTextEdit) contents (reverse $ sort edits) + +-- | Format Rzk code, returning the formatted version. +format :: String -> String +format = applyTextEdits =<< formatTextEdits + +-- | Format Rzk code from a file +formatFile :: FilePath -> IO String +formatFile path = format <$!> readFile path -- strict because possibility of writing to same file + +-- | Format the file and write the result back to the file. +formatFileWrite :: FilePath -> IO () +formatFileWrite path = formatFile path >>= writeFile path + +-- | Check if the given Rzk source code is well formatted. +-- This is useful for automation tasks. +isWellFormatted :: String -> Bool +isWellFormatted src = null (formatTextEdits src) + +-- | Same as 'isWellFormatted', but reads the source code from a file. +isWellFormattedFile :: FilePath -> IO Bool +isWellFormattedFile path = isWellFormatted <$> readFile path diff --git a/src/Rzk/Main.hs b/src/Rzk/Main.hs --- a/src/Rzk/Main.hs +++ b/src/Rzk/Main.hs @@ -1,6 +1,3 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} @@ -8,54 +5,17 @@ module Rzk.Main where -import Control.Monad (forM, void) +import Control.Monad (forM, when) import Data.List (sort) -import Data.Version (showVersion) - -#ifdef LSP -import Language.Rzk.VSCode.Lsp (runLsp) -#endif - import qualified Data.Yaml as Yaml -import Options.Generic import System.Directory (doesPathExist) -import System.Exit (exitFailure) import System.FilePath.Glob (glob) - import qualified Language.Rzk.Syntax as Rzk -import Paths_rzk (version) import Rzk.Project.Config import Rzk.TypeCheck -data Command - = Typecheck [FilePath] - | Lsp - | Version - deriving (Generic, Show, ParseRecord) -main :: IO () -main = getRecord "rzk: an experimental proof assistant for synthetic ∞-categories" >>= \case - Typecheck paths -> do - modules <- parseRzkFilesOrStdin paths - case defaultTypeCheck (typecheckModulesWithLocation modules) of - Left err -> do - putStrLn "An error occurred when typechecking!" - putStrLn $ unlines - [ "Type Error:" - , ppTypeErrorInScopedContext' BottomUp err - ] - exitFailure - Right _decls -> putStrLn "Everything is ok!" - Lsp -> -#ifdef LSP - void runLsp -#else - error "rzk lsp is not supported with this build" -#endif - - Version -> putStrLn (showVersion version) - parseStdin :: IO Rzk.Module parseStdin = do result <- Rzk.parseModule <$> getContents @@ -82,9 +42,26 @@ Right ProjectConfig{..} -> do return include +-- | Given a list of file paths (possibly including globs), expands the globs (if any) +-- or tries to read the list of files from the rzk.yaml file (if no paths are given). +-- Glob patterns in rzk.yaml are also expanded. +expandRzkPathsOrYaml :: [FilePath] -> IO [FilePath] +expandRzkPathsOrYaml = \case + [] -> do + let rzkYamlPath = "rzk.yaml" + rzkYamlExists <- doesPathExist rzkYamlPath + if rzkYamlExists + then do + paths <- extractFilesFromRzkYaml rzkYamlPath + when (null paths) (error $ "No files found in " <> rzkYamlPath) + expandRzkPathsOrYaml paths + else error ("No paths given and no " <> rzkYamlPath <> " found") + paths -> foldMap globNonEmpty paths + parseRzkFilesOrStdin :: [FilePath] -> IO [(FilePath, Rzk.Module)] parseRzkFilesOrStdin = \case -- if no paths are given — read from stdin + -- TODO: reuse the `expandRzkPathsOrYaml` function [] -> do let rzkYamlPath = "rzk.yaml" rzkYamlExists <- doesPathExist rzkYamlPath