* Closes#3079
* Closes#3086
* Depends on #3088
* Updates the coding style guidelines (CODING.md) to reflect issues not
foreseen originally
* Changes the unicode arrow printed in the REPL to `->`. This is to make
the output consistent with how function types are written in the
standard library.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
This PR adds `FromNatural` to package-base. The change is backwards
compatible for existing Juvix code so we don't need to make a new
version of package-base. The new trait is unused, it will be integrated
in subsequent PRs.
### `FromNatural` trait
The `FromNatural` trait has the following definition.
```
trait
type FromNatural A :=
mkFromNatural {
builtin from-nat
fromNat : Nat -> A
};
```
### `Natural` trait changes
The `Natural` trait is changed to remove its `fromNat` field and add a
new instance field for `FromNatural A`.
### juvix-stdlib changes
`FromNatural` instances are added for `Int` and `Field` in the standard
library.
## Rationale
The `FromNatural` trait will be used for the Bytes type.
We want the following properties for Byte:
1. Values of the Bytes type should be assignable from a non-negative
numeric literal.
2. We don't want to implement + and * for Bytes.
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`.
* 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>
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#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
