Overlay Definition
Stratego -- Strategies for Program Transformation
Abstracting over Term Patterns with Overlays
Overlays are abstractions over term patterns that can be used just like ordinary term constructors.
Overlays can be used to abstract from complex term patterns.
For example, the following overlays define a term language on top of
AsFixTerms
:
signature
sorts AsFixTerm
constructors
layout : Sort
lit : String -> Sort
sort : String -> Sort
lex : Sort ->; Sort
prod : List(Sort) * Sort * List(Attr) -> Prod
appl : Prod * List(AsFixTerm) -> AsFixTer
overlays
DefaultLayout = " "
BinOp(o) =
prod([sort("E"), layout, lit(o), layout, sort("E")], sort("E"), [])
BinExp(x, l1, o, l2, y) =
appl(BinOp(o), [x, l1, lit(o), l2, y])
Add(x, l1, l2, y) = BinExp(x, l1, "+", l2, y)
Mul(x, l1, l2, y) = BinExp(x, l1, "*", l2, y)
Var(x) = appl(prod([lex(sort("Id"))], sort("E"), []), [x])
This makes it possible to write rules over
AsFixTerms
in terms of these higher level pseudo constructors:
rules
Dist : Mul(x, l1, l2, Add(y, l3, l4, z)) ->
Add(Mul(x, l1, l2, y), l3, l4, Mul(x, z))
Note that
AsFixTerms
preserve layout from the source code and that the rule Dist defines how to preserve layout through transformations.
Two limitations of overlays have been resolved:
Overlays can be overloaded and can define default build terms. In the example above, we would like to further abstract and also provide pseudo constructors that do not care about layout:
overlays
Add(x, y) = BinExp(x, "+", y)
Mul(x, y) = BinExp(x, "*", y)
So that we can write
rules
Dist : Mul(x, Add(y, z)) -> Add(Mul(x, y), Mul(x, z))
This is now possible because overlays can be overloaded, i.e., overlays with the same name but different arity can be defined.
To define
BinExp/3
it is necessary to do something with the layout, for example:
overlays
BinExp(x, o, y) =
appl(BinOp(o), [x, DefaultLayout, lit(o), DefaultLayout, y])
This requires that all layout has the form
DefaultLayout
(i.e., " ")
when matching and traversing the term with a congruence.
Overlays can use build default terms to indicate subterms that can be ignored during matching and in traversal, but need a default value when constructing an instance.
BinExp(x, o, y) =
appl(BinOp(o), [x, _ DefaultLayout, lit(o), _ DefaultLayout, y])
The last definition uses the pattern _
DefaultLayout
to indicate that the terms at those positions can be ignored during matching and during congruence traversal. That is, the overlay definition has the following meaning
?BinExp(x, o, y) ->
?appl(BinOp(o), [x, _, lit(o), _, y])
!BinExp(x, o, y) ->
!appl(BinOp(o), [x, DefaultLayout, lit(o), DefaultLayout, y])
BinExp(x, o, y) -> // as congruence
appl(BinOp(o), [x, id, lit(o), id, y])