* Closes#3013
* Removes all remaining problems with evaluation duplication that could
potentially lead to an exponential blow-up in the running time.
* Adds the capacity to generate saves of temporary values in the Nock
code generation backend.
* Removes the `TempHeight` transformation on JuvixTree. It is no longer
needed.
* Removes the `ComputeCaseANF` transformation on JuvixCore from the
Anoma pipeline. It is no longer necessary.
Juvix coding style guidelines for the standard library and Anoma apps.
Compiled from discussions with @janmasrovira @paulcadman @heueristik
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
For example, by default the build directory would now be:
```
.juvix-build/0.6.6
```
It is necessary to separate the build files by compiler version because
the structure of jvo files may be incompatible between compiler
releases.
* Closes https://github.com/anoma/juvix/issues/3019
In the nockma parser (e.g used when running `juvix dev nockma run`), the
strings "nil", "functionsPlaceholder", and "stdlibPlaceholder" all parse
to Nockma nil.
We added `stdlibPlaceholder` in:
* https://github.com/anoma/juvix/pull/3005
but we forgot to add it to the parser.
This PR removes the `-j` (concurrent jobs) argument from the C runtime
make invocation.
`-j` cannot be used in the juvix_c make invocation because it causes an
error in the 'Build Linux static binary workflow'
```
cd runtime && make
make[1]: Entering directory '/__w/juvix/juvix/runtime'
cd c && make -j 4 -s
make[3]: *** No rule to make target '_build.wasm32-wasi/src/juvix/arch/wasi.o', needed by 'all'. Stop.
make[3]: *** No rule to make target '_build.wasm32-wasi-debug/src/juvix/arch/wasi.o', needed by 'all'. Stop.
make[2]: *** [Makefile:20: wasm32-wasi] Error 2
make[2]: *** Waiting for unfinished jobs....
make[2]: *** [Makefile:35: wasm32-wasi-debug] Error 2
_build.native64/src/juvix/opts.d:1: *** recipe commences before first target. Stop.
make[2]: *** [Makefile:26: native64] Error 2
_build.native64-debug/src/juvix/opts.d:1: *** recipe commences before first target. Stop.
make[2]: *** [Makefile:41: native64-debug] Error 2
make[1]: *** [Makefile:9: juvix_c] Error 2
make[1]: Leaving directory '/__w/juvix/juvix/runtime'
make: *** [Makefile:206: runtime] Error 2
```
We cannot build linux static binaries with GHC 9.10.1:
* https://github.com/anoma/juvix/issues/3037
This PR reverts the GHC update to unblock Juvix releases / nightly
releases. We can try the update again when stackage nightly updates to
GHC 9.10.1.
After
* https://github.com/anoma/juvix/pull/2973
let-folding stopped being linear in the size of the input program. All
transformations should be linear whenever possible. This PR makes
let-folding linear again.
This PR updates the cabal freeze file to reflect the changes to
dependencies after the GHC 9.10.1 stack.yaml update.
@janmasrovira can you check this? The last time I think you updated this
and the freeze file was much smaller for you.
I downloaded the stack2cabal binary from
https://github.com/hasufell/stack2cabal/releases/latest and ran
`stack2cabal` in the root of our repo.
* Fixes https://github.com/anoma/juvix/issues/3036
This PR updates the GHC version and the stack version in the linux
static binary GitHub workflow. This is used to make Juvix linux binary
releases.
NB: The linux binary releases of stack no longer have the `-static`
suffix in the tar filename.
Since GHC 9.8.2 has a bug which blocks our development (see
https://github.com/anoma/juvix/pull/2977#issuecomment-2325866056), I
made a PR to update to GHC 9.10.1. Because stackage doesn't yet support
GHC 9.10.1, I had to add some explicit dependencies and use
`allow-newer-deps` in `stack.yaml`.
I think we should merge this not to get blocked by the bug, and later
clean up `stack.yaml` when GHC 9.10.1 becomes supported on stackage.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Implements a transformation `compute-case-anf` which lifts out
non-immediate values matched on in case expressions by introducing
let-bindings for them. In essence, this is a partial ANF transformation
for case expressions only.
For example, transforms
```
case f x of { c y := y + x; d y := y }
```
to
```
let z := f x in case z of { c y := y + x; d y := y }
```
This transformation is needed to avoid duplication of values matched on
in case-expressions in the Nockma backend.
* Closes#2804
* Requires #3003
* Front-end syntax for side conditions was implemented in #2852. This PR
implements compilation of side conditions.
* Adds side-conditions to `Match` nodes in Core. Updates Core parsing,
printing and the evaluator.
* Only side-conditions without an `else` branch are allowed in Core. If
there is an `else` branch, the side conditions are translated in
`fromInternal` into nested ifs. Because with `else` the conditions are
exhaustive, there are no implications for pattern exhaustiveness
checking.
* Adjusts the "wildcard row" case in the pattern matching compilation
algorithm to take into account the side conditions.
Type checking messes up the locations by substituting the holes
(instance holes and ordinary holes) without adjusting the location of
the expression substituted into the hole. Instead, the location of the
expression substituted into the hole is preserved. This messes up
locations in type-checked Internal, because the substituted expressions
can come from anywhere. Later on, the error locations are wrong in Core,
and get wrongly displayed e.g. for pattern matching coverage errors.
This PR implements a partial solution for the (most common) case when
the substituted expression is an identifier. In the future, we should
have a general solution to preserve the hole locations.
* Closes#2962
* Depends on #2963
* In Isabelle/HOL comments cannot appear in internal syntax. All
comments inside a Juvix definition are moved outside: to before the
definition or before the earliest function clause.
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
We now use a sum type:
```
data IsInstanceCoercion
= IsInstanceCoercionInstance
| IsInstanceCoercionCoercion
```
instead of two mutually exclusive Bools.
Moreover, we properly print the keyword in the internal prettyprinter.
This PR:
* Adds a new implementation of {decode, encode}ByteString functions,
used by anomaEncode and anomaDecode in the Core evaluator
* Adds property tests for roundtripping and benchmarks for the new
functions.
The old implementation used
[bitvec](https://hackage.haskell.org/package/bitvec) to manipulate the
ByteString. This was far too slow. The new implementation uses bit
operations directly on the input integer and ByteArray.
It's now possible to run
[anoma-app-patterns:`Tests/Swap.juvix`](https://github.com/anoma/anoma-app-patterns/blob/feature/tests/Tests/Swap.juvix)
to completion.
For encoding, if the size of the output integer exceeds 64 bits (and
therefore a BigInt must be used) then the new implementation has
quadratic time complexity in the number of input bytes if an
implementation of `ByteString -> Integer` is used as follows:
```
byteStringToIntegerLE :: ByteString -> Integer
byteStringToIntegerLE = BS.foldr (\b acc -> acc `shiftL` 8 .|. fromIntegral b) 0
```
```
byteStringToInteger' :: ByteString -> Integer
byteStringToInteger' = BS.foldl' (\acc b -> acc `shiftL` 8 .|. fromIntegral b) 0
```
I think this is because `shiftL` is expensive for large Integers. To
mitigate this I'm splitting the input ByteString into 1024 byte chunks
and processing each separately. Using this we get 100x speed up at
~0.25Mb input over the non-chunked approach and linear time-complexity
thereafter.
## Benchmarks
The benchmarks for encoding and decoding 250000 bytes:
```
ByteString Encoding to/from integer
encode bytes to integer: OK
59.1 ms ± 5.3 ms
decode bytes from integer: OK
338 ms ± 16 ms
```
The previous implementation would never complete for this input.
Benchmarks for encoding and decoding 2 * 250000 bytes:
```
ByteString Encoding to/from integer
encode bytes to integer: OK
121 ms ± 8.3 ms
decode bytes from integer: OK
651 ms ± 27 ms
```
Benchmarks for encoding and decoding 4 * 250000 bytes:
```
ByteString Encoding to/from integer
encode bytes to integer: OK
249 ms ± 17 ms
decode bytes from integer: OK
1.317 s ± 16 ms
```
---------
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
- Closes#2797
Changes:
1. The global flag `--dev-show-thread-ids` is now properly being passed.
Before it was ignored.
3. The progress log has been refactored out of the `ParallelTemplate`
into the `Pipeline.Driver`. With the extra information available, I've
improved how we display the progress log:
1. We show `Compiling`, `Recompiling`, `Loading` to tell if the module
is compiled for the first time (the jvo is missing), or it needs to be
recompiled (with the reason displayed in parentheses), or is loaded from
a jvo file. In the latter case, the message is only showed with
`--log-level verbose|debug`.
2. The modules in other packages are displayed as dependencies with
their own progress counter.
2. When using `-N 1` and compiling a whole project we also get progress
log.
Example screencast:
https://github.com/user-attachments/assets/7cc43cd4-9b23-4ad5-a863-832abacc1b6c
* Closes#2894
* Closes#2895
* The translation of pattern matching on records is a bit tricky because
one cannot pattern match on records in Isabelle, except in top patterns
of function clauses. We thus need to translate into nested pattern
matching and record projections. Named patterns can be translated with a
similar technique and are also handled in this PR.
Checklist
---------
- [x] record creation
- [x] record projections
- [x] record update
- [x] top-level record patterns
- [x] nested record patterns
- [x] named patterns
- [x] remove redundant pattern matching clauses
- [x] remove redundant single-branch pattern matches
