RewriteRule < Stratego

A rewrite rule has the form

  Lab : l -> r where s

where Lab is the label or name of the rule, l is the left-hand side term pattern, r the right-hand side term pattern and s a strategy used as condition.

The application of a rule Lab to a term t consists of matching the left-hand side l to t, applying the condition s, and then building the right-hand side r. On matching l the variables in l become bound. These variable bindings are used in the condition and the instantiation of the right-hand side.

Rules are implemented by translating them to more basic constructs. That is, a rule

  Lab : l -> r where s

is translated to a StrategyDefinition

  Lab = {x1,...,xn: ?l; where(s); !r}