Previous Page
Strategies Specification
Non-Deterministic Computations
Rules Specifications
Modularity and parameterization
Next Page

ELAN - Rules Specification

Until now, we have seen how to apply labelled rules and strategies at the top of a term. In order to apply strategies on subterms, the syntax of rewrite rules has been enriched by local evaluations, used to call strategies, to factorise sequences of computations and to specify conditions of application. The general syntax of an ELAN rule is as follows:

<rule> ::="["[<label>]"]"<term> "=>" <term>{ <local evaluation> }*
<local evaluation> ::= if <boolean term>
| where <variable> ":=" "(" [ <strategy> ] ")" <term>
| where <term> ":=" "(" [ <strategy> ] ")" <term>
| choose
{try { <local evaluation> }+ }+

After the selection of a rule by matching its left-hand side to the term to reduce, the local evaluations are evaluated in order and potentially enrich the matching substitution. If no evaluation fails, the rule can apply and the resulting term is built from the right-hand side and the enriched matching substitution. Let us see the three kinds of local evaluations which significantly increase the expressivity of rewrite rules: