Cache Pruning (Forcing)

At the moment we use a function prune (or force, depending on the version) to replace all solved meta-variables that occur as the head of a neutral term. In this way computation is not blocked anymore and can be advanced. As a result, pattern-matching on such a neutral term can reveal new information.

In the current implementation, each call to prune prunes the term from the very beginning. This can be improved when we remember intermediate pruning results by updating meta-variables. However, as meta-variables only occur as part of a neutral term, we cannot simply update their instance to the result of performing the corresponding application.