Standard library traits (#86)

* Operators for `Ord` and `Eq`.
* Conversion function from `Ord` to `Eq` in `Stdlib.Trait.Ord.Eq`.
* Numeric traits: `Natural` and `Integral`.
* By default the comparison and arithmetic operators refer to the
generic traits. The operators specific to the data types (`Nat`, `Int`)
need to be imported separately or prefixed with `Nat`, `Int`.
* Requires anoma/juvix#2433
* Requires anoma/juvix#2441
* The `quickcheck` library needs to be updated for tests to work.

Stdlib/Data/Int.juvix

@@ -1,28 +1,52 @@
 module Stdlib.Data.Int;
 
-import Stdlib.Data.Int.Base open public;
-
-import Stdlib.Data.Nat as Nat;
-open Nat using {Nat; suc; zero; sub};
+import Stdlib.Data.Int.Base open hiding {+; -; *; div; mod} public;
+-- should be re-exported qualified
+import Stdlib.Data.Int.Base as Int;
 
 import Stdlib.Data.String open;
 import Stdlib.Data.Bool open;
 
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
+import Stdlib.Trait.Natural open;
+import Stdlib.Trait.Integral open;
 
+-- should be re-exported qualified
 import Stdlib.Data.Int.Ord as Int;
 
 --- Converts an ;Int; into ;String;.
 builtin int-to-string
 axiom intToString : Int -> String;
 
+{-# specialize: true, inline: case #-}
 instance
 eqIntI : Eq Int := mkEq (Int.==);
 
+{-# specialize: true, inline: case #-}
 instance
 ordIntI : Ord Int := mkOrd Int.compare;
 
 instance
 showIntI : Show Int := mkShow intToString;
+
+{-# specialize: true, inline: case #-}
+instance
+naturalIntI : Natural Int :=
+  mkNatural@{
+    + := (Int.+);
+    * := (Int.*);
+    div := Int.div;
+    mod := Int.mod;
+    fromNat := ofNat
+  };
+
+{-# specialize: true, inline: case #-}
+instance
+integralIntI : Integral Int :=
+  mkIntegral@{
+    naturalI := naturalIntI;
+    - := (Int.-);
+    fromInt (x : Int) : Int := x
+  };

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;
+import Stdlib.Trait.Ord open using {EQ; LT; GT; Ordering};
 
 import Stdlib.Data.Nat.Ord as Nat;
 
@@ -45,6 +45,7 @@ syntax operator >= comparison;
 >= (m n : Int) : Bool := n <= m;
 
 --- Tests for ;Ordering;.
+{-# inline: true #-}
 compare (m n : Int) : Ordering :=
   if (m == n) EQ (if (m < n) LT GT);
 

Stdlib/Data/Nat.juvix

@@ -1,12 +1,16 @@
 module Stdlib.Data.Nat;
 
-import Stdlib.Data.Nat.Base open public;
+import Stdlib.Data.Nat.Base open hiding {+; *; div; mod} public;
+-- should be re-exported qualified
+import Stdlib.Data.Nat.Base as Nat;
 import Stdlib.Data.String.Base open;
 
 import Stdlib.Trait.Eq open public;
 import Stdlib.Trait.Ord open public;
 import Stdlib.Trait.Show open public;
+import Stdlib.Trait.Natural open public;
 
+-- should be re-exported qualified
 import Stdlib.Data.Nat.Ord as Nat;
 
 --- Converts a ;Nat; into a ;String;.
@@ -17,11 +21,24 @@ axiom natToString : Nat -> String;
 builtin string-to-nat
 axiom stringToNat : String -> Nat;
 
+{-# specialize: true, inline: case #-}
 instance
 eqNatI : Eq Nat := mkEq (Nat.==);
 
+{-# specialize: true, inline: case #-}
 instance
 ordNatI : Ord Nat := mkOrd Nat.compare;
 
 instance
 showNatI : Show Nat := mkShow natToString;
+
+{-# specialize: true, inline: case #-}
+instance
+naturalNatI : Natural Nat :=
+  mkNatural@{
+    + := (Nat.+);
+    * := (Nat.*);
+    div := Nat.div;
+    mod := Nat.mod;
+    fromNat (x : Nat) : Nat := x
+  };

Stdlib/Data/Nat/Ord.juvix

@@ -3,7 +3,7 @@ module Stdlib.Data.Nat.Ord;
 import Stdlib.Data.Fixity open;
 
 import Stdlib.Data.Nat.Base open;
-import Stdlib.Trait.Ord open;
+import Stdlib.Trait.Ord open using {EQ; LT; GT; Ordering};
 import Stdlib.Data.Bool.Base open;
 
 syntax operator == comparison;
@@ -47,11 +47,12 @@ syntax operator >= comparison;
 >= (n m : Nat) : Bool := m <= n;
 
 --- Tests for ;Ordering;.
+{-# inline: true #-}
 compare (n m : Nat) : Ordering :=
   if (n == m) EQ (if (n < m) LT GT);
 
---- Returns the smallest ;Nat;.
+--- Returns the smaller ;Nat;.
 min (x y : Nat) : Nat := if (x < y) x y;
 
---- Returns the biggest ;Nat;.
+--- Returns the larger ;Nat;.
 max (x y : Nat) : Nat := if (x > y) x y;

Stdlib/Data/Range.juvix

@@ -0,0 +1,42 @@
+module Stdlib.Data.Range;
+
+import Stdlib.Data.Fixity open;
+
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Trait.Natural open;
+import Stdlib.Trait.Ord open;
+
+--- A range of naturals
+type Range N :=
+  mkRange {
+    low : N;
+    high : N;
+    step : N
+  };
+
+syntax iterator for {init := 1; range := 1};
+
+{-# specialize: [1, 2, 3, 5] #-}
+for {A N} {{Ord N}} {{Natural N}} (f : A → N → A) (a : A)
+  : Range N → A
+  | mkRange@{low; high; step} :=
+    let
+      {-# specialize-by: [f] #-}
+      terminating
+      go (acc : A) (n : N) : A :=
+        if (n > high) acc (go (f acc n) (n + step));
+    in go a low;
+
+syntax operator to range;
+
+--- `x to y` is the range [x..y]
+{-# inline: always #-}
+to {N} {{Natural N}} (l h : N) : Range N :=
+  mkRange l h (fromNat 1);
+
+syntax operator step step;
+
+--- `x to y step s` is the range [x,x+s,..,y]
+{-# inline: always #-}
+step {N} (r : Range N) (s : N) : Range N :=
+  r@Range{step := s};

Stdlib/Data/Nat/Gcd.juvix → Stdlib/Extra/Gcd.juvix

@@ -1,14 +1,16 @@
-module Stdlib.Data.Nat.Gcd;
+module Stdlib.Extra.Gcd;
 
-import Stdlib.Data.Nat open;
+import Stdlib.Trait.Natural open;
+import Stdlib.Trait.Eq open;
+import Stdlib.Trait.Ord open;
 import Stdlib.Data.Bool open;
-import Stdlib.Data.Nat.Ord open;
 
 --- Computes the greatest common divisor.
-gcd (a b : Nat) : Nat :=
+gcd {A} {{Eq A}} {{Ord A}} {{Natural A}} (a b : A) : A :=
   let
     -- Internal helper for computing the greatest common divisor. The first element
     -- should be smaller than the second.
     terminating
-    gcd' (a b : Nat) : Nat := if (a == 0) b (gcd' (mod b a) a);
+    gcd' (a b : A) : A :=
+      if (a == fromNat 0) b (gcd' (mod b a) a);
   in if (a > b) (gcd' b a) (gcd' a b);

Stdlib/Prelude.juvix

@@ -8,7 +8,7 @@ import Stdlib.Data.Unit open public;
 import Stdlib.Data.List open public;
 import Stdlib.Data.Maybe open public;
 import Stdlib.Data.Nat open public;
-import Stdlib.Data.Int open hiding {+; *; div; mod} public;
+import Stdlib.Data.Int open public;
 import Stdlib.Data.Product open public;
 import Stdlib.Data.String open public;
 import Stdlib.Function open public;

Stdlib/Trait.juvix

@@ -4,3 +4,5 @@ import Stdlib.Trait.Eq as Eq open using {Eq; module Eq} public;
 import Stdlib.Trait.Show as Show open using {Show; module Show} public;
 import Stdlib.Trait.Ord as Ord open using {Ord; module Ord} public;
 import Stdlib.Trait.Partial open public;
+import Stdlib.Trait.Natural open public;
+import Stdlib.Trait.Integral open public;

Stdlib/Trait/Eq.juvix

@@ -1,7 +1,18 @@
 module Stdlib.Trait.Eq;
 
 import Stdlib.Data.Bool.Base open;
+import Stdlib.Data.Fixity open;
 
 --- A trait defining equality
 trait
 type Eq A := mkEq {eq : A -> A -> Bool};
+
+syntax operator == comparison;
+syntax operator /= comparison;
+
+{-# inline: always #-}
+== {A} {{Eq A}} : A -> A -> Bool := Eq.eq;
+
+--- Tests for inequality.
+{-# inline: always #-}
+/= {A} {{Eq A}} (x y : A) : Bool := not (x == y);

Stdlib/Trait/Integral.juvix

@@ -0,0 +1,16 @@
+module Stdlib.Trait.Integral;
+
+import Stdlib.Data.Int.Base open using {Int};
+import Stdlib.Data.Fixity open;
+import Stdlib.Trait.Natural open;
+
+trait
+type Integral A :=
+  mkIntegral {
+    naturalI : Natural A;
+    syntax operator - additive;
+    - : A -> A -> A;
+    fromInt : Int -> A
+  };
+
+open Integral using {fromInt; -} public;

Stdlib/Trait/Natural.juvix

@@ -0,0 +1,18 @@
+module Stdlib.Trait.Natural;
+
+import Stdlib.Data.Nat.Base open using {Nat};
+import Stdlib.Data.Fixity open;
+
+trait
+type Natural A :=
+  mkNatural {
+    syntax operator + additive;
+    + : A -> A -> A;
+    syntax operator * multiplicative;
+    * : A -> A -> A;
+    div : A -> A -> A;
+    mod : A -> A -> A;
+    fromNat : Nat -> A
+  };
+
+open Natural public;