- ⚠️ Depends on #2644
The `effectful` library does not support the `Embed` effect out of the
box. However, it offers `IOE`, which is equivalent to `Embed IO` from
polysemy. In preparation to a possible migration to `effectful`, this pr
hides the general `Embed` effect from the prelude and it exports a
specialized `EmbedIO` in its place.
This pr addresses a number of problems.
1. It fixes a bug where paths were annotated as operations rather than
paths in the parser.
2. It fixes a bug that happened when unfolding cells in the pretty
printer in order to minimize delimiters. It caused the stdlibcall hints
to be ignored for the unfolded arguments.
3. In order to properly test this, we can't ignore the hints for the Eq
instance, so I've changed that.
4. I've introduced the class NockmaEq for nockma semantic equality. This
is used in the evaluator as well as in the semantic tests.
5. I've added a bigger test. I found these bugs while working with this
file.
* Closes#2578
* Implements JuvixReg parser and pretty printer.
* Adds the `juvix dev reg read file.jvr` command.
* Adds the `reg` target to the `compile` commands.
* Adds tests for the JuvixReg parser.
This PR introduces the `pow2` function from the Anoma/Nock stdlib,
replacing the 'Builtin function' version we wrote in the Tree->Nockma
translation. This will be more efficient because it will be jetted in
Anoma.
## New Anoma/nockma stdlib locations
The Nock stdlib now has multiple layers. We now use a Nock term to
to fetch each stdlib symbol's code because this can be obtained from
Urbit's dojo,
for example:
> => anoma !=(add)
[9 20 0 15]
where `anoma` is the symbol where the anoma stdlib is loaded.
The stdlib is the Nock code associated with
6a4e15fe9c/hoon/anoma.hoon
## Tests
This commit also adds unit tests for the stdlib / appendRights
functions. The tests use the evaluator with 'interceptStdlibCalls' both
enabled and disabled.
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>
* 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
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 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.
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>
* 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
- 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.
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
## 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>
This PR adds an initial support for Literate Juvix Markdown files, files
with the extension `.juvix.md`.
Here is a small example of such a file: `Test.juvix.md`.
<pre>
# This is a heading
Lorem ...
```juvix
module Test;
type A := a;
fun : A -> A
| _ := a;
```
Other text
</pre>
This initial support enables users to execute common commands such as
typechecking, compilation, and HTML generation. Additionally, a new
command called `markdown` has been introduced. This command replaces
code blocks marked with the juvix attribute with their respective HTML
output, much like the output we obtain when running `juvix html`. In
this version, comments are ignored in the output, including judoc
blocks.
- We intend to use this new feature in combination with this Python
plugin (https://github.com/anoma/juvix-mkdocs) to enhance our
documentation site.
https://github.com/anoma/juvix/assets/1428088/a0c17f36-3d76-42cc-a571-91f885866874
## Future work
Open as issues once this PR is merged, we can work on the following:
- Support imports of Juvix Markdown modules (update the path resolver to
support imports of Literate Markdown files)
- Support (Judoc) comments in md Juvix blocks
- Support Markdown in Judoc blocks
- Update Text editor support, vscode extension and emacs mode (the
highlighting info is a few characters off in the current state)
- Closes#1839
- Closes#1719
* Closes#2365
* Implements the syntax `f@{x1 := def1; ...; xn := defn}` and `f@?{x1 :=
def1; ..; xn := defn}`. Each definition inside the `@{..}` is an
ordinary function definition. The `@?` version allows partial
application (not all explicit named arguments need to be provided). This
subsumes the old record creation syntax.
