Formatter - initial basic implementation

README.md

@@ -89,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

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;
 

hie.yaml

@@ -1,2 +1,2 @@
 cradle:
-  cabal:
+  stack:

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 ({

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)
+

rzk/package.yaml

@@ -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:

rzk/rzk.cabal

@@ -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,15 +114,15 @@ 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
     , yaml >=0.11.0.0
   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

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
+          ]
+      ]

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 ()