Add FromNatural trait in Juvix.Builtin.V2

The FromNatural trait will be used for the Bytes type.

We want the following properties for Byte:

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

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

A coercion instance is defined between Natural and FromNatural so you
don't need to write instances for both traits.

For this PR the new `FromNatural` trait is unused. A new builtin module
in package-base is defined: `Juvix.Builtin.V2` which contains the new
trait. I will make the changes to juvix-stdlib to use the new V2 modules
when I incorporate compiler changes for the Bytes type.

1. It's important to keep the `Juvix.Builtin.V1` modules in package-base so
that old juvix-stdlib versions and Package.juvix will continue to work with the new compiler.

2. I copied the whole `Juvix.Builtin` tree into `V2` even though only
`Juvix.Builtn.V2.Trait.Natural` and `Juvix.Builtin.V2.Nat` are changed.
This is to avoid confusion when updating the version numbers from V1 to
V2 in juvix-stdlib.

3. It would be possible to expose the V1 modules in the V2 modules to
avoid copying the whole body of the V1 module in the V2 module. I
decided against this because it adds another level of indirection when
looking up definitions and because confusing ambiguity errors may result
if a user mixes usage of V1 and V2 modules in that case.

include/package-base/Juvix/Builtin/V2.juvix

@@ -0,0 +1,9 @@
+module Juvix.Builtin.V2;
+
+import Juvix.Builtin.V2.Nat open public;
+import Juvix.Builtin.V2.Trait.Natural open public;
+import Juvix.Builtin.V2.String open public;
+import Juvix.Builtin.V2.Bool open public;
+import Juvix.Builtin.V2.Maybe open public;
+import Juvix.Builtin.V2.List open public;
+import Juvix.Builtin.V2.Fixity open public;

include/package-base/Juvix/Builtin/V2/Bool.juvix

@@ -0,0 +1,7 @@
+module Juvix.Builtin.V2.Bool;
+
+--- Inductive definition of booleans.
+builtin bool
+type Bool :=
+  | true
+  | false;

include/package-base/Juvix/Builtin/V2/Fixity.juvix

@@ -0,0 +1,24 @@
+module Juvix.Builtin.V2.Fixity;
+
+syntax fixity none := none;
+
+syntax fixity rapp := binary {assoc := right};
+syntax fixity lapp := binary {assoc := left; same := rapp};
+syntax fixity seq := binary {assoc := left; above := [lapp]};
+
+syntax fixity functor := binary {assoc := right};
+
+syntax fixity logical := binary {assoc := right; above := [seq]};
+syntax fixity comparison := binary {assoc := none; above := [logical]};
+
+syntax fixity pair := binary {assoc := right};
+syntax fixity cons := binary {assoc := right; above := [pair]};
+
+syntax fixity step := binary {assoc := right};
+syntax fixity range := binary {assoc := right; above := [step]};
+
+syntax fixity additive := binary {assoc := left; above := [comparison; range; cons]};
+syntax fixity multiplicative := binary {assoc := left; above := [additive]};
+
+syntax fixity composition := binary {assoc := right; above := [multiplicative]};
+syntax fixity lcomposition := binary {assoc := left; above := [multiplicative]};

include/package-base/Juvix/Builtin/V2/List.juvix

@@ -0,0 +1,12 @@
+module Juvix.Builtin.V2.List;
+
+import Juvix.Builtin.V2.Fixity open;
+
+syntax operator :: cons;
+--- Inductive list.
+builtin list
+type List (a : Type) :=
+  | --- The empty list
+    nil
+  | --- An element followed by a list
+    :: a (List a);

include/package-base/Juvix/Builtin/V2/Maybe.juvix

@@ -0,0 +1,8 @@
+module Juvix.Builtin.V2.Maybe;
+
+--- Represents an optional value that may or may not be present. Provides a way
+--- to handle null or missing values in a type-safe manner.
+builtin maybe
+type Maybe A :=
+  | nothing
+  | just A;

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

@@ -0,0 +1,14 @@
+module Juvix.Builtin.V2.Nat;
+
+import Juvix.Builtin.V2.Trait.Natural open public;
+import Juvix.Builtin.V2.Nat.Base open hiding {+; *; div; mod} public;
+import Juvix.Builtin.V2.Nat.Base as Nat;
+
+{-# specialize: true, inline: case #-}
+instance
+naturalNatI : Natural Nat :=
+  mkNatural@{
+    + := (Nat.+);
+    * := (Nat.*);
+    fromNat (x : Nat) : Nat := x
+  };

include/package-base/Juvix/Builtin/V2/Nat/Base.juvix

@@ -0,0 +1,47 @@
+module Juvix.Builtin.V2.Nat.Base;
+
+import Juvix.Builtin.V2.Fixity open;
+
+--- Inductive natural numbers. I.e. whole non-negative numbers.
+builtin nat
+type Nat :=
+  | zero
+  | suc Nat;
+
+syntax operator + additive;
+
+--- Addition for ;Nat;s.
+builtin nat-plus
++ : Nat → Nat → Nat
+  | zero b := b
+  | (suc a) b := suc (a + b);
+
+syntax operator * multiplicative;
+
+--- Multiplication for ;Nat;s.
+builtin nat-mul
+* : Nat → Nat → Nat
+  | zero _ := zero
+  | (suc a) b := b + a * b;
+
+--- Truncated subtraction for ;Nat;s.
+builtin nat-sub
+sub : Nat → Nat → Nat
+  | zero _ := zero
+  | n zero := n
+  | (suc n) (suc m) := sub n m;
+
+--- Division for ;Nat;s. Returns ;zero; if the first element is ;zero;.
+builtin nat-udiv
+terminating
+udiv : Nat → Nat → Nat
+  | zero _ := zero
+  | n m := suc (udiv (sub n m) m);
+
+--- Division for ;Nat;s.
+builtin nat-div
+div (n m : Nat) : Nat := udiv (sub (suc n) m) m;
+
+--- Modulo for ;Nat;s.
+builtin nat-mod
+mod (n m : Nat) : Nat := sub n (div n m * m);

include/package-base/Juvix/Builtin/V2/String.juvix

@@ -0,0 +1,12 @@
+module Juvix.Builtin.V2.String;
+
+import Juvix.Builtin.V2.Fixity open;
+
+--- Primitive representation of a sequence of characters.
+builtin string
+axiom String : Type;
+
+syntax operator ++str cons;
+--- Concatenation of two ;String;s.
+builtin string-concat
+axiom ++str : String -> String -> String;

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

@@ -0,0 +1,10 @@
+module Juvix.Builtin.V2.Trait.FromNatural;
+
+import Juvix.Builtin.V2.Nat.Base open using {Nat};
+
+trait
+type FromNatural A :=
+  mkFromNatural {
+    builtin from-nat
+    fromNat : Nat -> A
+};

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

@@ -0,0 +1,22 @@
+module Juvix.Builtin.V2.Trait.Natural;
+
+import Juvix.Builtin.V2.Nat.Base open using {Nat};
+import Juvix.Builtin.V2.Fixity open;
+import Juvix.Builtin.V2.Trait.FromNatural open;
+
+trait
+type Natural A :=
+  mkNatural {
+    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;
+    fromNat : Nat -> A
+  };
+
+open Natural public;
+
+coercion instance
+FromNaturalNaturalI {A} {{N : Natural A}} : FromNatural A := mkFromNatural@{fromNat};