Sequential Combinators¶
Rather than defining rewrite rules and highlevel strategies as primitives of the language, Stratego provides strategy combinators as basic building blocks from which these can defined^{1}. Thus, Stratego consists of a core language^{2} and a 'sugar' language defined by reduction to the core language.
Identity and Failure¶
The most basic operations in Stratego are id
and fail
.
The identity strategy id
always succeeds and behaves as the identity function on terms.
The failure strategy fail
always fails.
The operations have no side effects.
Sequential Composition¶
The sequential composition s1 ; s2
of the strategies s1
and s2
first applies the strategy s1
to the subject term and then s2
to the result of that first application.
The strategy fails if either s1
or s2
fails.
Sequential composition is associative.
Identity is a left and right unit for sequential composition; since id
always succeeds and leaves the term alone, it has no additional effect to the strategy that it is composed with.
Failure is a left zero for sequential composition; since fail
always fails the next strategy will never be reached.
This leads to the following equations:
(s1; s2) ; s3 = s1; (s2; s3)
id; s = s
s; id = s
fail; s = fail
However, not for all strategies s
we have that failure is a right zero for sequential composition:
s ; fail = fail // is not a law
Although the composition s; fail
will always fail, the execution of s
may have side effects that are not performed by fail
.
For example, consider printing a term in s
.
As an example of the use of sequential composition consider the following rewrite rules.
A : P(Z(),x) > x
B : P(S(x),y) > P(x,S(y))
The following applications shows the effect of first applying B
and then A
:
<B> !P(S(Z()), Z()) => P(S(Z),Z)
<A> P(Z,S(Z)) => S(Z)
Using the sequential composition of the two rules, this effect can be achieved ‘in one step’:
<B; A> !P(S(Z()),Z()) => S(Z)
The following application shows that the application of a composition fails if the second strategy in the composition fails to apply to the result of the first:
<B; B> !P(S(Z()),Z()) // fails
Left Choice¶
Choosing between rules to apply is achieved using one of several choice combinators, all of which are based on the guarded choice combinator. The common approach is that failure to apply one strategy leads to backtracking to an alternative strategy.
The left choice or deterministic choice s1 <+ s2
tries to apply s1
and s2
in that order.
That is, it first tries to apply s1
, and if that succeeds the choice succeeds.
However, if the application of s1
fails, s2
is applied to the original term.
Properties. Left choice is associative. Identity is a left zero for left choice; since id always succeeds, the alternative strategy will never be tried. Failure is a left and right unit for left choice; since fail always fails, the choice will always backtrack to the alternative strategy, and use of fail as alternative strategy is pointless.
(s1 <+ s2) <+ s3 = s1 <+ (s2 <+ s3)
id <+ s = id
fail <+ s = s
s <+ fail = s
However, identity is not a right zero for left choice. That is, not for all strategies s we have that
s <+ id = s // is not a law
The expression s <+ id
always succeeds, even (especially) in the case that s
fails, in which case the righthand side of the equation fails of course.
Local Backtracking. The left choice combinator is a local backtracking combinator. That is, the choice is committed once the lefthand side strategy has succeeded, even if the continuation strategy fails. This is expressed by the fact that the property
(s1 <+ s2); s3 = (s1; s3) <+ (s2; s3) // is not a law
does not hold for all s1
, s2
, and s3
.
The difference is illustrated by the following applications:
<(B <+ id); B> P(S(Z),Z) // fails
<(B; B) <+ (id; B)> P(S(Z()),Z()) => P(Z,S(Z))
In the application of (B <+ id); B
, the first application of B
succeeds after which the choice is committed.
The subsequent application of B
then fails.
This is equivalent to first applying (B <+ id)
and then applying B
to the result.
The application of (B; B) <+ (id; B)
, however, is successful; the application of B; B
fails, after which the choice backtracks to id; B
, which succeeds.
Choosing between Transformations.¶
The typical use of left choice is to create a composite strategy trying one from several possible transformations. If the strategies that are composed are mutually exclusive, that is, don’t succeed for the same terms, their sum is a transformation that (deterministically) covers a larger set of terms. For example, consider the following two rewrite rules:
PlusAssoc : Plus(Plus(e1, e2), e3) > Plus(e1, Plus(e2, e3))
PlusZero : Plus(Int("0"),e) > e
These rules are mutually exclusive, since there is no term that matches the lefthand sides of both rules.
Combining the rules with left choice into PlusAssoc <+ PlusZero
creates a strategy that transforms terms matching both rules as illustrated by the following applications:
<PlusAssoc>
Plus(Int("0"),Int("3")) // fails
<PlusAssoc <+ PlusZero>
Plus(Int("0"),Int("3")) => Int("3")
<PlusZero>
Plus(Plus(Var("x"),Int("42")),Int("3")) // fails
<PlusAssoc <+ PlusZero>
Plus(Plus(Var("x"),Int("42")),Int("3")) => Plus(Var("x"),Plus(Int("42"),Int("3")))
Ordering Overlapping Rules.¶
When two rules or strategies are mutually exlusive the order of applying them does not matter. In cases where strategies are overlapping, that is, succeed for the same terms, the order becomes crucial to determining the semantics of the composition. For example, consider the following rewrite rules reducing applications of Mem:
Mem1 : Mem(x,[]) > False()
Mem2 : Mem(x,[xxs]) > True()
Mem3 : Mem(x,[yys]) > Mem(x,ys)
Rules Mem2
and Mem3
have overlapping lefthand sides.
Rule Mem2
only applies if the first argument is equal to the head element of the list in the second argument.
Rule Mem3
applies always if the list in the second argument is nonempty.
<Mem2>Mem(1, [1,2,3]) => True()
<Mem3>Mem(1, [1,2,3]) => Mem(1,[2,3])
In such situations, depending on the order of the rules, different results are produced.
(The rules form a nonconfluent rewriting system.)
By ordering the rules as Mem2 <+ Mem3
, rule Mem2
is tried before Mem3
, and we have a deterministic transformation strategy.
Try¶
A useful application of <+
in combination with id
is the reflexive closure of a strategy s:
try(s) = s <+ id
The userdefined strategy combinator try tries to apply its argument strategy s
, but if that fails, just succeeds using id
.
Guarded Left Choice¶
Sometimes it is not desirable to backtrack to the alternative specified in a choice.
Rather, after passing a guard, the choice should be committed.
This can be expressed using the guarded left choice operator s1 < s2 + s3
.
If s1
succeeds s2
is applied, else s3
is applied.
If s2
fails, the complete expression fails; no backtracking to s3
takes place.
Properties.
This combinator is a generalization of the left choice combinator <+
.
s1 <+ s2 = s1 < id + s2
The following laws make clear that the ‘branches’ of the choice are selected by the success or failure of the guard:
id < s2 + s3 = s2
fail < s2 + s3 = s3
If the right branch always fails, the construct reduces to the sequential composition of the guard and the left branch.
s1 < s2 + fail = s1; s2
Guarded choice is not associative:
(s1 < s2 + s3) < s4 + s5 = s1 < s2 + (s3 < s4 + s5) // not a law
To see why consider the possible traces of these expressions.
For example, when s1
and s2
succeed subsequently, the lefthand side expression calls s4
, while the righthand side expression does not.
However, sequential composition distributes over guarded choice from left and right:
(s1 < s2 + s3); s4 = s1 < (s2; s4) + (s3; s4)
s0; (s1 < s2 + s3) = (s0; s1) < s2 + s3
Examples.
The guarded left choice operator is most useful for the implementation of higherlevel controlflow strategies.
For example, the negation not(s)
of a strategy s
, succeeds if s
fails, and fails when it succeeds:
not(s) = s < fail + id
Since failure discards the effect of a (successful) transformation, this has the effect of testing whether s
succeeds.
So we have the following laws for not:
not(id) = fail
not(fail) = id
However, side effects performed by s
are not undone, of course.
Therefore, the following equation does not hold:
not(not(s)) = s // not a law
Another example of the use of guarded choice is the restorealways combinator:
restorealways(s, r) = s < r + (r; fail)
It applies a ‘restore’ strategy r
after applying a strategy s
, even if s
fails, and preserves the success/failure behavior of s
.
Since fail
discards the transformation effect of r
, this is mostly useful for ensuring that some sideeffecting operation is done (or undone) after applying s
.
Ifthenelse¶
The guarded choice combinator is similar to the traditional ifthenelse construct of programming languages.
The difference is that the ‘then’ branch applies to the result of the application of the condition.
Stratego’s if s1 then s2 else s3 end
construct is more like the traditional construct since both branches apply to the original term.
The condition strategy is only used to test if it succeeds or fails, but it’s transformation effect is undone.
However, the condition strategy s1
is still applied to the current term.
The if s1 then s2 end
strategy is similar; if the condition fails, the strategy succeeds.
The ifthenelseend strategy is just syntactic sugar for a combination of guarded choice and the where combinator:
if s1 then s2 else s3 end
==> // transforms to
where(s1) < s2 + s3
The strategy where(s)
succeeds if s
succeeds, but returns the original subject term.
The implementation of the where
combinator is discussed in the section on matching and building terms.
The following laws show that the branches are selected by success or failure of the condition:
if id then s2 else s3 end = s2
if fail then s2 else s3 end = s3
The ifthenend strategy is an abbreviation for the ifthenelseend with the identity strategy as right branch:
if s1 then s2 end = where(s1) < s2 + id
Examples. The inclusive or or(s1, s2)
succeeds if one of the strategies s1
or s2
succeeds, but guarantees that both are applied, in the order s1
first, then s2
:
or(s1, s2) =
if s1 then try(where(s2)) else where(s2) end
This ensures that any side effects are always performed, in contrast to s1 <\+ s2
, where s2
is only executed if s1
fails.
(Thus, left choice implements a short circuit Boolean or.)
Similarly, the following and(s1, s2)
combinator is the nonshort circuit version of Boolean conjunction:
and(s1, s2) =
if s1 then where(s2) else where(s2); fail end
Switch¶
The switch construct is an nary branching construct similar to its counter parts in other programming languages. It is defined in terms of guarded choice. The switch construct has the following form:
switch s0
case s1 : s1'
case s2 : s2'
...
otherwise : sdef
end
The switch
first applies the s0
strategy to the current term t
resulting in a term t'
.
Then it tries the cases in turn applying each si
to t'
.
As soon as this succeeds the corresponding case is selected and si'
is applied to the t
, the term to which the switch was applied.
If none of the cases applies, the default strategy sdef
from the otherwise
is applied.
The switch
construct is syntactic sugar for a nested ifthenelse:
{x : where(s0 => x);
if <s1> x
then s1'
else if <s2> x
then s2'
else if ...
then ...
else sdef
end
end
end}
NonDeterministic Choice¶
The deterministic left choice operator prescribes that the left alternative should be tried before the right alternative, and that the latter is only used if the first fails. There are applications where it is not necessary to define the order of the alternatives. In those cases nondeterministic choice can be used.
The nondeterministic choice operator s1 + s2
chooses one of the two strategies s1
or s2
to apply, such that the one it chooses succeeds.
If both strategies fail, then the choice fails as well.
Operationally the choice operator first tries one strategy, and, if that fails, tries the other.
The order in which this is done is undefined, i.e., arbitrarily chosen by the compiler.
The +
combinator is used to model modular composition of rewrite rules and strategies with the same name, but in different modules.
Multiple definitions with the same name in different modules, are merged into a single definition with that name, where the bodies are composed with +
.
The following transformation illustrates this:
module A
f = s1
module B
f = s2
module main
imports A B
=>
f = s2 + s1
This transformation is somewhat simplified; the complete transformation needs to take care of local variables and parameters.
While the +
combinator is used internally by the compiler for this purpose, programmers are advised not to use this combinator, but rather use the left choice combinator <+
to avoid surprises.
In the past, the +
combinator was also used to compose definitions with the same name within a module.
This has been replaced by interpreting such compositions with the textual order of the definitions.
The following transformation illustrates this:
module A
f = s1
f = s2
=>
f = s1 <+ s2
Recursion¶
Repeated application of a strategy can be achieved with recursion.
There are two styles for doing this; with a recursive definition or using the fixpoint operator rec
.
A recursive definition is a normal strategy definition with a recursive call in its body.
f(s) = ... f(s) ...
Another way to define recursion is using the fixpoint operator rec x(s)
, which recurses on applications of x within s. For example, the definition
f(s) = rec x(... x ...)
is equivalent to the one above. The advantage of the rec operator is that it allows the definition of an unnamed strategy expression to be recursive. For example, in the definition
g(s) = foo; rec x(... x ...); bar
the strategy between foo and bar is a recursive strategy that does not recurse to g(s)
.
Originally, the rec
operator was the only way to define recursive strategies.
It is still in the language in the first place because it is widely used in many existing programs, and in the second place because it can be a concise expression of a recursive strategy, since call parameters are not included in the call.
Furthermore, all free variables remain in scope.
The repeat
strategy applies a transformation s
until it fails.
It is defined as a recursive definition using try
as follows:
try(s) = s <+ id
repeat(s) = try(s; repeat(s))
An equivalent definition using rec
is:
repeat(s) = rec x(try(s; x))
A Library of Iteration Strategies.¶
Using sequential composition, choice, and recursion a large variety of iteration strategies can be defined. The following definitions are part of the Stratego Library (in module strategy/iteration).
repeat(s) =
rec x(try(s; x))
repeat(s, c) =
(s; repeat(s, c)) <+ c
repeat1(s, c) =
s; (repeat1(s, c) <+ c)
repeat1(s) =
repeat1(s, id)
repeatuntil(s, c) =
s; if c then id else repeatuntil(s, c) end
while(c, s) =
if c then s; while(c, s) end
dowhile(s, c) =
s; if c then dowhile(s, c) end
References¶

Eelco Visser, ZineElAbidine Benaissa, and Andrew P. Tolmach. Building program optimizers with rewriting strategies. In Matthias Felleisen, Paul Hudak, and Christian Queinnec, editors, Proceedings of the third ACM SIGPLAN international conference on Functional programming, 13–26. Baltimore, Maryland, United States, 1998. ACM. URL: http://doi.acm.org/10.1145/289423.289425, doi:10.1145/289423.289425. ↩

Eelco Visser and ZineElAbidine Benaissa. A core language for rewriting. Electronic Notes in Theoretical Computer Science, 15:422–441, 1998. URL: http://dx.doi.org/10.1016/S15710661(05)800271, doi:10.1016/S15710661(05)800271. ↩
Created: May 17, 2023