stdlib style update

Stdlib/Data/BinaryTree.juvix

@@ -4,21 +4,21 @@ import Stdlib.Data.Nat open;
 import Stdlib.Data.List open;
 
 type BinaryTree (A : Type) :=
-  | leaf : BinaryTree A
+  | leaf
   | node {
-    left : BinaryTree A;
-    element : A;
-    right : BinaryTree A;
-   };
+      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;
 
-toList : {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;

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"
+  };

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 #-}

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;

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
   };