* Closes#2813
Implements a translation from Juvix functions to Isabelle/HOL functions.
This extends the previous Juvix -> Isabelle translation which could
handle only type signatures.
Checklist
---------
- [x] Basic translation
- [x] Polymorphism
- [x] Arithmetic operators
- [x] Numeric literals
- [x] List literals
- [x] Comparison operators
- [x] Boolean operators
- [x] `if` translated to Isabelle `if`
- [x] `true` and `false` translated to Isabelle `True` and `False`
- [x] `zero` and `suc` translated to Isabelle `0` and `Suc`
- [x] `Maybe` translated to Isabelle `option`
- [x] Pairs translated to Isabelle tuples
- [x] Quote Isabelle identifier names (e.g. cannot begin with `_`)
- [x] Rename variables to avoid clashes (in Isabelle/HOL pattern
variables don't shadow function identifiers)
- [x] Common stdlib functions (`map`, `filter`, etc) translated to
corresponding Isabelle functions
- [x] Multiple assignments in a single `let`
- [x] CLI
- [x] Test
- The test is very fragile, similar to the markdown test. It just
compares the result of translation to Isabelle against a predefined
expected output file.
Limitations
-----------
The translation is not designed to be completely correct under all
circumstances. There are aspects of the Juvix language that cannot be
straightforwardly translated to Isabelle/HOL, and these are not planned
to ever be properly handled. There are other aspects that are difficult
but not impossible to translate, and these are left for future work.
Occasionally, the generated code may need manual adjustments to
type-check in Isabelle/HOL.
In particular:
* Higher-rank polymorphism or functions on types cannot be translated as
these features are not supported by Isabelle/HOL. Juvix programs using
these features will not be correctly translated (the generated output
may need manual adjustment).
* In cases where Juvix termination checking diverges from Isabelle/HOL
termination checking, providing a termination proof manually may be
necessary. Non-terminating Juvix functions cannot be automatically
translated and need to be manually modelled in Isabelle/HOL in a
different way (e.g. as relations).
* Comments (including judoc) are ignored. This is left for future work.
* Traits are not translated to Isabelle/HOL type classes / locales. This
is left for future work.
* Mutually recursive functions are not correctly translated. This is
left for future work.
* Record creation, update, field access and pattern matching are not
correctly translated. This is left for future work.
* Named patterns are not correctly translated. This is left for future
work.
* Side conditions in patterns are not supported. This is left for future
work.
* If a Juvix function in the translated module has the same name as some
function from the Isabelle/HOL standard library, there will be a name
clash in the generated code.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Since it is common to want to assign a named argument a variable of the
same name, we add special syntax for it. E.g.
```
f (fieldA : A) (fieldB : B) : S :=
mkS@{
fieldC := fieldA; -- normal named argument
fieldA; -- pun
fieldB -- pun
};
```
- Closes#2668
This pr migrates the old named application syntax to the new one. In
order to migrate a juvix file to the new syntax it suffices to run the
formatter.
After the next release, we should completely remove the support for the
old syntax.
## Other changes
I've improved Scope negative tests. Previously, when a negative test
failed, you could only see the title of the test and the message
"Incorrect Error", as well as the Haskell file and line where the test
is defined.
This is extremely incovenient because you have to go to the haskell test
file, go to the line where the error is defined, look at the name of the
file and then visit that file. Moreover, you need to manually run the
scoper on that file to see the error that was returned.
I've fixed that and it now shows all relevant information. Example:
I've implemented this only using the `Generic` instance for the
`ScoperError` type, so doing something similar for the rest of negative
tests should be straightforward.
The stdlib composition function `∘` has fixity `composition` which means
it is right associative.
We will rename `∘` to `<<` in the stdlib and add a new function:
```
>> {a b c} : (a -> b) -> (b -> c) -> a -> c
```
for consistency with `<<` this should be left associative.
This is not a breaking change to package-base so we don't need to
increment the version number.
* Closes#2763.
* Fixes a bug in the scoper, likely introduced in
https://github.com/anoma/juvix/pull/2468 by making later declarations
depend on earlier ones. The problem was that the inductive modules were
always added at the beginning of a section, which resulted in an
incorrect definition dependency graph (an inductive type depended on its
associated projections).
* Now inductive modules are added just after a group of inductive
definitions, before the next function definition. This implies that
inductive type definitions which depend on each other cannot be
separated by function definitions. Existing Juvix code needs to be
adjusted.
* The behaviour is now equivalent to "manually" inserting module
declarations with projections after each group of inductive definitions.
* Closes#2571
* It is reasonable to finish this PR before tackling #2562, because the
field element type is the primary data type in Cairo.
* Depends on #2653
Checklist
---------
- [x] Add field type and operations to intermediate representations
(JuvixCore, JuvixTree, JuvixAsm, JuvixReg).
- [x] Add CLI option to choose field size.
- [x] Add frontend field builtins.
- [x] Automatic conversion of integer literals to field elements.
- [x] Juvix standard library support for fields.
- [x] Check if field size matches when loading a stored module.
- [x] Update the Cairo Assembly (CASM) interpreter to use the field type
instead of integer type.
- [x] Add field type to VampIR backend.
- [x] Tests
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
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](ab4376cf9e/include/package-base)
and contains the minimal set of definitions required to load a Package
file.
The
[`Juvix.Builtin`](ab4376cf9e/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`](ab4376cf9e/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 https://github.com/anoma/juvix/issues/2511
This PR adds a Package.juvix file to the global 'package' package (that
is the package containing the `PackageDescription.{Basic, V1}` modules.
This means that users can now go-to-definition on Package.juvix types
and identifiers and navigate to fully highlighted
`PackageDescription.{Basic, V1}` modules.
* Closes https://github.com/anoma/juvix/issues/2525
This PR adds the `PackageDescription.Basic` module, available to
Package.juvix files.
```
module Package;
import PackageDescription.Basic open;
package : Package := basicPackage;
```
The `PackageDescription.Basic` module provides a Package type that is
translated to a Juvix Package with all default arguments. It is not
possible to customize a basic package.
A basic package does not depend on the standard library, so loads much
more quickly.
Additionally this PR:
* Adds `juvix init --basic/-b` option to generate a basic Package.juvix.
* Migrates Package.juvix files that only use default arguments, or only
customise the name field, to basic Package files.
* Closes https://github.com/anoma/juvix/issues/2508
This PR adds a version number to the module name of the
`PackageDescription` module. This allows us to change the Package file
format in a backwards compatible way in the future.
Now the simplest Package.juvix file looks like:
```
module Package;
import PackageDescription.V1 open;
package : Package := defaultPackage;
```
## Adding new versions
The idea is that new versions of the PackageDescription format will be
added as files of the form:
include/package/PackageDescription/Vx.juvix
The correspondence between a version of the PackageDescription file and
the package type name is recorded in
[`packageDescriptionTypes`](9ba869d836/src/Juvix/Compiler/Pipeline/Package/Loader.hs (L15)).
The `package` identifier type must come from **one** of the versions
of the PackageDescription module.
* Closes https://github.com/anoma/juvix/issues/2452
Depends on:
* ~~https://github.com/anoma/juvix/pull/2459~~
* https://github.com/anoma/juvix/pull/2462
This PR is part of a series implementing:
* https://github.com/anoma/juvix/issues/2336
This PR adds the package file loading function, including a file
evaluation effect. It integrates this with the existing `readPackage`
function and adds tests / smoke tests.
## Package.juvix format
Instead of `juvix.yaml` (which is still supported currently) users can
now place a `Package.juvix` file in the root of their project. The
simplest `Package.juvix` file you can write is:
```
module Package;
import PackageDescription open;
package : Package := defaultPackage;
```
The
[PackageDescription](35b2f618f0/include/package/PackageDescription.juvix)
module defines the `Package` type. Users can use "go-to definition" in
their IDE from the Package file to see the documentation and
definitions.
Users may also import `Stdlib.Prelude` in their Package file. This is
loaded from the global project. No other module imports are supported.
Notes:
* If a directory contains both `Package.juvix` and `juvix.yaml` then
`Package.juvix` is used in preference.
## Default stdlib dependency
The `Dependency` type has a constructor called `defaultStdlib`. This
means that any project can use the compiler builtin standard library
dependency. With `juvix.yaml` this dependency is only available when the
`dependencies` field is unspecified.
```
module Package;
import PackageDescription open;
package : Package := defaultPackage { dependencies := [defaultStdlib] };
```
## Validation
As well as the standard type checking validation that the Juvix compiler
provides additional validation is made on the file.
* The Package module must contain the identifier `package` and it must
have type `Package` that's obtained from the global `PackageDescription`
module.
* Every dependency specified in the Package.juvix must be unique.
* Closes https://github.com/anoma/juvix/issues/2336
## Examples
### Package with name and version
```
module Package;
import PackageDescription open;
package : Package :=
defaultPackage {name := "a-package";
version := mkVersion 0 1 0};
```
### Package with GitHub dependency
```
module Package;
import PackageDescription open;
package : Package :=
defaultPackage {name := "a-package";
version := mkVersion 0 1 0;
dependencies := [defaultStdlib;
github (org := "anoma";
repo := "juvix-containers";
ref := "v0.7.1")]};
```
## Package with main and buildDir fields
```
module Package;
import Stdlib.Prelude open;
import PackageDescription open;
package : Package :=
defaultPackage {name := "a-package";
version := mkVersion 0 1 0;
dependencies := [defaultStdlib;
github (org := "anoma";
repo := "juvix-containers";
ref := "v0.7.1")];
buildDir := just "/tmp/build";
main := just "HelloWorld.juvix"
};
```
The special PathResolver puts files from the global package stdlib and
files from the global package description files in scope of the
$root/Package.juvix module.
Currently this means that PackageDescription module is in scope for the
module so that the user can write:
```
module Package;
import Stdlib.Prelude open;
import PackageDescription open;
package : Package :=
mkPackageDefault
(name := "foo")
{ version := mkVersion 0 1 0
; dependencies :=
[ github "anoma" "juvix-stdlib" "adf58a7180b361a022fb53c22ad9e5274ebf6f66"
; github "anoma" "juvix-containers" "v0.7.1"]};
```
