TC-5 Improvements

Maximal node sharing

The proposed implementation of Tree creates new nodes for equal expressions; for instance two uses of the variable foo lead to two equal instantiations of tree::Temp. The same applies to more complex constructs such as the same translation if foo is actually a frame resident variable etc. Because memory consumption may have a negative impact on performances, it is desirable to implement maximal sharing: whenever a Tree is needed, we first check whether it already exists and then reuse it. This must be done recursively: the translation of (x + x) * (x + x) should have a single instantiation of x + x instead of two, but also a single instantiation of x instead of four.

Node sharing makes some algorithms, such as rewriting, more complex, especially wrt memory management. Garbage collection is almost required, but fortunately the node of Tree are reference counted! Therefore, almost everything is ready to implement maximal node sharing. See SPOT, for an explanation on how this approach was successfully implemented. See The ATerm library for a general implementation of maximally shared trees.