This PR updates the stackage LTS resolver to `nightly-2024-02-06` which
uses GHC 9.8.1
## Upgrade notes
You will need to update your HLS to
[2.6.0.0](https://github.com/haskell/haskell-language-server/releases/tag/2.6.0.0),
this release contains support for GHC 9.8.1
## Fixes
### `haskeline` / `repline`
We have removed the custom haskeline / repline forks used in the build.
This is because we had trouble overriding haskeline as it is bundled
with GHC and the stackage resolver uses this bundled version. We were
using a custom fork of haskeline to implement
[mapInputT_](15c0685c91/app/Commands/Repl.hs (L409))
in the Juvix REPL, required to implement error handling. This requires
private API from the Haskeline library.
Instead of using a custom fork we use TemplateHaskell to obtain access
to the private API we need. See
[DarkArts.hs](15c0685c91/src/Juvix/Prelude/DarkArts.hs)
and
[HaskelineJB.hs](15c0685c91/app/HaskelineJH.hs).
To obtain access to the private API, we adapted a method from [a Tweag
blogpost](https://www.tweag.io/blog/2021-01-07-haskell-dark-arts-part-i/)
and [repo](https://github.com/tweag/th-jailbreak) - updating it for GHC
9.8.1.
### `aeson-better-errors`
The `aeson-better-errors` library has not been updated to work with
`mtl-2.3.0` so it cannot work with the new stackage resolver. We are
using a [fork](https://github.com/Vekhir/aeson-better-errors.git) which
has been updated.
We should consider replacing this library in future, see
https://github.com/anoma/juvix/issues/2621
### `path`
The `path` library now includes API `splitDrive` and `dropDrive` so we
can remove our versions of those functions from the prelude.
### `with-utf8`
We no longer need to depend on `with-utf8`. We were using this package
for UTF-8 versions of `readFile` and `writeFile` APIs. These APIs are
now available in the `text` package.
### Compiler warnings
GHC 9.8.1 introduces several new compiler warnings.
* We have suppressed `missing-role-annotations` and
`missing-poly-kind-signatures`
* We added our own versions of `head` and `tail` to work around the new
`partial-tx` warning introduced for those functions in `Data.List`.
* We fixed up the code to avoid the
[term-variable-capture](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html#ghc-flag--Wterm-variable-capture)
warning.
This PR replaces the JuvixAsm -> Nockma translation with a JuvixTree ->
Nockma translation.
We can now enable some of the JuvixTree tests that did not work with
JuvixAsm->Nockma because they were too slow.
## Notes
We have changed [test031: temp stack with
branching](22ee87f0e7/tests/Tree/positive/test031.jvt)
to avoid using negative numbers (because negative integers are not
supported in Nockma).
Three tree tests trace/output lists. Lists are serialised differently by
the asm and nockma pretty printers so they cannot share a single test
output file. We have created separate nockma output files for these
tests (see eg.
[test028.nockma.out](22ee87f0e7/tests/Tree/positive/out/test028.nockma.out)).
* Closes https://github.com/anoma/juvix/issues/2606
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
Quoting the [release notes of gnu
`grep-3.8`](https://lists.gnu.org/archive/html/info-gnu/2022-09/msg00001.html)
> The egrep and fgrep commands, which have been deprecated since
release 2.5.3 (2007), now warn that they are obsolescent and should
be replaced by grep -E and grep -F.
In order to fix the warning, I've replaced all instances of `egrep` with
`grep -E`
This PR adds a https://github.com/casey/just
```
$ just
Available recipes:
build *opts # Build the project. `build runtime` builds only the runtime.
clean *opts # Clean the project. `clean runtime` cleans only the runtime. `clean juvix-build` cleans only juvix-build dirs.
format *opts # Formats all Haskell files in the project. `format changed` formats only changed files. `format FILES` formats individual files.
install # Install juvix
test *filter # Run the tests in the project. Use the filter arg to set a Tasty pattern.
```
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* Adds negative tests for the JuvixTree evaluator
* Depends on #2600
* Depends on #2599
* Depends on #2598
* Depends on #2597
* Depends on #2596
* Depends on #2595
* Depends on #2594
* Depends on #2590
* Adds the `--transforms`, `--eval` and `--no-print` options to the
`juvix dev tree read` command.
* Depends on #2598
* Depends on #2597
* Depends on #2596
* Depends on #2595
* Depends on #2594
* Depends on #2590
This PR fixes an issue with importing `syntax alias` and using them from
another module:
Say you have a module defining a syntax alias:
```
module SyntaxAlias;
import Stdlib.Prelude open;
syntax alias MyNat := Nat;
```
and another which imports / uses it:
```
module test073;
import SyntaxAlias open;
main : MyNat := 11;
```
The compiler crashed with the following error:
```
^?!): empty Fold
CallStack (from HasCallStack):
error, called at src/Lens/Micro.hs:711:28 in microlens-0.4.13.1-ARwI8t2x86cAxRs56XPcG1:Lens.Micro
^?!, called at src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs:565:29 in juvix-0.5.5-G7jC6MbkbsJGkMT9u4BkYQ:Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping
```
We fix this by adding the aliases to the store's [scoper info
table](6649209d26/src/Juvix/Compiler/Store/Scoped/Data/InfoTable.hs (L14))
and then use it to initialise the scoper state when scoping a module.
Now we guarantee that whenever we write a file there is a newline
character at the end, which is a [Unix
convention](https://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap03.html#tag_03_205).
The juvix prelude now exports `writeFileEnsureLn` and it no longer
exports `writeFile`. If at some point we need the behaviour of
`writeFile` I'd suggest that we export it renamed as `writeFileVerbatim`
or something similar.
* Adds smoke tests for `juvix dev tree` CLI commands.
* Fixes a bug with printing JuvixAsm.
* Depends on #2597
* Depends on #2596
* Depends on #2595
* Depends on #2594
* Depends on #2590
* Adds the `FilterUnreachable` transformation in JuvixTree.
* Depends on #2596
* Depends on #2595
* Depends on #2594
* Depends on #2590
* Depends on #2589
* Depends on #2587
* Moves the "apply" transformation from JuivxAsm to JuvixTree. This
transformation removes the `CallClosures` nodes.
* Makes Nockma compilation tests use JuvixTree instead of JuvixAsm
files.
* Depends on #2594
* Depends on #2590
* Depends on #2589
* Depends on #2587
* Generalizes JuvixCore map and fold recursors to work also for
JuvixTree.
* Adds a transformation framework to JuvixTree.
* Adds identity trasformation tests for JuvixTree.
* Depends on #2590
* Depends on #2589
* Depends on #2587
This PR fixes the generation and evaluation of the Nock isCell op.
As we can see from its
[definition](https://developers.urbit.org/reference/nock/definition),
the isCell op (Nock 3) evaluates its argument:
```
*[a 3 b] ?*[a b]
```
Previously we were not evaluating the argument before checking if it is
an atom/cell.
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* Implements a translation from JuvixAsm to JuvixTree. It does not work
in general, but works for all code generated from Juvix and all JuvixAsm
tests.
* Adds the `juvix dev tree from-asm` command.
* Adds tests automatically converted from JuvixAsm tests.
* Depends on #2583
This PR changes the Nockma representation of builtin Bool and list-like
types to make them compatible with Anoma.
True and False are now compiled to the Nockma atoms 0 and 1
respectively.
For inductive types that have exactly two constructors, one of arity
zero and one of arity two, we compile the arity zero constructor to
Nockma zero, and the arity two constructor to a Nockma cell. In
particular a Juvix stdlib List will be compiled to an Anoma/Nockma list.
This is necessary for compatibility with the layout of resource and
resource logic types in Anoma.
In tests we avoid using the StackRef memory reference because it will be
removed as part of the JuvixTree work.
---------
Co-authored-by: Łukasz Czajka <62751+lukaszcz@users.noreply.github.com>
This PR implements:
* JuvixTree parser.
* JuvixTree pretty printer.
* `juvix dev tree read file.jvt` command which reads and pretty prints a
JuvixTree file.
* The `tree` target in the `compile` command.
* Removal of `StackRef` in JuvixAsm. This makes JuvixAsm more consistent
with JuvixTree and simplifies the data structures. `StackRef` is not
needed for compilation from Core.
Tests for the parser will appear in a separate PR, when I implement an
automatic translation of JuvixAsm to JuvixTree files.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
We can represent Anoma types like
[resource](e18e50e3c3/hoon/resource-machine.hoon (L7))
as Juvix records.
The Nockma encoding of types uses Nockma 'tuples' where each component
of the tuple holds a value of a field. So for Juvix->Anoma integration
it is convenient to compile values of record types as Nockma tuples.
We already have the concept of representing constructors of inductive
types that have only one non-zero-field constructor in the compiler, see
[`MemRepTuple`](1147e1fce1/src/Juvix/Compiler/Tree/Language/Rep.hs (L13)).
In this PR, as part of the Nockma step, we mark constructors that
satisfy the requirements of the `MemRepTuple` translation as such. Then
we use a tuple encoding for those constructors.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Adds annotations to cells to indicate that it is a call to the stdlib
and might be evaluated faster in the Haskell evaluator.
The syntax for stdlib calls is as follows:
```
[stdlib@add args@<args-term> <left-term> <right-term>]
```
where `add` is the name of the function being called, `<args-term>` is a
nockma term that points to the position of the arguments, and
`<left-term>` and `<right-term>` are the actual components of the cell.
This PR:
* introduces the JuvixTree language which is like JuvixAsm except that
instead of the value stack there is an applicative structure,
* refactors the JuvixCore -> JuvixAsm translation into JuvixCore ->
JuvixTree -> JuvixAsm.
JuvixAsm is a bit too low level for efficient compilation to Nock.
Translating the value stack explicitly is a bad idea and it's
unnecessary, because the value stack just represents an applicative
structure which can be represented directly in Nock. It's possible, but
cumbersome and unnecessary, to recover the applicative structure from
JuvixAsm code. It's better to have a bit more high-level JuvixTree
language which still retains the explicit applicative structure.
After this change there are only two types of variables in JuvixReg:
arguments and local variables. The previous distinction between stack
and temporary variables was spurious and complicated things
unnecessarily.
This PR is a snapshot of the current work on the JuvixAsm -> Nockma
translation. The compilation of Juvix programs to Nockma now works so we
decided to raise this PR now to avoid it getting too large.
## Juvix -> Nockma compilation
You can compile a frontend Juvix file to Nockma as follows:
example.juvix
```
module example;
import Stdlib.Prelude open;
fib : Nat → Nat → Nat → Nat
| zero x1 _ := x1
| (suc n) x1 x2 := fib n x2 (x1 + x2);
fibonacci (n : Nat) : Nat := fib n 0 1;
sumList (xs : List Nat) : Nat :=
for (acc := 0) (x in xs)
acc + x;
main : Nat := fibonacci 9 + sumList [1; 2; 3; 4];
```
```
$ juvix compile -t nockma example.juvix
```
This will generate a file `example.nockma` which can be run using the
nockma evaluator:
```
$ juvix dev nockma eval example.nockma
```
Alternatively you can compile JuvixAsm to Nockma:
```
$ juvix dev asm compile -t nockma example.jva
```
## Tests
We compile an evaluate the JuvixAsm tests in
cb3659e08e/test/Nockma/Compile/Asm/Positive.hs
We currently skip some because either:
1. They are too slow to run in the current evaluator (due to arithmetic
operations using the unjetted nock code from the anoma nock stdlib).
2. They trace data types like lists and booleans which are represented
differently by the asm interpreter and the nock interpreter
3. They operate on raw negative numbers, nock only supports raw natural
numbers
## Next steps
On top of this PR we will work on improving the evaluator so that we can
enable the slow compilation tests.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
This PR contains refactors split out from the Nockma compile PR
https://github.com/anoma/juvix/pull/2570. Each refactor is associated
with a separate commit in this PR.
* Closes#2561
* Defines an extended subset of Cairo Assembly, following Section 5 of
[1].
* Adds the commands `juvix dev casm read file.casm` and `juvix dev casm
run file.casm` to print and run `*.casm` files.
* The tests cover CASM semantics. Some are "manual translations" of
corresponding JuvixAsm tests according to the JuvixAsm -> CASM
compilation concept.
This PR adds an parser, pretty printer, evaluator, repl and quasi-quoter
for Nock terms.
## Parser / Pretty Printer
The parser and pretty printer handle both standard Nock terms and
'pretty' Nock terms (where op codes and paths can be named). Standard
and pretty Nock forms can be mixed in the same term.
For example instead of `[0 2]` you can write `[@ L]`.
See
a6028b0d92/src/Juvix/Compiler/Nockma/Language.hs (L79)
for the correspondence between pretty Nock and Nock operators.
In pretty Nock, paths are represented as strings of `L` (for head) and
`R` (for tail) instead of the number encoding in standard nock. The
character `S` is used to refer to the whole subject, i.e it is sugar for
`1` in standard Nock.
See
a6028b0d92/src/Juvix/Compiler/Nockma/Language.hs (L177)
for the correspondence between pretty Nock path and standard Nock
position.
## Quasi-quoter
A quasi-quoter is added so Nock terms can be included in the source, e.g
`[nock| [@ LL] |]`.
## REPL
Launch the repl with `juvix dev nockma repl`.
A Nock `[subject formula]` cell is input as `subject / formula` , e.g:
```
nockma> [1 0] / [@ L]
1
```
The subject can be set using `:set-stack`.
```
nockma> :set-stack [1 0]
nockma> [@ L]
1
```
The subject can be viewed using `:get-stack`.
```
nockma> :set-stack [1 0]
nockma> :get-stack
[1 0]
```
You can assign a Nock term to a variable and use it in another
expression:
```
nockma> r := [@ L]
nockma> [1 0] / r
1
```
A list of assignments can be read from a file:
```
$ cat stack.nock
r := [@ L]
$ juvix dev nockma repl
nockma> :load stack.nock
nockma> [1 0] / r
1
```
* Closes https://github.com/anoma/juvix/issues/2557
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
This makes the syntax more uniform. It was especially confusing with
nested branching, where some closing braces had to and others couldn't
be followed by a semicolon. Now all have to be followed by a semicolon
(except function ending braces).
* Closes#2392
Changes checklist
-----------------
* [X] Abstract out data types for stored module representation
(`ModuleInfo` in `Juvix.Compiler.Store.Language`)
* [X] Adapt the parser to operate per-module
* [X] Adapt the scoper to operate per-module
* [X] Adapt the arity checker to operate per-module
* [X] Adapt the type checker to operate per-module
* [x] Adapt Core transformations to operate per-module
* [X] Adapt the pipeline functions in `Juvix.Compiler.Pipeline`
* [X] Add `Juvix.Compiler.Pipeline.Driver` which drives the per-module
compilation process
* [x] Implement module saving / loading in `Pipeline.Driver`
* [x] Detect cyclic module dependencies in `Pipeline.Driver`
* [x] Cache visited modules in memory in `Pipeline.Driver` to avoid
excessive disk operations and repeated hash re-computations
* [x] Recompile a module if one of its dependencies needs recompilation
and contains functions that are always inlined.
* [x] Fix identifier dependencies for mutual block creation in
`Internal.fromConcrete`
- Fixed by making textually later definitions depend on earlier ones.
- Now instances are used for resolution only after the textual point of
their definition.
- Similarly, type synonyms will be unfolded only after the textual point
of their definition.
* [x] Fix CLI
* [x] Fix REPL
* [x] Fix highlighting
* [x] Fix HTML generation
* [x] Adapt test suite
* Replaces the `pusht` and `popt` instructions with block-based `save`
and `tsave`. This encodes the structure of temporary stack manipulation
syntactically, making it impossible to manipulate it in unexpected ways.
Also simplifies compilation to Nock.
* Adds optional names for temporaries and function arguments.
- Closes#2549
The implementation of wildcard constructors was previously done in the
arity checker. I did not realise I was missing it because there was not
tests for it that included typechecking (we were only checking
formatting).
This patch dramatically increases the efficiency of `juvix dev root`,
which was unnecessarily parsing all dependencies included in the
`Package.juvix` file. Other commands that do not require the `Package`
will also be faster.
It also refactors some functions so that the `TaggedLock` effect is run
globally.
I've added `singletons-base` as a dependency so we can have `++` on the
type level. We've tried to define a type family ourselves but inference
was not working properly.
This PR updates the juvix-stdlib submodule ref to the current
juvix-stdlib/main.
NB: The Markdown test is not stable after changes to the stdlib - the
ids (deriving from internal name ids?) will change and so the expected
file must be regenerated.
This pr adds support for default values that depend on previous
arguments. For instance, see
[test071](ca7d0fa06d/tests/Compilation/positive/test071.juvix).
- After #2540 is implemented, we'll be able to remove the old type
checker (including the aritychecker).
