From 183d4e9329a648b339ebecf2122b3e9621c99ee8 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Fri, 1 Dec 2023 10:44:33 +0000
Subject: [PATCH] Reuse types and definitions from the builtin package-base
 module (#91)

The package-base module was added in
https://github.com/anoma/juvix/pull/2535 - this PR updates the standard
library to reused the contents of this package to avoid duplication.
---
 Package.juvix                 |  2 +-
 Stdlib/Data/Bool/Base.juvix   |  7 +-----
 Stdlib/Data/Fixity.juvix      | 22 +----------------
 Stdlib/Data/List/Base.juvix   | 11 +--------
 Stdlib/Data/Maybe/Base.juvix  |  6 +----
 Stdlib/Data/Nat.juvix         | 12 +--------
 Stdlib/Data/Nat/Base.juvix    | 46 +----------------------------------
 Stdlib/Data/String/Base.juvix | 10 +-------
 Stdlib/Trait/Natural.juvix    | 18 +-------------
 test/Package.juvix            |  2 +-
 test/juvix.lock.yaml          |  2 ++
 11 files changed, 12 insertions(+), 126 deletions(-)

diff --git a/Package.juvix b/Package.juvix
index c4a84687..f9e5479e 100644
--- a/Package.juvix
+++ b/Package.juvix
@@ -1,6 +1,6 @@
 module Package;
 
-import PackageDescription.V1 open;
+import PackageDescription.V2 open;
 
 package : Package :=
   defaultPackage
diff --git a/Stdlib/Data/Bool/Base.juvix b/Stdlib/Data/Bool/Base.juvix
index d91be1f3..79578322 100644
--- a/Stdlib/Data/Bool/Base.juvix
+++ b/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
diff --git a/Stdlib/Data/Fixity.juvix b/Stdlib/Data/Fixity.juvix
index df8fe107..e1a9ed8b 100644
--- a/Stdlib/Data/Fixity.juvix
+++ b/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;
diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix
index d6a8b120..2d11526b 100644
--- a/Stdlib/Data/List/Base.juvix
+++ b/Stdlib/Data/List/Base.juvix
@@ -1,7 +1,7 @@
 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;
@@ -9,15 +9,6 @@ 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] #-}
diff --git a/Stdlib/Data/Maybe/Base.juvix b/Stdlib/Data/Maybe/Base.juvix
index cce7c603..1ef6cc60 100644
--- a/Stdlib/Data/Maybe/Base.juvix
+++ b/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 #-}
diff --git a/Stdlib/Data/Nat.juvix b/Stdlib/Data/Nat.juvix
index 2612aae7..0573299f 100644
--- a/Stdlib/Data/Nat.juvix
+++ b/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
-  };
diff --git a/Stdlib/Data/Nat/Base.juvix b/Stdlib/Data/Nat/Base.juvix
index 8f5d56b6..f02d2874 100644
--- a/Stdlib/Data/Nat/Base.juvix
+++ b/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;
diff --git a/Stdlib/Data/String/Base.juvix b/Stdlib/Data/String/Base.juvix
index 447c2337..91b3493d 100644
--- a/Stdlib/Data/String/Base.juvix
+++ b/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) "";
 
diff --git a/Stdlib/Trait/Natural.juvix b/Stdlib/Trait/Natural.juvix
index 9b88cb83..92768536 100644
--- a/Stdlib/Trait/Natural.juvix
+++ b/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;
diff --git a/test/Package.juvix b/test/Package.juvix
index 15639d9f..dfa250ca 100644
--- a/test/Package.juvix
+++ b/test/Package.juvix
@@ -1,6 +1,6 @@
 module Package;
 
-import PackageDescription.V1 open;
+import PackageDescription.V2 open;
 
 package : Package :=
   defaultPackage
diff --git a/test/juvix.lock.yaml b/test/juvix.lock.yaml
index ebfbf86f..aae038bc 100644
--- a/test/juvix.lock.yaml
+++ b/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: []