From bb1c352ab9facf9989d249b1cef4cf383a4c5ddc Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 20 Feb 2024 20:51:52 +0100
Subject: [PATCH 1/7] field type base

---
 Stdlib/Data/Field/Base.juvix | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 Stdlib/Data/Field/Base.juvix

diff --git a/Stdlib/Data/Field/Base.juvix b/Stdlib/Data/Field/Base.juvix
new file mode 100644
index 00000000..286191f8
--- /dev/null
+++ b/Stdlib/Data/Field/Base.juvix
@@ -0,0 +1,33 @@
+module Stdlib.Data.Field.Base;
+
+import Stdlib.Data.Fixity open;
+import Stdlib.Data.Int.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;
+
+builtin field-from-int
+axiom fromInt : Int -> Field;
+
+builtin field-to-int
+axiom toInt : Field -> Int;

From cd57a91e270cd40fc058bfb8850af62196b77969 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 21 Feb 2024 17:24:10 +0100
Subject: [PATCH 2/7] field functions

---
 Stdlib/Data/Field.juvix      | 19 +++++++++++++++++++
 Stdlib/Data/Field/Base.juvix | 17 ++++++++++++++---
 2 files changed, 33 insertions(+), 3 deletions(-)
 create mode 100644 Stdlib/Data/Field.juvix

diff --git a/Stdlib/Data/Field.juvix b/Stdlib/Data/Field.juvix
new file mode 100644
index 00000000..b715d9cd
--- /dev/null
+++ b/Stdlib/Data/Field.juvix
@@ -0,0 +1,19 @@
+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;
+
+{-# specialize: true, inline: case #-}
+instance
+eqFieldI : Eq Field := mkEq (Field.==);
+
+instance
+showFieldI : Show Field :=
+  mkShow@{
+    show (f : Field) : String := Show.show (Field.toNat f)
+  };
diff --git a/Stdlib/Data/Field/Base.juvix b/Stdlib/Data/Field/Base.juvix
index 286191f8..c23eae15 100644
--- a/Stdlib/Data/Field/Base.juvix
+++ b/Stdlib/Data/Field/Base.juvix
@@ -1,7 +1,9 @@
 module Stdlib.Data.Field.Base;
 
 import Stdlib.Data.Fixity open;
-import Stdlib.Data.Int.Base 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;
@@ -26,8 +28,17 @@ 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-int
-axiom toInt : Field -> Int;
+builtin field-to-nat
+axiom toNat : Field -> Nat;
+
+fromNat (n : Nat) : Field := fromInt (ofNat n);
+
+toInt (f : Field) : Int := ofNat (toNat f);

From 6eb7ac818f8f2e4e28c208fa8ec32ba7411cab04 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Thu, 22 Feb 2024 11:14:46 +0100
Subject: [PATCH 3/7] traits

---
 Stdlib/Data/Field.juvix    | 29 +++++++++++++++++++++++++++++
 Stdlib/Data/Int.juvix      | 11 +++++++++--
 Stdlib/Data/Nat.juvix      |  9 +++++++++
 Stdlib/Prelude.juvix       |  1 +
 Stdlib/Trait.juvix         |  2 ++
 Stdlib/Trait/DivMod.juvix  | 10 ++++++++++
 Stdlib/Trait/Numeric.juvix | 14 ++++++++++++++
 7 files changed, 74 insertions(+), 2 deletions(-)
 create mode 100644 Stdlib/Trait/DivMod.juvix
 create mode 100644 Stdlib/Trait/Numeric.juvix

diff --git a/Stdlib/Data/Field.juvix b/Stdlib/Data/Field.juvix
index b715d9cd..c5066352 100644
--- a/Stdlib/Data/Field.juvix
+++ b/Stdlib/Data/Field.juvix
@@ -7,6 +7,9 @@ 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
@@ -17,3 +20,29 @@ 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./)
+  };
diff --git a/Stdlib/Data/Int.juvix b/Stdlib/Data/Int.juvix
index 7f5adeeb..25ff9cd4 100644
--- a/Stdlib/Data/Int.juvix
+++ b/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;
+  };
diff --git a/Stdlib/Data/Nat.juvix b/Stdlib/Data/Nat.juvix
index 0573299f..3ec1659d 100644
--- a/Stdlib/Data/Nat.juvix
+++ b/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;
+  };
diff --git a/Stdlib/Prelude.juvix b/Stdlib/Prelude.juvix
index 1cd8acf4..11016da9 100644
--- a/Stdlib/Prelude.juvix
+++ b/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;
diff --git a/Stdlib/Trait.juvix b/Stdlib/Trait.juvix
index 4ca6121f..e5df0de0 100644
--- a/Stdlib/Trait.juvix
+++ b/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;
diff --git a/Stdlib/Trait/DivMod.juvix b/Stdlib/Trait/DivMod.juvix
new file mode 100644
index 00000000..376b3bf7
--- /dev/null
+++ b/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;
diff --git a/Stdlib/Trait/Numeric.juvix b/Stdlib/Trait/Numeric.juvix
new file mode 100644
index 00000000..d572e7d0
--- /dev/null
+++ b/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;

From de1a46773f7368938efdd1e54a9ff1aa4257a8f5 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Wed, 28 Feb 2024 12:53:59 +0000
Subject: [PATCH 4/7] empty commit to run checks


From a1fa387adbba27997413d248c861d75cc0a50098 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Thu, 29 Feb 2024 15:02:20 +0000
Subject: [PATCH 5/7] Fix Stdlib.Extra.Gcd.gcd

---
 Stdlib/Extra/Gcd.juvix | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Stdlib/Extra/Gcd.juvix b/Stdlib/Extra/Gcd.juvix
index a1e3b6a7..8f353dd6 100644
--- a/Stdlib/Extra/Gcd.juvix
+++ b/Stdlib/Extra/Gcd.juvix
@@ -1,12 +1,13 @@
 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.

From 27f54ef11c3b21cea18c6b00c54b1d4f3b0cb9f8 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Thu, 29 Feb 2024 15:04:58 +0000
Subject: [PATCH 6/7] Format project

---
 Stdlib/Data/Int.juvix       | 2 +-
 Stdlib/Data/List/Base.juvix | 4 ++--
 Stdlib/Data/Nat.juvix       | 2 +-
 Stdlib/Data/Product.juvix   | 4 ++--
 Stdlib/Data/Range.juvix     | 7 ++++++-
 Stdlib/Extra/Gcd.juvix      | 9 ++++++++-
 Stdlib/Trait/DivMod.juvix   | 2 +-
 Stdlib/Trait/Numeric.juvix  | 2 +-
 test/Test/Arb.juvix         | 8 ++++----
 9 files changed, 26 insertions(+), 14 deletions(-)

diff --git a/Stdlib/Data/Int.juvix b/Stdlib/Data/Int.juvix
index 25ff9cd4..6bcfc200 100644
--- a/Stdlib/Data/Int.juvix
+++ b/Stdlib/Data/Int.juvix
@@ -55,5 +55,5 @@ instance
 divModIntI : DivMod Int :=
   mkDivMod@{
     div := Int.div;
-    mod := Int.mod;
+    mod := Int.mod
   };
diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix
index 2d11526b..63459d2c 100644
--- a/Stdlib/Data/List/Base.juvix
+++ b/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;
diff --git a/Stdlib/Data/Nat.juvix b/Stdlib/Data/Nat.juvix
index 3ec1659d..59087ebd 100644
--- a/Stdlib/Data/Nat.juvix
+++ b/Stdlib/Data/Nat.juvix
@@ -39,5 +39,5 @@ instance
 divModNatI : DivMod Nat :=
   mkDivMod@{
     div := Nat.div;
-    mod := Nat.mod;
+    mod := Nat.mod
   };
diff --git a/Stdlib/Data/Product.juvix b/Stdlib/Data/Product.juvix
index de67ab8e..31c6623d 100644
--- a/Stdlib/Data/Product.juvix
+++ b/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) :=
diff --git a/Stdlib/Data/Range.juvix b/Stdlib/Data/Range.juvix
index a4379b14..8b2089ce 100644
--- a/Stdlib/Data/Range.juvix
+++ 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
diff --git a/Stdlib/Extra/Gcd.juvix b/Stdlib/Extra/Gcd.juvix
index 8f353dd6..cfcc5300 100644
--- a/Stdlib/Extra/Gcd.juvix
+++ b/Stdlib/Extra/Gcd.juvix
@@ -7,7 +7,14 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Data.Bool open;
 
 --- Computes the greatest common divisor.
-gcd {A} {{Eq A}} {{Ord A}} {{Natural A}} {{DivMod 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.
diff --git a/Stdlib/Trait/DivMod.juvix b/Stdlib/Trait/DivMod.juvix
index 376b3bf7..ca813c8b 100644
--- a/Stdlib/Trait/DivMod.juvix
+++ b/Stdlib/Trait/DivMod.juvix
@@ -4,7 +4,7 @@ trait
 type DivMod A :=
   mkDivMod {
     div : A -> A -> A;
-    mod : A -> A -> A;
+    mod : A -> A -> A
   };
 
 open DivMod public;
diff --git a/Stdlib/Trait/Numeric.juvix b/Stdlib/Trait/Numeric.juvix
index d572e7d0..df08e6cf 100644
--- a/Stdlib/Trait/Numeric.juvix
+++ b/Stdlib/Trait/Numeric.juvix
@@ -8,7 +8,7 @@ type Numeric A :=
   mkNumeric {
     integralI : Integral A;
     syntax operator / multiplicative;
-    / : A -> A -> A;
+    / : A -> A -> A
   };
 
 open Numeric using {/} public;
diff --git a/test/Test/Arb.juvix b/test/Test/Arb.juvix
index cf9f3966..fe836ede 100644
--- a/test/Test/Arb.juvix
+++ b/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 :=

From 64cf5ef88e6c9da897ab385fb16f848484658c6e Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Thu, 29 Feb 2024 15:15:49 +0000
Subject: [PATCH 7/7] Update quickcheck dependency to a compatible version

---
 test/Package.juvix | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/test/Package.juvix b/test/Package.juvix
index dfa250ca..8471173f 100644
--- a/test/Package.juvix
+++ b/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"
                      ]};