Update standard library coding style according to the guidelines (#3092)

* Closes #3079
* Closes #3086
* Depends on #3088 
* Updates the coding style guidelines (CODING.md) to reflect issues not
foreseen originally
* Changes the unicode arrow printed in the REPL to `->`. This is to make
the output consistent with how function types are written in the
standard library.

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>

CODING.md

@@ -1,31 +1,62 @@
 # Juvix coding style guidelines for the standard library and Anoma apps
 
+## Definitions
+
+- _enumeration type_ is an inductive type whose all constructors have zero
+  arguments
+
 ## General rules
 
 - always use the formatter
 - don't use unicode, except perhaps for judoc
 - avoid `Pair`
-- prefer enumerations with meaningful names over booleans, e.g., instead of using `Bool` define:
+- prefer enumeration types with meaningful constructor names over booleans,
+  e.g., instead of using `Bool` define:
 
 ```
-type Transferability := Transferable | NonTransferable;
+type Transferability :=
+  | Transferable
+  | NonTransferable;
 ```
 
 ## Imports
 
 - all imports at the beginning of the file
 - explicit names for imported identifiers (`import X open using {iden1; iden2}`)
-  - exception: `import Stdlib.Prelude open`, `import Anoma open` are allowed
+  - exception: `import Stdlib.Prelude open` and `import Anoma open` are allowed
 
 ## Names
 
 - types: upper camel case (`Nat`, `PublicKey`)
 - functions, constructors, etc: lower camel case (`tokenLogic`, `transferLogic`)
+  - exception: constructors of enumeration types: upper camel case
+
+```
+type BalanceFactor :=
+  | --- Left child is higher.
+    LeanLeft
+  | --- Equal heights of children.
+    LeanNone
+  | --- Right child is higher.
+    LeanRight;
+
+type Ordering :=
+  | LessThan
+  | Equal
+  | GreaterThan;
+```
+
 - instances: lower camel case with `I` at the end (`instance eqNatI : Eq Nat := ..`)
 - boolean check functions: start with `is` (`isWhatever`)
 - record constructors: `mk` + type name (`mkResource`)
 - meaningful descriptive long names for arguments of public functions, e.g., `element`, `list`, `initialValue`
-  - exception: common abbreviations allowed: `fun`, `acc`
+  - exception: common abbreviations allowed: `fun`, `acc`, `elem`
+  - exception: generic functions whose arguments have no specific meaning, e.g.,
+
+```
+id {A} (x : A) : A := x
+```
+
 - short names like `x` are okay for local definitions
 
 ## Function signatures
@@ -41,6 +72,7 @@ isMember {A} (testEq : A -> A -> Bool) (element : A) : (list : List A) -> Bool
 ## Type variables
 
 - type variables uppercase (upper camel case, like with types)
+- higher-order type variables also upper camel case (`F : Type -> Type`)
 - implicit type variables: use short version `{A}` in function signatures on the left
 - prefer `{A B}` over `{A} {B}` in function signatures
 - meaningful type variable names for more "high-level" functions where this makes sense
@@ -77,10 +109,33 @@ find {A} (predicate : A -> Bool) : (list : List A) -> Maybe A
 ## Application
 
 - don't use "pipes" (i.e., `|>`, `<|`, `>>`, `<<`, etc.)
-  - weak exception: there is a "natural" data processing pipeline in several steps
+  - exception: there is a "natural" data processing pipeline in several steps, e.g.,
+
+```
+map (+ 1) >> filter (< 0) >> sum
+```
+
 - use iterators `for` , `map`, etc., instead of the function application syntax with `fold`, etc.
 - use named application when reasonable
 
+## Type definitions
+
+- use ADT syntax
+- every constructor on a separate line
+- give meaningful names to constructor arguments
+
+Example:
+
+```
+type BinaryTree (A : Type) :=
+  | leaf
+  | node {
+      left : BinaryTree A;
+      element : A;
+      right : BinaryTree A
+    };
+```
+
 ## Documentation
 
 - the documentation string should be an English sentence

cntlines.sh

@@ -45,6 +45,7 @@ FRONT=$((CONCRETE + INTERNAL + BUILTINS + PIPELINE))
 BACK=$((BACKENDC + BACKENDRUST + VAMPIR + NOCK + REG + ASM + TREE + CORE + CASM + CAIRO))
 OTHER=$((APP + STORE + HTML + MARKDOWN + ISABELLE + EXTRA + DATA + PRELUDE))
 TESTS=$(count test/)
+STDLIB=$(count_ext '*.juvix' juvix-stdlib/Stdlib)
 
 TOTAL=$((FRONT+BACK+OTHER+TESTS))
 
@@ -79,5 +80,6 @@ echo "   Extra: $EXTRA LOC"
 echo "   Data: $DATA LOC"
 echo "   Prelude: $PRELUDE LOC"
 echo "Tests: $TESTS LOC"
+echo "Standard library: $STDLIB LOC"
 echo ""
-echo "Total: $TOTAL Haskell LOC + $RUNTIME_C C LOC + $RUNTIME_RUST Rust LOC + $RUNTIME_JVT JuvixTree LOC + $RUNTIME_CASM CASM LOC + $RUNTIME_VAMPIR VampIR LOC"
+echo "Total: $TOTAL Haskell LOC + $RUNTIME_C C LOC + $RUNTIME_RUST Rust LOC + $RUNTIME_JVT JuvixTree LOC + $RUNTIME_CASM CASM LOC + $RUNTIME_VAMPIR VampIR LOC + $STDLIB Juvix LOC"

examples/demo/Demo.juvix

@@ -3,40 +3,46 @@ module Demo;
 -- standard library prelude
 import Stdlib.Prelude open;
 
-even : Nat → Bool
+even : (n : Nat) -> Bool
   | zero := true
   | (suc zero) := false
   | (suc (suc n)) := even n;
 
-even' : Nat → Bool
-  | n := mod n 2 == 0;
+even' (n : Nat) : Bool := mod n 2 == 0;
 
--- base 2 logarithm rounded down
+--- Returns base 2 logarithm of `n` rounded down
 terminating
-log2 : Nat → Nat
-  | n := ite (n <= 1) 0 (suc (log2 (div n 2)));
+log2 (n : Nat) : Nat :=
+  if
+    | n <= 1 := 0
+    | else := log2 (div n 2) + 1;
 
 type Tree (A : Type) :=
-  | leaf : A → Tree A
-  | node : A → Tree A → Tree A → Tree A;
-
-mirror : {A : Type} → Tree A → Tree A
-  | t@(leaf _) := t
+  | leaf {element : A}
+  | node {
+      element : A;
+      left : Tree A;
+      right : Tree A
+    };
+
+mirror {A} : (tree : Tree A) -> Tree A
+  | tree@(leaf _) := tree
   | (node x l r) := node x (mirror r) (mirror l);
 
 tree : Tree Nat := node 2 (node 3 (leaf 0) (leaf 1)) (leaf 7);
 
-preorder : {A : Type} → Tree A → List A
+preorder : {A : Type} -> Tree A -> List A
   | (leaf x) := x :: nil
   | (node x l r) := x :: nil ++ preorder l ++ preorder r;
 
 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));
+sort {A} {{Ord A}} (list : List A) : List A :=
+  case list of
+    | nil := nil
+    | xs@(_ :: nil) := xs
+    | xs := uncurry merge (both sort (splitAt (div (length xs) 2) xs));
 
-printNatListLn : List Nat → IO
+printNatListLn : (list : List Nat) -> IO
   | nil := printStringLn "nil"
   | (x :: xs) := printNat x >>> printString " :: " >>> printNatListLn xs;
 

examples/midsquare/MidSquareHash.juvix

@@ -6,15 +6,18 @@ module MidSquareHash;
 
 import Stdlib.Prelude open;
 
---- `pow N` is 2 ^ N
-pow : Nat -> Nat
+--- `pow n` is 2 ^ n
+pow : (n : 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
+--- `hash' n x` hashes a number x 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))
+hash' : (n : Nat) -> (x : Nat) -> Nat
+  | (suc n'@(suc (suc m))) x :=
+    if
+      | x < pow n' := hash' n' x
+      | else := mod (div (x * x) (pow m)) (pow 6)
   | _ x := x * x;
 
 hash : Nat -> Nat := hash' 16;

examples/midsquare/MidSquareHashUnrolled.juvix

@@ -44,56 +44,78 @@ 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
-  | x := 0;
-
-hash1 : Nat -> Nat
-  | x := x * x;
-
-hash2 : Nat -> Nat
-  | x := x * x;
-
-hash3 : Nat -> Nat
-  | x := x * x;
-
-hash4 : Nat -> Nat
-  | 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);
-
-hash6 : Nat -> Nat
-  | 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);
-
-hash8 : Nat -> Nat
-  | 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);
-
-hash10 : Nat -> Nat
-  | 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);
-
-hash12 : Nat -> Nat
-  | 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);
-
-hash14 : Nat -> Nat
-  | 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);
-
-hash16 : Nat -> Nat
-  | x := ite (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
+hash0 (x : Nat) : Nat := 0;
+
+hash1 (x : Nat) : Nat := x * x;
+
+hash2 (x : Nat) : Nat := x * x;
+
+hash3 (x : Nat) : Nat := x * x;
+
+hash4 (x : Nat) : Nat :=
+  if
+    | x < pow3 := hash3 x
+    | else := mod (div (x * x) pow1) pow6;
+
+hash5 (x : Nat) : Nat :=
+  if
+    | x < pow4 := hash4 x
+    | else := mod (div (x * x) pow2) pow6;
+
+hash6 (x : Nat) : Nat :=
+  if
+    | x < pow5 := hash5 x
+    | else := mod (div (x * x) pow3) pow6;
+
+hash7 (x : Nat) : Nat :=
+  if
+    | x < pow6 := hash6 x
+    | else := mod (div (x * x) pow4) pow6;
+
+hash8 (x : Nat) : Nat :=
+  if
+    | x < pow7 := hash7 x
+    | else := mod (div (x * x) pow5) pow6;
+
+hash9 (x : Nat) : Nat :=
+  if
+    | x < pow8 := hash8 x
+    | else := mod (div (x * x) pow6) pow6;
+
+hash10 (x : Nat) : Nat :=
+  if
+    | x < pow9 := hash9 x
+    | else := mod (div (x * x) pow7) pow6;
+
+hash11 (x : Nat) : Nat :=
+  if
+    | x < pow10 := hash10 x
+    | else := mod (div (x * x) pow8) pow6;
+
+hash12 (x : Nat) : Nat :=
+  if
+    | x < pow11 := hash11 x
+    | else := mod (div (x * x) pow9) pow6;
+
+hash13 (x : Nat) : Nat :=
+  if
+    | x < pow12 := hash12 x
+    | else := mod (div (x * x) pow10) pow6;
+
+hash14 (x : Nat) : Nat :=
+  if
+    | x < pow13 := hash13 x
+    | else := mod (div (x * x) pow11) pow6;
+
+hash15 (x : Nat) : Nat :=
+  if
+    | x < pow14 := hash14 x
+    | else := mod (div (x * x) pow12) pow6;
+
+hash16 (x : Nat) : Nat :=
+  if
+    | x < pow15 := hash15 x
+    | else := mod (div (x * x) pow13) pow6;
 
 hash : Nat -> Nat := hash16;