Update traits (#80)

* Closes #79 --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
anoma · Sep 13, 2023 · f9ebce1 · f9ebce1
1 parent bc6ec82
commit f9ebce1
Show file tree

Hide file tree

Showing 23 changed files with 222 additions and 269 deletions.
diff --git a/Stdlib/Data/Bool.juvix b/Stdlib/Data/Bool.juvix
@@ -1,38 +1,33 @@
 module Stdlib.Data.Bool;
 
 import Stdlib.Data.Bool.Base open public;
+import Stdlib.Trait.Eq open;
+import Stdlib.Trait.Ord open;
+import Stdlib.Trait.Show open;
 
-import Stdlib.Trait.Eq as Eq;
-open Eq using {Eq};
+instance
+boolEqI : Eq Bool :=
+  mkEq
+    λ {
+      | true true := true
+      | false false := true
+      | _ _ := false
+    };
 
-import Stdlib.Trait.Ord as Ord;
-open Ord using {Ord};
+instance
+boolOrdI : Ord Bool :=
+  mkOrd
+    λ {
+      | false false := EQ
+      | false true := LT
+      | true false := GT
+      | true true := EQ
+    };
 
-import Stdlib.Trait.Show as Show;
-open Show using {Show};
-
-module BoolTraits;
-  Eq : Eq.Eq Bool :=
-    Eq.mkEq
-      λ {
-        | true true := true
-        | false false := true
-        | _ _ := false
-      };
-
-  Ord : Ord.Ord Bool :=
-    Ord.mkOrd
-      λ {
-        | false false := Ord.EQ
-        | false true := Ord.LT
-        | true false := Ord.GT
-        | true true := Ord.EQ
-      };
-
-  Show : Show.Show Bool :=
-    Show.mkShow
-      λ {
-        | true := "true"
-        | false := "false"
-      };
-end;
+instance
+showBoolI : Show Bool :=
+  mkShow
+    λ {
+      | true := "true"
+      | false := "false"
+    };
diff --git a/Stdlib/Data/Int.juvix b/Stdlib/Data/Int.juvix
@@ -7,25 +7,21 @@ open Nat using {Nat; suc; zero; sub};
 import Stdlib.Data.String open;
 import Stdlib.Data.Bool open;
 
-import Stdlib.Trait.Eq as Eq;
-open Eq using {Eq};
-
-import Stdlib.Trait.Ord as Ord;
-open Ord using {Ord};
-
-import Stdlib.Trait.Show as Show;
-open Show using {Show};
+import Stdlib.Trait.Eq open;
+import Stdlib.Trait.Ord open;
+import Stdlib.Trait.Show open;
 
 import Stdlib.Data.Int.Ord as Int;
 
 --- Converts an ;Int; into ;String;.
 builtin int-to-string
 axiom intToString : Int -> String;
 
-module IntTraits;
-  Eq : Eq.Eq Int := Eq.mkEq (Int.==);
+instance
+eqIntI : Eq Int := mkEq (Int.==);
 
-  Ord : Ord.Ord Int := Ord.mkOrd Int.compare;
+instance
+ordIntI : Ord Int := mkOrd Int.compare;
 
-  Show : Show.Show Int := Show.mkShow intToString;
-end;
+instance
+showIntI : Show Int := mkShow intToString;
diff --git a/Stdlib/Data/Int/Base.juvix b/Stdlib/Data/Int/Base.juvix
@@ -28,9 +28,10 @@ nonNeg : Int -> Bool
 --- Subtraction for ;Nat;s.
 builtin int-sub-nat
 intSubNat (n m : Nat) : Int :=
-  case sub n m
+  case sub n m of {
     | zero := ofNat (Nat.sub m n)
-    | suc k := negSuc k;
+    | suc k := negSuc k
+  };
 
 syntax operator + additive;
 

diff --git a/Stdlib/Data/Int/Range.juvix b/Stdlib/Data/Int/Range.juvix
@@ -8,11 +8,11 @@ import Stdlib.Data.Int.Ord open;
 
 --- A range of integers
 type Range :=
-  | mkRange {
-      low : Int;
-      high : Int;
-      step : Int
-    };
+  mkRange {
+    low : Int;
+    high : Int;
+    step : Int
+  };
 
 syntax iterator for {init: 1, range: 1};
 

diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix
@@ -5,54 +5,48 @@ import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
 import Stdlib.Debug.Fail open;
 
-import Stdlib.Trait.Eq as Eq;
-open Eq using {Eq};
-
-import Stdlib.Trait.Ord as Ord;
-open Ord using {Ord};
-
-import Stdlib.Trait.Show as Show;
-open Show using {Show};
+import Stdlib.Trait.Eq open;
+import Stdlib.Trait.Ord open;
+import Stdlib.Trait.Show open;
 
 --- 𝒪(1). Partial function that returns the first element of a ;List;.
-head {A} : List A → A
+head {A} : List A -> A
   | (x :: _) := x
   | nil := fail "head: empty list";
 
-module ListTraits;
-  Eq {A} : Eq.Eq A -> Eq.Eq (List A)
-    | (Eq.mkEq eq-a) :=
-      let
-        go : List A -> List A -> Bool
-          | nil nil := true
-          | nil _ := false
-          | _ nil := false
-          | (x :: xs) (y :: ys) := if (eq-a x y) (go xs ys) false;
-      in Eq.mkEq go;
-
-  Ord {A} : Ord.Ord A -> Ord.Ord (List A)
-    | (Ord.mkOrd cmp-a) :=
-      let
-        go : List A -> List A -> Ord.Ordering
-          | nil nil := Ord.EQ
-          | nil _ := Ord.LT
-          | _ nil := Ord.GT
-          | (x :: xs) (y :: ys) :=
-            case cmp-a x y
-              | Ord.LT := Ord.LT
-              | Ord.GT := Ord.GT
-              | Ord.EQ := go xs ys;
-      in Ord.mkOrd go;
-
-  Show {A} : Show.Show A -> Show.Show (List A)
-    | (Show.mkShow to-str) :=
-      let
-        go : List A -> String
-          | nil := "nil"
-          | (x :: xs) := to-str x ++str " :: " ++str go xs;
-      in Show.mkShow
-        λ {
-          | nil := "nil"
-          | s := "(" ++str go s ++str ")"
+instance
+eqListI {A} {{Eq A}} : Eq (List A) :=
+  let
+    go : List A -> List A -> Bool
+      | nil nil := true
+      | nil _ := false
+      | _ nil := false
+      | (x :: xs) (y :: ys) := if (Eq.eq x y) (go xs ys) false;
+  in mkEq go;
+
+instance
+ordListI {A} {{Ord A}} : Ord (List A) :=
+  let
+    go : List A -> List A -> Ordering
+      | nil nil := EQ
+      | nil _ := LT
+      | _ nil := GT
+      | (x :: xs) (y :: ys) :=
+        case Ord.cmp x y of {
+          | LT := LT
+          | GT := GT
+          | EQ := go xs ys
         };
-end;
+  in mkOrd go;
+
+instance
+showListI {A} {{Show A}} : Show (List A) :=
+  let
+    go : List A -> String
+      | nil := "nil"
+      | (x :: xs) := Show.show x ++str " :: " ++str go xs;
+  in mkShow
+    λ {
+      | nil := "nil"
+      | s := "(" ++str go s ++str ")"
+    };
diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix
@@ -97,8 +97,7 @@ splitAt {A} : Nat → List A → List A × List A
   | zero xs := nil, xs
   | (suc zero) (x :: xs) := x :: nil, xs
   | (suc m) (x :: xs) :=
-    case splitAt m xs
-      | l1, l2 := x :: l1, l2;
+    case splitAt m xs of {l1, l2 := x :: l1, l2};
 
 --- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering.
 merge {A} : Ord A → List A → List A → List A
@@ -115,8 +114,8 @@ merge {A} : Ord A → List A → List A → List A
 partition {A} (f : A → Bool) : List A → List A × List A
   | nil := nil, nil
   | (x :: xs) :=
-    case partition f xs
-      | l1, l2 := if (f x) (x :: l1, l2) (l1, x :: l2);
+    case partition f xs of {l1, l2 :=
+      if (f x) (x :: l1, l2) (l1, x :: l2)};
 
 syntax operator ++ cons;
 
@@ -211,8 +210,8 @@ quickSort {A} : Ord A → List A → List A
         | nil := nil
         | xs@(_ :: nil) := xs
         | (x :: xs) :=
-          case partition (isGT ∘ cmp x) xs
-            | l1, l2 := go l1 ++ x :: go l2;
+          case partition (isGT ∘ cmp x) xs of {l1, l2 :=
+            go l1 ++ x :: go l2};
     in go;
 
 --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;.

diff --git a/Stdlib/Data/Maybe.juvix b/Stdlib/Data/Maybe.juvix
@@ -2,43 +2,36 @@ module Stdlib.Data.Maybe;
 
 import Stdlib.Data.Maybe.Base open public;
 
-import Stdlib.Trait.Eq as Eq;
-open Eq using {Eq};
-
-import Stdlib.Trait.Ord as Ord;
-open Ord using {Ord};
-
-import Stdlib.Trait.Show as Show;
-open Show using {Show};
+import Stdlib.Trait.Eq open;
+import Stdlib.Trait.Ord open;
+import Stdlib.Trait.Show open;
 
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
 
-module MaybeTraits;
-  Eq {A} : Eq.Eq A -> Eq.Eq (Maybe A)
-    | (Eq.mkEq eq) :=
-      Eq.mkEq
-        λ {
-          | nothing nothing := true
-          | (just a1) (just a2) := eq a1 a2
-          | _ _ := false
-        };
-
-  Show {A} : Show.Show A -> Show.Show (Maybe A)
-    | (Show.mkShow show) :=
-      Show.mkShow
-        λ {
-          | nothing := "nothing"
-          | (just a) := "just " ++str show a
-        };
-
-  Ord {A} : Ord.Ord A -> Ord.Ord (Maybe A)
-    | (Ord.mkOrd cmp) :=
-      Ord.mkOrd
-        λ {
-          | nothing nothing := Ord.EQ
-          | (just a1) (just a2) := cmp a1 a2
-          | nothing (just _) := Ord.LT
-          | (just _) nothing := Ord.GT
-        };
-end;
+instance
+eqMaybeI {A} {{Eq A}} : Eq (Maybe A) :=
+  mkEq
+    λ {
+      | nothing nothing := true
+      | (just a1) (just a2) := Eq.eq a1 a2
+      | _ _ := false
+    };
+
+instance
+showMaybeI {A} {{Show A}} : Show (Maybe A) :=
+  mkShow
+    λ {
+      | nothing := "nothing"
+      | (just a) := "just " ++str Show.show a
+    };
+
+instance
+ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
+  mkOrd
+    λ {
+      | nothing nothing := EQ
+      | (just a1) (just a2) := Ord.cmp a1 a2
+      | nothing (just _) := LT
+      | (just _) nothing := GT
+    };
diff --git a/Stdlib/Data/Nat.juvix b/Stdlib/Data/Nat.juvix
@@ -3,14 +3,9 @@ module Stdlib.Data.Nat;
 import Stdlib.Data.Nat.Base open public;
 import Stdlib.Data.String.Base open;
 
-import Stdlib.Trait.Eq as Eq;
-open Eq using {Eq};
-
-import Stdlib.Trait.Ord as Ord;
-open Ord using {Ord};
-
-import Stdlib.Trait.Show as Show;
-open Show using {Show};
+import Stdlib.Trait.Eq open public;
+import Stdlib.Trait.Ord open public;
+import Stdlib.Trait.Show open public;
 
 import Stdlib.Data.Nat.Ord as Nat;
 
@@ -22,10 +17,11 @@ axiom natToString : Nat -> String;
 builtin string-to-nat
 axiom stringToNat : String -> Nat;
 
-module NatTraits;
-  Eq : Eq.Eq Nat := Eq.mkEq (Nat.==);
+instance
+eqNatI : Eq Nat := mkEq (Nat.==);
 
-  Ord : Ord.Ord Nat := Ord.mkOrd Nat.compare;
+instance
+ordNatI : Ord Nat := mkOrd Nat.compare;
 
-  Show : Show.Show Nat := Show.mkShow natToString;
-end;
+instance
+showNatI : Show Nat := mkShow natToString;
diff --git a/Stdlib/Data/Nat/Range.juvix b/Stdlib/Data/Nat/Range.juvix
@@ -8,11 +8,11 @@ import Stdlib.Data.Nat.Ord open;
 
 --- A range of natural numbers
 type Range :=
-  | mkRange {
-      low : Nat;
-      high : Nat;
-      step : Nat
-    };
+  mkRange {
+    low : Nat;
+    high : Nat;
+    step : Nat
+  };
 
 syntax iterator for {init: 1, range: 1};