Previous
Page

NonDeterministic Computations Rules Specifications Modularity and parameterization 
Next Page

<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 lefthand 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 righthand side and the enriched matching substitution. Let us see the three kinds of local evaluations which significantly increase the expressivity of rewrite rules:
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.
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 recomputed. 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