Started as a small fix but expanded to a complete refactoring of
`PublicDeclaration` and `PublicReference`.
Now public reference work the same way as any reference and the syntax
is without the colon (`:out` -> `out`). `PublicDeclaration` are also put
under definitions in the analyzer. Both public reference and public
declaration use the absolute path, so it's easy to refer from one to the
other now.
This is needed for #2502 to match public reference to public declaration
in the backend. Currently, different namespaces can have public
references with the same name, and it will confuse the backend on which
public reference value to fetch.
Rust's function types are more complicated than powdr's: It has `fn`,
`Fn` and closures (we ignore generic functions and trait functions for
now). This PR adds an
[enum](https://github.com/powdr-labs/powdr/pull/1866/files#diff-0b9128f385080144659241b59a28702f0a85a684895f59bf06f5a0b4440070fdR90)
that can hold either an `fn` or an `Fn` (which is used for closures).
This enum will be used as the rust type for a powdr function.
Rust closures that capture variables have to be handled specially: We
need to make sure that we can move the captured values into the closure
(the other option would be to use references, but we cannot say anything
about the lifetime of the captured value, so this is not viable). We do
this by first cloning the captured value into a new local variable (of
the same name), which we can then move into the closure. In order to do
this, we need to check which local variables references reach out of the
lambda and which ones stay inside the lambda. This is done by keeping
track of the current "variable height" during expression conversion.
Since we also need name and type pairs for structs, it makes sense to
rename `TraitFunction` to something more general (`NamedType` in this
case).
There are also `NamedExpressions` and everything could be combined into
a `NamedElement` or something similar that covers both cases. Personally
I prefer this option, but the discussion is open.
We currently hardcode the range of degrees that variable degree machines
are preprocessed for. Expose that in machines instead.
This changes pil namespaces to accept a min and max degree:
```
namespace main(123..456);
namespace main(5); // allowed for backward compatibility, translates to `5..5`
```
It adds two new builtins:
```
std::prover::min_degree
std::prover::max_degree
```
And sets the behavior of the `std::prover::degree` builtin to only
succeed if `min_degree` and `max_degree` are equal.
This PR fixes issue #1728.
1) Removes the blank space that was printed even if the body of the
blocks was empty.
2) Adds the Precedence trait to LambdaExpressions to correctly handle
the use of parentheses.
This PR 'parameterise' Expressions to be able to choose when they can be
converted into a StructExpression and when they cannot. This
modification allows us to overcome ambiguities with Structs and to adopt
the standard Structs syntax:
```
struct Point{ x: int, y: int }
let p: Point = Point{ x: 1, y: 2 };
```
This PR replace #1591 to be able to include this modifications before
merging structs.
---------
Co-authored-by: chriseth <chris@ethereum.org>
Fixes#1190
Fixes https://github.com/powdr-labs/powdr/issues/1488
```
// creates intermediate column.
let x: inter = ...
// same here, expects an array on the rhs
let x: inter[k] = ...
// Creates an intermediate column, this is printed from Analyzed
col x = ...;
// Creates an array of intermediate columns, this is printed from analyzed and it's actually new syntax.
col x[k] = ...;
// old syntax for intermediate columns, this just defines a "generic variable" after the change,
// essentially an intermediate column that is always inlined.
let x: expr = ...;
```
---------
Co-authored-by: Leo <leo@powdrlabs.com>
This PR splits from the main Trait implementation PR
https://github.com/powdr-labs/powdr/pull/1450 to simplify the review
process.
It includes only the parsing of the impls (trait parsing PR here: #1489
) and some functionality necessary for the code to compile.
---------
Co-authored-by: chriseth <chris@ethereum.org>
This PR splits from the main Trait implementation PR #1450 to simplify
the review process.
It includes only the parsing of the traits (not impls) and some
functionality necessary for the code to compile.
---------
Co-authored-by: chriseth <chris@ethereum.org>
This PR builds on top of #1393.
It mainly modifies the grammar by changing the way SelectedExpressions
are declared, to allow blocks to be empty.
---------
Co-authored-by: chriseth <chris@ethereum.org>
Fixes#1493
Allow passing machines as argument when instantiating submachines, as
in:
```
use std::machines::binary::Binary;
machine Main with degree: 262144 {
reg pc[@pc];
reg X[<=];
reg Y[<=];
reg Z[<=];
reg A;
Binary binary;
WithArg sub(binary);
instr and X, Y -> Z ~ binary.and;
instr or X, Y -> Z ~ binary.or;
instr xor X, Y -> Z ~ binary.xor;
...
}
machine WithArg(bin: Binary) {
reg pc[@pc];
reg X[<=];
reg Y[<=];
reg Z[<=];
reg A;
reg B;
instr and X, Y -> Z ~ bin.and;
instr or X, Y -> Z ~ bin.or;
instr xor X, Y -> Z ~ bin.xor;
...
}
```
Allow VM instructions to use the `link` notation, unifying the way
machines are linked from VMs and block machines.
Previous syntax for "external instructions" not allowed anymore, and
should use the new `link` syntax.
This PR is part of issue https://github.com/powdr-labs/powdr/pull/1345.
In particular, it adds the struct BlockExpression to Expressions to
homogenize the structure before including source references.
This PR is part of issue https://github.com/powdr-labs/powdr/pull/1345.
In particular, it adds the struct MatchExpression to Expressions to
homogenise the structure before including source references.
This PR is part of issue https://github.com/powdr-labs/powdr/pull/1345.
In particular, it adds the struct UnaryOperation to Expressions to
homogenise the structure before including source references.
This PR is part of issue #1345.
In particular, it adds the struct BinaryOperation to Expressions to
homogenise the structure before including source references.
---------
Co-authored-by: Thibaut Schaeffer <schaeffer.thibaut@gmail.com>
This PR is part of issue https://github.com/powdr-labs/powdr/pull/1345.
In particular, it adds the struct Number to Expressions to homogenize
the structure before including source references.
Adds binary operation precedence support to avoid unnecessary
parentheses in expression printed format
- #962
---------
Co-authored-by: chriseth <chris@ethereum.org>
