A *rewrite rule* has the form

CategoryGlossary

Lab : l -> r where swhere

`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 sis translated to a StrategyDefinition

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

See also

-- EelcoVisser - 08 Jan 2002

CategoryGlossary

Revision: r1.4 - 28 Apr 2005 - 22:24 - Main.wiki

Copyright © 1999-2020 by the contributing authors.
All material on this collaboration platform is the property of the contributing authors.

Ideas, requests, problems regarding TWiki? Send feedback

Ideas, requests, problems regarding TWiki? Send feedback