Example file:
```
module error;
import empty; -- error only happens if we have at least one import
type T := t;
x : T := t t; -- type error
```
If one loads this file into emacs (or vscode) they'll get a type error
as expected, but name colors and go-to information is lost, which is
annoying. This pr fixes this.
I'm not sure why, but this bug only occurs when there is at least one
import.
This pr has two relevant changes:
## Errors instead of crases
When registering a builtin, we perform some sanity checks. When
unsuccessful, the compiler crashes. This seldom happens because builtins
are defined in libraries that we write ourselves. However, any compiler
crash is a bug, so this pr refactors these crashes into proper errors.
## Registering builtins during scoping
Before this pr, builtins are registered and sanity checked during the
translation from Concrete to Internal. This imposes that the order in
which we translate stuff is relevant, as we must register a builtin
before we use it. For the most part this is fine when the dependency is
explicit in the code, but sometimes there are explicit dependencies.
E.g. do notation and the builtin `monad-bind`. In order to avoid adding
special rules, it is easier to just register builtins during scoping, so
I've refactored the code to do this.
I've also removed the `Builtins` effect and moved its methods to the
`InfoTableBuilder` since the builtins table is now part of the Scoped
InfoTable. Consequently, I've removed the the field `_artifactBuiltins`.
## Future work
- Fix#2952. I didn't find a good way to fix this problem in this pr, so
it is left for a separate pr.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
The `anoma-bytearray-{to, from}-anoma-contents` are intended to be used
to convert to/from atoms representing `ByteArrays`. These builtins are
required temporarily until Anoma Node makes ByteArray representation
uniform across all of its APIs.
We represent ByteArrays in nock as a cell:
```
[size contents]
```
Where `size` is the size of the ByteArray and `contents` is an Atom
representing the bytes in LSB ordering.
The `size` is required in general because the encoding of ByteArrays to
Atoms is ambiguous. For example the ByteArrays [0x01; 0x00] and [0x01]
are represented by `1`.
Some Anoma ByteArrays like keys and signatures are represented using on
the `contents` atom because the size is constant.
Users of Anoma APIs have to strip / add size information from ByteArrays
depending on where the data is used. The new builtins provide this
facility.
These builtins are temporary because it's been agreed with Anoma
engineering team to change the Anoma APIs to make the ByteArray
representation uniform, i.e always represent ByteArrays using `[size
content]`. When this is implemented in Anoma Node we can remove these
builtins.
```
builtin anoma-bytearray-to-anoma-contents
axiom toAnomaContents : ByteArray -> Nat;
builtin anoma-bytearray-from-anoma-contents
axiom fromAnomaContents :
-- | The size of the ByteArray
Nat
-- | The contents of the ByteArray
-> Nat
-- | The resulting ByteArray
-> ByteArray;
```
This PR updates:
- [x] Package version
- [x] Smoke test
- [x] Changelog
We can't merge this until the stdlib submodule pointer is fixed-up to
point to stdlib main.
* Specialization has become less effective after recent changes to the
codebase. This PR fixes issues with specialization.
* Closes#2939
* Closes#2945
Checklist
---------
- [X] Preserve pragmas for letrec and lambda in Stored Core
- [x] Remove the assumption that all type variables are at the front
(closes#2945)
- [x] Allow specialization when the argument is a constructor
application
- [x] Make renaming adjust pragmas
- [x] Allow pragmas for fields in record definitions (closes#2939)
- [x] Update standard library pragmas
- [x] Fix JuvixTree printing
This PR adds support for ByteArray in the Anoma cryptographic functions.
```
builtin anoma-sign
axiom anomaSign : {A : Type} -> A -> ByteArray -> ByteArray;
builtin anoma-verify-with-message
axiom anomaVerifyWithMessage : {A : Type} -> ByteArray -> ByteArray -> Maybe A;
builtin anoma-sign-detached
axiom anomaSignDetached : {A : Type} -> A -> ByteArray -> ByteArray;
builtin anoma-verify-detached
axiom anomaVerifyDetached : {A : Type} -> ByteArray -> A -> ByteArray -> Bool;
```
The Anoma / Hoon Stdlib function `length` needs to be exposed as a
StdlibFunction because a ByteArray stores its length and the value
returned by `anomaSign` is not a fixed length.
This PR adds support for a builtin `ByteArray` type and associated
functions for constructing a `ByteArray` from a list of bytes and a
function to query the size of the `ByteArray`. It is only available in
the Anoma backend.
In Core / Tree, ByteArray constant is stored using a Haskell ByteString.
In Anoma the ByteArray is stored as a cell where the head is the length
of the ByteArray and the tail is an integer is an integer formed by
concatenating the bytes in the array using little-endian byte ordering.
The Nock for constructing a `ByteArray` uses the `length`, `add`,
`folder` and `lsh` functions from the Anoma hoon stdlib. See the [code
comment](fa068a30e7/src/Juvix/Compiler/Nockma/StdlibFunction.hs (L37))
for more details.
Example:
```
module test082;
import Stdlib.Prelude open;
import Stdlib.Debug.Trace open;
builtin bytearray
axiom ByteArray : Type;
builtin bytearray-from-list-byte
axiom mkByteArray : List Byte -> ByteArray;
builtin bytearray-size
axiom size : ByteArray -> Nat;
bs0 : ByteArray := mkByteArray [];
bs1 : ByteArray := mkByteArray [0x0; 0x0; 0x0];
bs2 : ByteArray := mkByteArray [0x1; 0x0; 0x0; 0x0];
bs3 : ByteArray := mkByteArray [0x2; 0x1];
bs4 : ByteArray := mkByteArray [0x100];
main : ByteArray :=
trace (size bs0)
>-> trace bs0
>-> trace (size bs1)
>-> trace bs1
>-> trace (size bs2)
>-> trace bs2
>-> trace (size bs3)
>-> trace bs3
>-> trace (size bs4)
>-> bs4;
```
Output using `tests/Anoma/Compilation/positive/test082.juvix`
```
$ juvix compile anoma -g test082.juvix
$ juvix dev nockma run test082.pretty.nockma
0
[0 0]
3
[3 0]
4
[4 1]
2
[2 258]
1
[1 0]
```
This pr adds the `--statements` flag to `juvix dev latex export`. It can
be used like this:
```
juvix dev latex export --statements "List; elem; find" List.juvix
```
All statements are selectable by their 'label'. The label of a statement
is defined as:
1. The function/type/operator/alias/axiom/local_module/fixity/iterator
name being defined.
2. The module name being imported.
## Limitations:
1. Only top statements are allowed. I.e. statements inside local modules
cannot be selected.
1. Open statements are not selectable. Giving `--statements "My.Module"`
will refer to the import statement `import My.Module`.
4. Single constructors are not selectable. Only the whole type
definition.
5. No comments will be printed.
This pr adds two new commands related to latex.
1. `juvix dev latex getJuvixSty`. This command prints the contents of
the `juvix.sty` latex package to stdout. It has no options and the
expected usage is `juvix dev latex getJuvixSty > juvix.sty`.
2. `juvix dev latex export`. Expects a .juvix file as an argument and
outputs to stdout the highlighted module in latex format. Optional flags
`--from LINE`, `--to LINE` to output only the specified line range.
There is a `--mode` flag to choose how you want the output.
```
• standalone: Output a ready to compile LaTeX file
• wrap: Wrap the code in a Verbatim environment
• raw: Output only the code (default: standalone)
```
4. As shown in the standalone output, one is allowed to choose the theme
when importing the juvix package like this: `\usepackage[theme =
latte]{juvix}`. Available themes are `latte`, `frappe`, `macchiato`,
`mocha`.
Examples:
To generate the following output I ran these commands:
```
cd examples/milestones/HelloWorld
mkdir latex
juvix dev latex getJuvixSty > latex/juvix.sty
juvix dev latex export HelloWorld.juvix > latex/main.tex
cd latex
xelatex main.tex
open main.pdf
```
1. with `\usepackage[theme = latte]{juvix}`:
1. with `\usepackage[theme = frappe]{juvix}`:
1. with `\usepackage[theme = macchiato]{juvix}`:
1. with `\usepackage[theme = mocha]{juvix}`:
1. Refactors css theme to only use variables as source for colors to
make it easier to define themes. In order to define a theme, the
following variables need to be defined (these variables have been taken
mostly from the catppuchin theme):
```
/* Code */
--ju-inductive: var(--ctp-green);
--ju-constructor: var(--ctp-mauve);
--ju-function: var(--ctp-yellow);
--ju-module: var(--ctp-lavender);
--ju-axiom: var(--ctp-red);
--ju-string: var(--ctp-flamingo);
--ju-keyword: var(--ctp-sky);
--ju-delimiter: var(--ctp-overlay2);
--ju-var: var(--ctp-text);
--ju-fixity: var(--ctp-sapphire);
--ju-comment: var(--ctp-rosewater);
--ju-judoc: var(--ctp-teal);
--ju-number: var(--ctp-peach);
/* Text */
--ju-text: var(--ctp-text);
--ju-subtext1: var(--ctp-subtext1);
--ju-subtext0: var(--ctp-subtext0);
/* Overlay */
--ju-overlay0: var(--ctp-overlay0);
--ju-overlay1: var(--ctp-overlay1);
--ju-overlay2: var(--ctp-overlay2);
/* Surface */
--ju-surface0: var(--ctp-surface0);
--ju-surface1: var(--ctp-surface1);
--ju-surface2: var(--ctp-surface2);
/* Panes */
--ju-base: var(--ctp-base);
--ju-mantle: var(--ctp-mantle);
--ju-crust: var(--ctp-mantle);
/* Theme */
--ju-main: var(--ctp-maroon);
--ju-main-link: var(--ctp-maroon);
--ju-main-link-visited: var(--ctp-flamingo);
--ju-warning: var(--ctp-red);
```
2. When changing theme, the judoc documentation will also use that
theme, as opposed to only the source code.
3. Added highlighting for module names.
4. When hovering a juvix code element (axiom, constructor, inductive,
etc.), the underline will be of the correct color for the kind. Before
it was always a fixed color.
- In https://github.com/anoma/juvix/pull/2925, the flatparse scanner
always fails for .md files and silently falls back to megaparsec.
- In https://github.com/anoma/juvix/pull/2929, a warning is introduced
that informs the user when the fallback parser is being used. This is
causing a warning every time we scan a markdown file.
- This pr fixes the problem by changing the default strategy to directly
use megaparsec when a .md file is given.
This PR adds `Byte` as a builtin with builtin functions for equality,
`byte-from-nat` and `byte-to-nat`. The standard library is updated to
include this definition with instances for `FromNatural`, `Show` and
`Eq` traits.
The `FromNatural` trait means that you can assign `Byte` values using
non-negative numeric literals.
You can use byte literals in jvc files by adding the u8 suffix to a
numeric value. For example, 1u8 represents a byte literal.
Arithmetic is not supported as the intention is for this type to be used
to construct ByteArrays of data where isn't not appropriate to modify
using arithmetic operations. We may add a separate `UInt8` type in the
future which supports arithmetic.
The Byte is supported in the native, rust and Anoma backend. Byte is not
supported in the Cairo backend because `byte-from-nat` cannot be
defined.
The primitive builtin ops for `Byte` are called `OpUInt8ToInt` and
`OpUInt8FromInt`, named because these ops work on integers and in future
we may reuse these for a separate unsigned 8-bit integer type that
supports arithmetic.
Part of:
* https://github.com/anoma/juvix/issues/2865
This pr:
- Removes the light `ayu` theme.
- Adds the light `latte` theme (this now becomes the default theme).
- Adds the dark `frappe` theme.
- Adds the dark `moccha` theme.
- Refactor all source themes to use css variables instead of inlined
color definitions. This makes it much easier to maintain.
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`.
1. When the flatparse scanner fails and we fallback to megaparsec, a
warning is issued.
2. The flatparse scanner has been fixed so it is not confused when a
name starts with `import`.
This PR addresses a bug/missing case present since v0.6.2, introduced
specifically by
- PR #2779,
That PR involves detecting imports in Juvix files before type checking,
and that's the issue.
Detecting/scanning imports is done by running a flat parser (which
ignores the Juvix Markdown structure) and when it fails, it runs a
Megaparser parse. So, for simplicity,
we could just continue using the same Megaparser as before for Juvix
Markdown files.
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
- Closes#2923
This pr fixes a bug where all fields were assigned to be explicit
arguments in the NameSignature Builder. A single line change was enough
to fix it.
```diff
- RecordStatementField RecordField {..} -> addSymbol @s Explicit Nothing _fieldName _fieldType
+ RecordStatementField RecordField {..} -> addSymbol @s (fromIsImplicitField _fieldIsImplicit) Nothing _fieldName _fieldType
```
I've also added a compilation test for instance fields.
1. Adds the `--log-level LOG_LEVEL` flag to the CLI. This flag can be
given `error`, `warn`, `info`, `progress`, `debug` as argument to filter
the logged messages.
2. Removes the `--only-errors` flag.
3. Adds the `--ide-end-error-char CHAR`, which receives a character as
an argument, which is appended to the end of error messages. This is
handy to facilitate parsing of errors messages from the ide. This
functionality was previously embeded in the old `--only-errors` flag.
1. Adds the command `just format check`, which checks that all Haskell
files are formatted.
2. In CI, we use install ormolu from stackage and run it. This will
facilitate consistency between CI and local setups.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
* 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
};
```
Some tests require external dependencies, such as `rustc`, `wasmer`,
`run_cairo_vm.sh`, etc. If one does not have some of these available on
their computer, then the test suite will have a lot of failed tests with
the same fail message `X is not on $PATH`. This can be a bit ditracting
and it slows running the test suite.
I've introduced some preconditions that are checked before the actual
test suite so that if some of these commands are not on path then the
tests that need them are not run. Instead, you get a single failed test
(for each of the subtrees that failed the precondition).
- 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.
This PR updates the version of `cargo-risczero` in the CI. Ultimately,
we should figure out how to properly pin a fixed version, but apparently
that's not easy - it seems some dependencies need to be pinned and it's
not clear which ones, how, and to which versions. The problem is that to
execute the Rust code generated for RISC0 we need to compile it, and the
generated code depends on some RISC0-related libraries. Having the
correct version of the RISC0 Rust toolchain installed locally doesn't
fully solve the problem (doesn't seem to automatically select the right
versions of dependencies).
