An ordered collection of statements representing the context surrounding the current focus of our program transformation. That is, since some transformations work from the bottom up, we need to keep track of the statements we passed along the way when reaching for the bottom.

The tail of the list takes scope over the head of the list. Thus, the back/end of the list is towards the top of the program, whereas the front of the list is towards the bottom.

This type was formerly called Heap (presumably due to the Statement type being called Binding) but that seems like a misnomer to me since this really has nothing to do with allocation. However, it is still like a heap inasmuch as it's a dependency graph and we may wish to change the topological sorting or remove "garbage" (subject to correctness criteria).

TODO: Figure out what to do with SWeight, SGuard, SStuff, etc, so that we can use an IntMap (Statement abt) in order to speed up the lookup times in select. (Assuming callers don't use unsafePush unsafely: we can recover the order things were inserted from their varID since we've freshened them all and therefore their IDs are monotonic in the insertion order.)

Run a computation in the Dis monad, residualizing out all the statements in the final evaluation context. The second argument should include all the terms altered by the Dis expression; this is necessary to ensure proper hygiene; for example(s):

runDis (perform e) [Some2 e]
runDis (constrainOutcome e v) [Some2 e, Some2 v]

We use Some2 on the inputs because it doesn't matter what their type or locally-bound variables are, so we want to allow f to contain terms with different indices.

It is impossible to satisfy the constraints, or at least we give up on trying to do so. This function is identical to empty and mzero for Dis; we just give it its own name since this is the name used in our papers.

TODO: add some sort of trace information so we can get a better idea what caused a disintegration to fail.

The empty measure is a solution to the constraints. reject :: (ABT Term abt) => Dis abt a reject = Dis $ _ _ -> [syn (Superpose_ [])]

Emit some code that binds a variable, and return the variable thus bound. The function says what to wrap the result of the continuation with; i.e., what we're actually emitting.

Emit an MBind (i.e., "m >>= x ->") and return the variable thus bound (i.e., x).

A smart constructor for emitting let-bindings. If the input is already a variable then we just return it; otherwise we emit the let-binding. N.B., this function provides the invariant that the result is in fact a variable; whereas emitLet' does not.

A smart constructor for emitting let-bindings. If the input is already a variable or a literal constant, then we just return it; otherwise we emit the let-binding. N.B., this function provides weaker guarantees on the type of the result; if you require the result to always be a variable, then see emitLet instead.

A smart constructor for emitting "unpair". If the input argument is actually a constructor then we project out the two components; otherwise we emit the case-binding and return the two variables.

Emit some code that doesn't bind any variables. This function provides an optimisation over using emit and then discarding the generated variable.

Emit an MBind that discards its result (i.e., "m >>"). We restrict the type of the argument to be HUnit so as to avoid accidentally dropping things.

Emit an assertion that the condition is true.

Run each of the elements of the traversable using the same heap and continuation for each one, then pass the results to a function for emitting code.

Emit a Superpose_ of the alternatives, each with unit weight.

Emit a Superpose_ of the alternatives, each with unit weight.

Returns the current Indices. Currently, this is only applicable to the Disintegration Monad, but could be relevant as other partial evaluators begin to handle Plate and Array