* Closes#2990
* Allows type signatures for constructors, record fields and axioms to
have the same form as in function definitions, e.g.,
```
field {A} {{M A}} (arg1 arg2 : A) : List A
```
* For constructors, this introduces an ambiguity between record and GADT
syntax with names. For example,
```
ctr {
A : Type
}
```
can be confused by the parser with initial part of GADT type signature:
```
ctr {A : Type} : A -> C A
```
For now, this is resolved by preferring the record syntax. Hence, it's
currently not possible to use type signatures with implicit arguments
for constructors. Ultimately, the `@` in record syntax should be made
mandatory, which would resolve the ambiguity:
```
ctr@{
A : Type
}
```
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
This PR:
1. Adds a new interpretation for the Anoma effect, which makes gRPC
calls to an existing Anoma client instead of spawning a new one.
2. Adds a new `nockma run` mode, `with-client`, which can be used to run
an Anoma program against a running Anoma client, using its URL and gRPC
port.
3. separates the `nockma run` command into subcommands.
CLI docs:
## `nockma run`
```
Usage: juvix dev nockma run COMMAND
Subcommands used to run an Anoma program. Use with artefacts obtained from
compilation with the anoma target
Available options:
-h,--help Show this help text
Available commands:
builtin-evaluator Run with the builtin Nockma evaluator
ephemeral-client Run with an ephemeral Anoma client
with-client Run with a running Anoma client
```
### `with-client`
```
Usage: juvix dev nockma run with-client
NOCKMA_FILE [--args ARGS_FILE] (-p|--grpc-port PORT) [--url URL]
Run with a running Anoma client
Available options:
NOCKMA_FILE Path to a .nockma file
--args ARGS_FILE Path to file containing args. The args file should
contain a list (i.e. to pass 2 and [1 4] as args, the
contents should be [2 [1 4] 0]).
-p,--grpc-port PORT The GRPC port of a running Anoma client
--url URL The URL of a running Anoma client. default: localhost
-h,--help Show this help text
```
### `ephemeral-client`
```
Usage: juvix dev nockma run ephemeral-client
NOCKMA_FILE [--args ARGS_FILE] --anoma-dir ANOMA_DIR
Run with an ephemeral Anoma client
Available options:
NOCKMA_FILE Path to a .nockma file
--args ARGS_FILE Path to file containing args. The args file should
contain a list (i.e. to pass 2 and [1 4] as args, the
contents should be [2 [1 4] 0]).
--anoma-dir ANOMA_DIR Path to anoma repository
-h,--help Show this help text
```
### `builtin-evaluator`
```
Usage: juvix dev nockma run builtin-evaluator
NOCKMA_FILE [--args ARGS_FILE] [--profile]
Run with the builtin Nockma evaluator
Available options:
NOCKMA_FILE Path to a .nockma file
--args ARGS_FILE Path to file containing args. The args file should
contain a list (i.e. to pass 2 and [1 4] as args, the
contents should be [2 [1 4] 0]).
--profile Report evaluator profiling statistics
-h,--help Show this help text
```
* Closes#3147
When we call a function that is currently being defined (there may be
several such due to nested local definitions), we add a reflexive edge
in the call map instead of adding an edge from the most nested
definition. For example, for
```juvix
go {A B} (f : A -> B) : List A -> List B
| nil := nil
| (elem :: next) :=
let var1 := f elem;
var2 := go f next;
in var1 :: var2;
```
we add an edge from `go` to the recursive call `go f next`, instead of
adding an edge from `var2` to `go f next` as before.
This makes the above type-check.
The following still doesn't type-check, because `next'` is not a
subpattern of the clause pattern of `go`. But this is a less pressing
problem.
```juvix
go {A B} (f : A -> B) : List A -> List B
| nil := nil
| (elem :: next) :=
let var1 := f elem;
var2 (next' : List A) : List B := go f next';
in myCons var1 (var2 next);
```
This PR:
1. Fixes the compilation of the sha256 builtin anoma lib call
A sha256 hash is 32 bytes long, not 64 bytes. This number is used when
constructing the ByteArray representation (i.e `[length payload]` cell)
of the output of Anoma stdlib sha256 call. The Anoma stdlib sha256 call
just returns the atom payload.
2. Fixes the evaluation of the sha256 stdlib call
Previously we were converting the sha256 hash bytestring to Base16
format. This is convenient when displaying the ByteString hash. However
the Anoma nock interpreter outputs the raw bytes so we must change the
builtin evaluator to match this behaviour.
After these fixes we can re-enable the test084 anoma compilation test.
- Fixes#3030
The `ComputeTypeInfo` transformation was incorrectly assuming that the
type of the body couldn't refer to the let item. When inferring the type
of a let, we now inline the let item(s) into the type of the body.
```
NLet Let {..} ->
let bodyTy = Info.getNodeType _letBody
in subst (_letItem ^. letItemValue) bodyTy
```
The purpose of this release is to add support for the `--vscode` flag,
required by an update to the juvix vscode extension.
* https://github.com/anoma/juvix/pull/3162
* https://github.com/anoma/vscode-juvix/pull/153
This PR updates:
- [x] Package version
- [x] Smoke test
The CHANGELOG generator we use:
https://github.com/github-changelog-generator/github-changelog-generator
has stopped working with errors like the following:
```
Warning: PR 3148 merge commit was not found in the release branch or tagged git history and no rebased SHA comment was found
```
So we'll defer populating the CHANGELOG summary until after the release.
This PR updates:
- [x] Package version
- [x] Smoke test
The CHANGELOG generator we use:
https://github.com/github-changelog-generator/github-changelog-generator
has stopped working with errors like the following:
```
Warning: PR 3148 merge commit was not found in the release branch or tagged git history and no rebased SHA comment was found
```
So we'll defer populating the CHANGELOG summary until after the release
* Closes#2968
* Implements detection of function-like definitions, which either:
- have some arguments on the left of `:`, or
- have at least one clause.
* Only function-like definitions are recursive.
* Non-recursive definitions are not mutually recursive either, and can
be used only after their definition. This necessitates rearranging some
definitions in existing Juvix code.
* Changes the scoping of identifiers in record updates. Now field names
on the right side don't refer to the old values of the record fields but
to identifiers in scope defined outside the record update. To refer to
old values, one needs to explicitly use record projections, e.g.
```
r@Rec{x := Rec.x r}
```
This PR adds frontend support for the Anoma Random API:
The frontend builtin APIs are:
```
builtin anoma-random-generator
axiom RandomGenerator : Type;
builtin anoma-random-generator-init
axiom randomGeneratorInit : Nat -> RandomGenerator;
builtin anoma-random-generator-split
axiom randomGeneratorSplit : RandomGenerator
-> Pair RandomGenerator RandomGenerator;
builtin anoma-random-next-bytes
axiom randomNextBytes : Nat
-> RandomGenerator
-> Pair ByteArray RandomGenerator;
```
### Nockma Evaluator
The Nockma evaluator intercepts the corresponding Anoma random stdlib
calls using the
[System.Random](https://hackage.haskell.org/package/random-1.2.1.2/docs/System-Random.html)
API. The implementation uses the
[splitmix](https://hackage.haskell.org/package/splitmix-0.1.0.5/docs/System-Random-SplitMix.html)
generator directly because it has an API to destructure the generator
into a pair of integers. We can use this to serialise the generator.
* Closes https://github.com/anoma/juvix/issues/2902
* Closes#3039
* Closes#3043
* Closes#2970
* Closes#3089
* Parser allows trailing semicolons for any kind of semicolon-separated
items:
- let-block statements,
- module statements,
- record declaration statements,
- record update fields,
- record pattern fields,
- named application arguments,
- list literal items,
- list pattern items,
- open statement using/hiding items,
- `syntax iterator` declaration parameters,
- `syntax fixity` declaration parameters.
* Formatter prints trailing semicolons if the items are displayed on
separate lines, removes them if on a single line.
* The formatting of multiline lists is changed to make it consistent
with other semicolon-separated blocks:
```
[
1;
2;
3;
]
```
instead of
```
[ 1
; 2
; 3
]
```
# Changes
1. Adds a new command `juvix dev anoma node`. This command runs the
anoma node.
2. Adds a flag `--anoma-dir` to `juvix dev nockma run`. When given, it
must point to the anoma clone. Then, it will run the nockma code in the
anoma node and report the result (with no traces).
# Prerequisites
1. An anoma clone at some specific commit.
```
git clone git@github.com:anoma/anoma.git
cd anoma
git checkout 98e3660b91cd55f1d9424dcff9420425ae98f5f8
# build anoma
mix deps.get
mix escript.install hex protobuf
mix compile
# build the client
mix do --app anoma_client escript.build
```
2. The `mix` command (elixir).
3. The [`grpcurl`](https://github.com/fullstorydev/grpcurl) command. To
install a single binary in `~/.local/bin` you can run:
```
curl -sSL
"https://github.com/fullstorydev/grpcurl/releases/download/v1.9.1/grpcurl_1.9.1_linux_x86_64.tar.gz"
| tar -xz -C ~/.local/bin --no-wildcards grpcurl
```
# Testing
I've not included any test. It can be tested locally like this:
```
cd juvix/tests/Anoma/Compilation/positive
juvix compile anoma test001.juvix
echo 20 > args.debug.nockma
juvix dev nockma run --anoma-dir ~/projects/anoma test001.nockma --args args.debug.nockma
* Closes#3091
* Formatter adds braces when the body is not enclosed in braces or
parentheses. Braces-enclosed body is always printed as a block on a new
line:
```
for (acc := 0) (x in lst) {
x + acc
}
```
* If the body is enclosed in ordinary parentheses, then they are
preserved and the iterator is printed on a single line, if possible:
```
for (acc := 0) (x in lst) (x + acc)
```
This is sometimes useful when you want iterator application as an
argument to something.
* Updates the standard library to
https://github.com/anoma/juvix-stdlib/pull/130
* Also changes `null` to `isEmpty`, which required updating some tests
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
The Anoma API accepts jammed nock terms as input. The benefit to this is
that jammed terms are greatly compressed compared to the original term.
* Closes https://github.com/anoma/juvix/issues/3017
Remaining tasks:
- [x] Deserialize input nockma file in `juvix dev nockma {run, eval}`
- [x] Support debug input nockma file in `juvix dev nockma {run, eval,
repl}` i.e there should be a way to pass the `*.debug.nockma` (output of
`juvix compile anoma --debug`) file to `juvix dev nockma {run, eval,
repl}`
- [x] Add proper JuvixErrors for deserialisation failures
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
This PR adds frontend builtin support for the Anoma Resource machine
functions provided in
[resource-machine.hoon](4897751366/hoon/resource-machine.hoon),
*except* for the `prove-logic` function which still needs some
discussion.
Users must now mark the Anoma `Resource` type with
`builtin-anoma-resource` and the Anoma `Action` type with
`builtin-anoma-action`. This is required because the resource machine
functions use these types.
The compiler does not check that the constructors of `Resource` and
`Action` match the RM spec. I made this decision because the Anoma types
are sill in flux and it's easier to change if correctness is delegated
to the RM library for now. We can add the constructor checks when the
Anoma RM interface is stable.
The test file
[test085.juvix](47ba3e2746/tests/Anoma/Compilation/positive/test085.juvix)
demonstrates how each builtin should be used.
### Core Evaluator
The Core evaluator does not support these builtin functions in normal
mode. When used for normalisation (e.g when used in the constant folding
pass) the Core evaluator leaves the builtin functions unchanged.
### Nock Evaluator
The Nock evaluator does not intercept the Anoma lib functions that the
builtins correspond to in the Nock backend. It executes the underlying
Nock code instead. This means that several of the functions cannot be
tested because they're either too slow (e.g commitment) or do not have
an implementation in the Nock code (e.g addDelta).
* Closes: https://github.com/anoma/juvix/issues/3084
This PR adds frontend support for Anoma stdlib sha256 function (aka
`shax` in Nock).
* Closes https://github.com/anoma/juvix/issues/2901
The new builtin can be declared as follows:
```
builtin anoma-sha256
axiom anomaSha256 : Nat -> ByteArray;
```
The intention is that it wraps a call to anomaEncode as follows:
```
sha256 {A} (a : A) : ByteArray := anomaSha256 (anomaEncode a);
```
### Fix for atom to ByteString
This PR also includes a commit
6205dc9ff9
to fix an issue with functions like `integerToByteArray` when called
with negative integers (the solution is to change the argument types to
Natural, as this is all we need for Anoma).
* Closes#3079
* Closes#3086
* Depends on #3088
* Updates the coding style guidelines (CODING.md) to reflect issues not
foreseen originally
* Changes the unicode arrow printed in the REPL to `->`. This is to make
the output consistent with how function types are written in the
standard library.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
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
* 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.
* 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>
* 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
