Format examples (#1856)

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,9 +23,8 @@ module Collatz;
 
   -- IO
   --- -----------------------------------------------------------------------------
-
   output : Nat → Nat × IO;
-  output n := n , printNatLn n;
+  output n := n, printNatLn n;
 
   terminating
   run : (Nat → Nat) → Nat → IO;
@@ -33,8 +32,11 @@ module Collatz;
   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,11 +14,12 @@ 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;
@@ -26,18 +27,22 @@ module CLI.TicTacToe;
   --- 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;

examples/milestone/TicTacToe/Web/TicTacToe.juvix

@@ -20,7 +20,7 @@ module Web.TicTacToe;
   axiom hostFillText : Nat → Nat → String → Nat → String → Nat → IO;
 
   -- IO extensions
-    IOUnit : IO;
+  IOUnit : IO;
   IOUnit := printString "";
 
   ioseq : IO → IO → IO;
@@ -33,9 +33,9 @@ module Web.TicTacToe;
   mapIO f xs := sequenceIO (map f xs);
 
   -- List extensions
-    zip : {A : Type} → {B : Type} → List A → List B → List
-    (A × B);
-  zip (a :: as) (b :: bs) := (a , b) :: zip as bs;
+  zip : {A : Type} → {B : Type} → List A → List B → List
+      (A × B);
+  zip (a :: as) (b :: bs) := (a, b) :: zip as bs;
   zip _ _ := nil;
 
   rangeAux : Nat → Nat → List Nat;
@@ -49,7 +49,7 @@ module Web.TicTacToe;
   enumerate l := zip (range (length l)) l;
 
   -- Formatting constants
-    squareWidth : Nat;
+  squareWidth : Nat;
   squareWidth := 100;
 
   textSize : Nat;
@@ -85,43 +85,40 @@ module Web.TicTacToe;
   alignNum center := 2;
 
   renderText : String → Nat → Nat → Align → IO;
-  renderText t row col a := hostFillText
-    (squareWidth * row + xTextOffset)
-    (squareWidth * col + yTextOffset)
-    t
-    textSize
-    textColor
-    (alignNum a);
+  renderText t row col a :=
+    hostFillText
+      (squareWidth * row + xTextOffset)
+      (squareWidth * col + yTextOffset)
+      t
+      textSize
+      textColor
+      (alignNum a);
 
   renderSymbol : Symbol → Nat → Nat → IO;
-  renderSymbol s row col := renderText
-    (showSymbol s)
-    row
-    col
-    center;
+  renderSymbol s row col :=
+    renderText (showSymbol s) row col center;
 
   renderNumber : Nat → Nat → Nat → IO;
-  renderNumber n row col := renderText
-    (natToString n)
-    row
-    col
-    center;
+  renderNumber n row col :=
+    renderText (natToString n) row col center;
 
   renderSquare : Nat → Nat → Square → IO;
-  renderSquare row col (occupied s) := hostFillRect
-      (squareWidth * row)
-      (squareWidth * col)
-      squareWidth
-      squareWidth
-      backgroundColor
-    >> renderSymbol s row col;
-  renderSquare row col (empty n) := hostFillRect
-      (squareWidth * row)
-      (squareWidth * col)
-      squareWidth
-      squareWidth
-      lightBackgroundColor
-    >> renderNumber n row col;
+  renderSquare row col (occupied s) :=
+    hostFillRect
+        (squareWidth * row)
+        (squareWidth * col)
+        squareWidth
+        squareWidth
+        backgroundColor
+      >> renderSymbol s row col;
+  renderSquare row col (empty n) :=
+    hostFillRect
+        (squareWidth * row)
+        (squareWidth * col)
+        squareWidth
+        squareWidth
+        lightBackgroundColor
+      >> renderNumber n row col;
 
   renderRowAux : Nat → Nat × Square → IO;
   renderRowAux col (row , s) := renderSquare row col s;
@@ -130,9 +127,8 @@ module Web.TicTacToe;
   renderRow (n , xs) := mapIO (renderRowAux n) (enumerate xs);
 
   renderBoard : Board → IO;
-  renderBoard (board squares) := mapIO
-    renderRow
-    (enumerate squares);
+  renderBoard (board squares) :=
+    mapIO renderRow (enumerate squares);
 
   renderFooterText : String → IO;
   renderFooterText msg := renderText msg 0 3 left;
@@ -146,32 +142,34 @@ module Web.TicTacToe;
   renderError (terminate msg) := renderText msg 0 3 left;
 
   renderGameState : GameState → IO;
-  renderGameState (state b _ (terminate msg)) := renderBoard b
-    >> renderFooterText msg;
-  renderGameState (state b p (continue msg)) := renderBoard b
-    >> renderFooterText (nextPlayerText p)
-    >> renderText (msg) 0 4 left;
-  renderGameState (state b p _) := renderBoard b
-    >> renderFooterText (nextPlayerText p);
+  renderGameState (state b _ (terminate msg)) :=
+    renderBoard b >> renderFooterText msg;
+  renderGameState (state b p (continue msg)) :=
+    renderBoard b
+      >> renderFooterText (nextPlayerText p)
+      >> renderText (msg) 0 4 left;
+  renderGameState (state b p _) :=
+    renderBoard b >> renderFooterText (nextPlayerText p);
 
   renderAndReturn : GameState → GameState;
   renderAndReturn s := const s (renderGameState s);
 
   selectedSquare : Nat → Nat → Nat;
-  selectedSquare row col := 3 * div col squareWidth
-    + div row squareWidth
-    + 1;
+  selectedSquare row col :=
+    3 * div col squareWidth + div row squareWidth + 1;
 
   -- API
-    initGame : GameState;
-  initGame := const
-    beginState
-    (renderGameState beginState
-    >> renderText "Click on a square to make a move" 0 4 left);
+  initGame : GameState;
+  initGame :=
+    const
+      beginState
+      (renderGameState beginState
+        >> renderText "Click on a square to make a move" 0 4 left);
 
   move : GameState → Nat → Nat → GameState;
-  move (state b p (terminate e)) x y := renderAndReturn
-    (state b p (terminate e));
-  move s x y := renderAndReturn
-    (playMove (validMove (selectedSquare x y)) s);
+  move (state b p (terminate e)) x y :=
+    renderAndReturn (state b p (terminate e));
+  move s x y :=
+    renderAndReturn
+      (playMove (validMove (selectedSquare x y)) s);
 end;

examples/milestone/ValidityPredicates/Anoma/Base.juvix

@@ -39,10 +39,8 @@ module Anoma.Base;
   from-int i := if (i < Int_0) nothing (just i);
 
   from-string : String → Maybe String;
-  from-string s := if
-    (s Stdlib.Data.String.Ord.== "")
-    nothing
-    (just s);
+  from-string s :=
+    if (s Stdlib.Data.String.Ord.== "") nothing (just s);
 
   --- -----------------------------------------------------------------------------
 
@@ -76,8 +74,8 @@ module Anoma.Base;
   read-post s := from-int (readPost s);
 
   is-balance-key : String → String → Maybe String;
-  is-balance-key token key := from-string
-    (isBalanceKey token key);
+  is-balance-key token key :=
+    from-string (isBalanceKey token key);
 
   unwrap-default : Maybe Int → Int;
   unwrap-default := maybe Int_0 id;

examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix

@@ -9,41 +9,44 @@ module SimpleFungibleToken;
   import Data.Int.Ops;
 
   -- Misc
-    pair-from-optionString : (String → Int × Bool) → Maybe
-    String → Int × Bool;
-  pair-from-optionString := maybe (Int_0 , false);
+  pair-from-optionString : (String → Int × Bool) → Maybe
+      String → Int × Bool;
+  pair-from-optionString := maybe (Int_0, false);
 
   -- Validity Predicate
-    change-from-key : String → Int;
-  change-from-key key := unwrap-default (read-post key)
-    Data.Int.Ops.- unwrap-default (read-pre key);
+  change-from-key : String → Int;
+  change-from-key key :=
+    unwrap-default (read-post key)
+      Data.Int.Ops.- unwrap-default (read-pre key);
 
   check-vp : List String → String → Int → String → Int × Bool;
-  check-vp verifiers key change owner := if
-    (change-from-key key Data.Int.Ops.< Int_0)
-    (change Data.Int.Ops.+ change-from-key key
-    , elem (Stdlib.Data.String.Ord.==) owner verifiers)
-    (change Data.Int.Ops.+ change-from-key key , true);
+  check-vp verifiers key change owner :=
+    if
+      (change-from-key key Data.Int.Ops.< Int_0)
+      (change Data.Int.Ops.+ change-from-key key
+        , elem (Stdlib.Data.String.Ord.==) owner verifiers)
+      (change Data.Int.Ops.+ change-from-key key, true);
 
   -- make sure the spender approved the transaction
-    check-keys : String → List String → Int
-    × Bool → String → Int × Bool;
-  check-keys token verifiers (change , is-success) key := if
-    is-success
-    (pair-from-optionString
-      (check-vp verifiers key change)
-      (is-balance-key token key))
-    (Int_0 , false);
+  check-keys : String → List String → Int
+      × Bool → String → Int × Bool;
+  check-keys token verifiers (change , is-success) key :=
+    if
+      is-success
+      (pair-from-optionString
+        (check-vp verifiers key change)
+        (is-balance-key token key))
+      (Int_0, false);
 
   check-result : Int × Bool → Bool;
-  check-result (change , all-checked) := change
-      Data.Int.Ops.== Int_0
-    && all-checked;
+  check-result (change , all-checked) :=
+    change Data.Int.Ops.== Int_0 && all-checked;
 
   vp : String → List String → List String → Bool;
-  vp token keys-changed verifiers := check-result
-    (foldl
-      (check-keys token verifiers)
-      (Int_0 , true)
-      keys-changed);
+  vp token keys-changed verifiers :=
+    check-result
+      (foldl
+        (check-keys token verifiers)
+        (Int_0, true)
+        keys-changed);
 end;

examples/milestone/ValidityPredicates/Tests.juvix

@@ -29,7 +29,8 @@ module Tests;
   show-result false := "FAIL";
 
   main : IO;
-  main := printString "VP Status: "
-    >> printStringLn
-      (show-result (vp token keys-changed verifiers));
+  main :=
+    printString "VP Status: "
+      >> printStringLn
+        (show-result (vp token keys-changed verifiers));
 end;

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -22,7 +22,7 @@ class PrettyPrint a where
   ppCode :: Members '[ExactPrint, Reader Options] r => a -> Sem r ()
 
 instance PrettyPrint Keyword where
-  ppCode = noLoc . pretty
+  ppCode = noLoc . annotate AnnKeyword . pretty
 
 instance PrettyPrint KeywordRef where
   ppCode = ppMorpheme
@@ -76,7 +76,7 @@ instance SingI t => PrettyPrint (Module 'Scoped t) where
       lastSemicolon :: Sem r ()
       lastSemicolon = case sing :: SModuleIsTop t of
         SModuleLocal -> return ()
-        SModuleTop -> semicolon >> line <> end
+        SModuleTop -> semicolon <> line <> end
 
 instance PrettyPrint [Statement 'Scoped] where
   ppCode :: forall r. Members '[ExactPrint, Reader Options] r => [Statement 'Scoped] -> Sem r ()