Contextual Rule

---

Description

A contextual rule is a rewrite rule 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.

-- EelcoVisser - 08 Jan 2002

Note that for many applications (such as inlining) dynamic rules are often more appropriate than contextual rules since they allow the replacement traversal and the surrounding traversal to be merged.

-- EelcoVisser - 29 Jul 2003

---

Issues

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

-- EelcoVisser - 08 Jan 2002

---

Contexts in Strategy

I'm trying to use context matching inside a strategy.

For example,

rule1 : MyTerm(x[AnotherTerm]) -> MyTerm(x[AnotherTerm])

will match fine. but when I try to do it in a strategy the sc compiler complains (not a term-expression: Con ....)

strat1: ?MyTerm(x[AnotherTerm]) ; debug

So, can someone tell me how to do deep context matching inside a strategy? I need to do this so that I can use the contents of a variable as part of the search criteria. I can't see how to do this with a rule.

-- DAN - 29 Jul 2003

That is correct; contexts are only implemented for rules.

Here are some ways to do it:

(1) first match, then traverse

?MyTerm(x); where(<oncetd(?AnotherTerm)> x); debug

This actually corresponds to the desugaring of contextual rules. That is, rule1 is really sugar for

   rule1 : MyTerm(x) -> MyTerm(x')
             where <oncetd(?AnotherTerm1; !AnotherTerm2)> x => x'

(2) Using TermProject you can abbreviate (1) as

?MyTerm(<oncetd(?AnotherTerm)>); debug

you should note, however, that the debug will now print the subterm of MyTerm. That is (2) is the same as

?MyTerm(x); <oncetd(?AnotherTerm)> x; debug 

that is (1) without the where surrounding the traversal.

(3) If necessary you can of course use alternative traversals.

-- EelcoVisser - 29 Jul 2003

---

Different Implementation

A different implementation of contexual rules is possible though. The current implementation optimizes finding and replacing the holes in a context. It is of course possible to treat matching and building with context separately, just as is done with normal terms. This would mean that a context match ?MyTerm(x[t]) would bind to x an object representing the subterm of MyTerm with holes at the place (or places) where t was found. A build !MyTerm(x[t']) would fill the holes with t'. The more efficient implementation currently used might be derivable from the more general one.

-- EelcoVisser - 29 Jul 2003

---

CategoryGlossary