Short circuiting rewrite paths with cutrewrite

From version 2.3.0 onward, the cutrewrite(e) statement may be used wherever a rewrite(e) statement is expected. The cutrewrite statement can be used to selectively ignore certain subterms during the rewriting process.

The semantics of cutrewrite(e) is to replace the current redex with e but do not bother with looking for other redexes in the replacement term. This means that the replacement term will not be re-traversed immediately. Furthermore, the replaced term will not match any other left hand side sub-patterns except pattern variables and wildcards.

This feature is very useful for preventing the rewriter from looking inside certain terms.

To demonstrate, consider the simple following example:

   datatype Exp = NUM of int
                | ADD of Exp, Exp
                | SUB of Exp, Exp
                | MUL of Exp, Exp
                | DIV of Exp, Exp
                | FINAL of Exp
                ;
   Exp e = ADD(NUM(1),MUL(NUM(2),NUM(3)));

Suppose we want to find all numbers within the expression e and increment their values by 1. The straight forward way of writing:

   rewrite (e) type (Exp) {
      NUM x: NUM(x+1)
   }

will not work, since the replacement term is a new redex, and the rewriting system will not terminate.

We can reimplement the rewriting system as a two stage process. First, we mark all terms that we do not want to be changed; whenever we find a marked term, we execute a cutrewrite to prevent the term from being changed. Then we unmark the terms.

   rewrite (e) type (Exp) {
      NUM x:   FINAL(NUM(x+1));
   preorder:
      FINAL _: cutrewrite;
   }
   rewrite (e) type (Exp) {
      FINAL x: x
   }

In the first rewrite statement, replacement terms that we want to stay fixed are encapsulated within the auxiliary FINAL constructor. Recall that preorder rules are tried before the subterms of a redex are reduced. Thus we can make sure all that all terms that are arguments to a FINAL term is left unaltered by adding a preorder rule that executes a cutrewrite¹⁰ Finally, after the first rewrite statement finishes, we use the second rewrite statement to remove all FINAL terms generated in the first.

The semantics of cutrewrite needs further explanation. Consider the following rewrite system:

   rewrite (e) type (Exp) {
      NUM x:          cutrewrite(NUM(x+1))
   |  MUL(X, NUM 1):  X
   |  MUL(NUM 1,X):   X
   }

Given the term MUL(NUM(0),NUM(2)), the subterms NUM(0) and NUM(1) will be rewritten by the first rule into NUM(1) and NUM(3) respectively. Furthermore, the replacement term NUM(1) will not match the left subpattern in MUL(NUM 1,X). Thus the result of the rewrite will be MUL(NUM(1),NUM(3)).

Tips: the semantics of a rewriting system with cutrewrite can be tricky to analyze, its use should be avoided as much as possible.