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).
This pr explores the option to implement error handling in Juvix à la
mtl. It adds the following as a test:
1. `MonadError` trait.
2. `MonadTrans` trait.
3. `ExceptT` monad transformer and its `Functor`, `Monad`, `MonadTrans`,
`MonadError` instances.
This pr modifies the `HasExpressions` class to allow traversing direct
subexpressions rather than only leaf expressions. I've added the `lens`
library as a dependency to have access to generic traversals defined in
[Control.Lens.Plated](https://hackage.haskell.org/package/lens-5.3.2/docs/Control-Lens-Plated.html).
- Syntax for #2804.
- ⚠️ Depends on #2869.
This pr introduces:
1. front-end support (parsing, printing, typechecking) for boolean side
conditions for branches of case expressions.
2. Now `if` is a reserved keyword.
3. Multiway `if` is allowed to have only the `else` branch. I've also
refactored the parser to be simpler.
Example:
```
multiCaseBr : Nat :=
case 1 of
| zero
| if 0 < 0 := 3
| else := 4
| suc (suc n)
| if 0 < 0 := 3
| else := n
| suc n if 0 < 0 := 3;
```
The side if branches must satisfy the following.
1. There must be at least one `if` branch.
4. The `else` branch is optional. If present, it must be the last.
Future work:
1. Translate side if conditions to Core and extend the exhaustiveness
algorithm.
5. Add side if conditions to function clauses.
This PR updates the juvix-stdlib submodule ref to point to the current
main ref of the juvix-stdlib repository.
Previously it was pointing to the ref of a branch.
Currently formatting a project is equivalent to running `juvix format`
on each individual file. Hence, the performance is quadratic wrt the
number of modules in the project. This pr fixes that and we now we only
process each module once.
# Benchmark (1236% faster 🚀)
Checking the standard library
```
hyperfine --warmup 1 'juvix format --check' 'juvix-main format --check'
Benchmark 1: juvix format --check
Time (mean ± σ): 450.6 ms ± 33.7 ms [User: 707.2 ms, System: 178.7 ms]
Range (min … max): 396.0 ms … 497.0 ms 10 runs
Benchmark 2: juvix-main format --check
Time (mean ± σ): 6.019 s ± 0.267 s [User: 9.333 s, System: 1.512 s]
Range (min … max): 5.598 s … 6.524 s 10 runs
Summary
juvix format --check ran
13.36 ± 1.16 times faster than juvix-main format --check
```
# Other changes:
1. The `EntryPoint` field `entryPointModulePath` is now optional.
2. I've introduced a new type `TopModulePathKey` which is analogous to
`TopModulePath` but wihout location information. It is used in hashmap
keys where the location in the key is never used. This is useful as we
can now get a `TopModulePathKey` from a `Path Rel File`.
3. I've refactored the `_formatInput` field in `FormatOptions` so that
it doesn't need to be a special case anymore.
4. I've introduced a new effect `Forcing` that allows to individually
force fields of a record type with a convenient syntax.
5. I've refactored some of the constraints in scoping so that they only
require `Reader Package` instead of `Reader EntryPoint`.
6. I've introduced a new type family so that local modules are no longer
required to have `ModuleId` from their type. Before, they were assigned
one, but it was never used.
# Future work:
1. For project-wise formatting, the compilation is done in parallel, but
the formatting is still done sequentially. That should be improved.
* Closes#2394
* Removes the use of Uniplate in `letFunctionDefs` altogether, in favour
of handwritten traversal accumulating let definitions (implemented via
the new `HasLetDefs` typeclass).
Benchmark results
------------------
Using Uniplate:
```
heliax@imac bench % hyperfine --prepare 'juvix clean --global' -w 1 'juvix typecheck bench.juvix -N 1'
Benchmark 1: juvix typecheck bench.juvix -N 1
Time (mean ± σ): 1.399 s ± 0.023 s [User: 1.346 s, System: 0.041 s]
Range (min … max): 1.374 s … 1.452 s 10 runs
```
Using `HasLetDefs`:
```
heliax@imac bench % hyperfine --prepare 'juvix clean --global' -w 1 'juvix typecheck bench.juvix -N 1'
Benchmark 1: juvix typecheck bench.juvix -N 1
Time (mean ± σ): 1.098 s ± 0.015 s [User: 1.047 s, System: 0.040 s]
Range (min … max): 1.074 s … 1.120 s 10 runs
```
So it's roughly 1.1s vs. 1.4s, faster by 0.2s. About 14% improvement.
The benchmark file just imports the standard library:
```
module bench;
import Stdlib.Prelude open;
main : Nat := 0;
```
Both `juvix` binaries were compiled with optimizations, using `just
install`.
* Closes#2703
* Adds [peephole
optimization](https://en.wikipedia.org/wiki/Peephole_optimization) of
Cairo assembly.
* Adds a transformation framework for the CASM IR.
* Adds `--transforms`, `--run` and `--no-print` options to the `dev casm
read` command.
* Closes#2829
* Adds a transformation which converts `br` to `if` when the variable
branched on was assigned in the previous instruction. The transformation
itself doesn't check liveness and doesn't remove the assignment. Dead
code elimination should be run afterwards to remove the assignment.
* For Cairo, it only makes sense to convert `br` to `if` for equality
comparisons against zero. The assignment before `br` will always become
dead after converting `br` to `if`, because we convert to SSA before.
This PR adds support for the `anoma{encode, decode, sign, verify,
signDetached, verifyDetached}` functions to the Core evaluator.
## Encoding / Decoding
The serialization of values to `ByteString` for `anomaEncode` reuses the
Stored Core serialization. The Stored Core `Node` is extended to include
closures.
Anoma expects encoding of bytes as little-endian integers. In general
`ByteString -> Integer` is ambiguous because two `ByteString`s that
differ only by zero padding will map to the same integer. So we must
encode the length of the ByteString in the encoded integer alongside the
ByteString data so when it is decoded we can pad appropriately. We use
the same length encoding scheme that is used by Nockma jam.
## Verify
The Core evaluator implementation of `anomaVerify` crashes if the
verification fails. This matches the behaviour of Anoma node.
### `jvc` Support
You can now use `anoma-*` functions within `.jvc` core files.
* Closes https://github.com/anoma/juvix/issues/2808
- This PR adds a temporary compiler error for when the bug #2247
happens. We do not have plans to fix this bug until we move the
typechecker to Core, so it makes sense to add a better error message.
* Closes#2827
* Adds an optimization phase to the JuvixReg -> Casm pipeline, which
consists of repeated copy & constant propagation and dead code
elimination.
- Closes#2429
This pr introduces two enchancements to import statements:
1. They can have `using/hiding` list of symbols, with a behaviour
analogous to the open statement.
2. They can be public. When an import is marked as public, a local
module (or a series of nested local modules) is generated like this:
```
import A public;
-- equivalent to
import A;
module A;
open A public;
end;
```
It is easier to understand when there is an alias.
```
import A as X.Y public;
-- equivalent to
import A;
module X;
module Y;
open A public;
end;
end;
```
Public imports are allowed to be combined with `using/hiding` modifier
and open statements with the expected behaviour.
* Closes#2745
* Adds inlining of immediate values, i.e., values that don't require
computation or memory allocation.
* Non-immediate zero-argument functions / values should not be inlined,
because when not inlined they can be computed only once.
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.
