Fix Makefile target bugs for formatting and type Checking Juvix files (#2057)

This PR resolves a few bugs in the Makefile targets for formatting and
type checking Juvix files, which were preventing the capture of type
checking errors for our examples and bad formatting for all the Juvix
files in the repository. With this PR, our code should now be clean, and
we can expect every file to be properly formatted and type checked.

Changes made:

- [x] Updated `make format-juvix-files`
- [x] Updated `make check-format-juvix-files`
- [x] Formatted all Juvix files
- [x] Comment a fragment in `examples/milestone/Bank/Bank.juvix`

In the future, we will drastically simplify the Makefile once we improve
the `format` and the `type check` command for example posted here:

- #2066 
- #2087 

Related:

- #2063 
- #2040 (due to some typechecking errors we're not capturing before)
- #2105
- https://github.com/anoma/juvix/issues/2059

.github/workflows/ci.yml

@@ -116,13 +116,10 @@ jobs:
 
       - name: Typecheck and format Juvix examples
         if: ${{ success() }}
-        continue-on-error: true
+        shell: bash
         run: |
           cd main
-          make clean-juvix-build
-          make check-format-juvix-files
-          make clean-juvix-build
-          make typecheck-juvix-examples
+          make check-format-juvix-files && make typecheck-juvix-examples
 
       - name: Add ~/.local/bin to PATH
         run: |
@@ -218,12 +215,10 @@ jobs:
 
       - name: Typecheck and format Juvix examples
         if: ${{ success() }}
+        shell: bash
         run: |
           cd main
-          make clean-juvix-build
-          make check-format-juvix-files
-          make clean-juvix-build
-          make typecheck-juvix-examples
+          make check-format-juvix-files && make typecheck-juvix-examples
 
       - name: Install Smoke
         uses: jaxxstorm/action-install-gh-release@v1.10.0

Makefile

@@ -1,7 +1,7 @@
+SHELL := /bin/bash
 PWD=$(CURDIR)
 PREFIX="$(PWD)/.stack-work/prefix"
 UNAME := $(shell uname)
-
 EXAMPLEMILESTONE=examples/milestone
 EXAMPLEHTMLOUTPUT=docs/examples/html
 EXAMPLES= Collatz/Collatz.juvix \
@@ -18,9 +18,9 @@ DEMO_EXAMPLE=examples/demo/Demo.juvix
 MAKEAUXFLAGS?=-s
 MAKE=make ${MAKEAUXFLAGS}
 METAFILES:=README.md \
-		   CHANGELOG.md \
-		   CONTRIBUTING.md \
-		   LICENSE.md
+			 CHANGELOG.md \
+			 CONTRIBUTING.md \
+			 LICENSE.md
 
 STACKFLAGS?=--jobs $(THREADS)
 STACKTESTFLAGS?=--ta --hide-successes --ta --ansi-tricks=false
@@ -107,28 +107,48 @@ format:
 clang-format:
 	@cd runtime && ${MAKE} format
 
-JUVIXFILESTOFORMAT=$(shell find ./examples ./tests/positive -type d -name ".juvix-build" -prune -o -type f -name "*.juvix" -print)
+JUVIXFILESTOFORMAT=$(shell find  \
+	./examples  \
+	./tests/positive \
+	./tests/negative \
+	-type d \( -name ".juvix-build" -o -name "FancyPaths" \) -prune -o \
+	-type f -name "*.juvix" -print)
+
 JUVIXFORMATFLAGS?=--in-place
 JUVIXTYPECHECKFLAGS?=--only-errors
 
 .PHONY: format-juvix-files
 format-juvix-files:
 	@for file in $(JUVIXFILESTOFORMAT); do \
-		juvix format $(JUVIXFORMATFLAGS) "$$file"; \
-	done
+		${JUVIXBIN} format $(JUVIXFORMATFLAGS) "$$file" > /dev/null 2>&1; \
+		exit_code=$$?; \
+		if [ $$exit_code -eq 0 ]; then \
+			echo "[OK] $$file"; \
+      	elif [[ $$exit_code -ne 0 && "$$file" == *"tests/"* ]]; then \
+			echo "[CONTINUE] $$file is in tests directory."; \
+      	else \
+ 			echo "[FAIL] $$file formatting failed" && exit 1; \
+      	fi; \
+      	done;
 
 .PHONY: check-format-juvix-files
 check-format-juvix-files:
-	@export JUVIXFORMATFLAGS=--check
-	@make format-juvix-files
+	@JUVIXFORMATFLAGS=--check ${MAKE} format-juvix-files
 
-JUVIXEXAMPLEFILES=$(shell find ./examples  -name "*.juvix" -print)
+JUVIXEXAMPLEFILES=$(shell find ./examples \
+	-type d \( -name ".juvix-build" \) -prune -o \
+	-name "*.juvix" -print)
 
 .PHONY: typecheck-juvix-examples
 typecheck-juvix-examples:
 	@for file in $(JUVIXEXAMPLEFILES); do \
-		echo "Checking $$file"; \
 		${JUVIXBIN} typecheck "$$file" $(JUVIXTYPECHECKFLAGS); \
+		exit_code=$$?; \
+		if [ $$exit_code -eq 0 ]; then \
+			echo "[OK] $$file typechecks"; \
+		else \
+ 			echo "[FAIL] Typecking failed for $$file" && exit 1; \
+      	fi; \
 	done
 
 .PHONY: check-ormolu
@@ -166,7 +186,7 @@ check-only:
 		&& ${MAKE} install \
 		&& ${MAKE} test \
 		&& ${MAKE} smoke \
-		&& ${MAKE} check-format-juvix-examples \
+		&& ${MAKE} check-format-juvix-files \
 		&& ${MAKE} typecheck-juvix-examples \
 		&& ${MAKE} check-ormolu \
 		&& export SKIP=ormolu,format-juvix-examples,typecheck-juvix-examples \

examples/demo/Demo.juvix

@@ -1,9 +1,9 @@
 module Demo;
 
 -- standard library prelude
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 -- for comparisons on natural numbers
-open import Stdlib.Data.Nat.Ord;
+import Stdlib.Data.Nat.Ord open;
 -- for Ordering
 
 even : Nat → Bool;

examples/midsquare/MidSquareHash.juvix

@@ -4,8 +4,8 @@
 --- bits.
 module MidSquareHash;
 
-open import Stdlib.Prelude;
-open import Stdlib.Data.Nat.Ord;
+import Stdlib.Prelude open;
+import Stdlib.Data.Nat.Ord open;
 
 --- `pow N` is 2 ^ N
 pow : Nat -> Nat;

examples/midsquare/MidSquareHashUnrolled.juvix

@@ -5,8 +5,8 @@
 --- GEB backend, no recursion is used (it is manually unrolled).
 module MidSquareHashUnrolled;
 
-open import Stdlib.Prelude;
-open import Stdlib.Data.Nat.Ord;
+import Stdlib.Prelude open;
+import Stdlib.Data.Nat.Ord open;
 
 --- `powN` is 2 ^ N
 pow0 : Nat := 1;

examples/milestone/Bank/Bank.juvix

@@ -3,10 +3,10 @@
 --- https://github.com/AleoHQ/workshop/tree/master/basic_bank
 module Bank;
 
-open import Stdlib.Prelude;
-open import Stdlib.Debug.Fail;
+import Stdlib.Prelude open;
+import Stdlib.Debug.Fail open;
 
-open import Stdlib.Data.Nat.Ord;
+import Stdlib.Data.Nat.Ord open;
 
 import Stdlib.Data.Nat as Nat;
 
@@ -106,6 +106,9 @@ issue : Address -> Address -> Nat -> Token;
 issue caller owner amount :=
   assert (caller == bankAddress) (mkToken owner 0 amount);
 
+{-
+-- TODO: Uncomment this block once we fix
+-- https://github.com/anoma/juvix/issues/2056
 --- Deposits some amount of money into the bank.
 deposit : Balances -> Token -> Nat -> Token;
 deposit bal token amount :=
@@ -114,7 +117,7 @@ deposit bal token amount :=
     remaining :
         Token :=
           mkToken (getOwner token) (getGates token) difference;
-    hash : Field := hashAddress (getOwner token);
+    hash : Field := hashAddress (getOwner token);  # TODO: This raise an error
     bal' : Balances := increment hash amount bal;
   in runOnChain (commitBalances bal') remaining;
 
@@ -131,8 +134,9 @@ withdraw bal caller recipient amount rate periods :=
   assert
     (caller == bankAddress)
     (let
-      hash : Field := hashAddress recipient;
+      hash : Field := hashAddress recipient;  # TODO: Idem
       total : Nat := calculateInterest amount rate periods;
       token : Token := mkToken recipient 0 total;
       bal' : Balances := decrement hash amount bal;
     in runOnChain (commitBalances bal') token);
+-}

examples/milestone/Collatz/Collatz.juvix

@@ -1,7 +1,7 @@
 module Collatz;
 
-open import Stdlib.Prelude;
-open import Stdlib.Data.Nat.Ord;
+import Stdlib.Prelude open;
+import Stdlib.Data.Nat.Ord open;
 
 collatzNext : Nat → Nat;
 collatzNext n := if (mod n 2 == 0) (div n 2) (3 * n + 1);
@@ -28,7 +28,6 @@ main : IO;
 main :=
   printStringLn welcome
     >> readLn
-      λ {
-        | s :=
-          printStringLn resultHeading >> run collatz (stringToNat s)
-      };
+      λ {s :=
+        printStringLn resultHeading
+          >> run collatz (stringToNat s)};

examples/milestone/Fibonacci/Fibonacci.juvix

@@ -1,6 +1,6 @@
 module Fibonacci;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 fib : Nat → Nat → Nat → Nat;
 fib zero x1 _ := x1;

examples/milestone/Hanoi/Hanoi.juvix

@@ -12,7 +12,7 @@
 --- The function ;hanoi; computes the sequence of moves to solve puzzle.
 module Hanoi;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 --- Concatenates a list of strings
 --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"

examples/milestone/HelloWorld/HelloWorld.juvix

@@ -1,7 +1,7 @@
 -- HelloWorld.juvix
 module HelloWorld;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 main : IO;
 main := printStringLn "hello world!";

examples/milestone/PascalsTriangle/PascalsTriangle.juvix

@@ -4,7 +4,7 @@
 --- The function ;pascal; produces the triangle to a given depth.
 module PascalsTriangle;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 --- Return a list of repeated applications of a given function
 scanIterate : {A : Type} → Nat → (A → A) → A → List A;

examples/milestone/TicTacToe/Logic/Board.juvix

@@ -1,10 +1,10 @@
 module Logic.Board;
 
-open import Stdlib.Prelude;
-open import Stdlib.Debug.Fail;
-open import Logic.Square public;
-open import Logic.Symbol public;
-open import Logic.Extra;
+import Stdlib.Prelude open;
+import Stdlib.Debug.Fail open;
+import Logic.Square open public;
+import Logic.Symbol open public;
+import Logic.Extra open;
 
 --- A 3x3 grid of ;Square;s
 type Board :=

examples/milestone/TicTacToe/Logic/Extra.juvix

@@ -1,8 +1,8 @@
 --- Some generic helper definitions.
 module Logic.Extra;
 
-open import Stdlib.Data.Nat.Ord;
-open import Stdlib.Prelude;
+import Stdlib.Data.Nat.Ord open;
+import Stdlib.Prelude open;
 
 --- Concatenates a list of strings
 --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"

examples/milestone/TicTacToe/Logic/Game.juvix

@@ -4,11 +4,11 @@
 --- diagonal row is the winner. It is a solved game, with a forced draw assuming best play from both players.
 module Logic.Game;
 
-open import Stdlib.Data.Nat.Ord;
-open import Stdlib.Prelude;
-open import Logic.Extra public;
-open import Logic.Board public;
-open import Logic.GameState public;
+import Stdlib.Data.Nat.Ord open;
+import Stdlib.Prelude open;
+import Logic.Extra open public;
+import Logic.Board open public;
+import Logic.GameState open public;
 
 --- Checks if we reached the end of the game.
 checkState : GameState → GameState;

examples/milestone/TicTacToe/Logic/GameState.juvix

@@ -1,8 +1,8 @@
 module Logic.GameState;
 
-open import Stdlib.Prelude;
-open import Logic.Extra;
-open import Logic.Board;
+import Stdlib.Prelude open;
+import Logic.Extra open;
+import Logic.Board open;
 
 type Error :=
   | --- no error occurred

examples/milestone/TicTacToe/Logic/Square.juvix

@@ -1,9 +1,9 @@
 module Logic.Square;
 
-open import Stdlib.Prelude;
-open import Logic.Symbol;
-open import Stdlib.Data.Nat.Ord;
-open import Logic.Extra;
+import Stdlib.Prelude open;
+import Logic.Symbol open;
+import Stdlib.Data.Nat.Ord open;
+import Logic.Extra open;
 
 --- A square is each of the holes in a board
 type Square :=

examples/milestone/TicTacToe/Logic/Symbol.juvix

@@ -1,7 +1,7 @@
 --- This module defines the ;Symbol; type and some helper functions.
 module Logic.Symbol;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 --- A symbol represents a token that can be placed in a square
 type Symbol :=

examples/milestone/Tutorial/Tutorial.juvix

@@ -4,9 +4,9 @@
 module Tutorial;
 
 -- import the standard library prelude and bring it into scope
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 -- bring comparison operators on Nat into scope
-open import Stdlib.Data.Nat.Ord;
+import Stdlib.Data.Nat.Ord open;
 
 main : IO;
 main := printStringLn "Hello world!";

tests/negative/230/Foo.juvix

@@ -1,5 +1,4 @@
 module Foo;
 
-open import Foo.Data.Bool;
+import Foo.Data.Bool open;
 
-end;

tests/negative/230/Foo/Data/Bool.juvix

@@ -2,26 +2,25 @@ module Foo.Data.Bool;
 
 import Stdlib.Data.Bool;
 
-  type Bool :=
-    true : Bool |
-    false : Bool;
+type Bool :=
+  | true : Bool
+  | false : Bool;
 
-  not : Bool → Bool;
-  not true := false;
-  not false := true;
+not : Bool → Bool;
+not true := false;
+not false := true;
 
-  infixr 2 ||;
-  || : Bool → Bool → Bool;
-  || false a := a;
-  || true _ := true;
+infixr 2 ||;
+|| : Bool → Bool → Bool;
+|| false a := a;
+|| true _ := true;
 
-  infixr 2 &&;
-  && : Bool → Bool → Bool;
-  && false _ := false;
-  && true a := a;
+infixr 2 &&;
+&& : Bool → Bool → Bool;
+&& false _ := false;
+&& true a := a;
 
-  if : {A : Type} → Bool → A → A → A;
-  if true a _ := a;
-  if false _ b := b;
+if : {A : Type} → Bool → A → A → A;
+if true a _ := a;
+if false _ b := b;
 
-end;

tests/negative/258/M.juvix

@@ -1,10 +1,9 @@
 module M;
 
 type Nat :=
-  O : Nat |
-  S : Nat -> Nat;
+  | O : Nat
+  | S : Nat -> Nat;
 
 fun : Nat -> Nat;
 fun (S {S {x}}) := x;
 
-end;

tests/negative/265/M.juvix

@@ -1,14 +1,13 @@
 module M;
 
 type Bool :=
-     true : Bool
+  | true : Bool
   | false : Bool;
 
 type Pair (A : Type) (B : Type) :=
-  mkPair : A → B → Pair A B;
+  | mkPair : A → B → Pair A B;
 
 f : _ → _;
 f (mkPair false true) := true;
 f true := false;
 
-end;

tests/negative/AppLeftImplicit.juvix

@@ -1,6 +1,5 @@
 module AppLeftImplicit;
 
- x : Type;
- x := {x};
+x : Type;
+x := {x};
 
-end;

tests/negative/ConstructorExpectedLeftApplication.juvix

@@ -3,4 +3,3 @@ module ConstructorExpectedLeftApplication;
 f : {A : Type} -> A -> A;
 f (x y) := x;
 
-end;

tests/negative/DuplicateClause.juvix

@@ -2,9 +2,6 @@ module DuplicateClause;
 
 axiom T : Type;
 
-id : T → T := λ {
-  t := t
-};
+id : T → T := λ {t := t};
 id t := t;
 
-end;

tests/negative/ImplicitPatternLeftApplication.juvix

@@ -3,4 +3,3 @@ module ImplicitPatternLeftApplication;
 f : {A : Type} -> A -> A;
 f ({x} y) := y;
 
-end;

tests/negative/Internal/ExpectedExplicitArgument.juvix

@@ -1,7 +1,7 @@
 module ExpectedExplicitArgument;
-  type T (A : Type) :=
-    c : A → T A;
 
-  f : {A : Type} → A →  T A;
-  f {A} a := c {A} {a};
-end;
+type T (A : Type) :=
+  | c : A → T A;
+
+f : {A : Type} → A → T A;
+f {A} a := c {A} {a};

tests/negative/Internal/ExpectedExplicitPattern.juvix

@@ -1,7 +1,7 @@
 module ExpectedExplicitPattern;
-  type T (A : Type) :=
-    c : A → T A;
 
-  f : {A : Type} → T A → A;
-  f {_} {c a} := a;
-end;
+type T (A : Type) :=
+  | c : A → T A;
+
+f : {A : Type} → T A → A;
+f {_} {c a} := a;

tests/negative/Internal/ExpectedFunctionType.juvix

@@ -1,10 +1,10 @@
 module ExpectedFunctionType;
-  type Pair (A : Type) :=
-    mkPair : A → A → Pair A;
 
-  type B :=
-    b : B;
+type Pair (A : Type) :=
+  | mkPair : A → A → Pair A;
 
-  f : Pair B → Pair B;
-  f (mkPair a b) := a b;
-end;
+type B :=
+  | b : B;
+
+f : Pair B → Pair B;
+f (mkPair a b) := a b;

tests/negative/Internal/FunctionApplied.juvix

@@ -1,7 +1,7 @@
 module FunctionApplied;
-  type T (A : Type) :=
-    c : A → T A;
 
-  f : {A : Type} → A → T A;
-  f {A} a := c {(A → A) A} a;
-end;
+type T (A : Type) :=
+  | c : A → T A;
+
+f : {A : Type} → A → T A;
+f {A} a := c {(A → A) A} a;

tests/negative/Internal/FunctionPattern.juvix

@@ -1,7 +1,7 @@
 module FunctionPattern;
-  type T :=
-    A : T;
 
-  f : (T → T) → T;
-  f A := A;
-end;
+type T :=
+  | A : T;
+
+f : (T → T) → T;
+f A := A;

tests/negative/Internal/IdenFunctionArgsNoExplicit.juvix

@@ -1,6 +1,6 @@
 module IdenFunctionArgsNoExplicit;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 f : {A : Type} → Nat;
 f := zero;
@@ -8,4 +8,3 @@ f := zero;
 main : Nat;
 main := f;
 
-end;

tests/negative/Internal/LazyBuiltin.juvix

@@ -1,14 +1,15 @@
 module LazyBuiltin;
 
-builtin bool type 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 x _ := x;
 if false _ x := x;
 
 f : Bool -> Bool;
 f x := if x;
 
-end;

tests/negative/Internal/LhsTooManyPatterns.juvix

@@ -1,7 +1,7 @@
 module LhsTooManyPatterns;
-  type T :=
-    A : T;
 
-  f : T → T;
-  f A x := A;
-end;
+type T :=
+  | A : T;
+
+f : T → T;
+f A x := A;

tests/negative/Internal/LiteralInteger.juvix

@@ -1,6 +1,6 @@
 module LiteralInteger;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 h : Nat;
 h := div 1 -2;

tests/negative/Internal/LiteralIntegerString.juvix

@@ -1,6 +1,6 @@
 module LiteralIntegerString;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 f : String -> Nat;
 f _ := 0;

tests/negative/Internal/MultiWrongType.juvix

@@ -1,13 +1,13 @@
 module MultiWrongType;
-  type A :=
-    a : A;
 
-  type B :=
-    b : B;
+type A :=
+  | a : A;
 
-  f : A;
-  f := b;
+type B :=
+  | b : B;
 
-  g : B;
-  g := a;
-end;
+f : A;
+f := b;
+
+g : B;
+g := a;

tests/negative/Internal/PatternConstructor.juvix

@@ -1,11 +1,11 @@
 module PatternConstructor;
-  type A :=
-    a : A;
+
+type A :=
+  | a : A;
 
 type B :=
-    b : B;
+  | b : B;
 
-  f : A → B;
-  f b := b;
+f : A → B;
+f b := b;
 
-end;

tests/negative/Internal/Positivity/E1.juvix

@@ -1,7 +1,7 @@
 module E1;
 
 axiom B : Type;
-type X :=
-  c : (X -> B) -> X;
 
-end;
+type X :=
+  | c : (X -> B) -> X;
+

tests/negative/Internal/Positivity/E10.juvix

@@ -1,11 +1,11 @@
 module E10;
 
 type T0 (A : Type) :=
-t : (A -> T0 A) -> T0 A;
+  | t : (A -> T0 A) -> T0 A;
 
 alias : Type -> Type;
 alias := T0;
 
-type T1 := c : alias T1 -> T1;
+type T1 :=
+  | c : alias T1 -> T1;
 
-end;

tests/negative/Internal/Positivity/E11.juvix

@@ -1,12 +1,11 @@
 module E11;
 
 type T0 (A : Type) :=
-t : (A -> T0 A) -> T0 _;
+  | t : (A -> T0 A) -> T0 _;
 
 alias : Type -> Type -> Type;
 alias A B := A -> B;
 
 type T1 :=
-  c : alias T1 T1 -> _;
+  | c : alias T1 T1 -> _;
 
-end;

tests/negative/Internal/Positivity/E2.juvix

@@ -1,8 +1,7 @@
 module E2;
 
-open import NegParam;
+import NegParam open;
 
 type D :=
-d : T D -> D;
+  | d : T D -> D;
 
-end;

tests/negative/Internal/Positivity/E3.juvix

@@ -1,7 +1,7 @@
 module E3;
 
 axiom B : Type;
-type X  :=
-  c : B -> (X -> B) -> X;
 
-end;
+type X :=
+  | c : B -> (X -> B) -> X;
+

tests/negative/Internal/Positivity/E4.juvix

@@ -1,10 +1,9 @@
 module E4;
 
 type Tree (A : Type) :=
-  leaf : Tree A |
-  node : (A -> Tree A) -> Tree A;
+  | leaf : Tree A
+  | node : (A -> Tree A) -> Tree A;
 
 type Bad :=
-  bad : Tree Bad -> Bad;
+  | bad : Tree Bad -> Bad;
 
-end;

tests/negative/Internal/Positivity/E5.juvix

@@ -1,13 +1,13 @@
 module E5;
 
 type T0 (A : Type) :=
-c0 : (A -> T0 A) -> T0 A;
+  | c0 : (A -> T0 A) -> T0 A;
 
 axiom B : Type;
+
 type T1 (A : Type) :=
-c1 : (B -> T0 A) -> T1 A;
+  | c1 : (B -> T0 A) -> T1 A;
 
 type T2 :=
-c2 : (B -> (B -> T1 T2)) -> T2;
+  | c2 : (B -> B -> T1 T2) -> T2;
 
-end;

tests/negative/Internal/Positivity/E6.juvix

@@ -1,7 +1,7 @@
 module E6;
 
 axiom A : Type;
-type T (A : Type) :=
-c : (A -> (A -> (T A -> A))) -> T A;
 
-end;
+type T (A : Type) :=
+  | c : (A -> A -> T A -> A) -> T A;
+

tests/negative/Internal/Positivity/E7.juvix

@@ -1,9 +1,8 @@
 module E7;
 
 type T0 (A : Type) (B : Type) :=
-c0 : (B -> A) -> T0 A B;
+  | c0 : (B -> A) -> T0 A B;
 
 type T1 (A : Type) :=
-c1 : (A -> T0 A (T1 A)) -> T1 A;
+  | c1 : (A -> T0 A (T1 A)) -> T1 A;
 
-end;

tests/negative/Internal/Positivity/E8.juvix

@@ -1,4 +1,4 @@
 module E8;
+
 type B (A : Type) :=
-b : (A -> B (B A -> A)) -> B A;
-end;
+  | b : (A -> B (B A -> A)) -> B A;

tests/negative/Internal/Positivity/E9.juvix

@@ -1,9 +1,8 @@
 module E9;
 
 type B :=
-b : B;
+  | b : B;
 
 type T :=
-  c : ((B → T) -> T) -> T;
+  | c : ((B → T) -> T) -> T;
 
-end;

tests/negative/Internal/Positivity/NegParam.juvix

@@ -1,4 +1,4 @@
 module NegParam;
+
 type T (A : Type) :=
-c : (A -> T A) -> T A;
-end;
+  | c : (A -> T A) -> T A;

tests/negative/Internal/TooManyArguments.juvix

@@ -1,7 +1,7 @@
 module TooManyArguments;
-  type T (A : Type) :=
-    c : A → T A;
 
-  f : {A : Type} → A → T A;
-  f {A} a := c {A} a a {a} ;
-end;
+type T (A : Type) :=
+  | c : A → T A;
+
+f : {A : Type} → A → T A;
+f {A} a := c {A} a a {a};

tests/negative/Internal/UnsolvedMeta.juvix

@@ -1,9 +1,8 @@
 module UnsolvedMeta;
 
 type Proxy (A : Type) :=
-  x : Proxy A;
+  | x : Proxy A;
 
 t : Proxy _;
 t := x;
 
-end;

tests/negative/Internal/WrongConstructorArity.juvix

@@ -1,7 +1,7 @@
 module WrongConstructorArity;
-  type T :=
-    A : T → T;
 
-  f : T → T;
-  f (A i x) := i;
-end;
+type T :=
+  | A : T → T;
+
+f : T → T;
+f (A i x) := i;

tests/negative/Internal/WrongReturnType.juvix

@@ -1,7 +1,7 @@
 module WrongReturnType;
 
 axiom B : Type;
-type A :=
-c : B;
 
-end;
+type A :=
+  | c : B;
+

tests/negative/Internal/WrongReturnTypeParameters.juvix

@@ -1,6 +1,5 @@
 module WrongReturnTypeParameters;
 
 type A (B : Type) :=
-c : A B B;
+  | c : A B B;
 
-end;

tests/negative/Internal/WrongReturnTypeTooFewArguments.juvix

@@ -1,6 +1,5 @@
 module WrongReturnTypeTooFewArguments;
 
 type A (B : Type) :=
-c : A;
+  | c : A;
 
-end;

tests/negative/Internal/WrongReturnTypeTooManyArguments.juvix

@@ -1,6 +1,5 @@
 module WrongReturnTypeTooManyArguments;
 
 type A (B : Type) :=
-c : A B B;
+  | c : A B B;
 
-end;

tests/negative/Internal/WrongType.juvix

@@ -1,10 +1,10 @@
 module WrongType;
-  type A :=
-    a : A;
 
-  type B :=
-    b : B;
+type A :=
+  | a : A;
 
-  f : A;
-  f := b;
-end;
+type B :=
+  | b : B;
+
+f : A;
+f := b;

tests/negative/LacksFunctionClause.juvix

@@ -1,4 +1,3 @@
 module LacksFunctionClause;
 
-  id : Type → Type → Type;
-end;
+id : Type → Type → Type;

tests/negative/LetMissingClause.juvix

@@ -1,6 +1,7 @@
 module LetMissingClause;
-  id : {A : Type} → A → A;
-  id {A} := let
-      id' : A → A;
-     in id';
-end;
+
+id : {A : Type} → A → A;
+id {A} :=
+  let
+    id' : A → A;
+  in id';

tests/negative/StdlibConflict/Stdlib/Data/Bool.juvix

@@ -1,3 +1,2 @@
 module Stdlib.Data.Bool;
 
-end;

tests/negative/Termination/Data/Bool.juvix

@@ -1,24 +1,24 @@
 module Data.Bool;
-  type Bool :=
-    true : Bool |
-    false : Bool;
 
-  not : Bool → Bool;
-  not true := false;
-  not false := true;
+type Bool :=
+  | true : Bool
+  | false : Bool;
 
-  infixr 2 ||;
-  || : Bool → Bool → Bool;
-  || false a := a;
-  || true _ := true;
+not : Bool → Bool;
+not true := false;
+not false := true;
 
-  infixr 2 &&;
-  && : Bool → Bool → Bool;
-  && false _ := false;
-  && true a := a;
+infixr 2 ||;
+|| : Bool → Bool → Bool;
+|| false a := a;
+|| true _ := true;
 
-  ite : (a : Type) → Bool → a → a → a;
-  ite _ true a _ := a;
-  ite _ false _ b := b;
+infixr 2 &&;
+&& : Bool → Bool → Bool;
+&& false _ := false;
+&& true a := a;
+
+ite : (a : Type) → Bool → a → a → a;
+ite _ true a _ := a;
+ite _ false _ b := b;
 
-end;

tests/negative/Termination/Data/Nat.juvix

@@ -1,27 +1,28 @@
 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);
 
-  import Data.Bool;
-  open Data.Bool;
+infixl 7 *;
+* : ℕ → ℕ → ℕ;
+* zero b := zero;
+* (suc a) b := b + a * b;
 
-  even : ℕ → Bool;
-  odd : ℕ → Bool;
+import Data.Bool;
+open Data.Bool;
 
-  even zero := true;
-  even (suc n) := odd n;
+even : ℕ → Bool;
 
-  odd zero := false;
-  odd (suc n) := even n;
-end;
+odd : ℕ → Bool;
+
+even zero := true;
+even (suc n) := odd n;
+
+odd zero := false;
+odd (suc n) := even n;

tests/negative/Termination/Data/QuickSort.juvix

@@ -7,31 +7,36 @@ import Data.Nat;
 open Data.Nat;
 
 type List (A : Type) :=
-  nil  : List A |
-  cons : A → List A → List A;
+  | nil : List A
+  | cons : A → List A → List A;
 
 filter : (A : Type) → (A → Bool) → List A → List A;
-filter A f nil         := nil A;
-filter A f (cons h hs) := ite (List A) (f h)
-  (cons A h (filter A f hs))
-  (filter A f hs);
+filter A f nil := nil A;
+filter A f (cons h hs) :=
+  ite
+    (List A)
+    (f h)
+    (cons A h (filter A f hs))
+    (filter A f hs);
 
 concat : (A : Type) → List A → List A → List A;
-concat A nil ys         := ys;
+concat A nil ys := ys;
 concat A (cons x xs) ys := cons A x (concat A xs ys);
 
 ltx : (A : Type) → (A → A → Bool) → A → A → Bool;
 ltx A lessThan x y := lessThan y x;
 
 gex : (A : Type) → (A → A → Bool) → A → A → Bool;
-gex A lessThan x y := not (ltx A lessThan x y) ;
+gex A lessThan x y := not (ltx A lessThan x y);
 
 quicksort : (A : Type) → (A → A → Bool) → List A → List A;
 quicksort A _ nil := nil A;
 quicksort A _ (cons x nil) := cons A x (nil A);
 quicksort A lessThan (cons x ys) :=
-  concat A (quicksort A lessThan (filter A (ltx A lessThan x) ys))
-           (concat A
-           (cons A x (nil A))
-           (quicksort A lessThan (filter A (gex A lessThan x)) ys));
-end;
+  concat
+    A
+    (quicksort A lessThan (filter A (ltx A lessThan x) ys))
+    (concat
+      A
+      (cons A x (nil A))
+      (quicksort A lessThan (filter A (gex A lessThan x)) ys));

tests/negative/Termination/Data/Tree.juvix

@@ -1,14 +1,14 @@
 module Data.Tree;
+
 type Tree (A : Type) :=
-  leaf : Tree A |
-  branch  : Tree A → Tree A → Tree A;
+  | leaf : Tree A
+  | branch : Tree A → Tree A → Tree A;
 
 f : (A : Type) → Tree A → Tree A → Tree A;
-f A x leaf         := x;
+f A x leaf := x;
 f A x (branch y z) := f A (f A x y) z;
 
 g : (A : Type) → Tree A → Tree A → Tree A;
-g A x leaf         := x;
+g A x leaf := x;
 g A x (branch y z) := g A z (g A x y);
 
-end;

tests/negative/Termination/Mutual.juvix

@@ -3,9 +3,10 @@ module Mutual;
 axiom A : Type;
 
 f : A -> A -> A;
+
 g : A -> A -> A;
 
 g x y := f x x;
+
 f x y := g x (f x x);
 
-end;

tests/negative/Termination/Ord.juvix

@@ -4,16 +4,17 @@ import Data.Nat;
 open Data.Nat;
 
 type Ord :=
-  ZOrd : Ord |
-  SOrd : Ord -> Ord |
-  Lim  : (ℕ -> Ord) -> Ord;
+  | ZOrd : Ord
+  | SOrd : Ord -> Ord
+  | Lim : (ℕ -> Ord) -> Ord;
 
 addord : Ord -> Ord -> Ord;
-aux-addord : (ℕ -> Ord) -> Ord -> (ℕ -> Ord);
 
-addord (Zord)   y := y;
+aux-addord : (ℕ -> Ord) -> Ord -> ℕ -> Ord;
+
+addord Zord y := y;
 addord (SOrd x) y := SOrd (addord x y);
-addord (Lim f)  y := Lim (aux-addord f y);
+addord (Lim f) y := Lim (aux-addord f y);
+
 aux-addord f y z := addord (f z) y;
 
-end;

tests/negative/Termination/TerminatingF.juvix

@@ -8,6 +8,6 @@ f : A -> A -> A;
 g : A -> A -> A;
 
 g x y := f x x;
+
 f x y := g x (f x x);
 
-end;

tests/negative/Termination/TerminatingG.juvix

@@ -8,6 +8,6 @@ terminating
 g : A -> A -> A;
 
 g x y := f x x;
+
 f x y := g x (f x x);
 
-end;

tests/negative/issue1337/Braces.juvix

@@ -1,10 +1,9 @@
 module Braces;
 
 type Nat :=
-  O : Nat |
-  S : Nat -> Nat;
+  | O : Nat
+  | S : Nat -> Nat;
 
 fun : Nat -> Nat;
 fun (S {S {x}}) := x;
 
-end;

tests/negative/issue1344/D.juvix

@@ -1,8 +1,8 @@
 module D;
-  import Other;
-  import U;
 
-  u : Other.Unit;
-  u := U.t;
+import Other;
+import U;
+
+u : Other.Unit;
+u := U.t;
 
-end;

tests/negative/issue1344/M.juvix

@@ -1,10 +1,10 @@
 module M;
-  import Other;
 
-  type Unit :=
-  t : Unit;
+import Other;
 
-  u : Other.Unit;
-  u := t;
+type Unit :=
+  | t : Unit;
+
+u : Other.Unit;
+u := t;
 
-end;

tests/negative/issue1344/Other.juvix

@@ -1,6 +1,5 @@
 module Other;
 
-  type Unit :=
-  t : Unit;
+type Unit :=
+  | t : Unit;
 
-end;

tests/negative/issue1344/U.juvix

@@ -1,4 +1,5 @@
 module U;
-  type Unit := t : Unit;
-  
-end;
+
+type Unit :=
+  | t : Unit;
+

tests/negative/issue1700/SelfApplication.juvix

@@ -1,9 +1,8 @@
 -- self-application
 module SelfApplication;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 main : IO;
 main := printNatLn (λ {x := x x} id (3 + 4));
 
-end;

tests/positive/Builtins.juvix

@@ -1,6 +1,6 @@
 module Builtins;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 f : String -> IO;
 f s :=

tests/positive/BuiltinsMultiOpenImport/A.juvix

@@ -1,3 +1,3 @@
 module A;
 
-open import Nat;
+import Nat open;

tests/positive/BuiltinsMultiOpenImport/Input.juvix

@@ -1,4 +1,4 @@
 module Input;
 
-open import A;
-open import Nat;
+import A open;
+import Nat open;

tests/positive/Dependencies/.libs/Extra/Extra.juvix

@@ -1,6 +1,6 @@
 module Extra;
 
-open import Base;
+import Base open;
 
 axiom Extra : Type;
 

tests/positive/Dependencies/Input.juvix

@@ -1,7 +1,7 @@
 module Input;
 
-open import Extra;
-open import Base;
-open import Stdlib.Prelude;
+import Extra open;
+import Base open;
+import Stdlib.Prelude open;
 
 axiom x : Extra;

tests/positive/Internal/AsPattern.juvix

@@ -34,10 +34,7 @@ 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 p@(x, s@zero) := snd p + 1;

tests/positive/Internal/Lambda.juvix

@@ -18,37 +18,19 @@ infixr 9 ∘;
     → (A → B)
     → A
     → C;
-∘ {_} {B} {_} :=
-  λ {
-    | f g x := f (g x)
-  };
+∘ {_} {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}
@@ -57,45 +39,26 @@ uncurry :
     → (A → B → C)
     → A × B
     → C;
-uncurry :=
-  λ {
-    | f (a, b) := f a b
-  };
+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)
-      }
+    | (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}
@@ -104,10 +67,7 @@ first :
     → (A → A')
     → A × B
     → A' × B;
-first :=
-  λ {
-    | f (a, b) := f a, b
-  };
+first := λ {f (a, b) := f a, b};
 
 second :
   {A : Type}
@@ -119,10 +79,7 @@ second :
 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) :=
@@ -137,10 +94,7 @@ map {_} :=
   };
 
 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;
@@ -205,25 +159,13 @@ t :
     → {B : Type}
     → ({X : Type} → List X)
     → List A × List B;
-t :=
-  id
-    {({X : Type} → List X) → _}
-    λ {
-      | f := f {_}, f {_}
-    };
+t := id {({X : Type} → List X) → _} λ {f := f {_}, f {_}};
 
 type Box (A : Type) :=
   | 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
-  };
+t1 {A} := λ {(b f) := f A};

tests/positive/Internal/LiteralInt.juvix

@@ -1,6 +1,6 @@
 module LiteralInt;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 type A :=
   | a : A;

tests/positive/Internal/Norm.juvix

@@ -1,6 +1,6 @@
 module Norm;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 main : Nat;
-main := λ{x := x + 2} 1;
+main := λ {x := x + 2} 1;

tests/positive/Internal/Synonyms.juvix

@@ -1,6 +1,6 @@
 module Synonyms;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 Ty1 : Type;
 Ty1 := Bool → Bool;

tests/positive/LocalSynonym.juvix

@@ -1,6 +1,7 @@
 module LocalSynonym;
 
-type Unit := unit : Unit;
+type Unit :=
+  | unit : Unit;
 
 myUnit : Type;
 myUnit := Unit;

tests/positive/MutualLet.juvix

@@ -1,7 +1,7 @@
 module MutualLet;
 
-open import Stdlib.Data.Nat;
-open import Stdlib.Data.Bool;
+import Stdlib.Data.Nat open;
+import Stdlib.Data.Bool open;
 
 main : _;
 main :=

tests/positive/NestedPatterns.juvix

@@ -1,6 +1,6 @@
 module NestedPatterns;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 type MyList (A : Type) :=
   | myList : List A -> MyList A;

tests/positive/Reachability/M.juvix

@@ -1,10 +1,10 @@
 module M;
 
-open import Data.Nat;
-open import Data.Maybe;
-open import Data.Product;
-open import Data.Bool;
-open import Data.Ord;
+import Data.Nat open;
+import Data.Maybe open;
+import Data.Product open;
+import Data.Bool open;
+import Data.Ord open;
 
 f : Bool -> Bool;
 f x := x;

tests/positive/Reachability/N.juvix

@@ -1,7 +1,7 @@
 module N;
 
-open import M;
-open import Stdlib.Prelude;
+import M open;
+import Stdlib.Prelude open;
 
 test : {A : Type} -> A -> A;
 test x := x;

tests/positive/Reachability/O.juvix

@@ -1,7 +1,7 @@
 module O;
 
-open import M public;
-open import Stdlib.Data.Bool;
+import M open public;
+import Stdlib.Data.Bool open;
 
 k : Bool;
 k := true;

tests/positive/StdlibImport/StdlibImport.juvix

@@ -1,6 +1,6 @@
 module StdlibImport;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 import A;
 

tests/positive/Termination/TreeGen.juvix

@@ -1,6 +1,6 @@
 module TreeGen;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 type Tree :=
   | leaf : Tree

tests/positive/TypeAlias.juvix

@@ -39,10 +39,7 @@ funAlias : Type -> Type;
 funAlias a := a -> a;
 
 f : funAlias T;
-f :=
-  \ {
-    | t := t
-  };
+f := \ {t := t};
 
 f' : funAlias T;
 f' t := t;

tests/positive/issue1693/M.juvix

@@ -1,6 +1,6 @@
 module M;
 
-open import Stdlib.Prelude;
+import Stdlib.Prelude open;
 
 S :
   {A : Type}

tests/positive/issue1731/builtinFail.juvix

@@ -1,7 +1,7 @@
 module builtinFail;
 
-open import Stdlib.Data.String;
-open import Stdlib.System.IO;
+import Stdlib.Data.String open;
+import Stdlib.System.IO open;
 
 builtin fail
 axiom fail : {A : Type} → String → A;

tests/positive/issue1731/builtinTrace.juvix

@@ -1,7 +1,7 @@
 module builtinTrace;
 
-open import Stdlib.Prelude;
-open import Stdlib.Data.Nat.Ord;
+import Stdlib.Prelude open;
+import Stdlib.Data.Nat.Ord open;
 
 builtin trace
 axiom trace : {A : Type} → A → A;