Add juvix format command (#1886)

This PR adds `juvix format` that can be used to format either a single
Juvix file or all files in a Juvix project.

## Usage

```
$ juvix format --help
Usage: juvix format JUVIX_FILE_OR_PROJECT [--check] [--in-place]

  Format a Juvix file or Juvix project

  When the command is run with an unformatted file it prints the reformatted source to standard output.
  When the command is run with a project directory it prints a list of unformatted files in the project.

Available options:
  JUVIX_FILE_OR_PROJECT    Path to a .juvix file or to a directory containing a
                           Juvix project.
  --check                  Do not print reformatted sources or unformatted file
                           paths to standard output.
  --in-place               Do not print reformatted sources to standard output.
                           Overwrite the target's contents with the formatted
                           version if the formatted version differs from the
                           original content.
  -h,--help                Show this help text
```

## Location of main implementation

The implementation is split into two components:
* The src API: `format` and `formatProject`
73952ba15c/src/Juvix/Formatter.hs
* The CLI interface:  

73952ba15c/app/Commands/Format.hs

## in-place uses polysemy Resource effect

The `--in-place` option makes a backup of the target file and restores
it if there's an error during processing to avoid data loss. The
implementation of this uses the polysemy [Resource
effect](https://hackage.haskell.org/package/polysemy-1.9.0.0/docs/Polysemy-Resource.html).
The recommended way to interpret the resource effect is to use
`resourceToIOFinal` which makes it necessary to change the effects
interpretation in main to use `Final IO`:
73952ba15c/app/Main.hs (L15)

## Format input is `FilePath`

The format options uses `FilePath` instead of `AppFile f` for the input
file/directory used by other commands. This is because we cannot
determine if the input string is a file or directory in the CLI parser
(we require IO). I discussed some ideas with @janmasrovira on how to
improve this in a way that would also solve other issues with CLI input
file/parsing but I want to defer this to a separate PR as this one is
already quite large.

One consequence of Format using `FilePath` as the input option is that
the code that changes the working directory to the root of the project
containing the CLI input file is changed to work with `FilePath`:


f715ef6a53/app/TopCommand/Options.hs (L33)

## New dependencies

This PR adds new dependencies on `temporary` and `polysemy-zoo`.

`temporary` is used for `emptySystemTempFile` in the implementation of
the TempFile interpreter for IO:


73952ba15c/src/Juvix/Data/Effect/Files/IO.hs (L49)

`polysemy-zoo` is used for the `Fresh` effect and `absorbMonadThrow` in
the implementation of the pure TempFile interpreter:

73952ba15c/src/Juvix/Data/Effect/Files/Pure.hs (L91)

NB: The pure TempFile interpreter is not used, but it seemed a good idea
to include it while it's fresh in my mind.

* Closes https://github.com/anoma/juvix/issues/1777

---------

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>

.github/workflows/ci.yml

@@ -17,11 +17,13 @@ name: The Juvix compiler CI
       - reopened
       - synchronize
       - ready_for_review
+
 concurrency:
   group: "${{ github.workflow }}-${{ github.head_ref || github.run_id }}"
   cancel-in-progress: true
+
 env:
-  SKIP: ormolu,format-juvix-examples
+  SKIP: ormolu,format-juvix-examples,typecheck-juvix-examples
 
 jobs:
   pre-commit:
@@ -116,7 +118,8 @@ jobs:
         if: ${{ success() }}
         run: |
           cd main
-          make -s juvix-format
+          make -s check-format-juvix-examples
+          make -s typecheck-juvix-examples
 
       - name: Add ~/.local/bin to PATH
         run: |
@@ -313,7 +316,8 @@ jobs:
         if: ${{ success() }}
         run: |
           cd main
-          make -s juvix-format
+          make -s check-format-juvix-examples
+          make -s typecheck-juvix-examples
 
       - name: Install Smoke
         uses: jaxxstorm/action-install-gh-release@v1.10.0

.pre-commit-config.yaml

@@ -43,11 +43,19 @@ repos:
   - repo: local
     hooks:
       - id: format-juvix-examples
-        name: typecheck and format Juvix examples
-        entry: make -s juvix-format
+        name: format Juvix examples
+        entry: make -s format-juvix-examples
         language: system
         verbose: false
         pass_filenames: false
+
+      - id: typecheck-juvix-examples
+        name: typecheck Juvix examples
+        entry: make -s typecheck-juvix-examples
+        language: system
+        verbose: false
+        pass_filenames: false
+
       - id: ormolu
         name: format Haskell code with ormolu
         entry: make -s ormolu

Makefile

@@ -122,19 +122,27 @@ format:
 clang-format:
 	@cd runtime && ${MAKE} format
 
-TOFORMATJUVIXFILES = ./examples
-TOFORMAT = $(shell find ${TOFORMATJUVIXFILES} -name "*.juvix" -print)
+JUVIXEXAMPLEFILES=$(shell find ./examples -name "*.juvix" -print)
+JUVIXFORMATFLAGS?=--in-place
+JUVIXTYPECHECKFLAGS?=--only-errors
 
-$(TOFORMAT): %:
-	@echo "Formatting $@"
-	@juvix dev scope $@ --with-comments > $@.tmp
-	@mv $@.tmp $@
-	@echo "Typechecking formatted $@"
-	@juvix typecheck $@ --only-errors
+.PHONY: format-juvix-examples
+format-juvix-examples:
+	@for file in $(JUVIXEXAMPLEFILES); do \
+		juvix format $(JUVIXFORMATFLAGS) "$$file"; \
+	done
 
-.PHONY: $(TOFORMAT)
-juvix-format:
-	@${MAKE} $(TOFORMAT)
+.PHONY: check-format-juvix-examples
+check-format-juvix-examples:
+	@export JUVIXFORMATFLAGS=--check
+	@${MAKE} format-juvix-examples
+
+.PHONY: typecheck-juvix-examples
+typecheck-juvix-examples:
+	@for file in $(JUVIXEXAMPLEFILES); do \
+		echo "Checking $$file"; \
+		juvix typecheck "$$file" $(JUVIXTYPECHECKFLAGS); \
+	done
 
 .PHONY: check-ormolu
 check-ormolu: export ORMOLUMODE = check
@@ -175,8 +183,10 @@ check-only:
 	@${MAKE} install
 	@${MAKE} test
 	@${MAKE} smoke
-	@${MAKE} juvix-format
-	@${MAKE} format
+	@${MAKE} check-format-juvix-examples
+	@${MAKE} typecheck-juvix-examples
+	@${MAKE} check-ormolu
+	@export SKIP=ormolu,format-juvix-examples,typecheck-juvix-examples
 	@${MAKE} pre-commit
 
 .PHONY: check

app/App.hs

@@ -8,6 +8,7 @@ import Juvix.Compiler.Pipeline
 import Juvix.Data.Error qualified as Error
 import Juvix.Prelude.Pretty hiding (Doc)
 import System.Console.ANSI qualified as Ansi
+import System.Directory qualified as D
 
 data App m a where
   ExitMsg :: ExitCode -> Text -> App m a
@@ -62,7 +63,7 @@ runAppIO args@RunAppIOArgs {..} =
     ExitJuvixError e -> do
       printErr e
       embed exitFailure
-    ExitMsg exitCode t -> embed (putStrLn t >> exitWith exitCode)
+    ExitMsg exitCode t -> embed (putStrLn t >> hFlush stdout >> exitWith exitCode)
     SayRaw b -> embed (ByteString.putStr b)
   where
     g :: GlobalOptions
@@ -90,6 +91,15 @@ someBaseToAbs' f = do
   r <- askInvokeDir
   return (someBaseToAbs r f)
 
+filePathToAbs :: Members '[Embed IO, App] r => FilePath -> Sem r (Either (Path Abs File) (Path Abs Dir))
+filePathToAbs fp = do
+  invokeDir <- askInvokeDir
+  absPath <- embed (D.canonicalizePath (toFilePath invokeDir </> fp))
+  isDirectory <- embed (D.doesDirectoryExist absPath)
+  if
+      | isDirectory -> Right <$> embed @IO (parseAbsDir absPath)
+      | otherwise -> Left <$> embed @IO (parseAbsFile absPath)
+
 askGenericOptions :: (Members '[App] r) => Sem r GenericOptions
 askGenericOptions = project <$> askGlobalOptions
 

app/Commands/Format.hs

@@ -0,0 +1,61 @@
+module Commands.Format where
+
+import Commands.Base
+import Commands.Format.Options
+import Juvix.Formatter
+import Juvix.Prelude.Pretty
+
+data FormatNoEditRenderMode
+  = ReformattedFile (NonEmpty AnsiText)
+  | InputPath (Path Abs File)
+  | Silent
+
+data FormatRenderMode
+  = EditInPlace FormattedFileInfo
+  | NoEdit FormatNoEditRenderMode
+
+data FormatTarget
+  = TargetFile
+  | TargetDir
+
+runCommand :: forall r. Members '[Embed IO, App, Resource, Files] r => FormatOptions -> Sem r ()
+runCommand opts = do
+  f <- filePathToAbs (opts ^. formatInput)
+  let target = case f of
+        Left {} -> TargetFile
+        Right {} -> TargetDir
+  runOutputSem (renderFormattedOutput target opts) $ runScopeFileApp $ do
+    res <- case f of
+      Left p -> format p
+      Right p -> formatProject p
+    when (res == FormatResultFail) (embed (exitWith (ExitFailure 1)))
+
+renderModeFromOptions :: FormatTarget -> FormatOptions -> FormattedFileInfo -> FormatRenderMode
+renderModeFromOptions target opts formattedInfo
+  | opts ^. formatInPlace = EditInPlace formattedInfo
+  | opts ^. formatCheck = NoEdit Silent
+  | otherwise = case target of
+      TargetFile -> NoEdit (ReformattedFile (formattedInfo ^. formattedFileInfoContentsAnsi))
+      TargetDir -> NoEdit (InputPath (formattedInfo ^. formattedFileInfoPath))
+
+renderFormattedOutput :: forall r. Members '[Embed IO, App, Resource, Files] r => FormatTarget -> FormatOptions -> FormattedFileInfo -> Sem r ()
+renderFormattedOutput target opts fInfo = do
+  let renderMode = renderModeFromOptions target opts fInfo
+  outputResult renderMode
+  where
+    outputResult :: FormatRenderMode -> Sem r ()
+    outputResult = \case
+      EditInPlace i@(FormattedFileInfo {..}) ->
+        runTempFileIO $
+          restoreFileOnError _formattedFileInfoPath $
+            writeFile' _formattedFileInfoPath (i ^. formattedFileInfoContentsText)
+      NoEdit m -> case m of
+        ReformattedFile ts -> forM_ ts renderStdOut
+        InputPath p -> say (pack (toFilePath p))
+        Silent -> return ()
+
+runScopeFileApp :: Member App r => Sem (ScopeEff ': r) a -> Sem r a
+runScopeFileApp = interpret $ \case
+  ScopeFile p -> do
+    let appFile = AppPath (Abs p) False
+    runPipeline appFile upToScoping

app/Commands/Format/Options.hs

@@ -0,0 +1,36 @@
+module Commands.Format.Options where
+
+import CommonOptions
+
+data FormatOptions = FormatOptions
+  { _formatInput :: FilePath,
+    _formatCheck :: Bool,
+    _formatInPlace :: Bool
+  }
+  deriving stock (Data)
+
+makeLenses ''FormatOptions
+
+parseInputJuvixFileOrDir :: Parser FilePath
+parseInputJuvixFileOrDir =
+  strArgument
+    ( metavar "JUVIX_FILE_OR_PROJECT"
+        <> help "Path to a .juvix file or to a directory containing a Juvix project."
+        <> completer juvixCompleter
+        <> action "directory"
+    )
+
+parseFormat :: Parser FormatOptions
+parseFormat = do
+  _formatInput <- parseInputJuvixFileOrDir
+  _formatCheck <-
+    switch
+      ( long "check"
+          <> help "Do not print reformatted sources or unformatted file paths to standard output."
+      )
+  _formatInPlace <-
+    switch
+      ( long "in-place"
+          <> help "Do not print reformatted sources to standard output. Overwrite the target's contents with the formatted version if the formatted version differs from the original content."
+      )
+  pure FormatOptions {..}

app/Main.hs

@@ -12,4 +12,4 @@ main = do
   _runAppIOArgsInvokeDir <- getCurrentDir
   (_runAppIOArgsGlobalOptions, cli) <- customExecParser parserPreferences descr
   (_runAppIOArgsPkgDir, _runAppIOArgsPkg, _runAppIOArgsBuildDir) <- findRootAndChangeDir (topCommandInputFile cli) _runAppIOArgsGlobalOptions _runAppIOArgsInvokeDir
-  runM (runAppIO (RunAppIOArgs {..}) (runTopCommand cli))
+  runFinal (resourceToIOFinal (embedToFinal @IO (runAppIO (RunAppIOArgs {..}) (runTopCommand cli))))

app/Root.hs

@@ -12,14 +12,14 @@ type RootDir = Path Abs Dir
 type BuildDir = Path Abs Dir
 
 findRootAndChangeDir ::
-  Maybe (SomeBase File) ->
+  IO (Maybe (SomeBase Dir)) ->
   GlobalOptions ->
   Path Abs Dir ->
   IO (RootDir, Package, BuildDir)
 findRootAndChangeDir minputFile gopts invokeDir = do
-  whenJust minputFile $ \case
-    Abs d -> setCurrentDir (parent d)
-    Rel d -> setCurrentDir (parent d)
+  whenJustM minputFile $ \case
+    Abs d -> setCurrentDir d
+    Rel d -> setCurrentDir d
   r <- IO.try go
   case r of
     Left (err :: IO.SomeException) -> do

app/TopCommand.hs

@@ -1,10 +1,11 @@
 module TopCommand where
 
-import Commands.Base
+import Commands.Base hiding (Format)
 import Commands.Compile qualified as Compile
 import Commands.Dev qualified as Dev
 import Commands.Doctor qualified as Doctor
 import Commands.Eval qualified as Eval
+import Commands.Format qualified as Format
 import Commands.Html qualified as Html
 import Commands.Init qualified as Init
 import Commands.Repl qualified as Repl
@@ -21,7 +22,7 @@ showHelpText = do
       (msg, _) = renderFailure helpText progn
   putStrLn (pack msg)
 
-runTopCommand :: forall r. (Members '[Embed IO, App] r) => TopCommand -> Sem r ()
+runTopCommand :: forall r. (Members '[Embed IO, App, Resource] r) => TopCommand -> Sem r ()
 runTopCommand = \case
   DisplayVersion -> embed runDisplayVersion
   DisplayNumericVersion -> embed runDisplayNumericVersion
@@ -34,3 +35,4 @@ runTopCommand = \case
   Eval opts -> Eval.runCommand opts
   Html opts -> Html.runCommand opts
   JuvixRepl opts -> Repl.runCommand opts
+  JuvixFormat opts -> runFilesIO (Format.runCommand opts)

app/TopCommand/Options.hs

@@ -4,6 +4,7 @@ import Commands.Compile.Options
 import Commands.Dev.Options qualified as Dev
 import Commands.Doctor.Options
 import Commands.Eval.Options
+import Commands.Format.Options
 import Commands.Html.Options
 import Commands.Repl.Options
 import Commands.Typecheck.Options
@@ -11,6 +12,8 @@ import CommonOptions hiding (Doc)
 import Data.Generics.Uniplate.Data
 import GlobalOptions
 import Options.Applicative.Help.Pretty
+import Safe
+import System.Directory qualified as D
 
 data TopCommand
   = DisplayVersion
@@ -24,16 +27,30 @@ data TopCommand
   | Doctor DoctorOptions
   | Init
   | JuvixRepl ReplOptions
+  | JuvixFormat FormatOptions
   deriving stock (Data)
 
-topCommandInputFile :: TopCommand -> Maybe (SomeBase File)
-topCommandInputFile = firstJust getInputFile . universeBi
+topCommandInputFile :: TopCommand -> IO (Maybe (SomeBase Dir))
+topCommandInputFile t = do
+  d <- getFilePath (universeBi t)
+  return $ (firstJust getInputFile (universeBi t)) <|> d
   where
-    getInputFile :: AppPath File -> Maybe (SomeBase File)
+    getInputFile :: AppPath File -> Maybe (SomeBase Dir)
     getInputFile p
-      | p ^. pathIsInput = Just (p ^. pathPath)
+      | p ^. pathIsInput = Just (mapSomeBase parent (p ^. pathPath))
       | otherwise = Nothing
 
+    getFilePath :: [FilePath] -> IO (Maybe (SomeBase Dir))
+    getFilePath fs = mapM go (headMay fs)
+      where
+        go :: FilePath -> IO (SomeBase Dir)
+        go fp = do
+          nfp <- D.canonicalizePath fp
+          isDirectory <- D.doesDirectoryExist nfp
+          if
+              | isDirectory -> parseSomeDir nfp
+              | otherwise -> mapSomeBase parent <$> (parseSomeFile nfp)
+
 parseDisplayVersion :: Parser TopCommand
 parseDisplayVersion =
   flag'
@@ -69,7 +86,8 @@ parseUtility =
           commandDoctor,
           commandInit,
           commandDev,
-          commandRepl
+          commandRepl,
+          commandFormat
         ]
     )
   where
@@ -98,6 +116,23 @@ parseUtility =
             (progDesc "Run the Juvix REPL")
         )
 
+    commandFormat :: Mod CommandFields TopCommand
+    commandFormat =
+      command "format" $
+        info
+          (JuvixFormat <$> parseFormat)
+          ( progDescDoc
+              ( Just
+                  ( vsep
+                      [ "Format a Juvix file or Juvix project",
+                        "",
+                        "When the command is run with an unformatted file it prints the reformatted source to standard output.",
+                        "When the command is run with a project directory it prints a list of unformatted files in the project."
+                      ]
+                  )
+              )
+          )
+
 commandCheck :: Mod CommandFields TopCommand
 commandCheck =
   command "typecheck" $

package.yaml

@@ -55,6 +55,7 @@ dependencies:
   - path-io == 1.7.*
   - polysemy == 1.7.*
   - polysemy-plugin == 0.4.*
+  - polysemy-zoo == 0.8.*
   - pretty == 1.1.*
   - prettyprinter == 1.7.*
   - prettyprinter-ansi-terminal == 1.1.*
@@ -64,6 +65,7 @@ dependencies:
   - singletons-th == 3.1.*
   - Stream == 0.4.*
   - template-haskell == 2.18.*
+  - temporary == 1.3.*
   - text == 1.2.*
   - th-utilities == 0.2.*
   - time == 1.11.*

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/PathResolver.hs

@@ -77,7 +77,7 @@ mkPackageInfo mpackageEntry _packageRoot = do
   return PackageInfo {..}
   where
     juvixAccum :: Path Abs Dir -> [Path Rel Dir] -> [Path Rel File] -> [Path Abs File] -> Sem r ([Path Abs File], Recurse Rel)
-    juvixAccum cd _ files acc = return (newJuvixFiles <> acc, RecurseFilter (not . isHiddenDirectory))
+    juvixAccum cd _ files acc = return (newJuvixFiles <> acc, RecurseFilter (\hasJuvixYaml d -> not hasJuvixYaml || not (isHiddenDirectory d)))
       where
         newJuvixFiles :: [Path Abs File]
         newJuvixFiles = [cd <//> f | f <- files, isJuvixFile f]

src/Juvix/Data/Effect/Files.hs

@@ -10,6 +10,7 @@ import Data.HashSet qualified as HashSet
 import Juvix.Data.Effect.Files.Base
 import Juvix.Data.Effect.Files.IO
 import Juvix.Data.Effect.Files.Pure (runFilesPure)
+import Juvix.Extra.Paths.Base
 import Juvix.Prelude.Base
 import Juvix.Prelude.Path
 
@@ -47,11 +48,12 @@ walkDirRel handler topdir = do
       walktree curdir = do
         let fullDir :: Path Abs Dir = topdir <//> curdir
         (subdirs, files) <- listDirRel fullDir
+        let hasJuvixYaml = juvixYamlFile `elem` files
         action <- raise (handler fullDir subdirs files)
         case action of
           RecurseNever -> return ()
           RecurseFilter fi ->
-            let ds = map (curdir <//>) (filter fi subdirs)
+            let ds = map (curdir <//>) (filter (fi hasJuvixYaml) subdirs)
              in mapM_ walkAvoidLoop ds
       checkLoop :: Path Abs Dir -> Sem (State (HashSet Uid) ': r) Bool
       checkLoop dir = do
@@ -61,3 +63,14 @@ walkDirRel handler topdir = do
             | HashSet.member ufid visited -> return True
             | otherwise -> modify' (HashSet.insert ufid) $> False
   evalState mempty (walkAvoidLoop $(mkRelDir "."))
+
+-- | Restore the original contents of a file if an error occurs in an action.
+restoreFileOnError :: forall r a. Members '[Resource, Files, TempFile] r => Path Abs File -> Sem r a -> Sem r a
+restoreFileOnError p action = do
+  t <- tempFilePath
+  finally (restoreOnErrorAction t) (removeTempFile t)
+  where
+    restoreOnErrorAction :: Path Abs File -> Sem r a
+    restoreOnErrorAction tmpFile = do
+      copyFile' p tmpFile
+      onException action (renameFile' tmpFile p)

src/Juvix/Data/Effect/Files/Base.hs

@@ -16,10 +16,16 @@ data RecursorArgs = RecursorArgs
 
 data Recurse r
   = RecurseNever
-  | RecurseFilter (Path r Dir -> Bool)
+  | RecurseFilter (Bool -> Path r Dir -> Bool)
 
 makeLenses ''RecursorArgs
 
+data TempFile m a where
+  TempFilePath :: TempFile m (Path Abs File)
+  RemoveTempFile :: Path Abs File -> TempFile m ()
+
+makeSem ''TempFile
+
 data Files m a where
   EnsureDir' :: Path Abs Dir -> Files m ()
   DirectoryExists' :: Path Abs Dir -> Files m Bool
@@ -32,5 +38,8 @@ data Files m a where
   RemoveDirectoryRecursive' :: Path Abs Dir -> Files m ()
   WriteFile' :: Path Abs File -> Text -> Files m ()
   WriteFileBS :: Path Abs File -> ByteString -> Files m ()
+  RemoveFile' :: Path Abs File -> Files m ()
+  RenameFile' :: Path Abs File -> Path Abs File -> Files m ()
+  CopyFile' :: Path Abs File -> Path Abs File -> Files m ()
 
 makeSem ''Files

src/Juvix/Data/Effect/Files/IO.hs

@@ -4,35 +4,56 @@ module Juvix.Data.Effect.Files.IO
   )
 where
 
+import Control.Monad.Catch qualified as MC
 import Data.ByteString qualified as ByteString
 import Juvix.Data.Effect.Files.Base
 import Juvix.Prelude.Base
 import Juvix.Prelude.Path
 import Path.IO qualified as Path
+import System.IO.Error
+import System.IO.Temp
 import System.Posix.Types qualified as P
 import System.PosixCompat.Files qualified as P
 
 runFilesIO ::
   forall r a.
-  (Member (Embed IO) r) =>
+  (Members '[Embed IO] r) =>
   Sem (Files ': r) a ->
   Sem r a
 runFilesIO = interpret helper
   where
     helper :: forall rInitial x. Files (Sem rInitial) x -> Sem r x
-    helper = \case
-      ReadFile' f -> embed (readFile (toFilePath f))
-      WriteFileBS p bs -> embed (ByteString.writeFile (toFilePath p) bs)
-      WriteFile' f txt -> embed (writeFile (toFilePath f) txt)
+    helper = embed . helper'
+
+    helper' :: forall rInitial x. Files (Sem rInitial) x -> IO x
+    helper' = \case
+      ReadFile' f -> readFile (toFilePath f)
+      WriteFileBS p bs -> ByteString.writeFile (toFilePath p) bs
+      WriteFile' f txt -> writeFile (toFilePath f) txt
       EnsureDir' p -> Path.ensureDir p
       DirectoryExists' p -> Path.doesDirExist p
-      ReadFileBS' f -> embed (ByteString.readFile (toFilePath f))
+      ReadFileBS' f -> ByteString.readFile (toFilePath f)
       FileExists' f -> Path.doesFileExist f
       RemoveDirectoryRecursive' d -> removeDirRecur d
-      ListDirRel p -> embed @IO (Path.listDirRel p)
+      ListDirRel p -> Path.listDirRel p
       PathUid f -> do
-        status <- embed (P.getFileStatus (toFilePath f))
+        status <- P.getFileStatus (toFilePath f)
         let P.CDev dev = P.deviceID status
             P.CIno fid = P.fileID status
         return (Uid (dev, fid))
       GetDirAbsPath f -> canonicalizePath f
+      RemoveFile' f -> Path.removeFile f
+      RenameFile' p1 p2 -> Path.renameFile p1 p2
+      CopyFile' p1 p2 -> Path.copyFile p1 p2
+
+runTempFileIO ::
+  forall r a.
+  Members '[Embed IO] r =>
+  Sem (TempFile ': r) a ->
+  Sem r a
+runTempFileIO = interpret $ \case
+  TempFilePath -> embed (emptySystemTempFile "tmp" >>= parseAbsFile)
+  RemoveTempFile p -> embed (ignoringIOErrors (Path.removeFile p))
+    where
+      ignoringIOErrors :: IO () -> IO ()
+      ignoringIOErrors ioe = MC.catch ioe (\(_ :: IOError) -> return ())

src/Juvix/Data/Effect/Files/Pure.hs

@@ -2,9 +2,12 @@ module Juvix.Data.Effect.Files.Pure where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.Tree
+import Data.Unique
 import Juvix.Data.Effect.Files.Base
 import Juvix.Prelude.Base
 import Juvix.Prelude.Path
+import Polysemy.ConstraintAbsorber.MonadCatch
+import Polysemy.Fresh
 import Prelude qualified
 
 data FS = FS
@@ -78,10 +81,27 @@ re cwd = reinterpret $ \case
   ListDirRel p -> do
     n <- lookupDir' p
     return (HashMap.keys (n ^. dirDirs), HashMap.keys (n ^. dirFiles))
+  RemoveFile' p -> removeFileHelper p
+  RenameFile' p1 p2 -> renameFileHelper p1 p2
+  CopyFile' p1 p2 -> copyFileHelper p1 p2
   where
     cwd' :: FilePath
     cwd' = toFilePath cwd
 
+runTempFilePure ::
+  Members '[Files, Fresh Unique, Error SomeException] r =>
+  Sem (TempFile ': r) a ->
+  Sem r a
+runTempFilePure = interpret $ \case
+  TempFilePath -> do
+    tmpDir <- absorbMonadThrow (parseAbsDir "/tmp")
+    uid <- show . hashUnique <$> fresh
+    tmpFile <- absorbMonadThrow (parseRelFile uid)
+    let p = tmpDir <//> tmpFile
+    writeFile' p ""
+    return p
+  RemoveTempFile p -> removeFile' p
+
 missingErr :: (Members '[State FS] r) => FilePath -> Sem r a
 missingErr f = do
   root <- get @FS
@@ -140,6 +160,30 @@ writeFileHelper p contents = do
           helper :: Maybe FSNode -> FSNode
           helper = maybe (error "directory does not exist") (go ds)
 
+removeFileHelper :: (Members '[State FS] r) => Path Abs File -> Sem r ()
+removeFileHelper p = do
+  checkRoot r
+  modify (over fsNode (go dirs))
+  where
+    (r, dirs, f) = destructAbsFile p
+    go :: [Path Rel Dir] -> FSNode -> FSNode
+    go = \case
+      [] -> set (dirFiles . at f) Nothing
+      (d : ds) -> over dirDirs (HashMap.alter (Just . helper) d)
+        where
+          helper :: Maybe FSNode -> FSNode
+          helper = maybe (error "directory does not exist") (go ds)
+
+renameFileHelper :: (Members '[State FS] r) => Path Abs File -> Path Abs File -> Sem r ()
+renameFileHelper fromPath toPath = do
+  copyFileHelper fromPath toPath
+  removeFileHelper fromPath
+
+copyFileHelper :: (Members '[State FS] r) => Path Abs File -> Path Abs File -> Sem r ()
+copyFileHelper fromPath toPath = do
+  fromContents <- lookupFile' fromPath
+  writeFileHelper toPath fromContents
+
 lookupDir :: (Members '[State FS] r) => Path Abs Dir -> Sem r (Maybe FSNode)
 lookupDir p = do
   checkRoot p

src/Juvix/Extra/Paths/Base.hs

@@ -1,7 +1,8 @@
 module Juvix.Extra.Paths.Base where
 
 import Data.FileEmbed qualified as FE
-import Juvix.Prelude
+import Juvix.Prelude.Base
+import Juvix.Prelude.Path
 import Language.Haskell.TH.Syntax
 
 assetsDirQ :: Q Exp

src/Juvix/Formatter.hs

@@ -0,0 +1,108 @@
+module Juvix.Formatter where
+
+import Data.Text qualified as T
+import Juvix.Compiler.Concrete.Language
+import Juvix.Compiler.Concrete.Print (ppOutDefault)
+import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
+import Juvix.Prelude
+import Juvix.Prelude.Pretty
+
+data FormattedFileInfo = FormattedFileInfo
+  { _formattedFileInfoPath :: Path Abs File,
+    _formattedFileInfoContentsAnsi :: NonEmpty AnsiText
+  }
+
+data ScopeEff m a where
+  ScopeFile :: Path Abs File -> ScopeEff m Scoper.ScoperResult
+
+makeLenses ''FormattedFileInfo
+makeSem ''ScopeEff
+
+data FormatResult
+  = FormatResultOK
+  | FormatResultFail
+  deriving stock (Eq)
+
+combineResults :: [FormatResult] -> FormatResult
+combineResults rs
+  | FormatResultFail `elem` rs = FormatResultFail
+  | otherwise = FormatResultOK
+
+ansiPlainText :: NonEmpty AnsiText -> Text
+ansiPlainText = T.concat . toList . fmap toPlainText
+
+formattedFileInfoContentsText :: SimpleGetter FormattedFileInfo Text
+formattedFileInfoContentsText = to infoToPlainText
+  where
+    infoToPlainText :: FormattedFileInfo -> Text
+    infoToPlainText fInfo = ansiPlainText (fInfo ^. formattedFileInfoContentsAnsi)
+
+-- | Format a single Juvix file.
+--
+-- If the file requires formatting then the function returns FormatResultFail
+-- and outputs a FormattedFileInfo containing the formatted contents of the file.
+--
+-- If the file does not require formatting then the function returns
+-- FormatResultOK and nothing is output.
+format ::
+  forall r.
+  Members '[ScopeEff, Files, Output FormattedFileInfo] r =>
+  Path Abs File ->
+  Sem r FormatResult
+format p = do
+  originalContents <- readFile' p
+  formattedContents <- formatPath p
+  if
+      | originalContents /= (ansiPlainText formattedContents) -> do
+          output
+            ( FormattedFileInfo
+                { _formattedFileInfoPath = p,
+                  _formattedFileInfoContentsAnsi = formattedContents
+                }
+            )
+          return FormatResultFail
+      | otherwise -> return FormatResultOK
+
+-- | Format a Juvix project.
+--
+-- Format all files in the Juvix project containing the passed directory.
+--
+-- If any file requires formatting then the function returns FormatResultFail.
+-- This function also outputs a FormattedFileInfo (containing the formatted
+-- contents of a file) for every file in the project that requires formatting.
+--
+-- If all files in the project are already formatted then the function returns
+-- FormatResultOK and nothing is output.
+--
+-- NB: This function does not traverse into Juvix sub-projects, i.e into
+-- subdirectories that contain a juvix.yaml file.
+formatProject ::
+  forall r.
+  Members '[ScopeEff, Files, Output FormattedFileInfo] r =>
+  Path Abs Dir ->
+  Sem r FormatResult
+formatProject p = do
+  walkDirRelAccum handler p FormatResultOK
+  where
+    handler ::
+      Path Abs Dir ->
+      [Path Rel Dir] ->
+      [Path Rel File] ->
+      FormatResult ->
+      Sem r (FormatResult, Recurse Rel)
+    handler cd _ files _ = do
+      let juvixFiles = [cd <//> f | f <- files, isJuvixFile f]
+      res <- combineResults <$> mapM format juvixFiles
+      return (res, RecurseFilter (\hasJuvixYaml d -> not (hasJuvixYaml && isHiddenDirectory d)))
+
+formatPath :: Member ScopeEff r => Path Abs File -> Sem r (NonEmpty AnsiText)
+formatPath p = do
+  res <- scopeFile p
+  let cs = res ^. Scoper.comments
+      formattedModules = run (runReader cs (mapM formatTopModule (res ^. Scoper.resultModules)))
+  return formattedModules
+  where
+    formatTopModule :: Member (Reader Comments) r => Module 'Scoped 'ModuleTop -> Sem r AnsiText
+    formatTopModule m = do
+      cs <- ask
+      return (ppOutDefault cs m)

src/Juvix/Prelude/Base.hs

@@ -57,6 +57,7 @@ module Juvix.Prelude.Base
     module Polysemy.Fixpoint,
     module Polysemy.Output,
     module Polysemy.Reader,
+    module Polysemy.Resource,
     module Polysemy.State,
     module Language.Haskell.TH.Syntax,
     module Prettyprinter,
@@ -158,6 +159,7 @@ import Polysemy.Error hiding (fromEither)
 import Polysemy.Fixpoint
 import Polysemy.Output
 import Polysemy.Reader
+import Polysemy.Resource
 import Polysemy.State
 import Prettyprinter (Doc, (<+>))
 import Safe.Exact

src/Juvix/Prelude/Pretty.hs

@@ -81,6 +81,9 @@ toAnsiText useColors
   | useColors = Ansi.renderStrict . toAnsiStream
   | otherwise = Text.renderStrict . toTextStream
 
+toPlainText :: HasTextBackend a => a -> Text
+toPlainText = Text.renderStrict . toTextStream
+
 prettyText :: (Pretty a) => a -> Text
 prettyText = Text.renderStrict . layoutPretty defaultLayoutOptions . pretty
 

test/Format.hs

@@ -4,7 +4,6 @@ import Base
 import Juvix.Compiler.Builtins (iniState)
 import Juvix.Compiler.Concrete qualified as Concrete
 import Juvix.Compiler.Concrete.Print qualified as P
-import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser
 import Juvix.Compiler.Pipeline
@@ -25,16 +24,6 @@ root = relToProject $(mkRelDir "tests/positive")
 renderCode :: (HasLoc a, P.PrettyPrint a) => P.Comments -> a -> Text
 renderCode c = prettyText . P.ppOutDefault c
 
-type Pipe =
-  '[ PathResolver,
-     Reader EntryPoint,
-     Files,
-     NameIdGen,
-     Error JuvixError,
-     Reader GenericOptions,
-     Embed IO
-   ]
-
 posTest :: String -> Path Rel Dir -> Path Rel File -> PosTest
 posTest _name rdir rfile =
   let _dir = root <//> rdir

test/Formatter.hs

@@ -0,0 +1,7 @@
+module Formatter where
+
+import Base
+import Formatter.Positive qualified as P
+
+allTests :: TestTree
+allTests = testGroup "Formatter tests" [P.allTests]

test/Formatter/Positive.hs

@@ -0,0 +1,42 @@
+module Formatter.Positive where
+
+import Base
+import Juvix.Compiler.Builtins
+import Juvix.Compiler.Pipeline
+import Juvix.Formatter
+import Scope.Positive qualified
+import Scope.Positive qualified as Scope
+
+runScopeEffIO :: Member (Embed IO) r => Path Abs Dir -> Sem (ScopeEff ': r) a -> Sem r a
+runScopeEffIO testRoot' = interpret $ \case
+  ScopeFile p -> do
+    let entry = defaultEntryPoint testRoot' p
+    embed (snd <$> runIO' iniState entry upToScoping)
+
+makeFormatTest' :: Scope.PosTest -> TestDescr
+makeFormatTest' Scope.PosTest {..} =
+  let tRoot = Scope.Positive.root <//> _relDir
+      file' = tRoot <//> _file
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Single $ do
+            d <- runM $ runError $ runOutputList @FormattedFileInfo $ runScopeEffIO tRoot $ runFilesIO $ format file'
+            case d of
+              Right (_, FormatResultOK) -> return ()
+              Right (_, FormatResultFail) -> assertFailure ("File: " <> show file' <> " is not formatted")
+              Left {} -> assertFailure ("Error: ")
+        }
+
+filterOutTests :: [String] -> [Scope.PosTest] -> [Scope.PosTest]
+filterOutTests out = filter (\Scope.PosTest {..} -> _name `notElem` out)
+
+-- Ignore tests that use the stdlib
+ignoredTests :: [String]
+ignoredTests = ["Import embedded standard library", "Basic dependencies"]
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "Formatter positive tests"
+    (map (mkTest . makeFormatTest') (filterOutTests ignoredTests Scope.Positive.tests))

test/Main.hs

@@ -8,6 +8,7 @@ import Compilation qualified
 import Core qualified
 import Examples qualified
 import Format qualified
+import Formatter qualified
 import Internal qualified
 import Parsing qualified
 import Reachability qualified
@@ -39,7 +40,8 @@ fastTests =
       Arity.allTests,
       Typecheck.allTests,
       Reachability.allTests,
-      Format.allTests
+      Format.allTests,
+      Formatter.allTests
     ]
 
 main :: IO ()

tests/positive/Ape.juvix

@@ -1,29 +1,32 @@
 module Ape;
-  builtin string axiom String : Type;
 
-  infixl 7 *;
-  axiom * : String → String → String;
+builtin string axiom String : Type;
 
-  infixr 3 -;
-  axiom - : String → String → String;
+infixl 7 *;
+axiom * : String → String → String;
 
-  infixl 1 >>;
-  axiom >> : String → String → String;
+infixr 3 -;
+axiom - : String → String → String;
 
-  infixl 6 +;
-  axiom + : String → String → String;
+infixl 1 >>;
+axiom >> : String → String → String;
 
-  infixr 6 ++;
-  axiom ++ : String → String → String;
-  axiom f : String → String;
+infixl 6 +;
+axiom + : String → String → String;
 
-  x : String;
-  x := "" + ("" ++ "");
+infixr 6 ++;
+axiom ++ : String → String → String;
+axiom f : String → String;
 
-  axiom wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww : String → String;
+x : String;
+x := "" + ("" ++ "");
 
-  nesting : String;
-  nesting := wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
+axiom wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww : String
+  → String;
+
+nesting : String;
+nesting :=
+  wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
     (wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
       (wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
         (wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
@@ -45,8 +48,9 @@ module Ape;
                                         (wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
                                           ("" + "" + "" + "" + ""))))))))))))))))))));
 
-  t : String;
-  t := "Hellooooooooo"
+t : String;
+t :=
+  "Hellooooooooo"
     >> "Hellooooooooo"
     >> "Hellooooooooo"
     >> "Hellooooooooo"
@@ -70,4 +74,3 @@ module Ape;
         * "Hellooooooooo"
         * "Hellooooooooo"
         * "Hellooooooooo";
-end;

tests/positive/Axiom.juvix

@@ -1,5 +1,3 @@
 module Axiom;
 
 axiom Action : Type;
-
-end;

tests/positive/Builtins.juvix

@@ -1,9 +1,13 @@
 module Builtins;
-  open import Stdlib.Prelude;
 
-  f : String -> IO;
-  f s := printStringLn (natToString (stringToNat "290" + 3) ++str natToString 7 ++str s);
+open import Stdlib.Prelude;
 
-  main : IO;
-  main := readLn f;
-end;
+f : String -> IO;
+f s :=
+  printStringLn
+    (natToString (stringToNat "290" + 3)
+      ++str natToString 7
+      ++str s);
+
+main : IO;
+main := readLn f;

tests/positive/BuiltinsBool.juvix

@@ -1,13 +1,9 @@
 module BuiltinsBool;
 
-builtin bool
-type Bool :=
-     true : Bool
+builtin bool type Bool :=
+  | true : Bool
   | false : Bool;
 
-builtin bool-if
-if : {A : Type} → Bool → A → A → A;
+builtin bool-if if : {A : Type} → Bool → A → A → A;
 if true t _ := t;
 if false _ e := e;
-
-end;

tests/positive/Format.juvix

@@ -1,20 +1,8 @@
---- This module tests the Juvix formater
---- This is the second line of the first paragraph
----
---- The second paragraph starts.
---- Second line of the second paragraph
----
---- An example follows:
----
---- >>> Type;
----
---- Third paragraph
 module Format;
 
 open import Stdlib.Prelude hiding {,};
 open import Stdlib.Data.Nat.Ord;
 
---- a function we call ;go;
 terminating
 go : Nat → Nat → Nat;
 go n s :=
@@ -135,8 +123,7 @@ exampleFunction2 :
 module Patterns;
   infixr 4 ,;
   type Pair :=
-    | --- The , is used to build ;Pair;s
-      , : String → String → String;
+    | , : String → String → String;
 
   -- Commas in patterns
   f : _;

tests/positive/ImportShadow/Main.juvix

@@ -1,19 +1,19 @@
 module Main;
-  open import Nat;
 
-  type Unit :=
-    | unit : Unit;
+open import Nat;
 
-  f : Nat;
-  f :=
-    case unit
-      | is-zero := zero;
+type Unit :=
+  | unit : Unit;
 
-  f2 : Nat;
-  f2 :=
-    case suc zero
-      | suc is-zero := zero;
+f : Nat;
+f :=
+  case unit
+    | is-zero := zero;
 
-  f3 : Nat → Nat;
-  f3 (suc is-zero) := is-zero;
-end;
+f2 : Nat;
+f2 :=
+  case suc zero
+    | suc is-zero := zero;
+
+f3 : Nat → Nat;
+f3 (suc is-zero) := is-zero;

tests/positive/ImportShadow/Nat.juvix

@@ -1,15 +1,15 @@
 module Nat;
-  type Bool :=
-    | true : Bool
-    | false : Bool;
 
-  type Nat :=
-    | zero : Nat
-    | suc : Nat → Nat;
+type Bool :=
+  | true : Bool
+  | false : Bool;
 
-  is-zero : Nat → Bool;
-  is-zero n :=
-    case n
-      | zero := true
-      | suc _ := false;
-end;
+type Nat :=
+  | zero : Nat
+  | suc : Nat → Nat;
+
+is-zero : Nat → Bool;
+is-zero n :=
+  case n
+    | zero := true
+    | suc _ := false;

tests/positive/Imports/A.juvix

@@ -1,14 +1,17 @@
 module A;
-  module M;
+
+module M;
   module N;
-   infix 3 t;
-   type T :=
-    t : T;
-  end ;
+    infix 3 t;
+    type T :=
+      | t : T;
+  end;
+
   infixr 2 +;
   axiom + : Type → Type → Type;
-  end;
-  import M;
-  f : M.N.T;
-  f (_ M.N.t _) := Type M.+ Type M.+ M.MType;
 end;
+
+import M;
+
+f : M.N.T;
+f (_ M.N.t _) := Type M.+ Type M.+ M.MType;

tests/positive/Imports/M.juvix

@@ -1,3 +1,3 @@
 module M;
-  axiom MType : Type;
-end;
+
+axiom MType : Type;

tests/positive/Inductive.juvix

@@ -1,5 +1,4 @@
 module Inductive;
 
-  type T := t : T;
-  
-end ;
+type T :=
+  | t : T;

tests/positive/InductivePipes.juvix

@@ -1,9 +1,9 @@
 module InductivePipes;
 
-  type T := | t : T;
-  type T2 :=
+type T :=
+  | t : T;
+
+type T2 :=
   | t1 : T2
   | t2 : T2
   | t3 : T2;
-  
-end ;

tests/positive/Internal/AsPattern.juvix

@@ -1,39 +1,44 @@
 module AsPattern;
 
 infixr 9 ∘;
-∘ : {A : Type} → {B : Type} → {C : Type} → (B → C) → (A → B) → A → C;
+∘ :
+  {A : Type}
+    → {B : Type}
+    → {C : Type}
+    → (B → C)
+    → (A → B)
+    → A
+    → C;
 ∘ {_} {B} {_} f g x := f (g x);
 
-builtin nat
-type Nat :=
-  zero : Nat |
-  suc : Nat → Nat;
+builtin nat type Nat :=
+  | zero : Nat
+  | suc : Nat → Nat;
 
 infixl 6 +;
-builtin nat-plus
-+ : Nat → Nat → Nat;
+builtin nat-plus + : Nat → Nat → Nat;
 + zero b := b;
 + (suc a) b := suc (a + b);
 
 infixr 2 ×;
 infixr 4 ,;
 type × (A : Type) (B : Type) :=
-  , : A → B → A × B;
+  | , : A → B → A × B;
 
-fst : {A : Type} → {B : Type} → (A × B) → A;
+fst : {A : Type} → {B : Type} → A × B → A;
 fst p@(a, _) := a;
 
-snd : {A : Type} → {B : Type} → (A × B) → B;
-snd (p@(_, b)) := b;
+snd : {A : Type} → {B : Type} → A × B → B;
+snd p@(_, b) := b;
 
 lambda : Nat → Nat → Nat;
-lambda x := λ { a@(suc _) := a + x + zero };
+lambda x :=
+  λ {
+    | a@(suc _) := a + x + zero
+  };
 
-a : {A : Type} → (A × Nat) → Nat;
+a : {A : Type} → A × Nat → Nat;
 a p@(x, s@zero) := snd p + 1;
 
-b : {A : Type} → (A × Nat) → ({B : Type} → B → B) → A;
+b : {A : Type} → A × Nat → ({B : Type} → B → B) → A;
 b p@(_, zero) f := (f ∘ fst) p;
-
-end;
-

tests/positive/Internal/Box.juvix

@@ -1,10 +1,10 @@
 module Box;
 
- type Box (A : Type) :=
-   box : A → Box A;
+type Box (A : Type) :=
+  | box : A → Box A;
 
- type T :=
-   t : T;
+type T :=
+  | t : T;
 
 b : Box _;
 b := box t;
@@ -13,6 +13,4 @@ id : {A : Type} → A → A;
 id x := x;
 
 tt : _;
-tt := id t
-
-end;
+tt := id t;

tests/positive/Internal/Case.juvix

@@ -1,35 +1,42 @@
 module Case;
-  open import Stdlib.Prelude;
 
-  isZero : Nat → Bool;
-  isZero n := case n
-      | zero := true
-      | k@(suc _) := false;
+open import Stdlib.Prelude;
 
-  id' : Bool → {A : Type} → A → A;
-  id' b := case b
-      | true := id
-      | false := id;
+isZero : Nat → Bool;
+isZero n :=
+  case n
+    | zero := true
+    | k@(suc _) := false;
 
-  pred : Nat → Nat;
-  pred n := case n
-      | zero := zero
-      | suc n := n;
+id' : Bool → {A : Type} → A → A;
+id' b :=
+  case b
+    | true := id
+    | false := id;
 
-  appIf : {A : Type} → Bool → (A → A) → A → A;
-  appIf b f := case b
+pred : Nat → Nat;
+pred n :=
+  case n
+    | zero := zero
+    | suc n := n;
+
+appIf : {A : Type} → Bool → (A → A) → A → A;
+appIf b f :=
+  case b
+    | true := f
+    | false := id;
+
+appIf2 : {A : Type} → Bool → (A → A) → A → A;
+appIf2 b f a :=
+  (case b
       | true := f
-      | false := id;
-
-  appIf2 : {A : Type} → Bool → (A → A) → A → A;
-  appIf2 b f a := (case b
-        | true := f
-        | false := id)
+      | false := id)
     a;
 
-  nestedCase1 : {A : Type} → Bool → (A → A) → A → A;
-  nestedCase1 b f := case b
-      | true := (case b
+nestedCase1 : {A : Type} → Bool → (A → A) → A → A;
+nestedCase1 b f :=
+  case b
+    | true :=
+      (case b
         | _ := id)
-      | false := id;
-end;
+    | false := id;

tests/positive/Internal/HoleInSignature.juvix

@@ -1,15 +1,14 @@
 module HoleInSignature;
+
 type Pair (A : Type) (B : Type) :=
-  mkPair : A → B → Pair A B;
+  | mkPair : A → B → Pair A B;
 
 type Bool :=
-  true : Bool |
-  false : Bool;
+  | true : Bool
+  | false : Bool;
 
 p : Pair _ _;
 p := mkPair true false;
 
 p2 : (A : Type) → (B : Type) → _ → B → Pair A _;
 p2 _ _ a b := mkPair a b;
-
-end;

tests/positive/Internal/Implicit.juvix

@@ -1,19 +1,32 @@
 module Implicit;
 
 infixr 9 ∘;
-∘ : {A : Type} → {B : Type} → {C : Type} → (B → C) → (A → B) → A → C;
+∘ :
+  {A : Type}
+    → {B : Type}
+    → {C : Type}
+    → (B → C)
+    → (A → B)
+    → A
+    → C;
 ∘ f g x := f (g x);
 
 type Nat :=
-  zero : Nat |
-  suc : Nat → Nat;
+  | zero : Nat
+  | suc : Nat → Nat;
 
 infixr 2 ×;
 infixr 4 ,;
 type × (A : Type) (B : Type) :=
-  , : A → B → A × B;
+  | , : A → B → A × B;
 
-uncurry : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → A × B → C;
+uncurry :
+  {A : Type}
+    → {B : Type}
+    → {C : Type}
+    → (A → B → C)
+    → A × B
+    → C;
 uncurry f (a, b) := f a b;
 
 fst : {A : Type} → {B : Type} → A × B → A;
@@ -25,17 +38,29 @@ snd (_, b) := b;
 swap : {A : Type} → {B : Type} → A × B → B × A;
 swap (a, b) := b, a;
 
-first : {A : Type} → {B : Type} → {A' : Type} → (A → A') → A × B → A' × B;
+first :
+  {A : Type}
+    → {B : Type}
+    → {A' : Type}
+    → (A → A')
+    → A × B
+    → A' × B;
 first f (a, b) := f a, b;
 
-second : {A : Type} → {B : Type} → {B' : Type} → (B → B') → A × B → A × B';
+second :
+  {A : Type}
+    → {B : Type}
+    → {B' : Type}
+    → (B → B')
+    → A × B
+    → A × B';
 second f (a, b) := a, f b;
 
 both : {A : Type} → {B : Type} → (A → B) → A × A → B × B;
 both f (a, b) := f a, f b;
 
 type Bool :=
-     true : Bool
+  | true : Bool
   | false : Bool;
 
 if : {A : Type} → Bool → A → A → A;
@@ -44,17 +69,17 @@ if false _ b := b;
 
 infixr 5 ::;
 type List (A : Type) :=
-  nil : List A
+  | nil : List A
   | :: : A → List A → List A;
 
 upToTwo : _;
 upToTwo := zero :: suc zero :: suc (suc zero) :: nil;
 
 p1 : Nat → Nat → Nat × Nat;
-p1 a b := a, b ;
+p1 a b := a, b;
 
 type Proxy (A : Type) :=
- proxy : Proxy A;
+  | proxy : Proxy A;
 
 t2' : {A : Type} → Proxy A;
 t2' := proxy;
@@ -62,14 +87,15 @@ t2' := proxy;
 t2 : {A : Type} → Proxy A;
 t2 := proxy;
 
-t3 : ({A : Type} → Proxy A) → {B : Type} → Proxy B → Proxy B;
+t3 :
+  ({A : Type} → Proxy A) → {B : Type} → Proxy B → Proxy B;
 t3 _ _ := proxy;
 
 t4 : {B : Type} → Proxy B;
 t4 {_} := t3 proxy proxy;
 
 t4' : {B : Type} → Proxy B;
-t4' := t3 proxy proxy ;
+t4' := t3 proxy proxy;
 
 map : {A : Type} → {B : Type} → (A → B) → List A → List B;
 map f nil := nil;
@@ -93,25 +119,27 @@ f a b := a;
 pairEval : {A : Type} → {B : Type} → (A → B) × A → B;
 pairEval (f, x) := f x;
 
-pairEval' : {A : Type} → {B : Type} → ({C : Type} → A → B) × A → B;
+pairEval' :
+  {A : Type} → {B : Type} → ({C : Type} → A → B) × A → B;
 pairEval' (f, x) := f {Nat} x;
 
-foldr : {A : Type} → {B : Type} → (A → B → B) → B → List A → B;
+foldr :
+  {A : Type} → {B : Type} → (A → B → B) → B → List A → B;
 foldr _ z nil := z;
 foldr f z (h :: hs) := f h (foldr f z hs);
 
-foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
-foldl f z nil := z ;
+foldl :
+  {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
+foldl f z nil := z;
 foldl f z (h :: hs) := foldl f (f z h) hs;
 
 filter : {A : Type} → (A → Bool) → List A → List A;
 filter _ nil := nil;
-filter f (h :: hs) := if (f h)
-   (h :: filter f hs)
-   (filter f hs);
+filter f (h :: hs) :=
+  if (f h) (h :: filter f hs) (filter f hs);
 
-partition : {A : Type} → (A → Bool) → List A → List A × List A;
+partition :
+  {A : Type} → (A → Bool) → List A → List A × List A;
 partition _ nil := nil, nil;
-partition f (x :: xs) := (if (f x) first second) ((::) x) (partition f xs);
-
-end;
+partition f (x :: xs) :=
+  if (f x) first second ((::) x) (partition f xs);

tests/positive/Internal/Lambda.juvix

@@ -1,111 +1,231 @@
 module Lambda;
 
 type Nat :=
-  zero : Nat
+  | zero : Nat
   | suc : Nat → Nat;
 
 infixr 2 ×;
 infixr 4 ,;
 type × (A : Type) (B : Type) :=
-  , : A → B → A × B;
+  | , : A → B → A × B;
 
 infixr 9 ∘;
-∘ : {A : Type} → {B : Type} → {C : Type} → (B → C) → (A → B) → A → C;
-∘ {_} {B} {_} := λ {f g x := f (g x)};
+∘ :
+  {A : Type}
+    → {B : Type}
+    → {C : Type}
+    → (B → C)
+    → (A → B)
+    → A
+    → C;
+∘ {_} {B} {_} :=
+  λ {
+    | f g x := f (g x)
+  };
 
 id : {A : Type} → A → A;
-id := λ {a := a};
+id :=
+  λ {
+    | a := a
+  };
 
 id2 : {A : Type} → {B : Type} → A → A;
-id2 := λ {a := a};
+id2 :=
+  λ {
+    | a := a
+  };
 
 id' : (A : Type) → A → A;
-id' := λ {A a := a};
+id' :=
+  λ {
+    | A a := a
+  };
 
 id'' : (A : Type) → A → A;
-id'' := λ {A := λ {a := a}};
+id'' :=
+  λ {
+    | A := λ {
+      | a := a
+    }
+  };
 
-uncurry : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → A × B → C;
-uncurry := λ {f (a, b) := f a b};
+uncurry :
+  {A : Type}
+    → {B : Type}
+    → {C : Type}
+    → (A → B → C)
+    → A × B
+    → C;
+uncurry :=
+  λ {
+    | f (a, b) := f a b
+  };
 
 idB : {A : Type} → A → A;
-idB a := λ { a := a} a;
+idB a :=
+  λ {
+      | a := a
+    }
+    a;
 
 mapB : {A : Type} → (A → A) → A → A;
-mapB := λ { f a := f a};
+mapB :=
+  λ {
+    | f a := f a
+  };
 
 add : Nat → Nat → Nat;
-add := λ {zero n := n | (suc n) := λ {m := suc (add n m) }};
+add :=
+  λ {
+    | zero n := n
+    | (suc n) := λ {
+      | m := suc (add n m)
+    }
+  };
 
 fst : {A : Type} → {B : Type} → A × B → A;
-fst {_} := λ {(a, _) := a};
+fst {_} :=
+  λ {
+    | (a, _) := a
+  };
 
 swap : {A : Type} → {B : Type} → A × B → B × A;
-swap {_} {_} := λ {(a, b) := b, a};
+swap {_} {_} :=
+  λ {
+    | (a, b) := b, a
+  };
 
-first : {A : Type} → {B : Type} → {A' : Type} → (A → A') → A × B → A' × B;
-first := λ {f (a, b) := f a, b};
+first :
+  {A : Type}
+    → {B : Type}
+    → {A' : Type}
+    → (A → A')
+    → A × B
+    → A' × B;
+first :=
+  λ {
+    | f (a, b) := f a, b
+  };
 
-second : {A : Type} → {B : Type} → {B' : Type} → (B → B') → A × B → A × B';
-second f (a , b) := a , f b;
+second :
+  {A : Type}
+    → {B : Type}
+    → {B' : Type}
+    → (B → B')
+    → A × B
+    → A × B';
+second f (a, b) := a, f b;
 
 both : {A : Type} → {B : Type} → (A → B) → A × A → B × B;
-both {_} {B} := λ {f (a, b) := f a, f b};
+both {_} {B} :=
+  λ {
+    | f (a, b) := f a, f b
+  };
 
 infixr 5 ::;
 type List (a : Type) :=
-  nil : List a
+  | nil : List a
   | :: : a → List a → List a;
 
 map : {A : Type} → {B : Type} → (A → B) → List A → List B;
-map {_} := λ {f nil := nil
-              | f (x :: xs) := f x :: map f xs};
+map {_} :=
+  λ {
+    | f nil := nil
+    | f (x :: xs) := f x :: map f xs
+  };
 
 pairEval : {A : Type} → {B : Type} → (A → B) × A → B;
-pairEval := λ {(f, x) := f x};
+pairEval :=
+  λ {
+    | (f, x) := f x
+  };
 
-foldr : {A : Type} → {B : Type} → (A → B → B) → B → List A → B;
-foldr := λ {_ z nil := z
-            | f z (h :: hs) := f h (foldr f z hs)};
+foldr :
+  {A : Type} → {B : Type} → (A → B → B) → B → List A → B;
+foldr :=
+  λ {
+    | _ z nil := z
+    | f z (h :: hs) := f h (foldr f z hs)
+  };
 
-foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
-foldl := λ {f z nil := z
-            | f z (h :: hs) := foldl f (f z h) hs};
+foldl :
+  {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
+foldl :=
+  λ {
+    | f z nil := z
+    | f z (h :: hs) := foldl f (f z h) hs
+  };
 
 type Bool :=
-     true : Bool
+  | true : Bool
   | false : Bool;
 
 if : {A : Type} → Bool → A → A → A;
-if := λ {true a _ := a
-         | false _ b := b};
+if :=
+  λ {
+    | true a _ := a
+    | false _ b := b
+  };
 
 filter : {A : Type} → (A → Bool) → List A → List A;
-filter := λ {_ nil := nil
-             | f (h :: hs) := if (f h)
-                            (h :: filter f hs)
-                            (filter f hs)};
+filter :=
+  λ {
+    | _ nil := nil
+    | f (h :: hs) := if (f h) (h :: filter f hs) (filter f hs)
+  };
 
-partition : {A : Type} → (A → Bool) → List A → List A × List A;
-partition := λ {_ nil := nil, nil
-                | f (x :: xs) := (if (f x) first second) ((::) x) (partition f xs)};
+partition :
+  {A : Type} → (A → Bool) → List A → List A × List A;
+partition :=
+  λ {
+    | _ nil := nil, nil
+    | f (x :: xs) := if
+      (f x)
+      first
+      second
+      ((::) x)
+      (partition f xs)
+  };
 
-zipWith : {A : Type} → {B : Type} → {C : Type} → (_ → _ → _) → List A → List B → List C;
-zipWith := λ {_ nil _ := nil
-              | _ _ nil := nil
-              | f (x :: xs) (y :: ys) := f x y :: zipWith f xs ys
-             };
+zipWith :
+  {A : Type}
+    → {B : Type}
+    → {C : Type}
+    → (_ → _ → _)
+    → List A
+    → List B
+    → List C;
+zipWith :=
+  λ {
+    | _ nil _ := nil
+    | _ _ nil := nil
+    | f (x :: xs) (y :: ys) := f x y :: zipWith f xs ys
+  };
 
-t : {A : Type} → {B : Type} → ({X : Type} → List X) → List A × List B;
-t := id {({X : Type} → List X) → _} λ { f := f {_} , f {_} };
+t :
+  {A : Type}
+    → {B : Type}
+    → ({X : Type} → List X)
+    → List A × List B;
+t :=
+  id
+    {({X : Type} → List X) → _}
+    λ {
+      | f := f {_}, f {_}
+    };
 
 type Box (A : Type) :=
-  b : A → Box A;
+  | b : A → Box A;
 
 x : Box ((A : Type) → A → A);
-x := b λ {A a := a};
+x :=
+  b
+    λ {
+      | A a := a
+    };
 
 t1 : {A : Type} → Box ((A : Type) → A → A) → A → A;
-t1 {A} := λ {(b f) := f A};
-
-end;
+t1 {A} :=
+  λ {
+    | (b f) := f A
+  };

tests/positive/Internal/LiteralInt.juvix

@@ -1,11 +1,15 @@
 module LiteralInt;
-  open import Stdlib.Prelude;
-  type A := a : A;
-  type B := b : B;
 
-  f : Nat;
-  f := 1;
+open import Stdlib.Prelude;
 
-  main : IO;
-  main := printNatLn 2;
-end;
+type A :=
+  | a : A;
+
+type B :=
+  | b : B;
+
+f : Nat;
+f := 1;
+
+main : IO;
+main := printNatLn 2;

tests/positive/Internal/LiteralString.juvix

@@ -1,12 +1,12 @@
 module LiteralString;
-  builtin string axiom String : Type;
 
-  type A :=
-    a : A;
+builtin string axiom String : Type;
 
-  type B :=
-    b : B;
+type A :=
+  | a : A;
 
-  f : String;
-  f := "a";
-end;
+type B :=
+  | b : B;
+
+f : String;
+f := "a";

tests/positive/Internal/Mutual.juvix

@@ -1,11 +1,11 @@
 module Mutual;
 
 type Bool :=
-     true : Bool
+  | true : Bool
   | false : Bool;
 
 type Nat :=
-  zero : Nat
+  | zero : Nat
   | suc : Nat → Nat;
 
 not : _;
@@ -13,6 +13,7 @@ not false := true;
 not true := false;
 
 odd : _;
+
 even : _;
 
 odd zero := false;
@@ -20,5 +21,3 @@ odd (suc n) := even n;
 
 even zero := true;
 even (suc n) := odd n;
-
-end;

tests/positive/Internal/Simple.juvix

@@ -1,40 +1,38 @@
 module Simple;
-  type T :=
-    tt : T;
 
-  someT : T;
-  someT := tt;
+type T :=
+  | tt : T;
 
-  type Bool  :=
-    false : Bool |
-    true : Bool;
+someT : T;
+someT := tt;
 
+type Bool :=
+  | false : Bool
+  | true : Bool;
 
-  type Nat  :=
-     zero : Nat |
-     suc : Nat → Nat;
+type Nat :=
+  | zero : Nat
+  | suc : Nat → Nat;
 
-  infix 3 ==;
-  == : Nat → Nat → Bool;
-  == zero zero := true;
-  == (suc a) (suc b) := a == b;
-  == _ _ := false;
+infix 3 ==;
+== : Nat → Nat → Bool;
+== zero zero := true;
+== (suc a) (suc b) := a == b;
+== _ _ := false;
 
-  infixl 4 +;
-  + : Nat → Nat → Nat;
-  + zero b := b;
-  + (suc a) b := suc (a + b);
+infixl 4 +;
++ : Nat → Nat → Nat;
++ zero b := b;
++ (suc a) b := suc (a + b);
 
-  infixr 5 ::;
-  type List :=
-    nil : List |
-    :: : Nat → List → List;
+infixr 5 ::;
+type List :=
+  | nil : List
+  | :: : Nat → List → List;
 
-  foldr : (Nat → Nat → Nat) → Nat → List → Nat;
-  foldr _ v nil := v;
-  foldr f v (a :: as) := f a (foldr f v as);
+foldr : (Nat → Nat → Nat) → Nat → List → Nat;
+foldr _ v nil := v;
+foldr f v (a :: as) := f a (foldr f v as);
 
-  sum : List → Nat;
-  sum := foldr (+) zero;
-
-end;
+sum : List → Nat;
+sum := foldr (+) zero;

tests/positive/Internal/Synonyms.juvix

@@ -20,5 +20,3 @@ czero {_} f x := x;
 
 csuc : Num → Num;
 csuc n {_} f := f ∘ n {_} f;
-
-end;

tests/positive/Judoc.juvix

@@ -3,9 +3,12 @@ module Judoc;
 axiom A : Type;
 axiom b : Type;
 
-type T := t : T;
+type T :=
+  | t : T;
 
---- he ;id A; and ;A A id T A id; this is another ;id id id; example
+--- he ;id A; and ;A A id T A id; this is another ;id
+  id
+  id; example
 --- hahahah
 --- and another one ;T;
 id : {A : Type} → A → A;
@@ -14,6 +17,3 @@ id a := a;
 --- hellowww
 id2 : {A : Type} → A → A;
 id2 a := a;
-
-
-end;

tests/positive/LetShadow.juvix

@@ -1,16 +1,16 @@
 module LetShadow;
-  type Nat :=
-    | zero : Nat
-    | suc : Nat → Nat;
 
-  type Unit :=
-    | unit : Unit;
+type Nat :=
+  | zero : Nat
+  | suc : Nat → Nat;
 
-  t : Nat;
-  t :=
-    case unit
-      | x :=
-        let
-          x : Nat := suc zero;
-        in x;
-end;
+type Unit :=
+  | unit : Unit;
+
+t : Nat;
+t :=
+  case unit
+    | x :=
+      let
+        x : Nat := suc zero;
+      in x;

tests/positive/Literals.juvix

@@ -1,20 +1,20 @@
 module Literals;
-  axiom Int : Type;
-  axiom String : Type;
-  axiom + : Int → Int → Int;
-  a : Int;
-  a := 12313;
 
-  b : Int;
-  b := -008;
+axiom Int : Type;
+axiom String : Type;
+axiom + : Int → Int → Int;
 
-  - : Int;
-  - := 010;
+a : Int;
+a := 12313;
 
-  -+-- : Int;
-  -+-- := - + -+--;
+b : Int;
+b := -8;
 
+- : Int;
+- := 10;
 
-  c : String;
-  c := "hellooooo";
-end;
+-+-- : Int;
+-+-- := - + -+--;
+
+c : String;
+c := "hellooooo";

tests/positive/MultiParams.juvix

@@ -1,11 +1,12 @@
 module MultiParams;
-  type Multi (A B C : Type) :=
-    | mult : Multi A B C;
 
-  f : {A B : Type} → (C : Type) → {D E F : Type} → Type → Type;
-  f C _ := C;
+type Multi (A B C : Type) :=
+  | mult : Multi A B C;
 
-  g : {A B : Type} → (C : Type) → {D _ F : Type} → Type → Type;
-  g C _ := C;
+f :
+  {A B : Type} → (C : Type) → {D E F : Type} → Type → Type;
+f C _ := C;
 
-end;
+g :
+  {A B : Type} → (C : Type) → {D _ F : Type} → Type → Type;
+g C _ := C;

tests/positive/Operators.juvix

@@ -1,15 +1,13 @@
 module Operators;
 
-  infixl 5 + ;
-  axiom + : Type → Type → Type;
+infixl 5 +;
+axiom + : Type → Type → Type;
 
-  plus : Type → Type → Type;
-  plus := (+);
+plus : Type → Type → Type;
+plus := (+);
 
-  plus2 : Type → Type → Type → Type;
-  plus2 a b c := a + b + c;
+plus2 : Type → Type → Type → Type;
+plus2 a b c := a + b + c;
 
-  plus3 : Type → Type → Type → Type → Type;
-  plus3 a b c d := (+) (a + b) ((+) c d);
-
-end;
+plus3 : Type → Type → Type → Type → Type;
+plus3 a b c d := (+) (a + b) ((+) c d);

tests/positive/Parsing.juvix

@@ -1,8 +1,7 @@
 module Parsing;
 
- let' : Type;
- let' := Type;
+let' : Type;
+let' := Type;
 
- TypeMine : Type;
- TypeMine := Type;
-end;
+TypeMine : Type;
+TypeMine := Type;

tests/positive/Polymorphism.juvix

@@ -1,19 +1,19 @@
 module Polymorphism;
 
 type Pair (A : Type) (B : Type) :=
- mkPair : A → B → Pair A B;
+  | mkPair : A → B → Pair A B;
 
 type Nat :=
- zero : Nat |
- suc : Nat → Nat;
+  | zero : Nat
+  | suc : Nat → Nat;
 
 type List (A : Type) :=
- nil : List A |
- cons : A → List A → List A;
+  | nil : List A
+  | cons : A → List A → List A;
 
 type Bool :=
- false : Bool |
- true : Bool;
+  | false : Bool
+  | true : Bool;
 
 id : (A : Type) → A → A;
 id _ a := a;
@@ -42,12 +42,17 @@ p := mkPair true false;
 swap : (A : Type) → (B : Type) → Pair A B → Pair B A;
 swap A B (mkPair a b) := mkPair b a;
 
-curry : (A : Type) → (B : Type) → (C : Type)
-  → (Pair A B → C) → A → B → C;
-curry A B C f a b := f (mkPair a b) ;
+curry :
+  (A : Type)
+    → (B : Type)
+    → (C : Type)
+    → (Pair A B → C)
+    → A
+    → B
+    → C;
+curry A B C f a b := f (mkPair a b);
 
-ap : (A : Type) → (B : Type)
-  → (A → B) → A → B;
+ap : (A : Type) → (B : Type) → (A → B) → A → B;
 ap A B f a := f a;
 
 ite : (A : Type) → Bool → A → A → A;
@@ -60,25 +65,39 @@ headDef A _ (cons h _) := h;
 
 filter : (A : Type) → (A → Bool) → List A → List A;
 filter A f nil := nil;
-filter A f (cons x xs) := ite (List A) (f x) (cons x (filter A f xs)) (filter A f xs);
+filter A f (cons x xs) :=
+  ite
+    (List A)
+    (f x)
+    (cons x (filter A f xs))
+    (filter A f xs);
 
-map : (A : Type) → (B : Type) →
-  (A → B) → List A → List B;
-map A B f nil := nil ;
+map : (A : Type) → (B : Type) → (A → B) → List A → List B;
+map A B f nil := nil;
 map A B f (cons x xs) := cons (f x) (map A B f xs);
 
-zip : (A : Type) → (B : Type)
-    → List A → List B → List (Pair A B);
+zip :
+  (A : Type)
+    → (B : Type)
+    → List A
+    → List B
+    → List (Pair A B);
 zip A B nil _ := nil;
 zip A B _ nil := nil;
 zip A B (cons a as) (cons b bs) := nil;
 
-zipWith : (A : Type) → (B : Type) → (C : Type)
-  → (A → B → C)
-  → List A → List B → List C;
+zipWith :
+  (A : Type)
+    → (B : Type)
+    → (C : Type)
+    → (A → B → C)
+    → List A
+    → List B
+    → List C;
 zipWith A B C f nil _ := nil;
 zipWith A B C f _ nil := nil;
-zipWith A B C f (cons a as) (cons b bs) := cons (f a b) (zipWith A B C f as bs);
+zipWith A B C f (cons a as) (cons b bs) :=
+  cons (f a b) (zipWith A B C f as bs);
 
 rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat;
 rankn f b n := mkPair (f Bool b) (f Nat n);
@@ -94,7 +113,8 @@ pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B;
 pairEval _ _ (mkPair f x) := f x;
 
 main : Nat;
-main := headDef Nat (pairEval Nat Nat (mkPair (add zero) zero))
-   (zipWith Nat Nat Nat add l1 l1);
-
-end;
+main :=
+  headDef
+    Nat
+    (pairEval Nat Nat (mkPair (add zero) zero))
+    (zipWith Nat Nat Nat add l1 l1);

tests/positive/PolymorphismHoles.juvix

@@ -1,19 +1,19 @@
 module PolymorphismHoles;
 
 type Pair (A : Type) (B : Type) :=
- mkPair : A → B → Pair A B;
+  | mkPair : A → B → Pair A B;
 
 type Nat :=
- zero : Nat |
- suc : Nat → Nat;
+  | zero : Nat
+  | suc : Nat → Nat;
 
 type List (A : Type) :=
- nil : List A |
- cons : A → List A → List A;
+  | nil : List A
+  | cons : A → List A → List A;
 
 type Bool :=
- false : Bool |
- true : Bool;
+  | false : Bool
+  | true : Bool;
 
 id : (A : Type) → A → A;
 id _ a := a;
@@ -35,12 +35,17 @@ p := mkPair true false;
 swap : (A : Type) → (B : Type) → Pair A B → Pair B A;
 swap A B (mkPair a b) := mkPair b a;
 
-curry : (A : Type) → (B : Type) → (C : Type)
-  → (Pair A B → C) → A → B → C;
-curry A B C f a b := f (mkPair a b) ;
+curry :
+  (A : Type)
+    → (B : Type)
+    → (C : Type)
+    → (Pair A B → C)
+    → A
+    → B
+    → C;
+curry A B C f a b := f (mkPair a b);
 
-ap : (A : Type) → (B : Type)
-  → (A → B) → A → B;
+ap : (A : Type) → (B : Type) → (A → B) → A → B;
 ap A B f a := f a;
 
 headDef : (A : Type) → A → List A → A;
@@ -53,25 +58,35 @@ ite _ false _ ff := ff;
 
 filter : (A : Type) → (A → Bool) → List A → List A;
 filter _ f nil := nil;
-filter _ f (cons x xs) := ite _ (f x) (cons x (filter _ f xs)) (filter _ f xs);
+filter _ f (cons x xs) :=
+  ite _ (f x) (cons x (filter _ f xs)) (filter _ f xs);
 
-map : (A : Type) → (B : Type) →
-  (A → B) → List _ → List _;
+map : (A : Type) → (B : Type) → (A → B) → List _ → List _;
 map _ _ f nil := nil;
 map _ _ f (cons x xs) := cons (f x) (map _ _ f xs);
 
-zip : (A : Type) → (B : Type)
-    → List A → List B → List (Pair A B);
+zip :
+  (A : Type)
+    → (B : Type)
+    → List A
+    → List B
+    → List (Pair A B);
 zip A _ nil _ := nil;
 zip _ _ _ nil := nil;
 zip _ _ (cons a as) (cons b bs) := nil;
 
-zipWith : (A : Type) → (B : Type) → (C : Type)
-  → (A → B → C)
-  → List A → List B → List C;
+zipWith :
+  (A : Type)
+    → (B : Type)
+    → (C : Type)
+    → (A → B → C)
+    → List A
+    → List B
+    → List C;
 zipWith _ _ C f nil _ := nil;
 zipWith _ _ C f _ nil := nil;
-zipWith _ _ _ f (cons a as) (cons b bs) := cons (f a b) (zipWith _ _ _ f as bs);
+zipWith _ _ _ f (cons a as) (cons b bs) :=
+  cons (f a b) (zipWith _ _ _ f as bs);
 
 rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat;
 rankn f b n := mkPair (f _ b) (f _ n);
@@ -87,7 +102,8 @@ pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B;
 pairEval _ _ (mkPair f x) := f x;
 
 main : Nat;
-main := headDef _ (pairEval _ _ (mkPair (add zero) zero))
-   (zipWith _ _ _ add l1 l1);
-
-end;
+main :=
+  headDef
+    _
+    (pairEval _ _ (mkPair (add zero) zero))
+    (zipWith _ _ _ add l1 l1);

tests/positive/QualifiedConstructor/M.juvix

@@ -1,20 +1,19 @@
 module M;
 
-  module O;
-    axiom A : Type;
-  end;
-
-  open O;
-
-  module N;
-    module O;
-      type T :=
-        A : T;
-    end;
-  end;
-
-  open N.O;
-
-  fun : T → T;
-  fun A := T;
+module O;
+  axiom A : Type;
 end;
+
+open O;
+
+module N;
+  module O;
+    type T :=
+      | A : T;
+  end;
+end;
+
+open N.O;
+
+fun : T → T;
+fun A := T;

tests/positive/QualifiedSymbol/M.juvix

@@ -1,14 +1,15 @@
 module M;
 
-  module N;
-    module O;
-      axiom A : Type;
-    end;
-  end;
-  open N;
-
+module N;
   module O;
+    axiom A : Type;
   end;
-
-  axiom B : O.A;
 end;
+
+open N;
+
+module O;
+  
+end;
+
+axiom B : O.A;

tests/positive/QualifiedSymbol2/M.juvix

@@ -1,3 +1,3 @@
 module M;
 
-end;
+

tests/positive/QualifiedSymbol2/N.juvix

@@ -1,10 +1,9 @@
 module N;
-  import M;
 
-  module M;
-    axiom A : Type;
-  end;
-
-  axiom B : M.A;
+import M;
 
+module M;
+  axiom A : Type;
 end;
+
+axiom B : M.A;

tests/positive/ShadowPublicOpen.juvix

@@ -1,10 +1,13 @@
 module ShadowPublicOpen;
-  module M;
-    module N;
-      axiom A : Type;
-    end;
-    open N public;
+
+module M;
+  module N;
+    axiom A : Type;
   end;
-  open M;
-  axiom A : Type;
+
+  open N public;
 end;
+
+open M;
+
+axiom A : Type;

tests/positive/SignatureWithBody.juvix

@@ -1,15 +1,21 @@
 module SignatureWithBody;
-  open import Stdlib.Prelude;
 
-  isNull : {A : Type} → List A → Bool := λ {
+open import Stdlib.Prelude;
+
+isNull :
+  {A : Type} → List A → Bool :=
+    λ {
       | nil := true
       | _ := false
     };
 
-  isNull' : {A : Type} → List A → Bool := let
-      aux : {A : Type} → List A → Bool := λ {
-          | nil := true
-          | _ := false
-        };
-     in aux;
-end;
+isNull' :
+  {A : Type} → List A → Bool :=
+    let
+      aux :
+          {A : Type} → List A → Bool :=
+            λ {
+              | nil := true
+              | _ := false
+            };
+    in aux;

tests/positive/StdlibList/Data/Bool.juvix

@@ -1,10 +1,9 @@
 module Data.Bool;
-  type Bool :=
-    true : Bool |
-    false : Bool;
 
-  not : Bool → Bool;
-  not true := false;
-  not false := true;
+type Bool :=
+  | true : Bool
+  | false : Bool;
 
-end;
+not : Bool → Bool;
+not true := false;
+not false := true;

tests/positive/StdlibList/Data/List.juvix

@@ -5,18 +5,20 @@ open Data.Bool;
 
 -- infixr 5 ::; waiting for implicit arguments
 type List (A : Type) :=
-  nil : List A
+  | nil : List A
   | :: : A → List A → List A;
 
 match : {A : Type} → {B : Type} → A → (A → B) → B;
 match x f := f x;
 
-foldr : (a : Type) → (b : Type) → (a → b → b) → b → List a → b;
+foldr :
+  (a : Type) → (b : Type) → (a → b → b) → b → List a → b;
 foldr _ _ _ z nil := z;
 foldr a b f z (:: h hs) := f h (foldr a b f z hs);
 
-foldl : (a : Type) → (b : Type) → (b → a → b) → b → List a → b;
-foldl a b f z nil := z ;
+foldl :
+  (a : Type) → (b : Type) → (b → a → b) → b → List a → b;
+foldl a b f z nil := z;
 foldl a b f z (:: h hs) := foldl a b f (f z h) hs;
 
 map : (a : Type) → (b : Type) → (a → b) → List a → List b;
@@ -25,10 +27,13 @@ map a b f (:: h hs) := :: (f h) (map a b f hs);
 
 filter : (a : Type) → (a → Bool) → List a → List a;
 filter a f nil := nil;
-filter a f (:: h hs) := match (f h) λ {
-  | true := :: h (filter a f hs)
-  | false := filter a f hs
-};
+filter a f (:: h hs) :=
+  match
+    (f h)
+    λ {
+      | true := :: h (filter a f hs)
+      | false := filter a f hs
+    };
 
 import Data.Nat;
 open Data.Nat;
@@ -40,10 +45,10 @@ length a (:: _ l) := suc (length a l);
 reverse : (a : Type) → List a → List a;
 reverse a l :=
   let
-  rev : List a → List a → List a;
-  rev nil a := a;
-  rev (:: x xs) a := rev xs (:: x a)
-   in rev l nil;
+    rev : List a → List a → List a;
+    rev nil a := a;
+    rev (:: x xs) a := rev xs (:: x a);
+  in rev l nil;
 
 replicate : (a : Type) → ℕ → a → List a;
 replicate a zero _ := nil;
@@ -60,18 +65,30 @@ import Data.Product;
 open Data.Product;
 
 splitAt : (a : Type) → ℕ → List a → List a × List a;
-splitAt a _ nil := , nil nil ;
+splitAt a _ nil := , nil nil;
 splitAt a zero xs := , nil xs;
 splitAt a (suc zero) (:: x xs) := , (:: x nil) xs;
-splitAt a (suc (suc m)) (:: x xs) := match (splitAt a m xs) λ {
-    (, xs' xs'') := , (:: x xs') xs''
-  };
+splitAt a (suc (suc m)) (:: x xs) :=
+  match
+    (splitAt a m xs)
+    λ {
+      | (, xs' xs'') := , (:: x xs') xs''
+    };
 
-terminating merge : (a : Type) → (a → a → Ordering) → List a → List a → List a;
-merge a cmp (:: x xs) (:: y ys) := match (cmp x y) λ {
-    | LT := :: x (merge a cmp xs (:: y ys))
-    | _ := :: y (merge a cmp (:: x xs) ys)
-  };
+terminating
+merge :
+  (a : Type)
+    → (a → a → Ordering)
+    → List a
+    → List a
+    → List a;
+merge a cmp (:: x xs) (:: y ys) :=
+  match
+    (cmp x y)
+    λ {
+      | LT := :: x (merge a cmp xs (:: y ys))
+      | _ := :: y (merge a cmp (:: x xs) ys)
+    };
 merge _ _ nil ys := ys;
 merge _ _ xs nil := xs;
 
@@ -80,20 +97,24 @@ merge _ _ xs nil := xs;
 ++ a nil ys := ys;
 ++ a (:: x xs) ys := :: x (++ a xs ys);
 
-terminating quickSort : (a : Type) → (a → a → Ordering) → List a → List a;
+terminating
+quickSort :
+  (a : Type) → (a → a → Ordering) → List a → List a;
 quickSort a _ nil := nil;
 quickSort a _ (:: x nil) := :: x nil;
 quickSort a cmp (:: x ys) :=
   let
     ltx : a → Bool;
-    ltx y := match (cmp y x) λ{
-      | LT := true
-      | _  := false
-    };
+    ltx y :=
+      match
+        (cmp y x)
+        λ {
+          | LT := true
+          | _ := false
+        };
     gex : a → Bool;
-    gex y := not (ltx y)
-   in
-     ++ a (quickSort a cmp (filter a ltx ys))
+    gex y := not (ltx y);
+  in ++
+    a
+    (quickSort a cmp (filter a ltx ys))
     (++ a (:: x nil) (quickSort a cmp (filter a gex ys)));
-
-end;

tests/positive/StdlibList/Data/Maybe.juvix

@@ -1,7 +1,5 @@
 module Data.Maybe;
 
-  type Maybe (a : Type) :=
-     nothing : Maybe a |
-     just : a → Maybe a;
-
-end;
+type Maybe (a : Type) :=
+  | nothing : Maybe a
+  | just : a → Maybe a;

tests/positive/StdlibList/Data/Nat.juvix

@@ -1,16 +1,15 @@
 module Data.Nat;
-  type ℕ  :=
-    zero : ℕ |
-    suc : ℕ → ℕ;
 
-  infixl 6 +;
-  + : ℕ → ℕ → ℕ;
-  + zero b := b;
-  + (suc a) b := suc (a + b);
+type ℕ :=
+  | zero : ℕ
+  | suc : ℕ → ℕ;
 
-  infixl 7 *;
-  * : ℕ → ℕ → ℕ;
-  * zero b := zero;
-  * (suc a) b := b + a * b;
+infixl 6 +;
++ : ℕ → ℕ → ℕ;
++ zero b := b;
++ (suc a) b := suc (a + b);
 
-end;
+infixl 7 *;
+* : ℕ → ℕ → ℕ;
+* zero b := zero;
+* (suc a) b := b + a * b;

tests/positive/StdlibList/Data/Ord.juvix

@@ -1,6 +1,6 @@
 module Data.Ord;
-    type Ordering :=
-      LT : Ordering |
-      EQ : Ordering |
-      GT : Ordering;
-end;
+
+type Ordering :=
+  | LT : Ordering
+  | EQ : Ordering
+  | GT : Ordering;

tests/positive/StdlibList/Data/Product.juvix

@@ -3,6 +3,4 @@ module Data.Product;
 infixr 2 ×;
 -- infixr 4 ,; waiting for implicit arguments
 type × (a : Type) (b : Type) :=
-  , : a → b → a × b;
-
-end;
+  | , : a → b → a × b;

tests/positive/Symbols.juvix

@@ -1,36 +1,36 @@
 module Symbols;
-  open import Stdlib.Data.Nat;
 
-  ╘⑽╛ : Nat;
-  ╘⑽╛ := suc 9;
+open import Stdlib.Data.Nat;
 
-  -- no - function!?
-  - : Nat -> Nat -> Nat;
-  - := (+);
+╘⑽╛ : Nat;
+╘⑽╛ := suc 9;
 
-  （-） : Nat -> Nat -> Nat;
-  （-） := (-);
+-- no - function!?
+- : Nat -> Nat -> Nat;
+- := (+);
 
-  （*） : Nat -> Nat -> Nat;
-  （*） := (*);
+（-） : Nat -> Nat -> Nat;
+（-） := (-);
 
-  infixl 6 －;
-  － : Nat -> Nat -> Nat;
-  － := （-）;
+（*） : Nat -> Nat -> Nat;
+（*） := (*);
 
-  infixl 7 ·;
-  · : Nat -> Nat -> Nat;
-  · := （*）;
+infixl 6 －;
+－ : Nat -> Nat -> Nat;
+－ := （-）;
 
-  （0） : Nat;
-  （0） := ╘⑽╛ － ╘⑽╛ · zero;
+infixl 7 ·;
+· : Nat -> Nat -> Nat;
+· := （*）;
 
-  主功能 : Nat;
-  主功能 := （0）;
+（0） : Nat;
+（0） := ╘⑽╛ － ╘⑽╛ · zero;
 
-  axiom = : Type;
+主功能 : Nat;
+主功能 := （0）;
 
-  K : Nat → Nat → Nat;
-  K =a@zero (=) := =a · =;
-  K =a@(suc =) == := = · ==;
-end;
+axiom = : Type;
+
+K : Nat → Nat → Nat;
+K =a@zero (=) := =a · =;
+K =a@(suc =) == := = · ==;

tests/positive/TypeAlias.juvix

@@ -1,10 +1,10 @@
 module TypeAlias;
 
 type T :=
- t : T;
+  | t : T;
 
 type T2 :=
- t2 : T2;
+  | t2 : T2;
 
 alias : Type;
 alias := T;
@@ -22,16 +22,15 @@ infixr 9 ⊙;
 x2 : (id ⊙ id) alias;
 x2 := t;
 
-flip : (Type → Type → Type) → id Type → Type → (id ⊙ id) Type;
+flip :
+  (Type → Type → Type) → id Type → Type → (id ⊙ id) Type;
 flip f a b := f b a;
 
 type Pair (A : Type) (B : Type) :=
- mkPair : id T → id (id A) → B → Pair A B;
+  | mkPair : id T → id (id A) → B → Pair A B;
 
 p : {A : Type} → A → Pair A A;
 p a := mkPair t a a;
 
 x' : flip Pair (id _) T2;
 x' := mkPair x t2 t;
-
-end;

tests/smoke/Commands/format.smoke.yaml

@@ -0,0 +1,130 @@
+working-directory: ./../../../tests
+
+tests:
+  - name: shows-file-argument-for-autocompletion
+    command:
+      - juvix
+      - format
+      - --help
+    stdout:
+      contains:
+        JUVIX_FILE
+    exit-status: 0
+
+  - name: format-formatted-file
+    command:
+      - juvix
+      - format
+      - positive/Format.juvix
+    exit-status: 0
+    stdout: ""
+
+  - name: format-unformatted-file
+    command:
+      shell:
+        - bash
+      script: |
+        temp=$(mktemp -d)
+        trap 'rm -rf -- "$temp"' EXIT
+        cd $temp
+        touch juvix.yaml
+        echo "module Foo ;" >> Foo.juvix
+        juvix format Foo.juvix
+    stdout:
+      contains: module Foo;
+    exit-status: 1
+
+  - name: format-unformatted-file-check-no-stdout
+    command:
+      shell:
+        - bash
+      script: |
+        temp=$(mktemp -d)
+        trap 'rm -rf -- "$temp"' EXIT
+        cd $temp
+        touch juvix.yaml
+        echo "module Foo ;" >> Foo.juvix
+        juvix format --check Foo.juvix
+    stdout: ""
+    exit-status: 1
+
+  - name: format-formatted-file-check-no-stdout
+    command:
+      - juvix
+      - format
+      - --check
+      - positive/Format.juvix
+    exit-status: 0
+    stdout: ""
+
+  - name: format-dir-with-all-formatted
+    command:
+      shell:
+        - bash
+      script: |
+        temp=$(mktemp -d)
+        trap 'rm -rf -- "$temp"' EXIT
+        touch $temp/juvix.yaml
+        cp positive/Format.juvix $temp
+        juvix format $temp
+    stdout: ""
+    exit-status: 0
+
+  - name: format-dir-containing-unformatted
+    command:
+      shell:
+        - bash
+      script: |
+        temp=$(mktemp -d)
+        trap 'rm -rf -- "$temp"' EXIT
+        touch $temp/juvix.yaml
+        cp positive/Format.juvix $temp
+        cd $temp
+        echo "module Foo ;" >> Foo.juvix
+        juvix format $temp
+    stdout:
+      contains:
+        "Foo.juvix"
+    exit-status: 1
+
+  - name: format-dir-containing-unformatted-check-no-stdout
+    command:
+      shell:
+        - bash
+      script: |
+        temp=$(mktemp -d)
+        trap 'rm -rf -- "$temp"' EXIT
+        touch $temp/juvix.yaml
+        cp positive/Format.juvix $temp
+        cd $temp
+        echo "module Foo ;" >> Foo.juvix
+        juvix format --check $temp
+    stdout: ""
+    exit-status: 1
+
+  - name: format-dir-with-all-formatted-check-no-stdout
+    command:
+      shell:
+        - bash
+      script: |
+        temp=$(mktemp -d)
+        trap 'rm -rf -- "$temp"' EXIT
+        touch $temp/juvix.yaml
+        cp positive/Format.juvix $temp
+        juvix format --check $temp
+    stdout: ""
+    exit-status: 0
+
+  - name: format-file-with-scope-error
+    command:
+      shell:
+        - bash
+      script: |
+        temp=$(mktemp -d)
+        trap 'rm -rf -- "$temp"' EXIT
+        cd $temp
+        echo "module Bar;" > Foo.juvix
+        juvix format Foo.juvix
+    stderr:
+      contains: "error"
+    exit-status: 1