Add FromNatural trait in package-base (#2926)

This PR adds `FromNatural` to package-base. The change is backwards
compatible for existing Juvix code so we don't need to make a new
version of package-base. The new trait is unused, it will be integrated
in subsequent PRs.

### `FromNatural` trait

The `FromNatural` trait has the following definition.

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

### `Natural` trait changes

The `Natural` trait is changed to remove its `fromNat` field and add a
new instance field for `FromNatural A`.

### juvix-stdlib changes

`FromNatural` instances are added for `Int` and `Field` in the standard
library.

## Rationale

The `FromNatural` trait will be used for the Bytes type.

We want the following properties for Byte:

1. Values of the Bytes type should be assignable from a non-negative
numeric literal.
2. We don't want to implement + and * for Bytes.

Currently, in order for a type to have property 1. it must have an
instance of `Natural` so property 2. can't be satisfied.

To solve this we split the `from-nat` builtin from the `Natural` trait
into a new trait `FromNatural`.

include/package-base/Juvix/Builtin/V1/Nat.juvix

@@ -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
   };

include/package-base/Juvix/Builtin/V1/Trait/FromNatural.juvix

@@ -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;

include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix

@@ -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;

juvix-stdlib

@@ -1 +1 @@
-Subproject commit 67ac47e377560c3c871e3ec92731be7c06c6de6a
+Subproject commit 297601a98dcace657aaff6e42945f1430647885b

tests/positive/Markdown/markdown/Test.md

@@ -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.