feat(docs): add docs for list comprehension

docs/src/SUMMARY.md

@@ -6,6 +6,7 @@
   - [File structure](./description/structure.md)
   - [Type declarations](./description/declarations.md)
   - [Variables](./description/variables.md)
+  - [Convenience syntax](./description/convenience-syntax.md)
   - [Constraint descriptions](./description/constraints.md)
   - [AirScript Example](./description/example.md)
   - [Keywords](./description/keywords.md)

docs/src/description/convenience-syntax.md

@@ -0,0 +1,55 @@
+# Convenience syntax
+
+To make writing constraints easier, AirScript provides a number of syntactic conveniences. These are described in this section.
+
+## List comprehension
+
+List comprehension provides a simple way to create new vectors. It is similar to the list comprehension syntax in Python. The following examples show how to use list comprehension in AirScript.
+
+```
+let x = [a * 2 for a in b]
+```
+This will create a new vector with the same length as `b` and the value of each element will be twice that of the corresponding element in `b`.
+
+```
+let x = [a + b for (a, b) in (c, d)]
+```
+This will create a new vector with the same length as `c` and `d` and the value of each element will be the sum of the corresponding elements in `c` and `d`. This will throw an error if `c` and `d` vectors are of unequal lengths.
+
+```
+let x = [2^i * a for (i, a) in (0..5, b)]
+```
+Ranges can also be used as iterables, which makes it easy to refer to an element and its index at the same time. This will create a new vector with length 5 and each element will be the corresponding element in `b` multiplied by 2 raised to the power of the element's index. This will throw an error if `b` is not of length 5.
+
+```
+let x = [m + n + o for (m, n, o) in (a, 0..5, c[0..5])]
+```
+Slices can also be used as iterables. This will create a new vector with length 5 and each element will be the sum of the corresponding elements in `a`, the range 0 to 5, and the first 5 elements of `c`. This will throw an error if `a` is not of length 5 or if c is of length less than 5.
+
+## List folding
+
+List folding provides syntactic convenience for folding vectors into expressions. It is similar to the list folding syntax in Python. List folding can be applied to vectors, list comprehension or identifiers referring to vectors and list comprehension. The following examples show how to use list folding in AirScript.
+
+```
+trace_columns:
+    main: [a[5], b, c]
+
+integrity_constraints:
+    let x = sum(a)
+    let y = sum([a[0], a[1], a[2], a[3], a[4]])
+    let z = sum([a * 2 for a in a])
+```
+
+In the above, `x` and `y` both represent the sum of all trace column values in the trace column binding `a`. `z` represents the sum of all trace column values in the trace column binding `a` multiplied by `2`.
+
+```
+trace_columns:
+    main: [a[5], b, c]
+
+integrity_constraints:
+    let x = prod(a)
+    let y = prod([a[0], a[1], a[2], a[3], a[4]])
+    let z = prod([a + 2 for a in a])
+```
+
+In the above, `x` and `y` both represent the product of all trace column values in the trace column binding `a`. `z` represents the product of all trace column values in the trace column binding `a` added by `2`.

docs/src/description/keywords.md

@@ -11,8 +11,10 @@ AirScript defines the following keywords:
 - `integrity_constraints`: used to declare the [source section](./structure.md#source-sections) where the [integrity constraints are described](./constraints.md#integrity_constraints).
 - `let`: used to declare intermediate variables in the boundary_constraints or integrity_constraints source sections.
 - `periodic_columns`: used to declare the [source section](./structure.md#source-sections) where the [periodic columns are declared](./declarations.md). _They may only be referenced when defining integrity constraints._
+- `prod`: used to fold a list into a single value by multiplying all of the values in the list together.
 - `public_inputs`: used to declare the [source section](./structure.md#source-sections) where the [public inputs are declared](./declarations.md). _They may only be referenced when defining boundary constraints._
 - `random_values`: used to declare the [source section](./structure.md#source-sections) where the [random values are described](./declarations.md).
+- `sum`: used to fold a list into a single value by summing all of the values in the list.
 - `trace_columns`: used to declare the [source section](./structure.md#source-sections) where the [execution trace is described](./declarations.md). _They may only be referenced when defining integrity constraints._
   - `main`: used to declare the main execution trace.
   - `aux`: used to declare the auxiliary execution trace.

docs/src/description/main.md

@@ -4,6 +4,7 @@
 - [File structure](./structure.md)
 - [Type declarations](./declarations.md)
 - [Variables](./variables.md)
+- [Convenience syntax](./convenience-syntax.md)
 - [Constraint descriptions](./constraints.md)
 - [AirScript example](./example.md)
 - [Keywords](./keywords.md)

docs/src/introduction.md

@@ -27,6 +27,9 @@ AirScript includes the following features:
 
 - **Variables**: Local variables can be declared for use in defining boundary and integrity constraints. Variables can be scalars, vectors or matrices built from expressions (e.g. `let x = k * c[1]'`, `let y = [k * c[1], l * c[2], m * c[3]]` or `let z = [[k * c[1], l * c[2]], [m * c[3], n * c[4]]]`)
 
+The language also includes some convenience syntax like list comprehension and list folding to make writing constraints easier.
+(e.g. `let x = [k * c for (k, c) in (k, c[1..4])]`, `let y = sum([k * c for (k, c) in (k, c[1..4])])`)
+
 The language will be specified in detail in the rest of this book.
 
 ### CLI