Merge pull request #756 from powdr-labs/document_syntax

Document syntax a little.

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)

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 <name>;`` and they can be declared and defined
+using ``let <name> = <value>;``, where ``<value>`` 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)();
+```

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 <value> { <pattern 1> => <value 1>, <pattern 2> => <value 2>, _ => <default value> }``,
+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.