Stratego: do conditional rules work?
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
q? Are they strategies? You can use a semi-colon between two equal checks, but if
qare strategies then you need to use call syntax when they are in term argument position in the
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
equalin between everywhere.
andis 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?
;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)>)
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:
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
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
mtimesis 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
@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))'''
Log in to post comments