A contextual rule is a RewriteRule in which the left-hand side and right-hand side terms contain contexts of the form x[t].

A typical example of a contextual rule is the following inlining rule:

  Inline : Let(x, e1, e2[Var(x)]) -> Let(x, e1, e2[e1])

The idea is that an occurrence of Var(x) in =e2 is replaced with the term e1.

Contextual rules are treated as syntactic sugar and translated to a normal rule, which performs a traversal over the context subterm. The inlining rule above is translated to the rule:

  Inline : 
    Let(x, e1, e2) -> Let(x, e1, e2')
    where <oncetd(?Var(x); !e1)> e2 => e2'

The traversal strategy oncetd is used to find an occurrence of Var(x) and replace it with e1. Note that in the match of Var(x), the variable x is already bound by the match of the left-hand Let(x, e1, e2) side of the rule.

Issues

• traversal strategy
• multiple contexts
• conditions
• overlapping contextual rules
• backtracking

-- EelcoVisser - 08 Jan 2002

---

CategoryGlossary