format

examples/milestone/Bank/Bank.juvix

@@ -77,7 +77,8 @@ issue (caller owner : Address) (amount : Nat) : Token :=
 deposit (bal : Balances) (token : Token) (amount : Nat) : Token :=
   let
     difference : Nat := sub (Token.amount token) amount;
-    remaining : Token := mkToken (Token.owner token) (Token.gates token) difference;
+    remaining : Token :=
+      mkToken (Token.owner token) (Token.gates token) difference;
     hash : Field := hashAddress (Token.owner token);
     bal' : Balances := increment hash amount bal;
   in runOnChain (commitBalances bal') remaining;

examples/milestone/Collatz/Collatz.juvix

@@ -19,10 +19,12 @@ run (f : Nat -> Nat) (n : Nat) : IO :=
     | suc zero := printNatLn 1 >>> printStringLn "Finished!"
     | n := printNatLn n >>> run f (f n);
 
-welcome : String := "Collatz calculator\n------------------\n\nType a number then ENTER";
+welcome : String :=
+  "Collatz calculator\n------------------\n\nType a number then ENTER";
 
 resultHeading : String := "Collatz sequence:";
 
 main : IO :=
   printStringLn welcome
-    >>> readLn λ{s := printStringLn resultHeading >>> run collatz (stringToNat s)};
+    >>> readLn
+      λ{s := printStringLn resultHeading >>> run collatz (stringToNat s)};

examples/milestone/Hanoi/Hanoi.juvix

@@ -18,13 +18,15 @@ import Stdlib.Prelude open;
 --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil;
 concat (list : List String) : String := foldl (++str) "" list;
 
-intercalate (sep : String) (xs : List String) : String := concat (intersperse sep xs);
+intercalate (sep : String) (xs : List String) : String :=
+  concat (intersperse sep xs);
 
 --- Produce a singleton List
 singleton {A} (a : A) : List A := a :: nil;
 
 --- Produce a ;String; representation of a ;List Nat;
-showList (xs : List Nat) : String := "[" ++str intercalate "," (map natToString xs) ++str "]";
+showList (xs : List Nat) : String :=
+  "[" ++str intercalate "," (map natToString xs) ++str "]";
 
 --- A Peg represents a peg in the towers of Hanoi game
 type Peg :=
@@ -50,6 +52,7 @@ showMove (move : Move) : String :=
 --- Produce a list of ;Move;s that solves the towers of Hanoi game
 hanoi : Nat -> Peg -> Peg -> Peg -> List Move
   | zero _ _ _ := nil
-  | (suc n) p1 p2 p3 := hanoi n p1 p3 p2 ++ singleton (mkMove p1 p2) ++ hanoi n p3 p2 p1;
+  | (suc n) p1 p2 p3 :=
+    hanoi n p1 p3 p2 ++ singleton (mkMove p1 p2) ++ hanoi n p3 p2 p1;
 
 main : IO := printStringLn (unlines (map showMove (hanoi 5 left middle right)));

examples/milestone/PascalsTriangle/PascalsTriangle.juvix

@@ -18,15 +18,18 @@ singleton {A} (value : A) : List A := value :: nil;
 --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil;
 concat (list : List String) : String := foldl (++str) "" list;
 
-intercalate (sep : String) (xs : List String) : String := concat (intersperse sep xs);
+intercalate (sep : String) (xs : List String) : String :=
+  concat (intersperse sep xs);
 
-showList (xs : List Nat) : String := "[" ++str intercalate "," (map natToString xs) ++str "]";
+showList (xs : List Nat) : String :=
+  "[" ++str intercalate "," (map natToString xs) ++str "]";
 
 --- Compute the next row of Pascal's triangle
 pascalNextRow (row : List Nat) : List Nat :=
   zipWith (+) (singleton zero ++ row) (row ++ singleton zero);
 
 --- Produce Pascal's triangle to a given depth
-pascal (rows : Nat) : List (List Nat) := scanIterate rows pascalNextRow (singleton 1);
+pascal (rows : Nat) : List (List Nat) :=
+  scanIterate rows pascalNextRow (singleton 1);
 
 main : IO := printStringLn (unlines (map showList (pascal 10)));

examples/milestone/TicTacToe/CLI/TicTacToe.juvix

@@ -25,15 +25,20 @@ run (state : GameState) : IO :=
   case GameState.error state of
     | terminate msg :=
       printStringLn
-        ("\n" ++str showGameState state@GameState{error := noError} ++str "\n" ++str msg)
+        ("\n"
+          ++str showGameState state@GameState{error := noError}
+          ++str "\n"
+          ++str msg)
     | continue msg :=
       let
         state' := state@GameState{error := noError};
-      in printString (msg ++str prompt state') >>> readLn (nextMove state' >> run)
+      in printString (msg ++str prompt state')
+        >>> readLn (nextMove state' >> run)
     | _ := printString (prompt state) >>> readLn (nextMove state >> run);
 
 --- The welcome message
-welcome : String := "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move";
+welcome : String :=
+  "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move";
 
 --- The entry point of the program
 main : IO := printStringLn welcome >>> run beginState;

examples/milestone/TicTacToe/Logic/Board.juvix

@@ -23,16 +23,20 @@ full (list : List Square) : Bool :=
 
 diagonals (squares : List (List Square)) : List (List Square) :=
   case squares of
-    | (a1 :: _ :: b1 :: nil) :: (_ :: c :: _ :: nil) :: (b2 :: _ :: a2 :: nil) :: nil :=
-      (a1 :: c :: a2 :: nil) :: (b1 :: c :: b2 :: nil) :: nil
+    | (a1 :: _ :: b1 :: nil)
+      :: (_ :: c :: _ :: nil)
+      :: (b2 :: _ :: a2 :: nil)
+      :: nil := (a1 :: c :: a2 :: nil) :: (b1 :: c :: b2 :: nil) :: nil
     | _ := failwith "diagonals";
 
-columns (squares : List (List Square)) : List (List Square) := transpose squares;
+columns (squares : List (List Square)) : List (List Square) :=
+  transpose squares;
 
 rows (squares : List (List Square)) : List (List Square) := squares;
 
 --- Textual representation of a ;List Square;
-showRow (xs : List Square) : String := concat (surround "|" (map showSquare xs));
+showRow (xs : List Square) : String :=
+  concat (surround "|" (map showSquare xs));
 
 showBoard (board : Board) : String :=
   unlines (surround "+---+---+---+" (map showRow (Board.squares board)));

examples/milestone/TicTacToe/Logic/Extra.juvix

@@ -8,7 +8,9 @@ import Stdlib.Prelude open;
 concat (list : List String) : String := foldl (++str) "" list;
 
 --- It inserts the first ;String; at the beginning, in between, and at the end of the second list
-surround (x : String) (xs : List String) : List String := (x :: intersperse x xs) ++ x :: nil;
+surround (x : String) (xs : List String) : List String :=
+  (x :: intersperse x xs) ++ x :: nil;
 
 --- It inserts the first ;String; in between the ;String;s in the second list and concatenates the result
-intercalate (sep : String) (xs : List String) : String := concat (intersperse sep xs);
+intercalate (sep : String) (xs : List String) : String :=
+  concat (intersperse sep xs);

examples/milestone/TicTacToe/Logic/Game.juvix

@@ -14,21 +14,25 @@ checkState (state : GameState) : GameState :=
   if
     | won state :=
       state@GameState{error := terminate
-        ("Player " ++str showSymbol (switch (GameState.player state)) ++str " wins!")}
+        ("Player "
+          ++str showSymbol (switch (GameState.player state))
+          ++str " wins!")}
     | draw state := state@GameState{error := terminate "It's a draw!"}
     | else := state;
 
 --- Given a player attempted move, updates the state accordingly.
 playMove (attemptedMove : Maybe Nat) (state : GameState) : GameState :=
   case attemptedMove of
-    | nothing := state@GameState{error := continue "\nInvalid number, try again\n"}
+    | nothing :=
+      state@GameState{error := continue "\nInvalid number, try again\n"}
     | just k :=
       let
         squares := Board.squares (GameState.board state);
         player' := GameState.player state;
       in if
         | not (isMember k (possibleMoves (flatten squares))) :=
-          state@GameState{error := continue "\nThe square is already occupied, try again\n"}
+          state@GameState{error := continue
+            "\nThe square is already occupied, try again\n"}
         | else :=
           checkState
             mkGameState@{

examples/milestone/TicTacToe/Logic/GameState.juvix

@@ -29,7 +29,10 @@ beginState : GameState :=
       mkBoard
         (map
           (map empty)
-          ((1 :: 2 :: 3 :: nil) :: (4 :: 5 :: 6 :: nil) :: (7 :: 8 :: 9 :: nil) :: nil));
+          ((1 :: 2 :: 3 :: nil)
+            :: (4 :: 5 :: 6 :: nil)
+            :: (7 :: 8 :: 9 :: nil)
+            :: nil));
     player := X;
     error := noError
   };

tests/positive/Ape.juvix

@@ -51,7 +51,11 @@ nesting : String :=
                                     (wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
                                       (wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
                                         (wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
-                                          ("" + "" + "" + "" + ""))))))))))))))))))));
+                                          (""
+                                            + ""
+                                            + ""
+                                            + ""
+                                            + ""))))))))))))))))))));
 
 t : String :=
   "Hellooooooooo"

tests/positive/Format.juvix

@@ -126,7 +126,10 @@ t : String :=
         +l6 "Hellooooooooo"
         +l6 ("Hellooooooooo" +r6 "Hellooooooooo" +r6 "Hellooooooooo")
         +l6 "Hellooooooooo"
-        +l6 "Hellooooooooo" +l7 "Hellooooooooo" +l7 "Hellooooooooo" +l7 "Hellooooooooo"
+        +l6 "Hellooooooooo"
+          +l7 "Hellooooooooo"
+          +l7 "Hellooooooooo"
+          +l7 "Hellooooooooo"
       , "hi"
       , "hi";
 

tests/positive/Internal/Positivity2/main.juvix

@@ -55,5 +55,6 @@ module E6;
 
   type Box := mkBox@{unbox : Nat};
 
-  type Foldable := mkFoldable@{for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B};
+  type Foldable :=
+    mkFoldable@{for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B};
 end;

tests/positive/Isabelle/isabelle/Program.thy

@@ -225,7 +225,8 @@ fun funR3 :: "(R, R) Either' \<Rightarrow> R" where
                         r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))) |
             v'4 \<Rightarrow>
               (case v'4 of
-                 (Right' r') \<Rightarrow> r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))"
+                 (Right' r') \<Rightarrow>
+                   r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))"
 
 fun funR4 :: "R \<Rightarrow> R" where
   "funR4 r'0 = (r'0 (| R.r2 := R.r1 r'0 |))"

tests/positive/StdlibList/Data/List.juvix

@@ -65,7 +65,8 @@ splitAt : (a : Type) → ℕ → List a → List a × List a
   | a _ nil := , nil nil
   | a zero xs := , nil xs
   | a (suc zero) (:: x xs) := , (:: x nil) xs
-  | a (suc (suc m)) (:: x xs) := match (splitAt a m xs) λ{(, xs' xs'') := , (:: x xs') xs''};
+  | 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

tests/positive/issue3048/main.juvix

@@ -3,6 +3,14 @@ module main;
 import Other;
 
 type Tree (A : Type) :=
-  node (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A);
+  node (Tree A)
+       (Tree A)
+       (Tree A)
+       (Tree A)
+       (Tree A)
+       (Tree A)
+       (Tree A)
+       (Tree A)
+       (Tree A);
 
 type Foo := mkFoo (Tree Foo);