Extract builtin definitions for loading a Package into bundled packag…

…e-base package (#2535)

This PR creates a new package that's bundled with the compiler in a
similar way to the stdlib and the package description package.

## The `package-base` Package

This package is called
[package-base](https://github.com/anoma/juvix/tree/ab4376cf9e2e1330ff3feb98c5ba940a622d8964/include/package-base)
and contains the minimal set of definitions required to load a Package
file.

The
[`Juvix.Builtin`](https://github.com/anoma/juvix/blob/ab4376cf9e2e1330ff3feb98c5ba940a622d8964/include/package-base/Juvix/Builtin/V1.juvix)
module contains:

```
module Juvix.Builtin.V1;

import Juvix.Builtin.V1.Nat open public;
import Juvix.Builtin.V1.Trait.Natural open public;
import Juvix.Builtin.V1.String open public;
import Juvix.Builtin.V1.Bool open public;
import Juvix.Builtin.V1.Maybe open public;
import Juvix.Builtin.V1.List open public;
import Juvix.Builtin.V1.Fixity open public;
```

`Juvix.Builtin.V1.Bool` is required to support backend primitive
integers `Juvix.Builtin.V1.Trait.Natural` is required to support numeric
literals.

## The `PackageDescription.V2` module

This PR also adds a new
[`PackageDescription.V2`](https://github.com/anoma/juvix/blob/ab4376cf9e2e1330ff3feb98c5ba940a622d8964/include/package/PackageDescription/V2.juvix)
type that uses the `package-base`. This is to avoid breaking existing
Package files. The Packages files in the repo (except those that test
`PackageDescription.V1`) have also been updated.

## Updating the stdlib

The standard library will be updated to use `Juvix.Builtin.*` modules in
a subsequent PR.

* Part of #2511

app/App.hs

@@ -49,7 +49,7 @@ runAppIO ::
   Sem r a
 runAppIO args@RunAppIOArgs {..} =
   interpret $ \case
-    AskPackageGlobal -> return (_runAppIOArgsRoot ^. rootPackageGlobal)
+    AskPackageGlobal -> return (_runAppIOArgsRoot ^. rootPackageType `elem` [GlobalStdlib, GlobalPackageDescription, GlobalPackageBase])
     FromAppPathFile p -> embed (prepathToAbsFile invDir (p ^. pathPath))
     GetMainFile m -> getMainFile' m
     FromAppPathDir p -> embed (prepathToAbsDir invDir (p ^. pathPath))

app/Commands/Extra/Package.hs

@@ -6,8 +6,11 @@ import Juvix.Compiler.Pipeline.Package.Loader
 import Juvix.Extra.Paths
 import Juvix.Prelude
 
+currentPackageVersion :: PackageVersion
+currentPackageVersion = PackageVersion2
+
 renderPackage :: Package -> Text
-renderPackage = renderPackageVersion PackageVersion1
+renderPackage = renderPackageVersion currentPackageVersion
 
 writePackageFile' :: (Member (Embed IO) r) => PackageVersion -> Path Abs Dir -> Package -> Sem r ()
 writePackageFile' v root pkg =
@@ -18,7 +21,7 @@ writePackageFile' v root pkg =
     )
 
 writePackageFile :: (Member (Embed IO) r) => Path Abs Dir -> Package -> Sem r ()
-writePackageFile = writePackageFile' PackageVersion1
+writePackageFile = writePackageFile' currentPackageVersion
 
 writeBasicPackage :: (Member (Embed IO) r) => Path Abs Dir -> Sem r ()
 writeBasicPackage root = writePackageFile' PackageBasic root (emptyPackage DefaultBuildDir (root <//> packageFilePath))

examples/demo/Package.juvix

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

examples/midsquare/Package.juvix

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

examples/milestone/Bank/Package.juvix

@@ -1,5 +1,5 @@
 module Package;
 
-import PackageDescription.V1 open;
+import PackageDescription.V2 open;
 
 package : Package := defaultPackage {name := "bank"};

examples/milestone/Collatz/Package.juvix

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

examples/milestone/Fibonacci/Package.juvix

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

examples/milestone/Hanoi/Package.juvix

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

examples/milestone/HelloWorld/Package.juvix

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

examples/milestone/PascalsTriangle/Package.juvix

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

examples/milestone/TicTacToe/Package.juvix

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

examples/milestone/Tutorial/Package.juvix

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

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

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

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

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

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

@@ -0,0 +1,23 @@
+module Juvix.Builtin.V1.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]};

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

@@ -0,0 +1,12 @@
+module Juvix.Builtin.V1.List;
+
+import Juvix.Builtin.V1.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/V1/Maybe.juvix

@@ -0,0 +1,7 @@
+module Juvix.Builtin.V1.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.
+type Maybe A :=
+  | nothing
+  | just A;

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

@@ -0,0 +1,16 @@
+module Juvix.Builtin.V1.Nat;
+
+import Juvix.Builtin.V1.Trait.Natural 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
+naturalNatI : Natural Nat :=
+  mkNatural@{
+    + := (Nat.+);
+    * := (Nat.*);
+    div := Nat.div;
+    mod := Nat.mod;
+    fromNat (x : Nat) : Nat := x
+  };

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

@@ -0,0 +1,47 @@
+module Juvix.Builtin.V1.Nat.Base;
+
+import Juvix.Builtin.V1.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/V1/String.juvix

@@ -0,0 +1,12 @@
+module Juvix.Builtin.V1.String;
+
+import Juvix.Builtin.V1.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/V1/Trait/Natural.juvix

@@ -0,0 +1,19 @@
+module Juvix.Builtin.V1.Trait.Natural;
+
+import Juvix.Builtin.V1.Nat.Base open using {Nat};
+import Juvix.Builtin.V1.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;

include/package/PackageDescription/V2.juvix

@@ -0,0 +1,72 @@
+module PackageDescription.V2;
+
+import Juvix.Builtin.V1 open public;
+
+--- A ;Package; defines the configuration for a Juvix package
+type Package :=
+  mkPackage {
+    -- The name of the package
+    name : String;
+    -- The version for the package
+    version : SemVer;
+    -- The dependencies of this package
+    dependencies : List Dependency;
+    -- A path to the Main module for this package
+    main : Maybe String;
+    -- A path to a directory where Juvix should output intermediate build products
+    buildDir : Maybe String
+  };
+
+--- Construct a ;Package; with useful default arguments.
+defaultPackage {name : String := "my-project"} {version : SemVer := defaultVersion} {dependencies : List
+  Dependency := [defaultStdlib]} {main : Maybe
+  String := nothing} {buildDir : Maybe String := nothing}
+  : Package :=
+  mkPackage name version dependencies main buildDir;
+
+--- A ;SemVer; defines a version that conforms to the Semantic Versioning specification.
+type SemVer :=
+  mkSemVer {
+    major : Nat;
+    minor : Nat;
+    patch : Nat;
+    release : Maybe String;
+    meta : Maybe String
+  };
+
+--- Construct a ;SemVer; with useful default arguments.
+mkVersion (major minor patch : Nat) {release : Maybe
+  String := nothing} {meta : Maybe String := nothing}
+  : SemVer :=
+  mkSemVer
+    (major := major;
+    minor := minor;
+    patch := patch;
+    release := release;
+    meta := meta);
+
+--- The default version used in `defaultPackage`.
+defaultVersion : SemVer := mkVersion 0 0 0;
+
+--- A ;Dependency; defines a Juvix package dependency.
+type Dependency :=
+  | --- A filesystem path to another Juvix Package.
+    path {path : String}
+  | --- A ;git; repository containing a Juvix package at its root
+    git {
+      -- A name for this dependency
+      name : String;
+      -- The URL to the git repository
+      url : String;
+      -- The git ref to checkout
+      ref : String
+    }
+  | --- The ;defaultStdlib; that is bundled with the Juvix compiler.
+    defaultStdlib;
+
+--- Constructs a GitHub dependency.
+github (org repo ref : String) : Dependency :=
+  git
+    (org ++str "_" ++str repo)
+    ("https://github.com/" ++str org ++str "/" ++str repo)
+    ref;