diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index 4844a5c94..0ab704a41 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -19,6 +19,8 @@ - [Operations](./asm/operations.md) - [Links](./asm/links.md) - [pil](./pil/README.md) + - [Declarations](./pil/declarations.md) + - [Expressions](./pil/expressions.md) - [Fixed Columns](./pil/fixed_columns.md) - [Macros](./pil/macros.md) - [Frontends](./frontends/README.md) diff --git a/book/src/pil/declarations.md b/book/src/pil/declarations.md new file mode 100644 index 000000000..c5b7524af --- /dev/null +++ b/book/src/pil/declarations.md @@ -0,0 +1,37 @@ +# Declarations + +Powdr-pil allows the same syntax to declare various kinds of symbols. This includes +constants, fixed columns, witness columns and even macros. It deduces the symbol kind +by its type and the way the symbol is used. + +Symbols can be declared using ``let ;`` and they can be declared and defined +using ``let = ;``, where ```` is an expression. +This syntax can be used for constants, fixed columns, witness columns and even (higher-order) +functions that can transform expressions. The kind of symbol is deduced by its type and the +way the symbol is used: + +- symbols without a value are witness columns, +- symbols evaluating to a number are constants, +- symbols defined as a function with a single parameter are fixed columns and +- everything else is a "generic symbol" that is not a column. + +Examples: + +```rust +// This defines a constant +let rows = 2**16; +// This defines a fixed column that contains the row number in each row. +let step = |i| i; +// Here, we have a witness column. +let x; +// This functions returns the square of its input (classified as a fixed column). +let square = |x| x*x; +// A recursive function, taking a function and an integer as parameter +let sum = |f, i| match i { + 0 => f(0), + _ => f(i) + sum(f, i - 1) +}; +// The same function as "square" above, but employing a trick to avoid it +// being classified as a column. +let square_non_column = (|| |x| x*x)(); +``` \ No newline at end of file diff --git a/book/src/pil/expressions.md b/book/src/pil/expressions.md new file mode 100644 index 000000000..76217e0f2 --- /dev/null +++ b/book/src/pil/expressions.md @@ -0,0 +1,72 @@ +# Expressions + +Depending on the context, powdr allows more or less features for expressions. + +Inside values for declarations, you can use a very flexible language which includes +many different operators, function calls, lambda functions, tuple types, statement blocks, +match statements and others. + +In statements and expressions that are required to evaluate to polynomial identities, only a much more restrictive +language can be used. Expressions in that language are caleld Algebraic Expressions. While you can use +the full language everywhere, in the context of a polynomial identity, the result after function evaluation +and constant propagation has to be an algebraic expression. + +## Generic Expressions + +The expression language allows the following operators, in order of increased precedence: + +- lambda functions: ``|params| body``. Examples: ``|i| i`` (the identity), ``|a, b| a + b`` (sum) +- ``||`` - logical or +- ``&&`` - logical and +- ``<``, ``<=``, ``==``, ``!=``, ``>=``, ``>`` - comparisons +- ``|`` - bitwise or +- ``^`` - bitwise xor +- ``&`` - bitwise and +- ``<<``, ``>>`` - left and right shift +- ``+``, ``-`` - addition and subtraction (binary operator) +- ``*``, ``/``, ``%`` - multiplication, division and modulo +- ``**`` - exponentiation +- ``-``, ``!`` - numerical and logical negation (unary operators, prefix) +- ``'`` - "next row" operator (suffix) +- ``[]``, ``()`` - array index access and function calls + +Elementary expressions are +- number literals (integers) +- string literals, written in double quotes, e.g. ``"hello"`` +- array literals written in square brackets, e.g. ``[1, 2, 3]`` +- tuples, having at least two elements, e.g. `(1, "abc")` +- match expressions (see below). + +Parentheses are allowed at any point to force precedence. + +### Match Expressions + +Match expressions take the form ``match { => , => , _ => }``, +with an arbitrary number of match arms. + +The semantics are that the first match arm where the pattern equals the value after the `match` keyword is evaluated. +The "default" arm with the pattern `_` matches all values. + +Example: + +``` +let fib = |i| match i { + 0 => 1, + 1 => 1, + _ => fib(i - 2) + fib(i - 1), +}; +``` + +## Algebraic Expressions + +For identities (or functions called from identities), the expression syntax is limited: +After evaluating function calls and performing constant propagation, the resulting expression has to +be an "algebraic expression". These are restricted in the following way: + +- You can freely use the operators ``+``, ``-``,``*``. +- The operator ``**`` must have a number as exponent. +- The operator `[i]` must have a column name on the left-hand side and the index must be a number. +- The operator `'` must have a column or `[i]` on the left-hand-side. +- No other operators are allowed. + +Arbitrary parentheses are allowed. \ No newline at end of file