Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add FromNatural instances for Int and Field #117

Merged
merged 3 commits into from
Aug 5, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 9 additions & 2 deletions Stdlib/Data/Field.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -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 #-}
Expand Down
11 changes: 9 additions & 2 deletions Stdlib/Data/Int.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -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 #-}
Expand Down
1 change: 1 addition & 0 deletions Stdlib/Data/Nat.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions Stdlib/Trait.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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;
3 changes: 3 additions & 0 deletions Stdlib/Trait/FromNatural.juvix
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;
2 changes: 1 addition & 1 deletion test/Package.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -6,5 +6,5 @@ package : Package :=
defaultPackage@?{
name := "stdlib-test";
dependencies :=
[path "../"; github "anoma" "juvix-quickcheck" "8e5d49682fb0b861fc0a1aed95cfebab03231d85"]
[path "../"; github "anoma" "juvix-quickcheck" "eca0d109869eeb7b708162634f4917f270139da1"]
};
8 changes: 4 additions & 4 deletions test/juvix.lock.yaml
Original file line number Diff line number Diff line change
@@ -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: []
Loading