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.

Sign up for GitHub

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 trait in package-base #2926

Merged
merged 6 commits into from
Aug 1, 2024
Merged

Add FromNatural trait in package-base #2926

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
5061e04
Update juvix-stdlib to point to main
paulcadman Jul 30, 2024
7c524c5
Add FromNatural trait in Juvix.Builtin.V1
paulcadman Jul 29, 2024
a829eba
Add general Natural -> FromNatural coercion with specialize pragma
paulcadman Jul 30, 2024
ecbff8b
Use instance fields to make Natural into a FromNatural
paulcadman Jul 30, 2024
eed9793
Export FromNatural identifiers public
paulcadman Jul 30, 2024
d511b12
Fix markdown test output after stdlib change
paulcadman Jul 31, 2024
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
9 changes: 8 additions & 1 deletion include/package-base/Juvix/Builtin/V1/Nat.juvix
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,14 +1,21 @@
module Juvix.Builtin.V1.Nat;

import Juvix.Builtin.V1.Trait.Natural open public;
import Juvix.Builtin.V1.Trait.FromNatural open public;
import Juvix.Builtin.V1.Nat.Base open hiding {+; *; div; mod} public;
import Juvix.Builtin.V1.Nat.Base as Nat;

{-# specialize: true, inline: case #-}
instance
fromNaturalNatI : FromNatural Nat :=
mkFromNatural@{
fromNat (x : Nat) : Nat := x
};

{-# specialize: true, inline: case #-}
instance
naturalNatI : Natural Nat :=
mkNatural@{
+ := (Nat.+);
* := (Nat.*);
fromNat (x : Nat) : Nat := x
};
12 changes: 12 additions & 0 deletions include/package-base/Juvix/Builtin/V1/Trait/FromNatural.juvix
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
module Juvix.Builtin.V1.Trait.FromNatural;

import Juvix.Builtin.V1.Nat.Base open using {Nat};

trait
type FromNatural A :=
mkFromNatural {
builtin from-nat
fromNat : Nat -> A
};

open FromNatural public;
4 changes: 2 additions & 2 deletions include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,18 +2,18 @@ module Juvix.Builtin.V1.Trait.Natural;

import Juvix.Builtin.V1.Nat.Base open using {Nat};
import Juvix.Builtin.V1.Fixity open;
import Juvix.Builtin.V1.Trait.FromNatural open;

trait
type Natural A :=
mkNatural {
{{FromNaturalI}} : FromNatural A;
syntax operator + additive;
{-# isabelle-operator: {name: "+", prec: 65, assoc: left} #-}
+ : A -> A -> A;
syntax operator * multiplicative;
{-# isabelle-operator: {name: "*", prec: 70, assoc: left} #-}
* : A -> A -> A;
builtin from-nat
fromNat : Nat -> A
};

open Natural public;
2 changes: 1 addition & 1 deletion juvix-stdlib
Open in desktop
Submodule juvix-stdlib updated 5 files
+9 −2 Stdlib/Data/Field.juvix
+9 −2 Stdlib/Data/Int.juvix
+1 −0 Stdlib/Data/Nat.juvix
+1 −0 Stdlib/Trait.juvix
+3 −0 Stdlib/Trait/FromNatural.juvix
2 changes: 1 addition & 1 deletion tests/positive/Markdown/markdown/Test.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ Certain blocks can be hidden from the output by adding the `hide` attribute, as



<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="YTest:1"><span class="annot"><a href="X#YTest:1"><span class="annot"><a href="X#YTest:1"><span class="ju-function">fib</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:2"><span class="ju-constructor">zero</span></a></span> <span id="YTest:3"><span class="annot"><a href="X#YTest:3"><span class="annot"><a href="X#YTest:3"><span class="ju-var">x1</span></a></span></a></span></span> <span class="ju-keyword">_</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:3"><span class="ju-var">x1</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:3"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="YTest:4"><span class="annot"><a href="X#YTest:4"><span class="annot"><a href="X#YTest:4"><span class="ju-var">n</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span id="YTest:5"><span class="annot"><a href="X#YTest:5"><span class="annot"><a href="X#YTest:5"><span class="ju-var">x1</span></a></span></a></span></span> <span id="YTest:6"><span class="annot"><a href="X#YTest:6"><span class="annot"><a href="X#YTest:6"><span class="ju-var">x2</span></a></span></a></span></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:1"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#YTest:4"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#YTest:6"><span class="ju-var">x2</span></a></span> <span class="annot"><a href="X#YTest:5"><span class="ju-var"><span class="ju-delimiter">(</span>x1</span></a></span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Trait.Natural:7"><span class="ju-function">+</span></a></span> <span class="annot"><a href="X#YTest:6"><span class="ju-var">x2</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><br/><span id="YTest:2"><span class="annot"><a href="X#YTest:2"><span class="annot"><a href="X#YTest:2"><span class="ju-function">fibonacci</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#YTest:7"><span class="ju-var">n</span></a></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:1"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#YTest:7"><span class="ju-var">n</span></a></span> <span class="ju-number">0</span> <span class="ju-number">1</span><span class="ju-delimiter">;</span></pre></code></pre>
<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="YTest:1"><span class="annot"><a href="X#YTest:1"><span class="annot"><a href="X#YTest:1"><span class="ju-function">fib</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:2"><span class="ju-constructor">zero</span></a></span> <span id="YTest:3"><span class="annot"><a href="X#YTest:3"><span class="annot"><a href="X#YTest:3"><span class="ju-var">x1</span></a></span></a></span></span> <span class="ju-keyword">_</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:3"><span class="ju-var">x1</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:3"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="YTest:4"><span class="annot"><a href="X#YTest:4"><span class="annot"><a href="X#YTest:4"><span class="ju-var">n</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span id="YTest:5"><span class="annot"><a href="X#YTest:5"><span class="annot"><a href="X#YTest:5"><span class="ju-var">x1</span></a></span></a></span></span> <span id="YTest:6"><span class="annot"><a href="X#YTest:6"><span class="annot"><a href="X#YTest:6"><span class="ju-var">x2</span></a></span></a></span></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:1"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#YTest:4"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#YTest:6"><span class="ju-var">x2</span></a></span> <span class="annot"><a href="X#YTest:5"><span class="ju-var"><span class="ju-delimiter">(</span>x1</span></a></span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Trait.Natural:8"><span class="ju-function">+</span></a></span> <span class="annot"><a href="X#YTest:6"><span class="ju-var">x2</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><br/><span id="YTest:2"><span class="annot"><a href="X#YTest:2"><span class="annot"><a href="X#YTest:2"><span class="ju-function">fibonacci</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#YTest:7"><span class="ju-var">n</span></a></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:1"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#YTest:7"><span class="ju-var">n</span></a></span> <span class="ju-number">0</span> <span class="ju-number">1</span><span class="ju-delimiter">;</span></pre></code></pre>

The `extract-module-statements` attribute can be used to display only the statements contained in a module in the output.

Expand Down
Loading