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
Example file:
```
module error;
import empty; -- error only happens if we have at least one import
type T := t;
x : T := t t; -- type error
```
If one loads this file into emacs (or vscode) they'll get a type error
as expected, but name colors and go-to information is lost, which is
annoying. This pr fixes this.
I'm not sure why, but this bug only occurs when there is at least one
import.
This pr has two relevant changes:
## Errors instead of crases
When registering a builtin, we perform some sanity checks. When
unsuccessful, the compiler crashes. This seldom happens because builtins
are defined in libraries that we write ourselves. However, any compiler
crash is a bug, so this pr refactors these crashes into proper errors.
## Registering builtins during scoping
Before this pr, builtins are registered and sanity checked during the
translation from Concrete to Internal. This imposes that the order in
which we translate stuff is relevant, as we must register a builtin
before we use it. For the most part this is fine when the dependency is
explicit in the code, but sometimes there are explicit dependencies.
E.g. do notation and the builtin `monad-bind`. In order to avoid adding
special rules, it is easier to just register builtins during scoping, so
I've refactored the code to do this.
I've also removed the `Builtins` effect and moved its methods to the
`InfoTableBuilder` since the builtins table is now part of the Scoped
InfoTable. Consequently, I've removed the the field `_artifactBuiltins`.
## Future work
- Fix#2952. I didn't find a good way to fix this problem in this pr, so
it is left for a separate pr.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
The `anoma-bytearray-{to, from}-anoma-contents` are intended to be used
to convert to/from atoms representing `ByteArrays`. These builtins are
required temporarily until Anoma Node makes ByteArray representation
uniform across all of its APIs.
We represent ByteArrays in nock as a cell:
```
[size contents]
```
Where `size` is the size of the ByteArray and `contents` is an Atom
representing the bytes in LSB ordering.
The `size` is required in general because the encoding of ByteArrays to
Atoms is ambiguous. For example the ByteArrays [0x01; 0x00] and [0x01]
are represented by `1`.
Some Anoma ByteArrays like keys and signatures are represented using on
the `contents` atom because the size is constant.
Users of Anoma APIs have to strip / add size information from ByteArrays
depending on where the data is used. The new builtins provide this
facility.
These builtins are temporary because it's been agreed with Anoma
engineering team to change the Anoma APIs to make the ByteArray
representation uniform, i.e always represent ByteArrays using `[size
content]`. When this is implemented in Anoma Node we can remove these
builtins.
```
builtin anoma-bytearray-to-anoma-contents
axiom toAnomaContents : ByteArray -> Nat;
builtin anoma-bytearray-from-anoma-contents
axiom fromAnomaContents :
-- | The size of the ByteArray
Nat
-- | The contents of the ByteArray
-> Nat
-- | The resulting ByteArray
-> ByteArray;
```
This PR updates:
- [x] Package version
- [x] Smoke test
- [x] Changelog
We can't merge this until the stdlib submodule pointer is fixed-up to
point to stdlib main.
* Specialization has become less effective after recent changes to the
codebase. This PR fixes issues with specialization.
* Closes#2939
* Closes#2945
Checklist
---------
- [X] Preserve pragmas for letrec and lambda in Stored Core
- [x] Remove the assumption that all type variables are at the front
(closes#2945)
- [x] Allow specialization when the argument is a constructor
application
- [x] Make renaming adjust pragmas
- [x] Allow pragmas for fields in record definitions (closes#2939)
- [x] Update standard library pragmas
- [x] Fix JuvixTree printing
This PR adds support for ByteArray in the Anoma cryptographic functions.
```
builtin anoma-sign
axiom anomaSign : {A : Type} -> A -> ByteArray -> ByteArray;
builtin anoma-verify-with-message
axiom anomaVerifyWithMessage : {A : Type} -> ByteArray -> ByteArray -> Maybe A;
builtin anoma-sign-detached
axiom anomaSignDetached : {A : Type} -> A -> ByteArray -> ByteArray;
builtin anoma-verify-detached
axiom anomaVerifyDetached : {A : Type} -> ByteArray -> A -> ByteArray -> Bool;
```
The Anoma / Hoon Stdlib function `length` needs to be exposed as a
StdlibFunction because a ByteArray stores its length and the value
returned by `anomaSign` is not a fixed length.
This PR adds support for a builtin `ByteArray` type and associated
functions for constructing a `ByteArray` from a list of bytes and a
function to query the size of the `ByteArray`. It is only available in
the Anoma backend.
In Core / Tree, ByteArray constant is stored using a Haskell ByteString.
In Anoma the ByteArray is stored as a cell where the head is the length
of the ByteArray and the tail is an integer is an integer formed by
concatenating the bytes in the array using little-endian byte ordering.
The Nock for constructing a `ByteArray` uses the `length`, `add`,
`folder` and `lsh` functions from the Anoma hoon stdlib. See the [code
comment](fa068a30e7/src/Juvix/Compiler/Nockma/StdlibFunction.hs (L37))
for more details.
Example:
```
module test082;
import Stdlib.Prelude open;
import Stdlib.Debug.Trace open;
builtin bytearray
axiom ByteArray : Type;
builtin bytearray-from-list-byte
axiom mkByteArray : List Byte -> ByteArray;
builtin bytearray-size
axiom size : ByteArray -> Nat;
bs0 : ByteArray := mkByteArray [];
bs1 : ByteArray := mkByteArray [0x0; 0x0; 0x0];
bs2 : ByteArray := mkByteArray [0x1; 0x0; 0x0; 0x0];
bs3 : ByteArray := mkByteArray [0x2; 0x1];
bs4 : ByteArray := mkByteArray [0x100];
main : ByteArray :=
trace (size bs0)
>-> trace bs0
>-> trace (size bs1)
>-> trace bs1
>-> trace (size bs2)
>-> trace bs2
>-> trace (size bs3)
>-> trace bs3
>-> trace (size bs4)
>-> bs4;
```
Output using `tests/Anoma/Compilation/positive/test082.juvix`
```
$ juvix compile anoma -g test082.juvix
$ juvix dev nockma run test082.pretty.nockma
0
[0 0]
3
[3 0]
4
[4 1]
2
[2 258]
1
[1 0]
```
This pr adds the `--statements` flag to `juvix dev latex export`. It can
be used like this:
```
juvix dev latex export --statements "List; elem; find" List.juvix
```
All statements are selectable by their 'label'. The label of a statement
is defined as:
1. The function/type/operator/alias/axiom/local_module/fixity/iterator
name being defined.
2. The module name being imported.
## Limitations:
1. Only top statements are allowed. I.e. statements inside local modules
cannot be selected.
1. Open statements are not selectable. Giving `--statements "My.Module"`
will refer to the import statement `import My.Module`.
4. Single constructors are not selectable. Only the whole type
definition.
5. No comments will be printed.
