Format juvix files using new function syntax

examples/demo/Demo.juvix

@@ -6,51 +6,49 @@ import Stdlib.Prelude open;
 import Stdlib.Data.Nat.Ord open;
 -- for Ordering
 
-even : Nat → Bool;
-even zero := true;
-even (suc zero) := false;
-even (suc (suc n)) := even n;
+even : Nat → Bool
+  | zero := true
+  | (suc zero) := false
+  | (suc (suc n)) := even n;
 
-even' : Nat → Bool;
-even' n := mod n 2 == 0;
+even' : Nat → Bool
+  | n := mod n 2 == 0;
 
 -- base 2 logarithm rounded down
 terminating
-log2 : Nat → Nat;
-log2 n := if (n <= 1) 0 (suc (log2 (div n 2)));
+log2 : Nat → Nat
+  | n := if (n <= 1) 0 (suc (log2 (div n 2)));
 
 type Tree (A : Type) :=
   | leaf : A → Tree A
   | node : A → Tree A → Tree A → Tree A;
 
-mirror : {A : Type} → Tree A → Tree A;
-mirror t@(leaf _) := t;
-mirror (node x l r) := node x (mirror r) (mirror l);
+mirror : {A : Type} → Tree A → Tree A
+  | t@(leaf _) := t
+  | (node x l r) := node x (mirror r) (mirror l);
 
-tree : Tree Nat;
-tree := 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;
-preorder (leaf x) := x :: nil;
-preorder (node x l r) :=
-  x :: nil ++ preorder l ++ preorder r;
+preorder : {A : Type} → Tree A → List A
+  | (leaf x) := x :: nil
+  | (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 {A} cmp xs :=
-  uncurry
-    (merge (mkOrd 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;
-
-main : IO;
-main :=
+sort : {A : Type} → (A → A → Ordering) → List A → List A
+  | _ nil := nil
+  | _ xs@(_ :: nil) := xs
+  | {A} cmp xs :=
+    uncurry
+      (merge (mkOrd cmp))
+      (both (sort cmp) (splitAt (div (length xs) 2) xs));
+
+printNatListLn : List Nat → IO
+  | nil := printStringLn "nil"
+  | (x :: xs) :=
+    printNat x >> printString " :: " >> printNatListLn xs;
+
+main : IO :=
   printStringLn "Hello!"
     >> printNatListLn (preorder (mirror tree))
     >> printNatListLn (sort compare (preorder (mirror tree)))

examples/midsquare/MidSquareHash.juvix

@@ -8,22 +8,21 @@ import Stdlib.Prelude open;
 import Stdlib.Data.Nat.Ord open;
 
 --- `pow N` is 2 ^ N
-pow : Nat -> Nat;
-pow zero := 1;
-pow (suc n) := 2 * pow n;
+pow : Nat -> Nat
+  | zero := 1
+  | (suc n) := 2 * pow n;
 
 --- `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;
-hash' (suc n@(suc (suc m))) x :=
-  if
-    (x < pow n)
-    (hash' n x)
-    (mod (div (x * x) (pow m)) (pow 6));
-hash' _ x := x * x;
+hash' : Nat -> Nat -> Nat
+  | (suc n@(suc (suc m))) x :=
+    if
+      (x < pow n)
+      (hash' n x)
+      (mod (div (x * x) (pow m)) (pow 6))
+  | _ x := x * x;
 
 hash : Nat -> Nat := hash' 16;
 
-main : Nat;
-main := hash 1367;
+main : Nat := hash 1367;
 -- result: 3

examples/midsquare/MidSquareHashUnrolled.juvix

@@ -45,72 +45,71 @@ pow16 : Nat := 2 * pow15;
 
 --- `hashN` 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.
-hash0 : Nat -> Nat;
-hash0 x := 0;
+hash0 : Nat -> Nat
+  | x := 0;
 
-hash1 : Nat -> Nat;
-hash1 x := x * x;
+hash1 : Nat -> Nat
+  | x := x * x;
 
-hash2 : Nat -> Nat;
-hash2 x := x * x;
+hash2 : Nat -> Nat
+  | x := x * x;
 
-hash3 : Nat -> Nat;
-hash3 x := x * x;
+hash3 : Nat -> Nat
+  | x := x * x;
 
-hash4 : Nat -> Nat;
-hash4 x :=
-  if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
+hash4 : Nat -> Nat
+  | x :=
+    if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
 
-hash5 : Nat -> Nat;
-hash5 x :=
-  if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
+hash5 : Nat -> Nat
+  | x :=
+    if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
 
-hash6 : Nat -> Nat;
-hash6 x :=
-  if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
+hash6 : Nat -> Nat
+  | x :=
+    if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
 
-hash7 : Nat -> Nat;
-hash7 x :=
-  if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
+hash7 : Nat -> Nat
+  | x :=
+    if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
 
-hash8 : Nat -> Nat;
-hash8 x :=
-  if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
+hash8 : Nat -> Nat
+  | x :=
+    if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
 
-hash9 : Nat -> Nat;
-hash9 x :=
-  if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
+hash9 : Nat -> Nat
+  | x :=
+    if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
 
-hash10 : Nat -> Nat;
-hash10 x :=
-  if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
+hash10 : Nat -> Nat
+  | x :=
+    if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
 
-hash11 : Nat -> Nat;
-hash11 x :=
-  if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
+hash11 : Nat -> Nat
+  | x :=
+    if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
 
-hash12 : Nat -> Nat;
-hash12 x :=
-  if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
+hash12 : Nat -> Nat
+  | x :=
+    if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
 
-hash13 : Nat -> Nat;
-hash13 x :=
-  if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
+hash13 : Nat -> Nat
+  | x :=
+    if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
 
-hash14 : Nat -> Nat;
-hash14 x :=
-  if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
+hash14 : Nat -> Nat
+  | x :=
+    if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
 
-hash15 : Nat -> Nat;
-hash15 x :=
-  if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
+hash15 : Nat -> Nat
+  | x :=
+    if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
 
-hash16 : Nat -> Nat;
-hash16 x :=
-  if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
+hash16 : Nat -> Nat
+  | x :=
+    if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
 
 hash : Nat -> Nat := hash16;
 
-main : Nat;
-main := hash 1367;
+main : Nat := hash 1367;
 -- result: 3

examples/milestone/Bank/Bank.juvix

@@ -10,11 +10,9 @@ import Stdlib.Data.Nat.Ord open;
 
 import Stdlib.Data.Nat as Nat;
 
-Address : Type;
-Address := Nat;
+Address : Type := Nat;
 
-bankAddress : Address;
-bankAddress := 1234;
+bankAddress : Address := 1234;
 
 --- Some field type.
 axiom Field : Type;
@@ -28,47 +26,45 @@ module Token;
       mkToken : Address -> Nat -> Nat -> Token;
 
   --- Retrieves the owner from a ;Token;
-  getOwner : Token -> Address;
-  getOwner (mkToken o _ _) := o;
+  getOwner : Token -> Address
+    | (mkToken o _ _) := o;
 
   --- Retrieves the amount from a ;Token;
-  getAmount : Token -> Nat;
-  getAmount (mkToken _ _ a) := a;
+  getAmount : Token -> Nat
+    | (mkToken _ _ a) := a;
 
   --- Retrieves the gates from a ;Token;
-  getGates : Token -> Nat;
-  getGates (mkToken _ g _) := g;
+  getGates : Token -> Nat
+    | (mkToken _ g _) := g;
 end;
 
 open Token;
 
 --- This module defines the type for balances and its associated operations.
 module Balances;
-  Balances : Type;
-  Balances := List (Field × Nat);
+  Balances : Type := List (Field × Nat);
 
   --- Increments the amount associated with a certain ;Field;.
-  increment : Field -> Nat -> Balances -> Balances;
-  increment f n nil := (f, n) :: nil;
-  increment f n ((b, bn) :: bs) :=
-    if
-      (eqField f b)
-      ((b, bn + n) :: bs)
-      ((b, bn) :: increment f n bs);
+  increment : Field -> Nat -> Balances -> Balances
+    | f n nil := (f, n) :: nil
+    | f n ((b, bn) :: bs) :=
+      if
+        (eqField 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;
-  decrement _ _ nil := nil;
-  decrement f n ((b, bn) :: bs) :=
-    if
-      (eqField f b)
-      ((b, sub bn n) :: bs)
-      ((b, bn) :: decrement f n bs);
+  decrement : Field -> Nat -> Balances -> Balances
+    | _ _ nil := nil
+    | f n ((b, bn) :: bs) :=
+      if
+        (eqField f b)
+        ((b, sub bn n) :: bs)
+        ((b, bn) :: decrement f n bs);
 
-  emtpyBalances : Balances;
-  emtpyBalances := nil;
+  emtpyBalances : Balances := nil;
 
   --- Commit balances changes to the chain.
   axiom commitBalances : Balances -> IO;
@@ -83,17 +79,17 @@ axiom runOnChain : {B : Type} -> IO -> B -> B;
 axiom hashAddress : Address -> Field;
 
 --- Returns the total amount of tokens after compounding interest.
-calculateInterest : Nat -> Nat -> Nat -> Nat;
-calculateInterest principal rate periods :=
-  let
-    amount : Nat := principal;
-    incrAmount : Nat -> Nat;
-    incrAmount a := div (a * rate) 10000;
-  in iterate (min 100 periods) incrAmount amount;
+calculateInterest : Nat -> Nat -> Nat -> Nat
+  | principal rate periods :=
+    let
+      amount : Nat := principal;
+      incrAmount : Nat -> Nat;
+      incrAmount a := div (a * rate) 10000;
+    in iterate (min 100 periods) incrAmount amount;
 
 --- Asserts some ;Bool; condition.
-assert : {A : Type} -> Bool -> A -> A;
-assert c a := if c a (fail "assertion failed");
+assert : {A : Type} -> Bool -> A -> A
+  | c a := if c a (fail "assertion failed");
 
 --- Returns a new ;Token;. Arguments are:
 ---
@@ -102,9 +98,9 @@ assert c a := if c a (fail "assertion failed");
 --- `amount`: The amount of  tokens to issue
 ---
 --- `caller`: Who is creating the transaction. It must be the bank.
-issue : Address -> Address -> Nat -> Token;
-issue caller owner amount :=
-  assert (caller == bankAddress) (mkToken owner 0 amount);
+issue : Address -> Address -> Nat -> Token
+  | caller owner amount :=
+    assert (caller == bankAddress) (mkToken owner 0 amount);
 
 {-
 -- TODO: Uncomment this block once we fix