pub struct Inlining<'a> { /* private fields */ }
Expand description
This pass performs the following transformations on a Program:
- Monomorphizing and inlining evaluators/functions at their call sites
- Unrolling constraint comprehensions into a sequence of scalar constraints
- Unrolling list comprehensions into a tree of
let
statements which end in a vector expression (the implicit result of the tree). Each iteration of the unrolled comprehension is reified as a value and bound to a variable so that other transformations may refer to it directly. - Rewriting aliases of top-level declarations to refer to those declarations directly
- Removing let-bound variables which are unused, which is also used to clean up after the aliasing rewrite mentioned above.
The trickiest transformation comes with inlining the body of evaluators at their call sites, as evaluator parameter lists can arbitrarily destructure/regroup columns provided as arguments for each trace segment. This means that columns can be passed in a variety of configurations as arguments, and the patterns expressed in the evaluator parameter list can arbitrarily reconfigure them for use in the evaluator body.
For example, let’s say you call an evaluator foo
with three columns, passed as individual
bindings, like so: foo([a, b, c])
. Let’s further assume that the evaluator signature
is defined as ev foo([x[2], y])
. While you might expect that this would be an error,
and that the caller would need to provide the columns in the same configuration, that
is not the case. Instead, a
and b
are implicitly re-bound as a vector of trace column
bindings for use in the function body. There is further no requirement that a
and b
are consecutive bindings either, as long as they are from the same trace segment. During
compilation however, accesses to individual elements of the vector will be rewritten to use
the correct binding in the caller after inlining, e.g. an access like x[1]
becomes b
.
This pass accomplishes three goals:
- Remove all function abstractions from the program
- Remove all comprehensions from the program
- Inline all constraints into the integrity and boundary constraints sections
- Make all references to top-level declarations concrete
When done, it should be impossible for there to be any invalid trace column references.
It is expected that the provided Program has already been run through semantic analysis and constant propagation, so a number of assumptions are made with regard to what syntax can be observed at this stage of compilation (e.g. no references to constant declarations, no undefined variables, expressions are well-typed, etc.).