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 =
    (<eval> Not (B ()));
    <exit> 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:56

You’re using a version of [equals that takes two strategy arguments](http://releases.strategoxt.org/docs/api/libstratego-lib/libstratego-lib-docs-stable/docs/html/strategy/general/unification.html#area-in-file(%22strategy/general/unification.str%22,area(94,2,98,5,2291,173))). To check equality of two terms, you need [this one](http://releases.strategoxt.org/docs/api/libstratego-lib/libstratego-lib-docs-stable/docs/html/strategy/conditional.html#area-in-file(%22strategy/conditional.str%22,area(34,2,35,18,431,33))), which you call with equal(|B(), B()) (note the pipe symbol which separates strategy arguments from term arguments).

As for your second question: what are p and q? Are they strategies? You can use a semi-colon between two equal checks, but if p and q are strategies then you need to use call syntax when they are in term argument position in the equal(|) call: equal(|<p(x)>, true).

Thanks, equal(|B(), B()) is what I needed.

For the second question, what I need actually can now be written
and (equal (|p (x), true), equal (|q (x), r (x)))

However, for obscure reason (I am generating the Stratego code using awk scripts),
I would prefer using an infix “and” rather than a prefix “and”, because there can be
more than two conditions.

I checked that the prefix “and” only accepts two arguments, rather than a list.

This is why, I was trying to use an infix “;” rather than a prefix “and”.

If you have a quick solution to avoid writing nested “and”’s, I would love it!

Unless you need the special behaviour of and, you can probably use semi-colons (;), at least if you’re using equal in between everywhere. and is defined as:

/**
 * and(s1, s2) applies s1 and s2 to the current
 * term and succeeds if both succeed. s2 will always
 * be applied, i.e., and is *not* a short-circuit 
 * operator
 */

and(s1, s2) = 
  if s1 then test(s2) else test(s2); fail end

Thanks! Ideally (to get the best performance from Stratego) I would not
mind using a “and” operator that does short-circuits (like “&&” in C or
“and then” in Ada). Can I safely assume that “;” will do the job?

Yeah, ; shortcircuits. You can see it as an “and” as long as the strategies you combine with it don’t depend on the term context. You should probably read the docs of Stratego until at least here so you can be sure you understand what it’s doing.

Thanks for the pointer. One main problem with the Stratego doc is that it lacks
(or, at least, I could not find easily) a global definition of the language.

What is missing is for instance: a complete BNF syntax, the list of reserved
keywords, explanations of each construct, and ideally a formal semantics.

The present manual is a collection of examples and well-written paragraphs,
but one needs a good intuition to guess how the language can be used.
Fortunately, I have a collection of Stratego examples written in 2008, which
helps a lot. For instance, I discovered there the existence of “<exit> 0”,
which is very useful but not documented in the online manual pages
(i.e., searching for “exit” gives no answer).

Another problem is that many explanations are given in terms of
the interactive Stratego shell. It is unclear how these explanations
can be used when writing (non-interactive) “.str” files. Said
otherwise, the explanations are split 50%-50% between interactive
and non-interactive modes, so that they fail addressing all needs
of both classes of users, those typing interactive commands, and
those writing non-interactive .str files.

There is one (last) problem I face when translating to Stratego a conditional
rewrite rule of the following form:

 closure(L) -> L     if L -><- mtimes(L, L)

I translated it to

   E: closure (L) -> L where equal (|<L>, <mtimes (L, L)>)

but this leads to a run-time error:

    [ Main | error ] *** ("E",0,0) calls non-existing ("L",0,0)

I tried to remove the “<” and “>” around the first argument L of equal,
but this does not help. Help would be most welcome.

Note: this takes place in a functional evaluation (innermost) setting,
so that L has a defined value, and mtimes (L, L) has to be evaluated
first and then compared to L.

Depending on the definition of mtimes (which does seem to be in the standard library), you could need:

equal(|L, <mtimes(|L, L)>)

or

equal(|L, <mtimes(!L, !L)>)

or maybe even

equal(|L, <mtimes> (L, L))

As for the docs: The only other documentation I can think of are the slides of the compiler construction course on term rewriting. Have a look, maybe it’ll help clear some things up.

Thanks for the help. But which one of the three should I use? Actually, what I have to
express is very simple: just a Boolean guard that prevents the rule from being applied
if it evaluates to false. Such Boolean guards exist in most algebraic and functional
languages (but SML) and this is exactly what I am trying to express in StrategoXT.

Actually, what I am missing is the exact meaning of the “<” … “>” symbols. I introduced
them because you mentioned them earlier, but I am unsure about what they actually mean.

In this particular example, mtime is just a user-defined function that takes two arguments
and returns a result (everything computed using innermost strategy). Here is the actual
definition of mtimes and closure:

constructors
d0 : Bit
d1 : Bit
empty_vector : Vector
v : Bit * Vector -> Vector
empty_matrix : Matrix
m : Vector * Matrix -> Matrix
plus : Bit * Bit -> Bit
btimes : Bit * Bit -> Bit
vchop : Matrix -> Matrix
innerProduct : Vector * Matrix -> Bit
vecMat : Vector * Matrix -> Vector
mtimes : Matrix * Matrix -> Matrix
closure : Matrix -> Matrix
…
E: mtimes (m (U, N), L) -> m (vecMat (U, L), mtimes (N, L))
E: mtimes (empty_matrix(), L) -> empty_matrix()
E: closure (L) -> L where equal (|L, <mtimes (L, L)>)
E: closure (L) -> closure (mtimes (L, L)) where not (equal (|L, <mtimes (L, L)>))

I tried the three solutions you proposed:

1) equal(|L, <mtimes(|L, L)>)

=> Rejected at compile time: Syntax error near unexpected character ‘|’

2)  equal(|L, <mtimes(!L, !L)>)

=> Rejected at compile time: Syntax error near unexpected character ‘!’

3)  equal(|L, <mtimes> (L, L))

=> Rejected at run time: Exception in thread “main” org.strategoxt.lang.Strategy$IllegalArgumentException: Illegal arguments for mtimes_2_0 (none)

@hubert: can you please quote your code; use ``` for blocks of code

Other remarks:

If you want to write idiomatic Stratego code, please use the following conventions (this makes it easier for Stratego community to help you):

• Use CamelCase for constructor names, i.e. constructors start with a capital.
• Variables use lower-case.

Further, note that mtimes is not a user-defined function, it is a constructor. It looks like the condition you want to express is that mtimes(L, L) (which I would prefer you to write as Mtimes(l, l)) reduces to L (or has the same normal form as L). This requires that you call eval recursively. You should probably define your own equality:

  equal-mod-eval(|m1, m2) = equal(|<eval>m1, <eval>m2)

And then use that as guard

 E : Closure(m) -> m  where equal-mod-eval(|m, Mtimes(m, m))

But this may lead to non-termination because of your second rule for Closure.

@hubert: can you please quote your code; use ``` for blocks of code

Thanks for the hint. I saw you were using nice colors but could not find any
help on this in the YellowGrass About menu. Other wikis and forum sites propose
a palette to highlight text.

If you want to write idiomatic Stratego code, please use the following conventions
(this makes it easier for Stratego community to help you):
Use CamelCase for constructor names, i.e. constructors start with a capital.
Variables use lower-case.

Oops. My Stratego code is automatically generated. I was so far basing my
translation on a collection of Stratego examples written in 2008, where the conventions
for constructors and variables are just the opposite of those you mention. See
https://gforge.inria.fr/scm/viewvc.php/rec/2008-REC2/STRATEGO/

equal-mod-eval(|m1, m2) = equal(|<eval>m1, <eval>m2)

Thanks, this solved the problem, after defining strategy “eval” to be ```memo (innermost (E))'''