Format examples

Makefile

@@ -162,7 +162,6 @@ juvix-format: $(TOFORMAT)
 $(TOFORMAT): %:
 	@echo "Formatting $@"
 	@juvix dev scope $@ --with-comments > $@.tmp
-	@echo "" >> $@.tmp
 	@mv $@.tmp $@
 	@echo "Typechecking formatted $@"
 	@juvix typecheck $@ --only-errors

examples/demo/Demo.juvix

@@ -32,29 +32,28 @@ module Demo;
 
   preorder : {A : Type} → Tree A → List A;
   preorder (leaf x) := x :: nil;
-  preorder (node x l r) := x
-    :: nil
-    ++ preorder l
-    ++ preorder r;
+  preorder (node x l r) :=
+    x :: nil ++ preorder l ++ preorder r;
 
   terminating
   sort : {A : Type} → (A → A → Ordering) → List A → List A;
   sort _ nil := nil;
   sort _ xs@(_ :: nil) := xs;
-  sort cmp xs := uncurry
-    (merge cmp)
-    (both (sort cmp) (splitAt (div (length xs) 2) xs));
+  sort cmp xs :=
+    uncurry
+      (merge cmp)
+      (both (sort cmp) (splitAt (div (length xs) 2) xs));
 
   printNatListLn : List Nat → IO;
   printNatListLn nil := printStringLn "nil";
-  printNatListLn (x :: xs) := printNat x
-    >> printString " :: "
-    >> printNatListLn xs;
+  printNatListLn (x :: xs) :=
+    printNat x >> printString " :: " >> printNatListLn xs;
 
   main : IO;
-  main := printStringLn "Hello!"
-    >> printNatListLn (preorder (mirror tree))
-    >> printNatListLn (sort compare (preorder (mirror tree)))
-    >> printNatLn (log2 3)
-    >> printNatLn (log2 130);
+  main :=
+    printStringLn "Hello!"
+      >> printNatListLn (preorder (mirror tree))
+      >> printNatListLn (sort compare (preorder (mirror tree)))
+      >> printNatLn (log2 3)
+      >> printNatLn (log2 130);
 end;

examples/milestone/Collatz/Collatz.juvix

@@ -2,7 +2,7 @@ module Collatz;
   open import Stdlib.Prelude;
 
   mapMaybe : {A : Type} → {B : Type} → (A → B) → Maybe
-    A → Maybe B;
+      A → Maybe B;
   mapMaybe _ nothing := nothing;
   mapMaybe f (just x) := just (f x);
 
@@ -23,18 +23,20 @@ module Collatz;
 
   -- IO
   --- -----------------------------------------------------------------------------
-
   output : Nat → Nat × IO;
-  output n := n , printNatLn n;
+  output n := n, printNatLn n;
 
   terminating
   run : (Nat → Nat) → Nat → IO;
   run _ (suc zero) := printStringLn "Finished!";
   run f n := run f (fst (output (f n)));
 
   welcome : String;
-  welcome := "Collatz calculator\n------------------\n\nType a number then ENTER";
+  welcome :=
+    "Collatz calculator\n------------------\n\nType a number then ENTER";
 
   main : IO;
-  main := printStringLn welcome >> readLn (run collatz ∘ stringToNat);
+  main :=
+    printStringLn welcome
+      >> readLn (run collatz ∘ stringToNat);
 end;

examples/milestone/Hanoi/Hanoi.juvix

@@ -19,8 +19,8 @@ module Hanoi;
   --- Concatenates a list of strings
 
   --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
-  :: "b"
-  :: nil;
+    :: "b"
+    :: nil;
   concat : List String → String;
   concat := foldl (++str) "";
 
@@ -37,9 +37,8 @@ module Hanoi;
 
   --- Produce a ;String; representation of a ;List Nat;
   showList : List Nat → String;
-  showList xs := "["
-    ++str intercalate "," (map natToString xs)
-    ++str "]";
+  showList xs :=
+    "[" ++str intercalate "," (map natToString xs) ++str "]";
 
   --- A Peg represents a peg in the towers of Hanoi game
   type Peg :=
@@ -57,18 +56,19 @@ module Hanoi;
     | move : Peg → Peg → Move;
 
   showMove : Move → String;
-  showMove (move from to) := showPeg from
-    ++str " -> "
-    ++str showPeg to;
+  showMove (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;
   hanoi zero _ _ _ := nil;
-  hanoi (suc n) p1 p2 p3 := hanoi n p1 p3 p2
-    ++ singleton (move p1 p2)
-    ++ hanoi n p3 p2 p1;
+  hanoi (suc n) p1 p2 p3 :=
+    hanoi n p1 p3 p2
+      ++ singleton (move p1 p2)
+      ++ hanoi n p3 p2 p1;
 
   main : IO;
-  main := printStringLn
-    (unlines (map showMove (hanoi 5 left middle right)));
+  main :=
+    printStringLn
+      (unlines (map showMove (hanoi 5 left middle right)));
 end;

examples/milestone/PascalsTriangle/PascalsTriangle.juvix

@@ -9,7 +9,7 @@ module PascalsTriangle;
   open import Stdlib.Prelude;
 
   zipWith : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → List
-    A → List B → List C;
+      A → List B → List C;
   zipWith f nil _ := nil;
   zipWith f _ nil := nil;
   zipWith f (x :: xs) (y :: ys) := f x y :: zipWith f xs ys;
@@ -26,8 +26,8 @@ module PascalsTriangle;
   --- Concatenates a list of strings
 
   --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
-  :: "b"
-  :: nil;
+    :: "b"
+    :: nil;
   concat : List String → String;
   concat := foldl (++str) "";
 
@@ -39,16 +39,16 @@ module PascalsTriangle;
   unlines := intercalate "\n";
 
   showList : List Nat → String;
-  showList xs := "["
-    ++str intercalate "," (map natToString xs)
-    ++str "]";
+  showList xs :=
+    "[" ++str intercalate "," (map natToString xs) ++str "]";
 
   --- Compute the next row of Pascal's triangle
   pascalNextRow : List Nat → List Nat;
-  pascalNextRow row := zipWith
-    (+)
-    (singleton zero ++ row)
-    (row ++ singleton zero);
+  pascalNextRow row :=
+    zipWith
+      (+)
+      (singleton zero ++ row)
+      (row ++ singleton zero);
 
   --- Produce Pascal's triangle to a given depth
   pascal : Nat → List (List Nat);

examples/milestone/TicTacToe/CLI/TicTacToe.juvix

@@ -14,30 +14,35 @@ module CLI.TicTacToe;
 
   --- A ;String; that prompts the user for their input
   prompt : GameState → String;
-  prompt x := "\n"
-    ++str showGameState x
-    ++str "\nPlayer "
-    ++str showSymbol (player x)
-    ++str ": ";
+  prompt x :=
+    "\n"
+      ++str showGameState x
+      ++str "\nPlayer "
+      ++str showSymbol (player x)
+      ++str ": ";
 
   nextMove : GameState → String → GameState;
   nextMove s := flip playMove s ∘ validMove ∘ stringToNat;
 
   --- Main loop
   terminating
   run : GameState → IO;
-  run (state b p (terminate msg)) := printStringLn
-    ("\n"
-    ++str showGameState (state b p noError)
-    ++str "\n"
-    ++str msg);
-  run (state b p (continue msg)) := printString (msg ++str prompt (state b p noError)) >>
-    readLn (run ∘ nextMove (state b p noError));
-  run x := printString (prompt x) >> readLn (run ∘ nextMove x);
+  run (state b p (terminate msg)) :=
+    printStringLn
+      ("\n"
+        ++str showGameState (state b p noError)
+        ++str "\n"
+        ++str msg);
+  run (state b p (continue msg)) :=
+    printString (msg ++str prompt (state b p noError))
+      >> readLn (run ∘ nextMove (state b p noError));
+  run x :=
+    printString (prompt x) >> readLn (run ∘ nextMove x);
 
   --- The welcome message
   welcome : String;
-  welcome := "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move";
+  welcome :=
+    "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move";
 
   --- The entry point of the program
   main : IO;

examples/milestone/TicTacToe/Logic/Board.juvix

@@ -19,12 +19,8 @@ module Logic.Board;
   full (a :: b :: c :: nil) := ==Square a b && ==Square b c;
 
   diagonals : List (List Square) → List (List Square);
-  diagonals ((a1 :: _ :: b1 :: nil) :: (_ :: c :: _ :: nil) :: (b2 :: _ :: a2 :: nil) :: nil) := (a1
-      :: c
-      :: a2
-      :: nil)
-    :: (b1 :: c :: b2 :: nil)
-    :: nil;
+  diagonals ((a1 :: _ :: b1 :: nil) :: (_ :: c :: _ :: nil) :: (b2 :: _ :: a2 :: nil) :: nil) :=
+    (a1 :: c :: a2 :: nil) :: (b1 :: c :: b2 :: nil) :: nil;
 
   columns : List (List Square) → List (List Square);
   columns := transpose;
@@ -37,6 +33,6 @@ module Logic.Board;
   showRow xs := concat (surround "|" (map showSquare xs));
 
   showBoard : Board → String;
-  showBoard (board squares) := unlines
-    (surround "+---+---+---+" (map showRow squares));
+  showBoard (board squares) :=
+    unlines (surround "+---+---+---+" (map showRow squares));
 end;

examples/milestone/TicTacToe/Logic/Extra.juvix

@@ -5,7 +5,9 @@ module Logic.Extra;
 
   --- 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;
   concat := foldl (++str) "";
 

examples/milestone/TicTacToe/Logic/Game.juvix

@@ -14,35 +14,35 @@ module Logic.Game;
 
   --- Checks if we reached the end of the game.
   checkState : GameState → GameState;
-  checkState (state b p e) := if
-    (won (state b p e))
-    (state
-      b
-      p
-      (terminate
-        ("Player " ++str showSymbol (switch p) ++str " wins!")))
-    (if
-      (draw (state b p e))
-      (state b p (terminate "It's a draw!"))
-      (state b p e));
+  checkState (state b p e) :=
+    if
+      (won (state b p e))
+      (state
+        b
+        p
+        (terminate
+          ("Player " ++str showSymbol (switch p) ++str " wins!")))
+      (if
+        (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;
-  playMove nothing (state b p _) := state
-    b
-    p
-    (continue "\nInvalid number, try again\n");
-  playMove (just k) (state (board s) player e) := if
-    (not (elem (==) k (possibleMoves (flatten s))))
-    (state
-      (board s)
-      player
-      (continue "\nThe square is already occupied, try again\n"))
-    (checkState
+  playMove nothing (state b p _) :=
+    state b p (continue "\nInvalid number, try again\n");
+  playMove (just k) (state (board s) player e) :=
+    if
+      (not (elem (==) k (possibleMoves (flatten s))))
       (state
-        (board (map (map (replace player k)) s))
-        (switch player)
-        noError));
+        (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 : Nat → Maybe Nat;

examples/milestone/TicTacToe/Logic/GameState.juvix

@@ -24,25 +24,27 @@ module Logic.GameState;
 
   --- initial ;GameState;
   beginState : GameState;
-  beginState := state
-    (board
-      (map
-        (map empty)
-        ((1 :: 2 :: 3 :: nil)
-        :: (4 :: 5 :: 6 :: nil)
-        :: (7 :: 8 :: 9 :: nil)
-        :: nil)))
-    X
-    noError;
+  beginState :=
+    state
+      (board
+        (map
+          (map empty)
+          ((1 :: 2 :: 3 :: nil)
+            :: (4 :: 5 :: 6 :: nil)
+            :: (7 :: 8 :: 9 :: nil)
+            :: nil)))
+      X
+      noError;
 
   --- ;true; if some player has won the game
   won : GameState → Bool;
-  won (state (board squares) _ _) := any
-    full
-    (diagonals squares ++ rows squares ++ columns squares);
+  won (state (board squares) _ _) :=
+    any
+      full
+      (diagonals squares ++ rows squares ++ columns squares);
 
   --- ;true; if there is a draw
   draw : GameState → Bool;
-  draw (state (board squares) _ _) := null
-    (possibleMoves (flatten squares));
+  draw (state (board squares) _ _) :=
+    null (possibleMoves (flatten squares));
 end;

examples/milestone/TicTacToe/Logic/Square.juvix

@@ -23,9 +23,10 @@ module Logic.Square;
   showSquare (occupied s) := " " ++str showSymbol s ++str " ";
 
   replace : Symbol → Nat → Square → Square;
-  replace player k (empty n) := if
-    (n Stdlib.Data.Nat.Ord.== k)
-    (occupied player)
-    (empty n);
+  replace player k (empty n) :=
+    if
+      (n Stdlib.Data.Nat.Ord.== k)
+      (occupied player)
+      (empty n);
   replace _ _ s := s;
 end;