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).
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 fixes our positivity checker to support inductive definitions
with type families as type parameters. This kind of ind. type is
type-checked using the global flag `--new-type checker.`
For example, the following definition is not allowed:
```
module Evil;
type Evil (f : Type -> Type) :=
magic : f (Evil f) -> Evil f;
```
- Closes#2540
This pr applies a number of fixes to the new typechecker.
The fixes implemented are:
1. When guessing the arity of the body, we properly use the type
information of the variables in the patterns.
2. When generating wildcards, we name them properly so that they align
with the name in the type signature.
3. When compiling named applications, we inline all clauses of the form
`fun : _ := body`. This is a workaround to
https://github.com/anoma/juvix/issues/2247 and
https://github.com/anoma/juvix/issues/2517
4. I've had to ignore test027 (Church numerals). While the typechecker
passes and one can see that the types are correct, there is a lambda
where its clauses have different number of patterns. Our goal is to
support that in the near future
(https://github.com/anoma/juvix/issues/1706). This is the conflicting
lambda:
```
mutual num : Nat → Num
:= λ : Nat → Num {| (zero : Nat) := czero
| ((suc n : Nat)) {A} := csuc (num n) {A}}
```
5. I've added non-trivial a compilation test involving monad
transformers.
This is an attempt to fix a confusing situation where a user:
1. Builds the runtime with clang that does not support wasm32-wasi
2. Attempts to rebuild the runtime by passing the CC parameter pointing
to another installation of clang that does support wasm32-wasi.
In step 1. the runtime Makefile generates dependencies files which
contain the resolved value of `$(CC)`. When the user passes the correct
`CC` variable to the Makefile in step 2., the dependencies files are not
regenerated, the old value of `CC` is used in the build and the build
continues to fail.
In this PR we change the dependency file generation so that the
variables like `$(CC)` are written into the dependency file verbatim.
They are resolved when they are run in step 2. using the new value of
the CC parameter.
* Closes https://github.com/anoma/juvix/issues/2537
Adds a new version of the lock file that stores the hash (sha256 digest)
of the package file (Package.juvix, juvix.yaml) it was generated from as
a field:
```
# This file was autogenerated by Juvix version 0.5.4.
# Do not edit this file manually.
version: 2
checksum: d05940a4d3dc0e15451d02e1294819c875ba486ee54e26865ba8d190ac7c27c3
dependencies:
- git:
name: stdlib
ref: f68b0614ad695eaa13ead42f3466e0a78219f826
url: https://github.com/anoma/juvix-stdlib.git
dependencies: []
```
The lock file is regenerated when the hash of the package file doesn't
match the value of the `checksum` field, i.e when the user updates the
package file.
Existing lock files are automatically migrated to version 2.
* Closes https://github.com/anoma/juvix/issues/2464
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
## Overview
This PR makes the compiler pipeline thread-safe so that the test suite
can be run in parallel.
This is achieved by:
* Removing use of `{get, set, with}CurrentDir` functions.
* Adding locking around shared file resources like the the
global-project and internal build directory.
NB: **Locking is disabled for the main compiler target**, as it is
single threaded they are not required.
## Run test suite in parallel
To run the test suite in parallel you must add `--ta '+RTS -N -RTS'` to
your stack test arguments. For example:
```
stack test --fast --ta '+RTS -N -RTS'
```
The `-N` instructs the Haskell runtime to choose the number of threads
to use based on how many processors there are on your machine. You can
use `-Nn` to see the number of threads to `n`.
These flags are already [set in the
Makefile](e6dca22cfd/Makefile (L26))
when you or CI uses `stack test`.
## Locking
The Haskell package
[filelock](https://hackage.haskell.org/package/filelock) is used for
locking. File locks are used instead of MVars because Juvix code does
not control when new threads are created, they are created by the test
suite. This means that MVars created by Juvix code will have no effect,
because they are created independently on each test-suite thread.
Additionally the resources we're locking live on the filesystem and so
can be conveniently tagged by path.
### FileLock
The filelock library is wrapped in a FileLock effect:
e6dca22cfd/src/Juvix/Data/Effect/FileLock/Base.hs (L6-L8)
There is an [IO
interpreter](e6dca22cfd/src/Juvix/Data/Effect/FileLock/IO.hs (L8))
that uses filelock and an [no-op
interpreter](e6dca22cfd/src/Juvix/Data/Effect/FileLock/Permissive.hs (L7))
that just runs actions unconditionally.
### TaggedLock
To make the file locks simpler to use a TaggedLock effect is introduced:
e6dca22cfd/src/Juvix/Data/Effect/TaggedLock/Base.hs (L5-L11)
And convenience function:
e6dca22cfd/src/Juvix/Data/Effect/TaggedLock.hs (L28)
This allows an action to be locked, tagged by a directory that may or
may not exist. For example in the following code, an action is performed
on a directory `root` that may delete the directory before repopulating
the files. So the lockfile cannot be stored in the `root` itself.
e6dca22cfd/src/Juvix/Extra/Files.hs (L55-L60)
## Pipeline
As noted above, we only use locking in the test suite. The main app
target pipeline is single threaded and so locking is unnecessary. So the
interpretation of locks is parameterised so that locking can be disabled
e6dca22cfd/src/Juvix/Compiler/Pipeline/Run.hs (L64)
- Depends on #2481
This pr allows inductive type parameters to be any type. Until now, they
had to be exactly `Type`. This allows us to define more general traits
such as the `Monad` and `Functor`, as shown in the new test.
This is only supported under the temporary `--new-typechecker` flag.
Pending work:
Update the positivity checker if necessary (@jonaprieto).
Update the necessary compilation steps in Core (@lukaszcz).
Add compilation tests.
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
- Closes#2362
This pr implements a new typechecking algorithm. This algorithm can be
activated using the global flag `--new-typechecker`. This flag will only
take effect on the compilation pipeline but not the repl.
The main difference between the new and old algorithm is that the new
one inserts holes during typechecking. Thus, it does not require the
arity checker pass.
The new algorithm does not yet implement default arguments. The plan is
to make the change in the following steps:
1. Merge this pr.
2. Merge #2506.
3. Implement default arguments for the new algorithm.
4. Remove the arity checker and the old algorithm.
---------
Co-authored-by: Łukasz Czajka <62751+lukaszcz@users.noreply.github.com>
