Update the coding style according to the guidelines (#126)

* Depends on #125 --------- Co-authored-by: Paul Cadman <[email protected]>
anoma · Oct 11, 2024 · ff35179 · ff35179
1 parent dbf0463
commit ff35179
Show file tree

Hide file tree

Showing 52 changed files with 1,038 additions and 853 deletions.
diff --git a/Stdlib/Cairo/Ec.juvix b/Stdlib/Cairo/Ec.juvix
@@ -8,6 +8,7 @@ module Stdlib.Cairo.Ec;
 
 import Stdlib.Data.Field open;
 import Stdlib.Data.Bool open;
+import Stdlib.Data.Pair open;
 
 module StarkCurve;
   ALPHA : Field := 1;
@@ -37,77 +38,80 @@ module Internal;
 end;
 
 --- Checks if an EC point is on the STARK curve.
-isOnCurve : Point -> Bool
-  | (mkPoint x y) :=
-    if
-      | y == 0 := x == 0
-      | else := y * y == (x * x + StarkCurve.ALPHA) * x + StarkCurve.BETA;
-
---- Doubles a valid point p (computes p + p) on the elliptic curve.
-double : Point -> Point
-  | p@(mkPoint x y) :=
-    if
-      | y == 0 := p
-      | else :=
-        let
-          slope := (3 * x * x + StarkCurve.ALPHA) / (2 * y);
-          r_x := slope * slope - x - x;
-          r_y := slope * (x - r_x) - y;
-        in mkPoint@?{
-          x := r_x;
-          y := r_y
-        };
+isOnCurve (point : Point) : Bool :=
+  case point of
+    mkPoint x y :=
+      if
+        | y == 0 := x == 0
+        | else := y * y == (x * x + StarkCurve.ALPHA) * x + StarkCurve.BETA;
+
+--- Doubles a valid `point` (computes point + point) on the elliptic curve.
+double (point : Point) : Point :=
+  case point of
+    mkPoint x y :=
+      if
+        | y == 0 := point
+        | else :=
+          let
+            slope := (3 * x * x + StarkCurve.ALPHA) / (2 * y);
+            r_x := slope * slope - x - x;
+            r_y := slope * (x - r_x) - y;
+          in mkPoint@?{
+            x := r_x;
+            y := r_y
+          };
 
 --- Adds two valid points on the EC.
-add : Point -> Point -> Point
-  | p@(mkPoint x1 y1) q@(mkPoint x2 y2) :=
-    if
-      | y1 == 0 := q
-      | y2 == 0 := p
-      | x1 == x2 :=
-        if
-          | y1 == y2 := double p
-          | else := mkPoint 0 0
-      | else :=
-        let
-          slope := (y1 - y2) / (x1 - x2);
-          r_x := slope * slope - x1 - x2;
-          r_y := slope * (x1 - r_x) - y1;
-        in mkPoint r_x r_y;
-
---- Subtracts a point from another on the EC.
-sub (p q : Point) : Point := add p q@Point{y := 0 - y};
-
---- Computes p + m * q on the elliptic curve.
+add (point1 point2 : Point) : Point :=
+  case point1, point2 of
+    mkPoint x1 y1, mkPoint x2 y2 :=
+      if
+        | y1 == 0 := point2
+        | y2 == 0 := point1
+        | x1 == x2 :=
+          if
+            | y1 == y2 := double point1
+            | else := mkPoint 0 0
+        | else :=
+          let
+            slope := (y1 - y2) / (x1 - x2);
+            r_x := slope * slope - x1 - x2;
+            r_y := slope * (x1 - r_x) - y1;
+          in mkPoint r_x r_y;
+
+--- Subtracts point2 from point1 on the EC.
+sub (point1 point2 : Point) : Point := add point1 point2@Point{y := 0 - y};
+
+--- Computes point1 + alpha * point2 on the elliptic curve.
 --- Because the EC operation builtin cannot handle inputs where additions of points with the same x
 --- coordinate arise during the computation, this function adds and subtracts a nondeterministic
 --- point s to the computation, so that regardless of input, the probability that such additions
 --- arise will become negligibly small.
 --- The precise computation is therefore:
---- ((p + s) + m * q) - s
---- so that the inputs to the builtin itself are (p + s), m, and q.
+--- ((point1 + s) + alpha * point2) - s
+--- so that the inputs to the builtin itself are (point1 + s), alpha, and point2.
 ---
 --- Arguments:
---- p - an EC point.
---- m - the multiplication coefficient of q (a field element).
---- q - an EC point.
+--- point1 - an EC point.
+--- alpha - the multiplication coefficient of point2 (a field element).
+--- point2 - an EC point.
 ---
 --- Returns:
---- p + m * q.
+--- point1 + alpha * point2.
 ---
 --- Assumptions:
---- p and q are valid points on the curve.
-addMul (p : Point) (m : Field) (q : Point) : Point :=
+--- point1 and point2 are valid points on the curve.
+addMul (point1 : Point) (alpha : Field) (point2 : Point) : Point :=
   if
-    | Point.y q == 0 := p
+    | Point.y point2 == 0 := point1
     | else :=
       let
         s : Point := Internal.randomEcPoint;
-        r : Point := Internal.ecOp (add p s) m q;
+        r : Point := Internal.ecOp (add point1 s) alpha point2;
       in sub r s;
 
---- Computes m * p on the elliptic curve.
-mul (m : Field) (p : Point) : Point := addMul (mkPoint 0 0) m p;
+--- Computes alpha * point on the elliptic curve.
+mul (alpha : Field) (point : Point) : Point := addMul (mkPoint 0 0) alpha point;
 
 module Operators;
   import Stdlib.Data.Fixity open;

diff --git a/Stdlib/Cairo/Poseidon.juvix b/Stdlib/Cairo/Poseidon.juvix
@@ -27,11 +27,11 @@ poseidonHash2 (x y : Field) : Field := PoseidonState.s0 (poseidonHash (mkPoseido
 
 --- Hashes n elements and retrieves a single field element output.
 {-# eval: false #-}
-poseidonHashList (lst : List Field) : Field :=
+poseidonHashList (list : List Field) : Field :=
   let
     go (acc : PoseidonState) : List Field -> PoseidonState
       | [] := poseidonHash acc@PoseidonState{s0 := s0 + 1}
       | [x] := poseidonHash acc@PoseidonState{   s0 := s0 + x; s1 := s1 + 1 }
       | (x1 :: x2 :: xs) :=
         go (poseidonHash acc@PoseidonState{   s0 := s0 + x1; s1 := s1 + x2 }) xs;
-  in PoseidonState.s0 (go (mkPoseidonState 0 0 0) lst);
+  in PoseidonState.s0 (go (mkPoseidonState 0 0 0) list);
diff --git a/Stdlib/Data/BinaryTree.juvix b/Stdlib/Data/BinaryTree.juvix
@@ -4,17 +4,21 @@ import Stdlib.Data.Nat open;
 import Stdlib.Data.List open;
 
 type BinaryTree (A : Type) :=
-  | leaf : BinaryTree A
-  | node : BinaryTree A -> A -> BinaryTree A -> BinaryTree A;
+  | leaf
+  | node {
+      left : BinaryTree A;
+      element : A;
+      right : BinaryTree A
+    };
 
---- fold a tree in depth first order
-fold {A B} (f : A -> B -> B -> B) (acc : B) : BinaryTree A -> B :=
+--- fold a tree in depth-first order
+fold {A B} (f : A -> B -> B -> B) (acc : B) (tree : BinaryTree A) : B :=
   let
     go (acc : B) : BinaryTree A -> B
       | leaf := acc
       | (node l a r) := f a (go acc l) (go acc r);
-  in go acc;
+  in go acc tree;
 
-length : {A : Type} -> BinaryTree A -> Nat := fold λ {_ l r := 1 + l + r} 0;
+length {A} (tree : BinaryTree A) : Nat := fold \ {_ l r := 1 + l + r} 0 tree;
 
-to-list : {A : Type} -> BinaryTree A -> List A := fold λ {e ls rs := e :: ls ++ rs} nil;
+toList {A} (tree : BinaryTree A) : List A := fold \ {e ls rs := e :: ls ++ rs} nil tree;
diff --git a/Stdlib/Data/Bool.juvix b/Stdlib/Data/Bool.juvix
@@ -1,35 +1,40 @@
 module Stdlib.Data.Bool;
 
 import Stdlib.Data.Bool.Base open public;
+import Stdlib.Data.Pair.Base open;
+import Stdlib.Data.String.Base open;
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 
 {-# specialize: true, inline: case #-}
 instance
 boolEqI : Eq Bool :=
-  mkEq
-    λ {
-      | true true := true
-      | false false := true
-      | _ _ := false
-    };
+  mkEq@{
+    eq (x y : Bool) : Bool :=
+      case x, y of
+        | true, true := true
+        | false, false := true
+        | _ := false
+  };
 
 {-# specialize: true, inline: case #-}
 instance
 boolOrdI : Ord Bool :=
-  mkOrd
-    λ {
-      | false false := EQ
-      | false true := LT
-      | true false := GT
-      | true true := EQ
-    };
+  mkOrd@{
+    cmp (x y : Bool) : Ordering :=
+      case x, y of
+        | false, false := Equal
+        | false, true := LessThan
+        | true, false := GreaterThan
+        | true, true := Equal
+  };
 
 instance
 showBoolI : Show Bool :=
-  mkShow
-    λ {
-      | true := "true"
-      | false := "false"
-    };
+  mkShow@{
+    show (x : Bool) : String :=
+      if
+        | x := "true"
+        | else := "false"
+  };
diff --git a/Stdlib/Data/Bool/Base.juvix b/Stdlib/Data/Bool/Base.juvix
@@ -5,29 +5,29 @@ import Stdlib.Data.Fixity open;
 
 --- Logical negation.
 {-# isabelle-function: {name: "\\<not>"} #-}
-not : Bool → Bool
+not : Bool -> Bool
   | true := false
   | false := true;
 
 syntax operator || logical;
 
 --- Logical disjunction. Evaluated lazily. Cannot be partially applied
 builtin bool-or
-|| : Bool → Bool → Bool
+|| : Bool -> Bool -> Bool
   | true _ := true
   | false a := a;
 
 syntax operator && logical;
 
 --- Logical conjunction. Evaluated lazily. Cannot be partially applied.
 builtin bool-and
-&& : Bool → Bool → Bool
+&& : Bool -> Bool -> Bool
   | true a := a
   | false _ := false;
 
 --- Returns the first argument if ;true;, otherwise it returns the second argument. Evaluated lazily. Cannot be partially applied.
 builtin bool-if
-ite : {A : Type} → Bool → A → A → A
+ite : {A : Type} -> Bool -> A -> A -> A
   | true a _ := a
   | false _ b := b;
 

diff --git a/Stdlib/Data/Byte.juvix b/Stdlib/Data/Byte.juvix
@@ -17,7 +17,7 @@ eqByteI : Eq Byte := mkEq (Byte.==);
 instance
 showByteI : Show Byte :=
   mkShow@{
-    show := Byte.toNat >> Show.show
+    show (x : Byte) : String := Show.show (Byte.toNat x)
   };
 
 {-# specialize: true, inline: case #-}

diff --git a/Stdlib/Data/Int/Base.juvix b/Stdlib/Data/Int/Base.juvix
@@ -16,9 +16,10 @@ type Int :=
     negSuc Nat;
 
 --- Converts an ;Int; to a ;Nat;. If the ;Int; is negative, it returns ;zero;.
-toNat : Int -> Nat
-  | (ofNat n) := n
-  | (negSuc _) := zero;
+toNat (int : Int) : Nat :=
+  case int of
+    | ofNat n := n
+    | negSuc _ := zero;
 
 --- Non-negative predicate for ;Int;s.
 builtin int-nonneg
@@ -88,6 +89,7 @@ mod : Int -> Int -> Int
   | (negSuc m) (negSuc n) := negNat (Nat.mod (suc m) (suc n));
 
 --- Absolute value
-abs : Int -> Nat
-  | (ofNat n) := n
-  | (negSuc n) := suc n;
+abs (int : Int) : Nat :=
+  case int of
+    | ofNat n := n
+    | negSuc n := suc n;
diff --git a/Stdlib/Data/Int/Ord.juvix b/Stdlib/Data/Int/Ord.juvix
@@ -4,7 +4,7 @@ import Stdlib.Data.Fixity open;
 
 import Stdlib.Data.Int.Base open;
 import Stdlib.Data.Bool.Base open;
-import Stdlib.Trait.Ord open using {EQ; LT; GT; Ordering};
+import Stdlib.Trait.Ord open using {Equal; LessThan; GreaterThan; Ordering};
 
 import Stdlib.Data.Nat.Base as Nat;
 import Stdlib.Data.Nat.Ord as Nat;
@@ -49,9 +49,9 @@ syntax operator >= comparison;
 {-# inline: true #-}
 compare (m n : Int) : Ordering :=
   if
-    | m == n := EQ
-    | m < n := LT
-    | else := GT;
+    | m == n := Equal
+    | m < n := LessThan
+    | else := GreaterThan;
 
 --- Returns the smallest ;Int;.
 min (x y : Int) : Int := ite (x < y) x y;

diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix
@@ -27,18 +27,20 @@ eqListI {A} {{Eq A}} : Eq (List A) :=
       | (x :: xs) (y :: ys) := ite (Eq.eq x y) (go xs ys) false;
   in mkEq go;
 
+isMember {A} {{Eq A}} (elem : A) (list : List A) : Bool := isElement (Eq.eq) elem list;
+
 instance
 ordListI {A} {{Ord A}} : Ord (List A) :=
   let
     go : List A -> List A -> Ordering
-      | nil nil := EQ
-      | nil _ := LT
-      | _ nil := GT
+      | nil nil := Equal
+      | nil _ := LessThan
+      | _ nil := GreaterThan
       | (x :: xs) (y :: ys) :=
         case Ord.cmp x y of
-          | LT := LT
-          | GT := GT
-          | EQ := go xs ys;
+          | LessThan := LessThan
+          | GreaterThan := GreaterThan
+          | Equal := go xs ys;
   in mkOrd go;
 
 instance
@@ -47,11 +49,12 @@ showListI {A} {{Show A}} : Show (List A) :=
     go : List A -> String
       | nil := "nil"
       | (x :: xs) := Show.show x ++str " :: " ++str go xs;
-  in mkShow
-    λ {
-      | nil := "nil"
-      | s := "(" ++str go s ++str ")"
-    };
+  in mkShow@{
+    show (list : List A) : String :=
+      case list of
+        | nil := "nil"
+        | s := "(" ++str go s ++str ")"
+  };
 
 {-# specialize: true, inline: case #-}
 instance
@@ -80,7 +83,7 @@ instance
 applicativeListI : Applicative List :=
   mkApplicative@{
     pure {A} (a : A) : List A := [a];
-    ap {A B} : List (A -> B) -> List A -> List B
+    ap {A B} : (listOfFuns : List (A -> B)) -> (listOfAs : List A) -> List B
       | [] _ := []
       | (f :: fs) l := map f l ++ ap fs l
   };