Given the following Stratego program:

module bug
imports libstrategolib
signature
sorts Prop
constructors
A : Prop
B : Prop
Not : Prop -> Prop
rules
E : Not (B()) -> A () where equal (B (), B ())
strategies
eval = memo(innermost(E)) ; debug(!"result = ")
main =
( Not (B ()));
0

the result of “str bug.str” displays:

 result = Not(B)

It seems that the “where” clause prevents the rewrite rule from being applied.
If the “where” clause is removed, the result becomes:

result = A

So, my question is: how to write conditional rules? And more: how to write conditional rules
with multiple conditions: for instance, is it correct to write:

L (x) -> R (x) where equal (p (x), true); equal (q (x), r (x))

to specify that p(x) should be true and that q(x) should be equal to r(x)?

Thanks!

Submitted on 19 November 2016 at 13:52