Reformat examples

examples/demo/Demo.juvix

@@ -24,8 +24,7 @@ mirror : {A : Type} → Tree A → Tree A
   | t@(leaf _) := t
   | (node x l r) := node x (mirror r) (mirror l);
 
-tree : Tree Nat :=
-  node 2 (node 3 (leaf 0) (leaf 1)) (leaf 7);
+tree : Tree Nat := node 2 (node 3 (leaf 0) (leaf 1)) (leaf 7);
 
 preorder : {A : Type} → Tree A → List A
   | (leaf x) := x :: nil
@@ -35,15 +34,11 @@ terminating
 sort {A} {{Ord A}} : List A → List A
   | nil := nil
   | xs@(_ :: nil) := xs
-  | xs :=
-    uncurry
-      merge
-      (both sort (splitAt (div (length xs) 2) xs));
+  | xs := uncurry merge (both sort (splitAt (div (length xs) 2) xs));
 
 printNatListLn : List Nat → IO
   | nil := printStringLn "nil"
-  | (x :: xs) :=
-    printNat x >>> printString " :: " >>> printNatListLn xs;
+  | (x :: xs) := printNat x >>> printString " :: " >>> printNatListLn xs;
 
 main : IO :=
   printStringLn "Hello!"

examples/midsquare/MidSquareHash.juvix

@@ -14,11 +14,7 @@ pow : Nat -> Nat
 --- `hash' N` hashes a number with max N bits (i.e. smaller than 2^N) into 6 bits
 --- (i.e. smaller than 64) using the mid-square algorithm.
 hash' : Nat -> Nat -> Nat
-  | (suc n@(suc (suc m))) x :=
-    ite
-      (x < pow n)
-      (hash' n x)
-      (mod (div (x * x) (pow m)) (pow 6))
+  | (suc n@(suc (suc m))) x := ite (x < pow n) (hash' n x) (mod (div (x * x) (pow m)) (pow 6))
   | _ x := x * x;
 
 hash : Nat -> Nat := hash' 16;

examples/midsquare/MidSquareHashUnrolled.juvix

@@ -57,56 +57,43 @@ hash3 : Nat -> Nat
   | x := x * x;
 
 hash4 : Nat -> Nat
-  | x :=
-    ite (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
+  | x := ite (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
 
 hash5 : Nat -> Nat
-  | x :=
-    ite (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
+  | x := ite (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
 
 hash6 : Nat -> Nat
-  | x :=
-    ite (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
+  | x := ite (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
 
 hash7 : Nat -> Nat
-  | x :=
-    ite (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
+  | x := ite (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
 
 hash8 : Nat -> Nat
-  | x :=
-    ite (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
+  | x := ite (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
 
 hash9 : Nat -> Nat
-  | x :=
-    ite (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
+  | x := ite (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
 
 hash10 : Nat -> Nat
-  | x :=
-    ite (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
+  | x := ite (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
 
 hash11 : Nat -> Nat
-  | x :=
-    ite (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
+  | x := ite (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
 
 hash12 : Nat -> Nat
-  | x :=
-    ite (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
+  | x := ite (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
 
 hash13 : Nat -> Nat
-  | x :=
-    ite (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
+  | x := ite (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
 
 hash14 : Nat -> Nat
-  | x :=
-    ite (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
+  | x := ite (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
 
 hash15 : Nat -> Nat
-  | x :=
-    ite (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
+  | x := ite (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
 
 hash16 : Nat -> Nat
-  | x :=
-    ite (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
+  | x := ite (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
 
 hash : Nat -> Nat := hash16;
 

examples/milestone/Bank/Bank.juvix

@@ -39,22 +39,14 @@ module Balances;
   --- Increments the amount associated with a certain ;Field;.
   increment : Field -> Nat -> Balances -> Balances
     | f n nil := (f, n) :: nil
-    | f n ((b, bn) :: bs) :=
-      ite
-        (f == b)
-        ((b, bn + n) :: bs)
-        ((b, bn) :: increment f n bs);
+    | f n ((b, bn) :: bs) := ite (f == b) ((b, bn + n) :: bs) ((b, bn) :: increment f n bs);
 
   --- Decrements the amount associated with a certain ;Field;.
   --- If the ;Field; is not found, it does nothing.
   --- Subtraction is truncated to ;zero;.
   decrement : Field -> Nat -> Balances -> Balances
     | _ _ nil := nil
-    | f n ((b, bn) :: bs) :=
-      ite
-        (f == b)
-        ((b, sub bn n) :: bs)
-        ((b, bn) :: decrement f n bs);
+    | f n ((b, bn) :: bs) := ite (f == b) ((b, sub bn n) :: bs) ((b, bn) :: decrement f n bs);
 
   emtpyBalances : Balances := nil;
 
@@ -90,16 +82,13 @@ assert : {A : Type} -> Bool -> A -> A
 ---
 --- `caller`: Who is creating the transaction. It must be the bank.
 issue : Address -> Address -> Nat -> Token
-  | caller owner amount :=
-    assert (caller == bankAddress) (mkToken owner 0 amount);
+  | caller owner amount := assert (caller == bankAddress) (mkToken owner 0 amount);
 
 --- Deposits some amount of money into the bank.
-deposit
-  (bal : Balances) (token : Token) (amount : Nat) : Token :=
+deposit (bal : Balances) (token : Token) (amount : Nat) : Token :=
   let
     difference : Nat := sub (getAmount token) amount;
-    remaining : Token :=
-      mkToken (getOwner token) (getGates token) difference;
+    remaining : Token := mkToken (getOwner token) (getGates token) difference;
     hash : Field := hashAddress (getOwner token);
     bal' : Balances := increment hash amount bal;
   in runOnChain (commitBalances bal') remaining;

examples/milestone/Collatz/Collatz.juvix

@@ -2,8 +2,7 @@ module Collatz;
 
 import Stdlib.Prelude open;
 
-collatzNext (n : Nat) : Nat :=
-  ite (mod n 2 == 0) (div n 2) (3 * n + 1);
+collatzNext (n : Nat) : Nat := ite (mod n 2 == 0) (div n 2) (3 * n + 1);
 
 collatz : Nat → Nat
   | zero := zero
@@ -15,14 +14,10 @@ run (f : Nat → Nat) : 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/Fibonacci/Fibonacci.juvix

@@ -8,5 +8,4 @@ fib : Nat → Nat → Nat → Nat
 
 fibonacci (n : Nat) : Nat := fib n 0 1;
 
-main : IO :=
-  readLn (stringToNat >> fibonacci >> printNatLn);
+main : IO := readLn (stringToNat >> fibonacci >> printNatLn);

examples/milestone/Hanoi/Hanoi.juvix

@@ -15,9 +15,7 @@ module Hanoi;
 import Stdlib.Prelude open;
 
 --- Concatenates a list of strings
---- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
-  :: "b"
-  :: nil;
+--- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil;
 concat : List String → String := foldl (++str) "";
 
 intercalate : String → List String → String
@@ -29,8 +27,7 @@ singleton : {A : Type} → A → List A
 
 --- Produce a ;String; representation of a ;List Nat;
 showList : List Nat → String
-  | xs :=
-    "[" ++str intercalate "," (map natToString xs) ++str "]";
+  | xs := "[" ++str intercalate "," (map natToString xs) ++str "]";
 
 --- A Peg represents a peg in the towers of Hanoi game
 type Peg :=
@@ -47,17 +44,11 @@ showPeg : Peg → String
 type Move := move : Peg → Peg → Move;
 
 showMove : Move → String
-  | (move from to) :=
-    showPeg from ++str " -> " ++str showPeg to;
+  | (move from to) := showPeg from ++str " -> " ++str showPeg to;
 
 --- 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 (move p1 p2)
-      ++ hanoi n p3 p2 p1;
-
-main : IO :=
-  printStringLn
-    (unlines (map showMove (hanoi 5 left middle right)));
+  | (suc n) p1 p2 p3 := hanoi n p1 p3 p2 ++ singleton (move p1 p2) ++ hanoi n p3 p2 p1;
+
+main : IO := printStringLn (unlines (map showMove (hanoi 5 left middle right)));

examples/milestone/PascalsTriangle/PascalsTriangle.juvix

@@ -15,27 +15,18 @@ scanIterate {A} : Nat → (A → A) → A → List A
 singleton {A} (a : A) : List A := a :: nil;
 
 --- Concatenates a list of strings
---- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
-  :: "b"
-  :: nil;
+--- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil;
 concat : List String → String := foldl (++str) "";
 
-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);
+  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)));
+main : IO := printStringLn (unlines (map showList (pascal 10)));

examples/milestone/TicTacToe/CLI/TicTacToe.juvix

@@ -10,33 +10,22 @@ import Logic.Game open;
 
 --- A ;String; that prompts the user for their input
 prompt (x : GameState) : String :=
-  "\n"
-    ++str showGameState x
-    ++str "\nPlayer "
-    ++str showSymbol (player x)
-    ++str ": ";
+  "\n" ++str showGameState x ++str "\nPlayer " ++str showSymbol (player x) ++str ": ";
 
-nextMove (s : GameState) : String → GameState :=
-  stringToNat >> validMove >> flip playMove s;
+nextMove (s : GameState) : String → GameState := stringToNat >> validMove >> flip playMove s;
 
 --- Main loop
 terminating
 run : GameState → IO
   | (state b p (terminate msg)) :=
-    printStringLn
-      ("\n"
-        ++str showGameState (state b p noError)
-        ++str "\n"
-        ++str msg)
+    printStringLn ("\n" ++str showGameState (state b p noError) ++str "\n" ++str msg)
   | (state b p (continue msg)) :=
     printString (msg ++str prompt (state b p noError))
       >>> readLn (run << nextMove (state b p noError))
-  | x :=
-    printString (prompt x) >>> readLn (run << nextMove x);
+  | x := printString (prompt x) >>> readLn (run << nextMove x);
 
 --- 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

@@ -21,22 +21,16 @@ full : List Square → Bool
   | _ := failwith "full";
 
 diagonals : List (List Square) → List (List Square)
-  | ((a1 :: _ :: b1 :: nil)
-    :: (_ :: c :: _ :: nil)
-    :: (b2 :: _ :: a2 :: nil)
-    :: nil) :=
+  | ((a1 :: _ :: b1 :: nil) :: (_ :: c :: _ :: nil) :: (b2 :: _ :: a2 :: nil) :: nil) :=
     (a1 :: c :: a2 :: nil) :: (b1 :: c :: b2 :: nil) :: nil
   | _ := failwith "diagonals";
 
-columns : List (List Square) → List (List Square) :=
-  transpose;
+columns : List (List Square) → List (List Square) := transpose;
 
 rows : List (List Square) → List (List Square) := id;
 
 --- 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 → String
-  | (board squares) :=
-    unlines (surround "+---+---+---+" (map showRow squares));
+  | (board squares) := unlines (surround "+---+---+---+" (map showRow squares));

examples/milestone/TicTacToe/Logic/Extra.juvix

@@ -4,15 +4,11 @@ module Logic.Extra;
 import Stdlib.Prelude open;
 
 --- Concatenates a list of strings
---- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
-  :: "b"
-  :: nil;
+--- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil;
 concat : List String → String := foldl (++str) "";
 
 --- 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,33 +14,17 @@ checkState : GameState → GameState
   | (state b p e) :=
     ite
       (won (state b p e))
-      (state
-        b
-        p
-        (terminate
-          ("Player " ++str showSymbol (switch p) ++str " wins!")))
-      (ite
-        (draw (state b p e))
-        (state b p (terminate "It's a draw!"))
-        (state b p e));
+      (state b p (terminate ("Player " ++str showSymbol (switch p) ++str " wins!")))
+      (ite (draw (state b p e)) (state b p (terminate "It's a draw!")) (state b p e));
 
 --- Given a player attempted move, updates the state accordingly.
 playMove : Maybe Nat → GameState → GameState
-  | nothing (state b p _) :=
-    state b p (continue "\nInvalid number, try again\n")
+  | nothing (state b p _) := state b p (continue "\nInvalid number, try again\n")
   | (just k) (state (board s) player e) :=
     ite
       (not (elem (==) k (possibleMoves (flatten s))))
-      (state
-        (board s)
-        player
-        (continue "\nThe square is already occupied, try again\n"))
-      (checkState
-        (state
-          (board (map (map (replace player k)) s))
-          (switch player)
-          noError));
+      (state (board s) player (continue "\nThe square is already occupied, try again\n"))
+      (checkState (state (board (map (map (replace player k)) s)) (switch player) noError));
 
 --- Returns ;just; if the given ;Nat; is in range of 1..9
-validMove (n : Nat) : Maybe Nat :=
-  ite (n <= 9 && n >= 1) (just n) nothing;
+validMove (n : Nat) : Maybe Nat := ite (n <= 9 && n >= 1) (just n) nothing;