Add FromNatural instances for Int and Field (#117)

Adds `FromNatural` instances for `Int` and `Field`. Used by: * anoma/juvix#2926 A temporary version of juvix-quickcheck is used that works with the Natural/FromNatural changes.
anoma · Aug 5, 2024 · 0e6f82e · 0e6f82e
1 parent 67ac47e
commit 0e6f82e
Show file tree

Hide file tree

Showing 7 changed files with 28 additions and 9 deletions.
diff --git a/Stdlib/Data/Field.juvix b/Stdlib/Data/Field.juvix
@@ -8,6 +8,7 @@ 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.FromNatural open;
 import Stdlib.Trait.Integral open public;
 import Stdlib.Trait.Numeric open public;
 
@@ -21,13 +22,19 @@ showFieldI : Show Field :=
     show (f : Field) : String := Show.show (Field.toNat f)
   };
 
+{-# specialize: true, inline: case #-}
+instance
+fromNaturalFieldI : FromNatural Field :=
+  mkFromNatural@{
+    fromNat := Field.fromNat
+  };
+
 {-# specialize: true, inline: case #-}
 instance
 naturalFieldI : Natural Field :=
   mkNatural@{
     + := (Field.+);
-    * := (Field.*);
-    fromNat := Field.fromNat
+    * := (Field.*)
   };
 
 {-# specialize: true, inline: case #-}

diff --git a/Stdlib/Data/Int.juvix b/Stdlib/Data/Int.juvix
@@ -11,6 +11,7 @@ import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 import Stdlib.Trait.Natural open;
+import Stdlib.Trait.FromNatural open;
 import Stdlib.Trait.Integral open;
 import Stdlib.Trait.DivMod open;
 
@@ -32,13 +33,19 @@ ordIntI : Ord Int := mkOrd Int.compare;
 instance
 showIntI : Show Int := mkShow intToString;
 
+{-# specialize: true, inline: case #-}
+instance
+fromNaturalIntI : FromNatural Int :=
+  mkFromNatural@{
+    fromNat := ofNat
+  };
+
 {-# specialize: true, inline: case #-}
 instance
 naturalIntI : Natural Int :=
   mkNatural@{
     + := (Int.+);
-    * := (Int.*);
-    fromNat := ofNat
+    * := (Int.*)
   };
 
 {-# specialize: true, inline: case #-}

diff --git 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.FromNatural open public;
 import Stdlib.Trait.DivMod open public;
 
 -- should be re-exported qualified

diff --git a/Stdlib/Trait.juvix b/Stdlib/Trait.juvix
@@ -7,6 +7,7 @@ import Stdlib.Trait.Functor open public;
 import Stdlib.Trait.Foldable open public;
 import Stdlib.Trait.Partial open public;
 import Stdlib.Trait.Natural open public;
+import Stdlib.Trait.FromNatural 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/FromNatural.juvix b/Stdlib/Trait/FromNatural.juvix
@@ -0,0 +1,3 @@
+module Stdlib.Trait.FromNatural;
+
+import Juvix.Builtin.V1.Trait.FromNatural open public;
diff --git a/test/Package.juvix b/test/Package.juvix
@@ -6,5 +6,5 @@ package : Package :=
   defaultPackage@?{
     name := "stdlib-test";
     dependencies :=
-      [path "../"; github "anoma" "juvix-quickcheck" "8e5d49682fb0b861fc0a1aed95cfebab03231d85"]
+      [path "../"; github "anoma" "juvix-quickcheck" "eca0d109869eeb7b708162634f4917f270139da1"]
   };
diff --git a/test/juvix.lock.yaml b/test/juvix.lock.yaml
@@ -1,18 +1,18 @@
-# This file was autogenerated by Juvix version 0.6.3.
+# This file was autogenerated by Juvix version 0.6.4.
 # Do not edit this file manually.
 
 version: 2
-checksum: 6ad1c42b98c3512560e5de4a3502d387b92fe6ea883f40a59299d10f17bd3851
+checksum: fe279cadfedcac3f17d3557f5b1bbc168a153b29b6876bd56df33e21aad59ee5
 dependencies:
 - path: ../
   dependencies: []
 - git:
     name: anoma_juvix-quickcheck
-    ref: 8e5d49682fb0b861fc0a1aed95cfebab03231d85
+    ref: eca0d109869eeb7b708162634f4917f270139da1
     url: https://github.com/anoma/juvix-quickcheck
   dependencies:
   - git:
       name: anoma_juvix-stdlib
-      ref: 95f93e60e1033046d950414a805f7a4bc75adb62
+      ref: 297601a98dcace657aaff6e42945f1430647885b
       url: https://github.com/anoma/juvix-stdlib
     dependencies: []
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		module Stdlib.Trait.FromNatural;

		import Juvix.Builtin.V1.Trait.FromNatural open public;