diff --git a/.github/workflows/ghcjs.yml b/.github/workflows/ghcjs.yml index 9bdf67935..391d65630 100644 --- a/.github/workflows/ghcjs.yml +++ b/.github/workflows/ghcjs.yml @@ -92,6 +92,16 @@ jobs: clean: false single-commit: true + - name: '🚀 Publish JS "binaries" (latest)' + if: ${{ startsWith(github.ref, 'refs/tags/') && startsWith(github.ref_name, 'v') && github.event_name == 'push' }} + uses: JamesIves/github-pages-deploy-action@v4 + with: + token: ${{ secrets.GITHUB_TOKEN }} + folder: rzk-playground-release + target-folder: latest/playground + clean: false + single-commit: true + - name: '🚀 Publish JS "binaries"' if: ${{ github.ref_name == 'main' && github.event_name == 'push' }} uses: JamesIves/github-pages-deploy-action@v4 diff --git a/CITATION.cff b/CITATION.cff index 2b8940092..8f1b81569 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -3,6 +3,10 @@ authors: - family-names: Kudasov given-names: Nikolai orcid: "https://orcid.org/0000-0001-6572-7292" + - family-names: Abounegm + given-names: Abdelrahman + - family-names: Danko + given-names: Danila title: "Rzk: a proof assistant for synthetic $\\infty$-categories" -version: 0.6.7 +version: 0.7.0 url: "https://github.com/rzk-lang/rzk" diff --git a/README.md b/README.md index 40623508a..4a233160e 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,21 @@ -# rzk +# Rzk proof assistant -[![MkDocs](https://shields.io/badge/MkDocs-documentation-informational)](https://rzk-lang.github.io/rzk/) -[![Haddock](https://shields.io/badge/Haddock-documentation-informational)](https://rzk-lang.github.io/rzk/haddock/index.html) -[![GHCJS build](https://github.com/rzk-lang/rzk/actions/workflows/ghcjs.yml/badge.svg?branch=main)](https://github.com/rzk-lang/rzk/actions/workflows/ghcjs.yml) +[![Release](https://img.shields.io/github/v/release/rzk-lang/rzk.svg)](https://github.com/rzk-lang/rzk/releases/latest) +[![`rzk` on Hackage](https://img.shields.io/hackage/v/rzk)](http://hackage.haskell.org/package/rzk) +[![`rzk` on Stackage Nightly](https://stackage.org/package/rzk/badge/nightly)](http://stackage.org/package/rzk) +[![`rzk` on Stackage LTS](https://stackage.org/package/rzk/badge/lts)](http://stackage.org/package/rzk) + +[![Rzk documentation](https://shields.io/badge/MkDocs-Rzk%20documentation-informational)](https://rzk-lang.github.io/rzk/) +[![Rzk Playground]()](https://rzk-lang.github.io/rzk/latest/playground/) [![Rzk Zulip chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://rzk-lang.zulipchat.com) +[![Haddock]()](https://rzk-lang.github.io/rzk/haddock/index.html) +[![Rzk Playground]()](https://rzk-lang.github.io/rzk/develop/playground/) + An experimental proof assistant for synthetic ∞-categories. + + [![Early prototype demo.](images/split-demo-render.png)](https://rzk-lang.github.io/rzk/) ## About this project @@ -80,6 +89,26 @@ Inside of such directory, you can run `rzk typecheck` on all files using wildcar rzk typecheck *-*.md ``` +### Formatting + +Formatting can be done by calling `rzk format` and specifying the files to be formatted, e.g.: + +```sh +rzk format file1.rzk file2.rzk +``` + +This prints the formatted version of the file to `stdout`. + +To overwrite the file content, you must use the `--write` flag as such: + +```sh +rzk format --write examples/*.rzk related/*.rzk.md +``` + +Note that if no files are specified, `rzk format` will format all files listed in `rzk.yaml`. + +The CLI also supports the `--check` flag, which will exit with a non-zero exit code if any of the files are not formatted correctly. This is useful in CI pipelines to ensure that all files are formatted correctly. + ## How to contribute to `rzk` ### Building the Documentation Locally diff --git a/docs/docs/CHANGELOG.md b/docs/docs/CHANGELOG.md index 58a024af4..dedf7a500 100644 --- a/docs/docs/CHANGELOG.md +++ b/docs/docs/CHANGELOG.md @@ -6,6 +6,29 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.7.0 — 2023-12-08 + +Major changes: + +- Add an experimental `rzk format` command (by [Abdelrahman Abounegm](https://github.com/aabounegm), with feedback by [Fredrik Bakke](https://github.com/fredrik-bakke) (see [sHoTT#142](https://github.com/rzk-lang/sHoTT/pull/142)) and [Nikolai Kudasov](https://github.com/fizruk)): + - Automatically format files, partially automating the [Code Style of the sHoTT project](https://rzk-lang.github.io/sHoTT/STYLEGUIDE/) + - Notable features: + - Adds a space after the opening parenthesis to help with the [code tree structure](https://rzk-lang.github.io/sHoTT/STYLEGUIDE/#the-tree-structure-of-constructions) + - Puts the definition conclusion (type, starting with `:`) and construction (body, starting with `:=`) on new lines + - Adds a space after the `\` of a lambda term and around binary operators (like `,`) + - Moves binary operators to the beginning of the next line if they appear at the end of the previous one. + - Replaces [common ASCII sequences](https://rzk-lang.github.io/sHoTT/STYLEGUIDE/#use-of-unicode-characters) with their Unicode equivalent + - A CLI subcommand (`rzk format`) with `--check` and `--write` options + - Known limitations + - The 80 character line limit is currently not enforced due to the difficulty of determining where to add line breaks (for reference, check out [this post](https://journal.stuffwithstuff.com/2015/09/08/the-hardest-program-ive-ever-written/) by a Dart `fmt` engineer) + - Fixing indentation is not yet implemented due to the need for more semantics than the lexer provides to determine indentation level. + - There may be rare edge cases in which applying the formatter twice could result in additional edits that were not detected the first time. + +Minor changes: + +- Fix "latest" Rzk Playground link (see [#137](https://github.com/rzk-lang/rzk/pull/137)); +- Add more badges to README (see [#136](https://github.com/rzk-lang/rzk/pull/136)); + ## 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/flake.lock b/flake.lock index 8f9e48b36..597cef8b0 100644 --- a/flake.lock +++ b/flake.lock @@ -84,17 +84,17 @@ }, "nixpkgs": { "locked": { - "lastModified": 1694934517, - "narHash": "sha256-U9aI4/jw+kYTZye4LJC2eIU30SqvZgL/UeRY4VHIjK8=", + "lastModified": 1701842937, + "narHash": "sha256-xIhu/49t/xQaHQu/XyOI1HkK7Lva1dMosD1TM4P+iWc=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "e1b4c97ed4ce160afd9ef1574b6a2ff168482f2a", + "rev": "d1c3a8112f9d5d4840e0669727222e5fd9243451", "type": "github" }, "original": { "owner": "NixOS", "repo": "nixpkgs", - "rev": "e1b4c97ed4ce160afd9ef1574b6a2ff168482f2a", + "rev": "d1c3a8112f9d5d4840e0669727222e5fd9243451", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 595a589e8..14ab88ce5 100644 --- a/flake.nix +++ b/flake.nix @@ -1,7 +1,7 @@ { inputs = { flake-utils.url = "github:numtide/flake-utils"; - nixpkgs.url = "github:NixOS/nixpkgs/e1b4c97ed4ce160afd9ef1574b6a2ff168482f2a"; + nixpkgs.url = "github:NixOS/nixpkgs/d1c3a8112f9d5d4840e0669727222e5fd9243451"; miso = { url = "github:dmjio/miso/49edf0677253bbcdd473422b5dd5b4beffd83910"; flake = false; @@ -47,6 +47,7 @@ packages = { default = default.packages.default; rzk = default.packages.${rzk}; + rzk-ghcjs = ghcjs.packages.${rzk}; rzk-js = ghcjs.packages.${rzk-js}; } // scripts; diff --git a/hie.yaml b/hie.yaml index f0c7014d7..4ef275e05 100644 --- a/hie.yaml +++ b/hie.yaml @@ -1,2 +1,2 @@ cradle: - cabal: \ No newline at end of file + stack: diff --git a/nix/ghcjs.nix b/nix/ghcjs.nix index f243e9511..884e1ef04 100644 --- a/nix/ghcjs.nix +++ b/nix/ghcjs.nix @@ -1,34 +1,40 @@ { inputs, pkgs, scripts, rzk, rzk-js, rzk-src, rzk-js-src, ghcVersion, tools }: let inherit (pkgs.haskell.lib) overrideCabal; - misoNix = (import "${inputs.miso.outPath}/default.nix" { inherit (pkgs) system; }); + misoNix = (import "${inputs.miso}/default.nix" { inherit (pkgs) system; }); pkgsMiso = misoNix.pkgs; hpkgs = - # This isn't equivalent to `pkgsMiso.haskell.packages.ghcjs.override` ([link](https://nixos.wiki/wiki/Haskell#Overrides)) - # but avoids multiple rebuilds - pkgsMiso.haskell.packages.ghcjs // - { - rzk = overrideCabal - (hpkgs.callCabal2nix rzk rzk-src { }) - (x: { - isLibrary = true; - isExecutable = false; + pkgsMiso.haskell.packages.ghcjs.override { + overrides = final: prev: { + mkDerivation = args: prev.mkDerivation (args // { doCheck = false; doHaddock = false; - libraryToolDepends = [ pkgs.hpack pkgs.alex pkgs.happy ] ++ (x.libraryToolDepends or [ ]); - testToolDepends = [ pkgs.hpack pkgs.alex pkgs.happy ] ++ (x.testToolDepends or [ ]); - prePatch = "hpack --force"; }); - rzk-js = overrideCabal - (hpkgs.callCabal2nix rzk-js rzk-js-src { inherit (hpkgs) rzk; }) - (x: { - postInstall = (x.postInstall or "") + '' - cp $out/bin/${rzk-js} . - rm -r $out - cp ${rzk-js} $out - ''; + hpack = pkgs.hpack; + rzk = ( + (pkgsMiso.haskell.lib.overrideCabal + (prev.callCabal2nix rzk rzk-src { }) + (x: { + isLibrary = true; + isExecutable = false; + buildTarget = "lib:rzk"; + libraryToolDepends = [ pkgs.hpack pkgs.alex pkgs.happy ] ++ (x.libraryToolDepends or [ ]); + testToolDepends = [ pkgs.alex pkgs.happy ] ++ (x.testToolDepends or [ ]); + })) + ).overrideAttrs (x: { + installPhase = builtins.replaceStrings [ "Setup copy" ] [ "Setup copy lib:rzk" ] x.installPhase; }); + rzk-js = overrideCabal + (final.callCabal2nix rzk-js rzk-js-src { }) + (x: { + postInstall = (x.postInstall or "") + '' + cp $out/bin/${rzk-js} . + rm -r $out + cp ${rzk-js} $out + ''; + }); + }; }; hpkgsGHCJS_8_10_7 = pkgs.haskell.packages.ghcjs810.override ({ diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md index 58a024af4..cdec72ed9 100644 --- a/rzk/ChangeLog.md +++ b/rzk/ChangeLog.md @@ -6,6 +6,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), 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/rzk/app/Main.hs b/rzk/app/Main.hs index 5277b0eaa..fcef0a7cf 100644 --- a/rzk/app/Main.hs +++ b/rzk/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 + 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 - Rzk.Main.main + + 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/package.yaml b/rzk/package.yaml index 1a92ad2a3..6bfaa278f 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -1,5 +1,5 @@ name: rzk -version: 0.6.7 +version: 0.7.0 github: "rzk-lang/rzk" license: BSD3 author: "Nikolai Kudasov" @@ -45,7 +45,6 @@ dependencies: directory: ">= 1.2.7.0" Glob: ">= 0.9.3" 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" @@ -72,11 +71,12 @@ library: - Language.Rzk.Syntax.Skel - condition: 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 dependencies: aeson: ">= 1.4.2.0" co-log-core: ">= 0.3.2.0" @@ -102,6 +102,7 @@ executables: - condition: "!impl(ghcjs)" dependencies: with-utf8: ">= 1.0.2.4" + optparse-generic: ">= 1.4.0" tests: rzk-test: diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index e5a48f94f..5245b3c7c 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -5,7 +5,7 @@ cabal-version: 1.24 -- 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 @@ library Language.Rzk.Syntax.Par Language.Rzk.Syntax.Print Rzk + Rzk.Format Rzk.Main Rzk.Project.Config Rzk.TypeCheck @@ -70,18 +71,18 @@ library , 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 @@ executable rzk , 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 @@ executable rzk 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 @@ test-suite doctests , 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 @@ test-suite rzk-test , 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/rzk/src/Language/Rzk/VSCode/Config.hs b/rzk/src/Language/Rzk/VSCode/Config.hs new file mode 100644 index 000000000..4aef05372 --- /dev/null +++ b/rzk/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/rzk/src/Language/Rzk/VSCode/Env.hs b/rzk/src/Language/Rzk/VSCode/Env.hs index 263633580..1305f78e7 100644 --- a/rzk/src/Language/Rzk/VSCode/Env.hs +++ b/rzk/src/Language/Rzk/VSCode/Env.hs @@ -3,7 +3,8 @@ module Language.Rzk.VSCode.Env where 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 @@ defaultRzkEnv = do { 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/rzk/src/Language/Rzk/VSCode/Handlers.hs b/rzk/src/Language/Rzk/VSCode/Handlers.hs index d1b2bd01f..ab9a06f92 100644 --- a/rzk/src/Language/Rzk/VSCode/Handlers.hs +++ b/rzk/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.Lens (HasDetail (detail), 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 @@ import Language.Rzk.Free.Syntax (RzkPosition (RzkPosition), 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 @@ provideCompletions req res = do (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/rzk/src/Language/Rzk/VSCode/Lsp.hs b/rzk/src/Language/Rzk/VSCode/Lsp.hs index d3514e583..9a99d0ac6 100644 --- a/rzk/src/Language/Rzk/VSCode/Lsp.hs +++ b/rzk/src/Language/Rzk/VSCode/Lsp.hs @@ -6,6 +6,7 @@ module Language.Rzk.VSCode.Lsp where 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.Protocol.Types 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 @@ handlers = -- 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 @@ handlers = 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 @@ handlers = return () Right list -> responder (Right (InL SemanticTokens { _resultId = Nothing, _data_ = list })) + , requestHandler SMethod_TextDocumentFormatting formatDocument ] @@ -94,11 +101,14 @@ runLsp = do 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/rzk/src/Rzk/Format.hs b/rzk/src/Rzk/Format.hs new file mode 100644 index 000000000..35fd55866 --- /dev/null +++ b/rzk/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/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs index ecd750184..cde9a45a9 100644 --- a/rzk/src/Rzk/Main.hs +++ b/rzk/src/Rzk/Main.hs @@ -1,6 +1,3 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} @@ -8,53 +5,16 @@ 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 @@ -82,9 +42,26 @@ extractFilesFromRzkYaml rzkYamlPath = do 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 diff --git a/stack.yaml b/stack.yaml index 53ac76292..b6882cb84 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,3 +1,3 @@ -resolver: nightly-2023-09-30 +resolver: nightly-2023-12-08 packages: - rzk diff --git a/stack.yaml.lock b/stack.yaml.lock index a51a2da7e..b2aeb774b 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -6,7 +6,7 @@ packages: [] snapshots: - completed: - sha256: 402c22fcb980c23c960ce8249d20c572f26abb1395a5d581e71244e7635bc578 - size: 670169 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2023/9/30.yaml - original: nightly-2023-09-30 + sha256: 4bd22736896cecf9e1f3f6193e82b065d06c2bf5b5ec97d0079409d6d35f1f82 + size: 710668 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2023/12/8.yaml + original: nightly-2023-12-08