Field type (#93)

Co-authored-by: Paul Cadman <[email protected]>

Stdlib/Data/Field.juvix

@@ -0,0 +1,48 @@
+module Stdlib.Data.Field;
+
+import Stdlib.Data.Field.Base open using {Field} public;
+import Stdlib.Data.Field.Base as Field;
+import Stdlib.Data.String.Base open;
+import Stdlib.Data.Nat;
+
+import Stdlib.Trait.Eq open public;
+import Stdlib.Trait.Show open public;
+import Stdlib.Trait.Natural open public;
+import Stdlib.Trait.Integral open public;
+import Stdlib.Trait.Numeric open public;
+
+{-# specialize: true, inline: case #-}
+instance
+eqFieldI : Eq Field := mkEq (Field.==);
+
+instance
+showFieldI : Show Field :=
+  mkShow@{
+    show (f : Field) : String := Show.show (Field.toNat f)
+  };
+
+{-# specialize: true, inline: case #-}
+instance
+naturalFieldI : Natural Field :=
+  mkNatural@{
+    + := (Field.+);
+    * := (Field.*);
+    fromNat := Field.fromNat
+  };
+
+{-# specialize: true, inline: case #-}
+instance
+integralFieldI : Integral Field :=
+  mkIntegral@{
+    naturalI := naturalFieldI;
+    - := (Field.-);
+    fromInt := Field.fromInt
+  };
+
+{-# specialize: true, inline: case #-}
+instance
+numericFieldI : Numeric Field :=
+  mkNumeric@{
+    integralI := integralFieldI;
+    / := (Field./)
+  };

Stdlib/Data/Field/Base.juvix

@@ -0,0 +1,44 @@
+module Stdlib.Data.Field.Base;
+
+import Stdlib.Data.Fixity open;
+import Stdlib.Data.Nat.Base open;
+import Stdlib.Data.Int.Base open hiding {toNat};
+import Stdlib.Data.Bool.Base open;
+
+builtin field
+axiom Field : Type;
+
+syntax operator + additive;
+
+builtin field-add
+axiom + : Field -> Field -> Field;
+
+syntax operator - additive;
+
+builtin field-sub
+axiom - : Field -> Field -> Field;
+
+syntax operator * multiplicative;
+
+builtin field-mul
+axiom * : Field -> Field -> Field;
+
+syntax operator / multiplicative;
+
+builtin field-div
+axiom / : Field -> Field -> Field;
+
+syntax operator == comparison;
+
+builtin field-eq
+axiom == : Field -> Field -> Bool;
+
+builtin field-from-int
+axiom fromInt : Int -> Field;
+
+builtin field-to-nat
+axiom toNat : Field -> Nat;
+
+fromNat (n : Nat) : Field := fromInt (ofNat n);
+
+toInt (f : Field) : Int := ofNat (toNat f);

Stdlib/Data/Int.juvix

@@ -12,6 +12,7 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 import Stdlib.Trait.Natural open;
 import Stdlib.Trait.Integral open;
+import Stdlib.Trait.DivMod open;
 
 -- should be re-exported qualified
 import Stdlib.Data.Int.Ord as Int;
@@ -37,8 +38,6 @@ naturalIntI : Natural Int :=
   mkNatural@{
     + := (Int.+);
     * := (Int.*);
-    div := Int.div;
-    mod := Int.mod;
     fromNat := ofNat
   };
 
@@ -50,3 +49,11 @@ integralIntI : Integral Int :=
     - := (Int.-);
     fromInt (x : Int) : Int := x
   };
+
+{-# specialize: true, inline: case #-}
+instance
+divModIntI : DivMod Int :=
+  mkDivMod@{
+    div := Int.div;
+    mod := Int.mod
+  };

Stdlib/Data/List/Base.juvix

@@ -166,8 +166,8 @@ null {A} : List A → Bool
 --- 𝒪(min(𝓂, 𝓃)). Returns a list containing the results of applying a function
 --- to each pair of elements from the input lists.
 {-# specialize: [1] #-}
-zipWith {A B C} (f : A -> B -> C)
-  : List A -> List B -> List C
+zipWith
+  {A B C} (f : A -> B -> C) : List A -> List B -> List C
   | nil _ := nil
   | _ nil := nil
   | (x :: xs) (y :: ys) := f x y :: zipWith f xs ys;

Stdlib/Data/Nat.juvix

@@ -10,6 +10,7 @@ import Stdlib.Trait.Eq open public;
 import Stdlib.Trait.Ord open public;
 import Stdlib.Trait.Show open public;
 import Stdlib.Trait.Natural open public;
+import Stdlib.Trait.DivMod open public;
 
 -- should be re-exported qualified
 import Stdlib.Data.Nat.Ord as Nat;
@@ -32,3 +33,11 @@ ordNatI : Ord Nat := mkOrd Nat.compare;
 
 instance
 showNatI : Show Nat := mkShow natToString;
+
+{-# specialize: true, inline: case #-}
+instance
+divModNatI : DivMod Nat :=
+  mkDivMod@{
+    div := Nat.div;
+    mod := Nat.mod
+  };

Stdlib/Data/Product.juvix

@@ -25,8 +25,8 @@ ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (A × B)
         }};
 
 instance
-showProductI {A B}
-  : {{Show A}} -> {{Show B}} -> Show (A × B)
+showProductI
+  {A B} : {{Show A}} -> {{Show B}} -> Show (A × B)
   | {{mkShow show-a}} {{mkShow show-b}} :=
     mkShow
       λ {(a, b) :=

Stdlib/Data/Range.juvix

@@ -18,7 +18,12 @@ type Range 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)
+for
+  {A N}
+  {{Ord N}}
+  {{Natural N}}
+  (f : A → N → A)
+  (a : A)
   : Range N → A
   | mkRange@{low; high; step} :=
     let

Stdlib/Extra/Gcd.juvix

@@ -1,12 +1,20 @@
 module Stdlib.Extra.Gcd;
 
 import Stdlib.Trait.Natural open;
+import Stdlib.Trait.DivMod open;
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Data.Bool open;
 
 --- Computes the greatest common divisor.
-gcd {A} {{Eq A}} {{Ord A}} {{Natural A}} (a b : A) : A :=
+gcd
+  {A}
+  {{Eq A}}
+  {{Ord A}}
+  {{Natural A}}
+  {{DivMod A}}
+  (a b : A)
+  : A :=
   let
     -- Internal helper for computing the greatest common divisor. The first element
     -- should be smaller than the second.

Stdlib/Prelude.juvix

@@ -9,6 +9,7 @@ import Stdlib.Data.List open public;
 import Stdlib.Data.Maybe open public;
 import Stdlib.Data.Nat open public;
 import Stdlib.Data.Int open public;
+import Stdlib.Data.Field open public;
 import Stdlib.Data.Product open public;
 import Stdlib.Data.String open public;
 import Stdlib.Function open public;

Stdlib/Trait.juvix

@@ -6,3 +6,5 @@ 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;
+import Stdlib.Trait.Numeric open public;
+import Stdlib.Trait.DivMod open public;

Stdlib/Trait/DivMod.juvix

@@ -0,0 +1,10 @@
+module Stdlib.Trait.DivMod;
+
+trait
+type DivMod A :=
+  mkDivMod {
+    div : A -> A -> A;
+    mod : A -> A -> A
+  };
+
+open DivMod public;

Stdlib/Trait/Numeric.juvix

@@ -0,0 +1,14 @@
+module Stdlib.Trait.Numeric;
+
+import Stdlib.Data.Fixity open;
+import Stdlib.Trait.Integral open;
+
+trait
+type Numeric A :=
+  mkNumeric {
+    integralI : Integral A;
+    syntax operator / multiplicative;
+    / : A -> A -> A
+  };
+
+open Numeric using {/} public;

test/Package.juvix

@@ -6,5 +6,8 @@ package : Package :=
   defaultPackage
     {name := "stdlib-test";
      dependencies := [ path "../"
-                     ; github "anoma" "juvix-quickcheck" "v0.9.0"
+                     ; github
+                       "anoma"
+                       "juvix-quickcheck"
+                       "d9696bb0c038e12df4a7b736a4030b6940011404"
                      ]};

test/Test/Arb.juvix

@@ -6,8 +6,8 @@ import Test.QuickCheck.Arbitrary open;
 import Test.QuickCheck.Gen open;
 import Data.Random open;
 
-arbitrarySizedList {A} (size : Nat)
-  : Arbitrary A -> Arbitrary (List A)
+arbitrarySizedList
+  {A} (size : Nat) : Arbitrary A -> Arbitrary (List A)
   | (mkArbitrary g) :=
     mkArbitrary
       (mkGen
@@ -24,8 +24,8 @@ arbitrarySizedList {A} (size : Nat)
           in randList rand size});
 
 --- Generate an arbitrary rectangular matrix
-arbitraryMatrix {A} {{arbA : Arbitrary A}}
-  : Arbitrary (List (List A)) :=
+arbitraryMatrix
+  {A} {{arbA : Arbitrary A}} : Arbitrary (List (List A)) :=
   mkArbitrary
     (mkGen
       \ {rand :=