Struct Inlining

pub struct Inlining<'a> { /* private fields */ }

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.).

Implementations

impl<'a> Inlining<'a>

pub fn new(diagnostics: &'a DiagnosticsHandler) -> Inlining<'a>

Trait Implementations

impl Pass for Inlining<'_>

type Input<'a> = Program

type Output<'a> = Program

type Error = SemanticAnalysisError

fn run<'a>( &mut self, program: <Inlining<'_> as Pass>::Input<'a>, ) -> Result<<Inlining<'_> as Pass>::Output<'a>, <Inlining<'_> as Pass>::Error>

Runs the pass on the given input

fn chain<P, E>(self, pass: P) -> Chain<Self, P>

where Self: Sized, E: From<Self::Error>, P: for<'a> Pass<Input<'a> = Self::Output<'a>, Error = E>,

Chains two passes together to form a new, fused pass