Table of Contents
In Chapter 13 we saw a number of idioms of strategic rewriting, which all involved tree traversal. In the previous chapters we saw how strategies can be used to control transformations and how rules can be broken down into the primitive actions match, build and scope. The missing ingredient are combinators for defining traversals.
There are many ways to traverse a tree. For example, a bottom-up
traversal, visits the subterms of a node before it visits the node
itself, while a top-down traversal visits nodes before it visits
children. One-pass traversals traverse the tree one time, while
fixed-point traversals, such as innermost, repeatedly
traverse a term until a normal form is reached.
It is not desirable to provide built-in implementations for all traversals needed in transformations, since such a collection would necessarily be imcomplete. Rather we would like to define traversals in terms of the primitive ingredients of traversal. For example, a top-down, one-pass traversal strategy will first visit a node, and then descend to the children of a node in order to recursively traverse all subterms. Similarly, the bottom-up, fixed-point traversal strategy innermost, will first descend to the children of a node in order to recursively traverse all subterms, then visit the node itself, and possibly recursively reapply the strategy.
Traversal in Stratego is based on the observation that a full term traversal is a recursive closure of a one-step descent, that is, an operation that applies a strategy to one or more direct subterms of the subject term. By separating this one-step descent operator from recursion, and making it a first-class operation, many different traversals can be defined.
In this chapter we explore the ways in which Stratego supports the definition of traversal strategies. We start with explicitly programmed traversals using recursive traversal rules. Next, congruences operators provide a more concise notation for such data-type specific traversal rules. Finally, generic traversal operators support data type independent definitions of traversals, which can be reused for any data type. Given these basic mechanisms, we conclude with an an exploration of idioms for traversal and standard traversal strategies in the Stratego Library.
In Chapter 16 we saw
the following definition of the map strategy, which
applies a strategy to each element of a list:
map(s) : [] -> [] map(s) : [x | xs] -> [<s> x | <map(s)> xs]
The definition uses explicit recursive calls to the strategy in the
right-hand side of the second rule.
What map does is to traverse the
list in order to apply the argument strategy to all elements.
We can use the same technique to other term structures as well.
We will explore the definition of traversals using the propositional formulae from Chapter 13, where we introduced the following rewrite rules:
module prop-rules imports libstrategolib prop rules DefI : Impl(x, y) -> Or(Not(x), y) DefE : Eq(x, y) -> And(Impl(x, y), Impl(y, x)) DN : Not(Not(x)) -> x DMA : Not(And(x, y)) -> Or(Not(x), Not(y)) DMO : Not(Or(x, y)) -> And(Not(x), Not(y)) DAOL : And(Or(x, y), z) -> Or(And(x, z), And(y, z)) DAOR : And(z, Or(x, y)) -> Or(And(z, x), And(z, y)) DOAL : Or(And(x, y), z) -> And(Or(x, z), Or(y, z)) DOAR : Or(z, And(x, y)) -> And(Or(z, x), Or(z, y))
In Chapter 13 we saw how a
functional style of rewriting could be encoded using extra
constructors. In Stratego we can achieve a similar approach by using
rule names, instead of extra constructors. Thus, one way to achieve
normalization to disjunctive normal form, is the use of an
explicitly programmed traversal, implemented using recursive rules,
similarly to the map example above:
module prop-dnf4 imports libstrategolib prop-rules strategies main = io-wrap(dnf) rules dnf : True -> True dnf : False -> False dnf : Atom(x) -> Atom(x) dnf : Not(x) -> <dnfred> Not (<dnf>x) dnf : And(x, y) -> <dnfred> And (<dnf>x, <dnf>y) dnf : Or(x, y) -> Or (<dnf>x, <dnf>y) dnf : Impl(x, y) -> <dnfred> Impl(<dnf>x, <dnf>y) dnf : Eq(x, y) -> <dnfred> Eq (<dnf>x, <dnf>y) strategies dnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf)
The dnf rules recursively apply themselves to the
direct subterms and then apply dnfred to actually apply
the rewrite rules.
We can reduce this program by abstracting over the base cases. Since
there is no traversal into True, False,
and Atoms, these rules can be be left out.
module prop-dnf5 imports libstrategolib prop-rules strategies main = io-wrap(dnf) rules dnft : Not(x) -> <dnfred> Not (<dnf>x) dnft : And(x, y) -> <dnfred> And (<dnf>x, <dnf>y) dnft : Or(x, y) -> Or (<dnf>x, <dnf>y) dnft : Impl(x, y) -> <dnfred> Impl(<dnf>x, <dnf>y) dnft : Eq(x, y) -> <dnfred> Eq (<dnf>x, <dnf>y) strategies dnf = try(dnft) dnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf)
The dnf strategy is now defined in terms of the
dnft rules, which implement traversal over the
constructors. By using try(dnft), terms for which no
traversal rule has been specified are not transformed.
We can further simplify the definition by observing that the
application of dnfred does not necessarily have to take
place in the right-hand side of the traversal rules.
module prop-dnf6 imports libstrategolib prop-rules strategies main = io-wrap(dnf) rules dnft : Not(x) -> Not (<dnf>x) dnft : And(x, y) -> And (<dnf>x, <dnf>y) dnft : Or(x, y) -> Or (<dnf>x, <dnf>y) dnft : Impl(x, y) -> Impl(<dnf>x, <dnf>y) dnft : Eq(x, y) -> Eq (<dnf>x, <dnf>y) strategies dnf = try(dnft); dnfred dnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf)
In this program dnf first calls dnft to
transform the subterms of the subject term, and then calls
dnfred to apply the transformation rules (and possibly
a recursive invocation of dnf).
The program above has two problems. First, the traversal behaviour
is mostly uniform, so we would like to specify that more
concisely. We will address that concern below. Second, the traversal
is not reusable, for example, to define a conjunctive normal form
transformation. This last concern can be addressed by factoring out
the recursive call to dnf and making it a parameter of
the traversal rules.
module prop-dnf7 imports libstrategolib prop-rules strategies main = io-wrap(dnf) rules proptr(s) : Not(x) -> Not (<s>x) proptr(s) : And(x, y) -> And (<s>x, <s>y) proptr(s) : Or(x, y) -> Or (<s>x, <s>y) proptr(s) : Impl(x, y) -> Impl(<s>x, <s>y) proptr(s) : Eq(x, y) -> Eq (<s>x, <s>y) strategies dnf = try(proptr(dnf)); dnfred dnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf) cnf = try(proptr(cnf)); cnfred cnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf)
Now the traversal rules are reusable and used in two different
transformations, by instantiation with a call to the particular
strategy in which they are used (dnf or
cnf).
But we can do better, and also make the composition of this strategy reusable.
module prop-dnf8 imports libstrategolib prop-rules strategies main = io-wrap(dnf) rules proptr(s) : Not(x) -> Not (<s>x) proptr(s) : And(x, y) -> And (<s>x, <s>y) proptr(s) : Or(x, y) -> Or (<s>x, <s>y) proptr(s) : Impl(x, y) -> Impl(<s>x, <s>y) proptr(s) : Eq(x, y) -> Eq (<s>x, <s>y) strategies propbu(s) = proptr(propbu(s)); s strategies dnf = propbu(dnfred) dnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf) cnf = propbu(cnfred) cnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf)
That is, the propbu(s) strategy defines a complete
bottom-up traversal over propostion terms, applying the strategy
s to a term after transforming its subterms. The
strategy is completely independent of the dnf and
cnf transformations, which instantiate the strategy
using the dnfred and cnfred strategies.
Come to think of it, dnfred and cnfred are
somewhat useless now and can be inlined directly in the
instantiation of the propbu(s) strategy:
module prop-dnf9 imports libstrategolib prop-rules strategies main = io-wrap(dnf) rules proptr(s) : Not(x) -> Not (<s>x) proptr(s) : And(x, y) -> And (<s>x, <s>y) proptr(s) : Or(x, y) -> Or (<s>x, <s>y) proptr(s) : Impl(x, y) -> Impl(<s>x, <s>y) proptr(s) : Eq(x, y) -> Eq (<s>x, <s>y) strategies propbu(s) = proptr(propbu(s)); s strategies dnf = propbu(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf)) cnf = propbu(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf))
Now we have defined a transformation independent traversal strategy that is specific for proposition terms.
Next we consider cheaper ways for defining the traversal rules, and then ways to get completely rid of them.
The definition of the traversal rules above frequently occurs in the
definition of transformation strategies.
Congruence operators provide a convenient abbreviation of precisely
this operation.
A congruence operator applies a strategy to each direct subterm of a
specific constructor.
For each n-ary constructor c declared in a signature, there is a
corresponding congruence operator c(s1 ,
..., sn), which applies to terms of the form c(t1 ,
..., tn) by applying the argument strategies to the
corresponding argument terms.
A congruence fails if the application of one the argument strategies
fails or if constructor of the operator and that of the term do not
match.
Example. For example, consider the following signature of expressions:
module expressions
signature
sorts Exp
constructors
Int : String -> Exp
Var : String -> Exp
Plus : Exp * Exp -> Exp
Times : Exp * Exp -> Exp
The following Stratego Shell session applies the congruence
operators Plus and Times to a term:
stratego>import expressionsstratego>!Plus(Int("14"),Int("3")) Plus(Int("14"),Int("3"))stratego>Plus(!Var("a"), id) Plus(Var("a"),Int("3"))stratego>Times(id, !Int("42")) command failed
The first application shows how a congruence transforms a specific subterm, that is the strategy applied can be different for each subterm. The second application shows that a congruence only succeeds for terms constructed with the same constructor.
The import at the start of the session is necessary to
declare the constructors used; the definitions of congruences are
derived from constructor declarations.
Forgetting this import would lead to a complaint about an undeclared
operator:
stratego>!Plus(Int("14"),Int("3")) Plus(Int("14"),Int("3"))stratego>Plus(!Var("a"), id) operator Plus/(2,0) not defined command failed
Defining Traversals with Congruences.
Now we return to our dnf/cnf example, to
see how congruence operators can help in their implementation.
Since congruence operators basically define a one-step traversal for
a specific constructor, they capture the traversal rules defined above.
That is, a traversal rule such as
proptr(s) : And(x, y) -> And(<s>x, <s>y)
can be written by the congruence And(s,s).
Applying this to the prop-dnf program we can replace
the traversal rules by congruences as follows:
module prop-dnf10 imports libstrategolib prop-rules strategies main = io-wrap(dnf) strategies proptr(s) = Not(s) <+ And(s, s) <+ Or(s, s) <+ Impl(s, s) <+ Eq(s, s) propbu(s) = proptr(propbu(s)); s strategies dnf = propbu(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf)) cnf = propbu(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf))
Observe how the five traversal rules have been reduced to five congruences which fit on a single line.
Traversing Tuples and Lists.
Congruences can also be applied to tuples,
(s1,s2,...,sn), and lists,
[s1,s2,...,sn]. A special list congruence is
[] which 'visits' the empty list.
As an example, consider again the definition of map(s)
using recursive traversal rules:
map(s) : [] -> [] map(s) : [x | xs] -> [<s> x | <map(s)> xs]
Using list congruences we can define this strategy as:
map(s) = [] <+ [s | map(s)]
The [] congruence matches an empty list. The [s |
map(s)] congruence matches a non-empty list, and applies
s to the head of the list and map(s) to
the tail. Thus, map(s) applies s to each
element of a list:
stratego>import liblibstratego>![1,2,3] [1,2,3]stratego>map(inc) [2,3,4]
Note that map(s) only succeeds if s
succeeds for each element of the list.
The fetch and filter strategies are
variations on map that use the failure of
s to list elements.
fetch(s) = [s | id] <+ [id | fetch(s)]
The fetch strategy traverses a list
until it finds a element for which
s succeeds and then stops. That element is the only one
that is transformed.
filter(s) = [] + ([s | filter(s)] <+ ?[ |<id>]; filter(s))
The filter strategy applies s to each
element of a list, but only keeps the elements for which it
succeeds.
stratego>import liblibstratego>even = where(<eq>(<mod>(<id>,2),0))stratego>![1,2,3,4,5,6,7,8] [1,2,3,4,5,6,7,8]stratego>filter(even) [2,4,6,8]
Format Checking. Another application of congruences is in the definition of format checkers. A format checker describes a subset of a term language using a recursive pattern. This can be used to verify input or output of a transformation, and for documentation purposes. Format checkers defined with congruences can check subsets of signatures or regular tree grammars. For example, the subset of terms of a signature in a some normal form.
As an example, consider checking the output of the dnf
and cnf transformations.
conj(s) = And(conj(s), conj(s)) <+ s disj(s) = Or (disj(s), disj(s)) <+ s // Conjunctive normal form conj-nf = conj(disj(Not(Atom(x)) <+ Atom(x))) // Disjunctive normal form disj-nf = disj(conj(Not(Atom(x)) <+ Atom(x)))
The strategies conj(s) and disj(s) check
that the subject term is a conjunct or a disjunct, respectively,
with terms satisfying s at the leaves.
The strategies conj-nf and disj-nf check
that the subject term is in conjunctive or disjunctive normal form,
respectively.
Using congruence operators we constructed a generic,
i.e. transformation independent, bottom-up traversal for proposition
terms. The same can be done for other data types. However, since the
sets of constructors of abstract syntax trees of typical programming
languages can be quite large, this may still amount to quite a bit
of work that is not reusable across data types;
even though a strategy such as `bottom-up traversal', is basically
data-type independent.
Thus, Stratego provides generic traversal by means of several
generic one-step descent operators. The
operator all, applies a strategy to all direct
subterms. The operator one, applies a strategy to one
direct subterm, and the operator some, applies a
strategy to as many direct subterms as possible, and at least one.
The all(s) strategy transforms a constructor
application by applying the parameter strategy s to
each direct subterm. An application of all(s) fails if
the application to one of the subterms fails.
The following example shows how all (1) applies to any
term, and (2) applies its argument strategy uniformly to all direct
subterms. That is, it is not possible to do something special for a
particular subterm (that's what congruences are for).
stratego>!Plus(Int("14"),Int("3")) Plus(Int("14"),Int("3"))stratego>all(!Var("a")) Plus(Var("a"),Var("a"))stratego>!Times(Var("b"),Int("3")) Times(Var("b"),Int("3"))stratego>all(!Var("z")) Times(Var("z"),Var("z"))
The all(s) operator is really the ultimate replacement
for the traversal rules that we saw above. Instead of specifying a
rule or congruence for each constructor, the single application of
the all operator takes care of traversing all
constructors.
Thus, we can replace the propbu strategy by a
completely generic definition of bottom-up traversal. Consider again
the last definition of propbu:
proptr(s) = Not(s) <+ And(s, s) <+ Or(s, s) <+ Impl(s, s) <+ Eq(s, s) propbu(s) = proptr(propbu(s)); s
The role of proptr(s) in this definition can be
replaced by all(s), since that achieves exactly the
same, namely applying s to the direct subterms of
constructors:
propbu(s) = all(propbu(s)); s
However, the strategy now is completely generic, i.e. independent of
the particular structure it is applied to. In the Stratego Library
this strategy is called bottomup(s), and defined as
follows:
bottomup(s) = all(bottomup(s)); s
It first recursively transforms the subterms of the subject term and
then applies s to the result.
Using this definition, the normalization of propositions now reduces
to the following module, which is only concerned with the selection
and composition of rewrite rules:
module prop-dnf11 imports libstrategolib prop-rules strategies main = io-wrap(dnf) strategies dnf = bottomup(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf)) cnf = bottomup(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf))
In fact, these definitions still contain a reusable pattern. With a little squinting we see that the definitions match the following pattern:
dnf = bottomup(try(dnf-rules; dnf)) cnf = bottomup(try(cnf-rules; cnf))
In which we can recognize the definition of innermost reduction, which the Stratego Library defines as:
innermost(s) = bottomup(try(s; innermost(s)))
The innermost strategy performs a bottom-up traversal
of a term. After transforming the subterms of a term it tries to
apply the transformation s. If succesful the result is
recursively transformed with an application of
innermost.
This brings us to the final form for the proposition normalizations:
module prop-dnf12 imports libstrategolib prop-rules strategies main = io-wrap(dnf) strategies dnf = innermost(DN <+ DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR) cnf = innermost(DN <+ DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR)
Different transformations can be achieved by using a selection of rules and a strategy, which is generic, yet defined in Stratego itself using strategy combinators.
The one(s) strategy transforms a constructor
application by applying the parameter strategy s to
exactly one direct subterm. An application of one(s)
fails if the application to all of the subterms fails.
The following Stratego Shell session illustrates the behaviour of
the combinator:
stratego>!Plus(Int("14"),Int("3")) Plus(Int("14"),Int("3"))stratego>one(!Var("a")) Plus(Var("a"),Int("3"))stratego>one(\ Int(x) -> Int(<addS>(x,"1")) \ ) Plus(Var("a"),Int("4"))stratego>one(?Plus(_,_)) command failed
A frequently used application of one is the
oncetd(s) traversal, which performs a left to right
depth first search/transformation that stops as soon as
s has been successfuly applied.
oncetd(s) = s <+ one(oncetd(s))
Thus, s is first applied to the root of the subject
term. If that fails, its direct subterms are searched one by one
(from left to right), with a recursive call to
oncetd(s).
An application of oncetd is the
contains(|t) strategy, which checks whether the subject
term contains a subterm that is equal to t.
contains(|t) = oncetd(?t)
Through the depth first search of oncetd, either an
occurrence of t is found, or all subterms are verified
to be unequal to t.
Here are some other one-pass traversals using the one
combinator:
oncebu(s) = one(oncebu(s)) <+ s spinetd(s) = s; try(one(spinetd(s))) spinebu(s) = try(one(spinebu(s))); s
Exercise: figure out what these strategies do.
Here are some fixe-point traversals, i.e., traversals that apply their argument transformation exhaustively to the subject term.
reduce(s) = repeat(rec x(one(x) + s)) outermost(s) = repeat(oncetd(s)) innermostI(s) = repeat(oncebu(s))
The difference is the subterm selection strategy. Exercise: create rewrite rules and terms that demonstrate the differences between these strategies.
The some(s) strategy transforms a constructor
application by applying the parameter strategy s to as
many direct subterms as possible and at least one. An application of
some(s) fails if the application to all of the subterms
fails.
Some one-pass traversals based on some:
sometd(s) = s <+ some(sometd(s)) somebu(s) = some(somebu(s)) <+ s
A fixed-point traversal with some:
reduce-par(s) = repeat(rec x(some(x) + s))
Above we have seen the basic mechanisms for defining traversals in Stratego: custom traversal rules, data-type specific congruence operators, and generic traversal operators. Term traversals can be categorized into classes according to how much of the term they traverse and to which parts of the term they modify. We will consider a number of idioms and standard strategies from the Stratego Library that are useful in the definition of traversals.
One class of traversal strategies performs a full
traversal, that is visits and transforms every subterm of
the subject term.
We already saw the bottomup strategy defined as
bottomup(s) = all(bottomup(s)); s
It first visits the subterms of the subject term, recursively
transforming its subterms, and then applies the
transformation s to the result.
A related strategy is topdown, which is defined as
topdown(s) = s; all(topdown(s))
It first transforms the subject therm and then visits the subterms of the result.
A combination of topdown and bottomup is
downup, defined as
downup(s) = s; all(downup(s)); s
It applies s on the way down the tree, and again on the
way up.
A variation is downup(2,0)
downup(s1, s2) = s1; all(downup(s1, s2)); s2
which applies one strategy on the way down and another on the way up.
Since the parameter strategy is applied at every subterm, these
traversals only succeed if it succeeds everywhere. Therefore, these
traversals are typically applied in combination with
try or repeat.
topdown(try(R1 <+ R2 <+ ...))
This has the effect that the rules are tried at each subterm. If none of the rules apply the term is left as it was and traversal continues with its subterms.
Choosing a Strategy. The strategy to be used for a particular transformation depends on the rules and the goal to be achieved.
For example, a constant folding transformation for proposition
formulae can be defined as a bottom-up traversal that tries to apply
one of the truth-rules T at each subterm:
T : And(True(), x) -> x T : And(x, True()) -> x T : And(False(), x) -> False() T : And(x, False()) -> False() T : Or(True(), x) -> True() T : Or(x, True()) -> True() T : Or(False(), x) -> x T : Or(x, False()) -> x T : Not(False()) -> True() T : Not(True()) -> False() eval = bottomup(try(T))
Bottomup is the strategy of choice here because it evaluates
subterms before attempting to rewrite a term.
An evaluation strategy using topdown
eval2 = topdown(try(T)) // bad strategy
does not work as well, since it attempts to rewrite terms before their subterms have been reduced, thus missing rewriting opportunities. The following Stratego Shell session illustrates this:
stratego>!And(True(), Not(Or(False(), True()))) And(True,Not(Or(False,True)))stratego>eval Falsestratego>!And(True(), Not(Or(False(), True()))) And(True,Not(Or(False,True)))stratego>eval2 Not(True)
Exercise: find other terms that show the difference between these strategies.
On the other hand, a desugaring transformation for propositions,
which defines implication and equivalence in terms of other
connectives is best defined as a topdown traversal
which tries to apply one of the rules DefI or
DefE at every subterm.
DefI : Impl(x, y) -> Or(Not(x), y) DefE : Eq(x, y) -> And(Impl(x, y), Impl(y, x)) desugar = topdown(try(DefI <+ DefE))
Since DefE rewrites Eq terms to terms
involving Impl, a strategy with bottomup
does not work.
desugar2 = bottomup(try(DefI <+ DefE)) // bad strategy
Since the subterms of a node are traversed
before the node itself is visited, this
transformation misses the desugaring of the implications
(Impl) originating from the application of the
DefE rule.
The following Shell session illustrates this:
stratego>!Eq(Atom("p"), Atom("q")) Eq(Atom("p"),Atom("q"))stratego>desugar And(Or(Not(Atom("p")),Atom("q")),Or(Not(Atom("q")),Atom("p")))stratego>!Eq(Atom("p"), Atom("q")) Eq(Atom("p"),Atom("q"))stratego>desugar2 And(Impl(Atom("p"),Atom("q")),Impl(Atom("q"),Atom("p")))
Repeated Application.
In case one rule produces a term to which another desugaring rule
can be applied, the desugaring strategy should repeat the
application of rules to each subterm.
Consider the following rules and strategy for desugaring
propositional formulae to implicative normal form (using only
implication and False).
DefT : True() -> Impl(False(), False()) DefN : Not(x) -> Impl(x, False()) DefA2 : And(x, y) -> Not(Impl(x, Not(y))) DefO1 : Or(x, y) -> Impl(Not(x), y) DefE : Eq(x, y) -> And(Impl(x, y), Impl(y, x)) impl-nf = topdown(repeat(DefT <+ DefN <+ DefA2 <+ DefO1 <+ DefE))
Application of the rules with try instead of
repeat
impl-nf2 = topdown(try(DefT <+ DefN <+ DefA2 <+ DefO1 <+ DefE)) // bad strategy
is not sufficient, as shown by the following Shell session:
stratego>!And(Atom("p"),Atom("q")) And(Atom("p"),Atom("q"))stratego>impl-nf Impl(Impl(Atom("p"),Impl(Atom("q"),False)),False)stratego>!And(Atom("p"),Atom("q")) And(Atom("p"),Atom("q"))stratego>impl-nf2 Not(Impl(Atom("p"),Impl(Atom("q"),False)))
Note that the Not is not desugared with
impl-nf2.
Paramorphism. A variation on bottomup is a traversal that also provides the original term as well as the term in which the direct subterms have been transformed. (Also known as a paramorphism?)
bottomup-para(s) = <s>(<id>, <all(bottomup-para(s))>)
This is most useful in a bottom-up traversal; the original term is always available in a top-down traversal.
Exercise: give an example application of this strategy
Cascading transformations are transformations upon
transformations. While the full traversals discussed above walk over
the tree once, cascading transformations apply multiple `waves' of
transformations to the nodes in the tree.
The prototypical example is the innermost strategy,
which exhaustively applies a transformation, typically a set of
rules, to a tree.
simplify = innermost(R1 <+ ... <+ Rn)
The basis of innermost is a bottomup
traversal that tries to apply the transformation at each node after
visiting its subterms.
innermost(s) = bottomup(try(s; innermost(s)))
If the transformation s succeeds, the result term is
transformed again with a recursive call to innermost.
Application of innermost exhaustively applies
one set of rules to a tree.
Using sequential composition we can apply several
stages of reductions.
A special case of such a staged transformation,
is known as sequence of normal forms (in the
TAMPR system):
simplify = innermost(A1 <+ ... <+ Ak) ; innermost(B1 <+ ... <+ Bl) ; ... ; innermost(C1 <+ ... <+ Cm)
At each stage the term is reduced with respect to a different set of rules.
Of course it is possible to mix different types of transformations in such a stage pipeline, for example.
simplify = topdown(try(A1 <+ ... <+ Ak)) ; innermost(B1 <+ ... <+ Bl) ; ... ; bottomup(repeat(C1 <+ ... <+ Cm))
At each stage a different strategy and different set of rules can be used. (Of course one may use the same strategy several times, and some of the rule sets may overlap.)
While completely generic strategies such as bottomup
and innermost are often useful, there are also
situations where a mixture of generic and data-type specific
traversal is necessary. Fortunately, Stratego allows you to mix
generic traversal operators, congruences, your own traversal and
regular rules, any way you see fit.
A typical pattern for such strategies first tries a number of special cases that deal with traversal themselves. If none of the special cases apply, a generic traversal is used, followed by application of some rules applicable in the general case.
transformation = special-case1 <+ special-case2 <+ special-case3 <+ all(transformation); reduce reduce = ...
Constant Propagation. A typical example is the following constant propagation strategy. It uses the exceptions to the basic generic traversal to traverse the tree in the order of the control-flow of the program that is represented by the term. This program makes use of dynamic rewrite rules, which are used to propagate context-sensitive information through a program. In this case, the context-sensitive information concerns the constant values of some variables in the program, which should be propagated to the uses of those variables. Dynamic rules will be explained in Chapter 20; for now we are mainly concerned with the traversal strategy.
module propconst
imports
liblib
signature
constructors
Var : String -> Exp
Plus : Exp * Exp -> Exp
Assign : String * Exp -> Stat
If : Exp * Stat * Stat -> Stat
While : Exp * Stat -> Stat
strategies
propconst = 
PropConst 
<+ propconst-assign
<+ propconst-if
<+ propconst-while
<+ all(propconst); try(EvalBinOp)
EvalBinOp : 
Plus(Int(i), Int(j)) -> Int(k) where <addS>(i,j) => k
EvalIf :
If(Int("0"), s1, s2) -> s2
EvalIf :
If(Int(i), s1, s2) -> s1 where <not(eq)>(i, "0")
propconst-assign = 
Assign(?x, propconst => e)
; if <is-value> e then
rules( PropConst : Var(x) -> e )
else
rules( PropConst :- Var(x) )
end
propconst-if = 
If(propconst, id, id)
; (EvalIf; propconst
<+ (If(id, propconst, id) /PropConst\ If(id,id,propconst)))
propconst-while = 
While(id,id)
; (/PropConst\* While(propconst, propconst))
is-value = Int(id)
The main strategy of the constant propagation transformation , follows the pattern described
above; a number of special case alternatives followed by a generic
traversal alternative. The special cases are defined in their own
definitions.
Generic traversal is followed by the constant folding rule
EvalBinOp .
The first special case is an application of the dynamic rule
PropConst, which replaces a constant valued variable by
its constant value .
This rule is defined by the second special case strategy,
propconst-assign . It first traverses the
right-hand side of an assignment with an Assign
congruence operator, and a recursive call to
propconst. Then, if the expression evaluated to a
constant value, a new PropConst rule is
defined. Otherwise, any old instance of PropConst for
the left-hand side variable is undefined.
The third special case for If uses congruence operators
to order the application of propconst to its subterms
. The first congruence
applies propconst to the condition expression. Then an
application of the rule EvalIf attempts to eliminate
one of the branches of the statement, in case the condition
evaluated to a constant value. If that is not possible the branches
are visited by two more congruence operator applications joined by a
dynamic rule intersection operator, which distributes the constant
propagation rules over the branches and merges the rules afterwards,
keeping only the consistent ones.
Something similar happens in the case of While
statements .
For details concerning dynamic rules, see Chapter 20.
To see what propconst achieves, consider the following
abstract syntax tree (say in file foo.prg).
Block([
Assign("x", Int("1")),
Assign("y", Int("42")),
Assign("z", Plus(Var("x"), Var("y"))),
If(Plux(Var("a"), Var("z")),
Assign("b", Plus(Var("x"), Int("1"))),
Block([
Assign("z", Int("17")),
Assign("b", Int("2"))
])),
Assign("c", Plus(Var("b"), Plus(Var("z"), Var("y"))))
])
We import the module in the Stratego Shell, read the abstract syntax
tree from file, and apply the propconst transformation
to it:
stratego>import libstrategolibstratego>import propconststratego><ReadFromFile> "foo.prg" ...stratego>propconst Block([Assign("x",Int("1")),Assign("y",Int("42")),Assign("z",Int("43")), If(Plux(Var("a"),Int("43")),Assign("b",Int("2")),Block([Assign("z", Int("17")),Assign("b",Int("2"))])),Assign("c",Plus(Int("2"),Plus( Var("z"),Int("42"))))])
Since the Stratego Shell does not (yet) pretty-print terms, the result is rather unreadable. We can remedy this by writing the result of the transformation to a file, and pretty-printing it on the regular command-line with pp-aterm.
stratego><ReadFromFile> "foo.prg" ...stratego>propconst; <WriteToTextFile> ("foo-pc.prg", <id>) ...stratego>:quit ...$pp-aterm -i foo-pc.prg Block( [ Assign("x", Int("1")) , Assign("y", Int("42")) , Assign("z", Int("43")) , If( Plux(Var("a"), Int("43")) , Assign("b", Int("2")) , Block( [Assign("z", Int("17")), Assign("b", Int("2"))] ) ) , Assign( "c" , Plus(Int("2"), Plus(Var("z"), Int("42"))) ) ] )
Compare the result to the original program and try to figure out what has happened and why that is correct. (Assuming the `usual' semantics for this type of imperative language.)
Generic Strategies with Exceptional Cases.
Patterns for mixing specific and generic traversal can be captured
in parameterized strategies such as the following. They are
parameterized with the usual transformation parameter s
and with a higher-order strategy operator stop, which
implements the special cases.
topdownS(s, stop: (a -> a) * b -> b) = rec x(s; (stop(x) <+ all(x))) bottomupS(s, stop: (a -> a) * b -> b) = rec x((stop(x) <+ all(x)); s) downupS(s, stop: (a -> a) * b -> b) = rec x(s; (stop(x) <+ all(x)); s) downupS(s1, s2, stop: (a -> a) * b -> b) = rec x(s1; (stop(x) <+ all(x)); s2)
While normal strategies (parameters) are functions from terms to
terms, the stop parameter is a function from strategies
to strategies. Such exceptions to the default have to be declared
explicitly using a type annotation.
Note that the bottomupS strategy is slightly different
from the pattern of the propconst strategy; instead of
applying s only after the generic
traversal case, it is here applied in all cases.
However, the added value of these strategies is not very high. The
payoff in the use of generic strategies is provided by the basic
generic traversal operators, which provide generic behaviour for all
constructors. The stop callback can make it harder to
understand the control-flow structure of a strategy; use with care
and don't overdo it.
Separate rules and strategies
While it is possible to construct your own strategies by mixing traversal elements and rules, in general, it is a good idea to try to get a clean separation between pure rewrite rules and a (simple) strategy that applies them.
The full traversals introduced above mostly visit all nodes in the tree. Now we consider traversals that visit only some of the nodes of a tree.
The oncet and oncebu strategies apply the
argument strategy s at one position in the tree. That
is, application is tried at every node along the traversal until it
succeeds.
oncetd(s) = s <+ one(oncetd(s)) oncebu(s) = one(oncebu(s)) <+ s
The sometd and somebu strategies are
variations on oncet and oncebu that apply
s at least once at some positions, but possibly many
times. As soon as one is found, searching is stopped, i.e., in the
top-down case searching in subtrees is stopped, in bottom-up case,
searching in upper spine is stopped.
sometd(s) = s <+ some(sometd(s)) somebu(s) = some(somebu(s)) <+ s
Similar strategies that find as many applications as possible, but at
least one, can be built using some:
manybu(s) = rec x(some(x); try(s) <+ s) manytd(s) = rec x(s; all(try(x)) <+ some(x))
somedownup(s) = rec x(s; all(x); try(s) <+ some(x); try(s))
The alltd(s) strategy stops as soon as it has found a
subterm to which s can be succesfully applied.
alltd(s) = s <+ all(alltd(s))
If s does not succeed, the strategy is applied
recursively at all direct subterms. This means that s
is applied along a frontier of the subject term. This strategy is
typically used in substitution operations in which subterms are
replaced by other terms. For example, the strategy
alltd(?Var(x); !e) replaces all occurrences of
Var(x) by e.
Note that alltd(try(s)) is not a useful strategy.
Since try(s) succeeds at the root of the term, no
traversal is done.
A typical application of alltd is the definition of
local transformations, that only apply to some specific subterm.
transformation =
alltd(
trigger-transformation
; innermost(A1 <+ ... <+ An)
)
Some relatives of alltd that add a strategy to apply on
the way up.
alldownup2(s1, s2) = rec x((s1 <+ all(x)); s2) alltd-fold(s1, s2) = rec x(s1 <+ all(x); s2)
Finally, the following strategies select the leaves of a tree, where the determination of what is a leaf is upto a parameter strategy.
leaves(s, is-leaf, skip: a * (a -> a) -> a) = rec x((is-leaf; s) <+ skip(x) <+ all(x)) leaves(s, is-leaf) = rec x((is-leaf; s) <+ all(x))
A spine of a term is a chain of nodes from the root to some
subterm. spinetd goes down one spine and applies
s along the way to each node on the spine. The
traversal stops when s fails for all children of a
node.
spinetd(s) = s; try(one(spinetd(s))) spinebu(s) = try(one(spinebu(s))); s spinetd'(s) = s; (one(spinetd'(s)) + all(fail)) spinebu'(s) = (one(spinebu'(s)) + all(fail)); s
Apply s everywhere along al spines where s
applies.
somespinetd(s) = rec x(s; try(some(x))) somespinebu(s) = rec x(try(some(x)); s) spinetd'(s) = rec x(s; (one(x) + all(fail))) spinebu'(s) = rec x((one(x) + all(fail)); s)
While these strategies define the notion of applying along a spine, they are rarely used. In practice one would use more specific traversals with that determine which subterm to include in the search for a path.
TODO: examples
TODO: format checking
TODO: matching of complex patterns
TODO: contextual rules (local traversal)
We have seen that tree traversals can be defined in several ways.
Recursive traversal rules allow finegrained specification of a
traversal, but usually require too much boilerplate code.
Congruence operators provide syntactic sugar for traversal rules
that apply a strategy to each direct subterm of a term.
The generic traversal operators all, one,
and some allow consise, data-type independent
implementation of traversals.
A host of traversal strategies can be obtained by a combination of
the strategy combinators from the previous chapters with these
traversal operators.