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> }+ }+
end

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:

• A condition is a boolean expression  c introduced by the keyword if. The term c is put in normal form and compared to the predefined boolean value true. If they are equal, the condition is satisfied, and the next local evaluation is considered. Otherwise, one backtracks on the previous local evaluation.
• A local assignment where v:=(S) t allows calling a strategy. First the term t is normalised w.r.t. all unlabelled rules, then the strategy S is applied on its normal form. In practice only one result of S on t is computed and assigned to the variable v. If S fails, the local assignment fails too and backtracking is applied. Another result of the strategy S on t may be required by the backtracking mechanism.

• The notion of local assignment has been extended to a matching condition where p:=(S) t where p is now a term. In that case, the term p is matched to the result of S on t, which provides values for the variables of p.

• The third kind of local evaluation allows factorisation of computations, with the construction choose try ... end. This is especially useful when there are several rules with the same left-hand side:

• rules for int
x,y,z : ...
global
[] f(x) => r1(z)
where y:=() g(x)
where z:=(s1) x
end
[] f(x) => r2(z)
where y:=() g(x)
where z:=(s2) x
end
end

In order to reduce the term f(a) for instance, a rule is selected, say the first one. Assume that the strategy s1 on the term a fails. In this case, the second rule is tried and the normal form of g(a) is re-computed. To avoid this kind of redundancy, one can use the choose try ... end construction and write the equivalent ELAN program which avoids this drawback:
rules for int
x,y,z,result : ...
global
[] f(x) => result
where y:=() g(x)
choose try where z:=(s1) x
where result:=() r1(z)
try where z:=(s2) x
where result:=() r2(z)
end
end
end