Reuse types and definitions from the builtin package-base module (#91)

The package-base module was added in
anoma/juvix#2535 - this PR updates the standard
library to reused the contents of this package to avoid duplication.

Package.juvix

@@ -1,6 +1,6 @@
 module Package;
 
-import PackageDescription.V1 open;
+import PackageDescription.V2 open;
 
 package : Package :=
   defaultPackage

Stdlib/Data/Bool/Base.juvix

@@ -1,13 +1,8 @@
 module Stdlib.Data.Bool.Base;
 
+import Juvix.Builtin.V1.Bool open public;
 import Stdlib.Data.Fixity open;
 
---- Inductive definition of booleans.
-builtin bool
-type Bool :=
-  | true
-  | false;
-
 --- Logical negation.
 not : Bool → Bool
   | true := false

Stdlib/Data/Fixity.juvix

@@ -1,23 +1,3 @@
 module Stdlib.Data.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]};
+import Juvix.Builtin.V1.Fixity open public;

Stdlib/Data/List/Base.juvix

@@ -1,23 +1,14 @@
 module Stdlib.Data.List.Base;
 
+import Juvix.Builtin.V1.List open public;
 import Stdlib.Data.Fixity open;
-
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Function open;
 import Stdlib.Data.Nat.Base open;
 import Stdlib.Data.Maybe.Base open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Data.Product.Base 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);
-
 --- 𝒪(𝓃). Returns ;true; if the given
 --- object is in the ;List;.
 {-# specialize: [1] #-}

Stdlib/Data/Maybe/Base.juvix

@@ -1,10 +1,6 @@
 module Stdlib.Data.Maybe.Base;
 
---- 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.
-type Maybe A :=
-  | nothing
-  | just A;
+import Juvix.Builtin.V1.Maybe open public;
 
 --- Extracts the value from a ;Maybe; if present, else returns the given value.
 {-# inline: true #-}

Stdlib/Data/Nat.juvix

@@ -1,5 +1,6 @@
 module Stdlib.Data.Nat;
 
+import Juvix.Builtin.V1.Nat open public;
 import Stdlib.Data.Nat.Base open hiding {+; *; div; mod} public;
 -- should be re-exported qualified
 import Stdlib.Data.Nat.Base as Nat;
@@ -31,14 +32,3 @@ ordNatI : Ord Nat := mkOrd Nat.compare;
 
 instance
 showNatI : Show Nat := mkShow natToString;
-
-{-# specialize: true, inline: case #-}
-instance
-naturalNatI : Natural Nat :=
-  mkNatural@{
-    + := (Nat.+);
-    * := (Nat.*);
-    div := Nat.div;
-    mod := Nat.mod;
-    fromNat (x : Nat) : Nat := x
-  };

Stdlib/Data/Nat/Base.juvix

@@ -1,47 +1,3 @@
 module Stdlib.Data.Nat.Base;
 
-import Stdlib.Data.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);
+import Juvix.Builtin.V1.Nat.Base open public;

Stdlib/Data/String/Base.juvix

@@ -1,18 +1,10 @@
 module Stdlib.Data.String.Base;
 
+import Juvix.Builtin.V1.String open public;
 import Stdlib.Data.List.Base open;
 import Stdlib.Function open;
 import Stdlib.Data.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;
-
 --- Concatenates a ;List; of ;String;s.
 concatStr : List String -> String := foldl (++str) "";
 

Stdlib/Trait/Natural.juvix

@@ -1,19 +1,3 @@
 module Stdlib.Trait.Natural;
 
-import Stdlib.Data.Nat.Base open using {Nat};
-import Stdlib.Data.Fixity open;
-
-trait
-type Natural A :=
-  mkNatural {
-    syntax operator + additive;
-    + : A -> A -> A;
-    syntax operator * multiplicative;
-    * : A -> A -> A;
-    div : A -> A -> A;
-    mod : A -> A -> A;
-    builtin from-nat
-    fromNat : Nat -> A
-  };
-
-open Natural public;
+import Juvix.Builtin.V1.Trait.Natural open public;

test/Package.juvix

@@ -1,6 +1,6 @@
 module Package;
 
-import PackageDescription.V1 open;
+import PackageDescription.V2 open;
 
 package : Package :=
   defaultPackage

test/juvix.lock.yaml

@@ -1,6 +1,8 @@
 # This file was autogenerated by Juvix version 0.5.4.
 # Do not edit this file manually.
 
+version: 2
+checksum: 2f561eaa260dfb905209f9d9b442c88f3ed9b4d2952185270e377ce0baa818dc
 dependencies:
 - path: ../
   dependencies: []