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>
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
We can run `juvix format` on a whole juvix packages instead of
individual files.
This reduces the total time for `make check-format-juvix-files` from 10m
to 3m on my machine.
This PR:
* Modifies entry point `_entryPointBuildDir` to use the `BuildDir` type
instead of `SomeBase Dir`. This allows delayed resolution of the default
build directory which was useful for the Package -> Concrete translation
point below.
* Modifies `juvix dev root` to render the current package as a
Package.juvix file.
* Modifies the Package -> Concrete translation to recognise default
arguments. So, for example, an empty `juvix.yaml` file will be
translated into the following (instead of the `name`, `version`, and
`dependencies` arguments being populated).
module Package;
import Stdlib.Prelude open;
import PackageDescription.V1 open;
package : Package := defaultPackage;
* Adds a temporary command (removed when juvix.yaml support is removed)
`juvix dev migrate-juvix-yaml` that translates `juvix.yaml` into an
equivalent `Package.juvix` in the current project.
* Adds a temporary script `migrate-juvix-yaml.sh` (removed when
juvix.yaml support is removed) which can be run in the project to
translate all Juvix projects in the repository.
* Actually translate all of the `juvix.yaml` files to `Package.juvix`
using the script.
* Part of https://github.com/anoma/juvix/issues/2487
* 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.
The file walker `RecurseFilter` indictates if the the walker recurses
into
a directory which contains a Juvix project.
Previously the file walker would detect juvix.yaml. It now detects both
juvix.yaml and Package.juvix.
* Part of https://github.com/anoma/juvix/issues/2487
When moving to Package.juvix, the package configuration file cannot be
empty. So it's convenient to have a quick way to create a Package.juvix
file (previously you could run `touch juvix.yaml`.
This PR adds the `-n / --non-interactive` option to `juvix init`. This
will create a default `Package.juvix`, using the name of the current
directory to populate the package name.
Similarly for the interactive version of juvix init, if the name of the
current directory is not a valid Juvix module then a fallback name is
used instead.
For example:
```
$ mkdir /tmp/new-package
$ cd /tmp/new-package
$ juvix init -n
$ cat Package.juvix
module Package;
import PackageDescription.V1 open;
package : Package :=
defaultPackage
{name := "new-package";
version := mkVersion 0 0 0;
dependencies := [defaultStdlib]};
```
* Part of https://github.com/anoma/juvix/issues/2487
## Global package configuration
This PR updates the global-project to use `Package.juvix` instead of
`juvix.yaml`.
The global package gets the following `Package.juvix`:
```
module Package;
import PackageDescription.V1 open;
package : Package :=
defaultPackage
{name := "global-juvix-package";
version := mkVersion 0 0 0;
dependencies := [defaultStdlib]};
```
## juvix clean --global
This PR also adds an option `-g/--global` to `juvix clean` that removes
the `$XDG_CONFIG_HOME/juvix/VERSION` directory.
## Testing notes
If you've already run Juvix 0.5.3 you'll need to run `juvix clean -g`
before you'll use the new global project. This will not be an issue for
users of Juvix 0.5.4 (as this version of Juvix will never generate
juvix.yaml in the global project).
Part of:
* https://github.com/anoma/juvix/issues/2487
Paths are used as keys in the PathResolver ResolverCache. These paths
must be normalised because a path may have a different representation
when it is used to set an entry in the cache and when it is used to
lookup from the cache.
Path normalisation is also used in the REPL before a directory is
compared with the standard library path.
* Closes https://github.com/anoma/juvix/issues/2497