Generations

You may have noticed by now that each node carries with it a type parameter, usually denoted G, Pre or Post. This type parameter is not used or stored anywhere in the tree, and due to type erasure it is in fact entirely compiled away: it has no operational effect in the tool. Instead it is a facility by which we can make COL trees have entirely disjoint types. We maintain by hand the invariant that the subnodes of each node have the same "generation" type parameter as the node itself in the node declarations. Each node declares a type parameter G, which is passed along in all node types that the node contains.

All normal tree operations make sense as long as the generation type parameter matches between trees: we can take a tree of type Node[G], and replace all occurences of a Local[G] with an Expr[G]. On the other hand, there is no way to place a tree of type Node[L] in a tree of type Node[R] (unless L and R resolve to the same type).

This trick is useful in rewriters: we make the input tree type unrelated to the output tree type. The input node type uses Pre for the generation, whereas the output uses Post. This makes it so that you cannot return an input tree as though it is an output tree: you are required to rewrite the input explicitly. Although it is possible that optimizations exist where it would not be necessary to recurse into a particular type of tree, we find that eventually it becomes necessary anyway. A short parable: contract expressions are pure, so we should not have to rewrite them if we are only transforming method invocations (a side effect). Afterwards we add a feature where a method can be marked /*@ pure */, which translates the method to a pure function. It should afterwards be possible to use this method in contract expressions, but this introduces a bug at great distance in our original rewriter.