rzk 0.6.7 → 0.7.0
raw patch · 9 files changed
+493/−59 lines, 9 filesdep ~optparse-generic
Dependency ranges changed: optparse-generic
Files
- ChangeLog.md +4/−0
- app/Main.hs +84/−5
- rzk.cabal +6/−7
- src/Language/Rzk/VSCode/Config.hs +34/−0
- src/Language/Rzk/VSCode/Env.hs +3/−2
- src/Language/Rzk/VSCode/Handlers.hs +36/−1
- src/Language/Rzk/VSCode/Lsp.hs +13/−3
- src/Rzk/Format.hs +295/−0
- src/Rzk/Main.hs +18/−41
ChangeLog.md view
@@ -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))
app/Main.hs view
@@ -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)+
rzk.cabal view
@@ -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 <https://github.com/rzk-lang/rzk#readme> 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
+ src/Language/Rzk/VSCode/Config.hs view
@@ -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+ ]+ ]
src/Language/Rzk/VSCode/Env.hs view
@@ -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 ()
src/Language/Rzk/VSCode/Handlers.hs view
@@ -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
src/Language/Rzk/VSCode/Lsp.hs view
@@ -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 }
+ src/Rzk/Format.hs view
@@ -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
src/Rzk/Main.hs view
@@ -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