Congruence Operator
Stratego -- Strategies for Program Transformation
A term consisting of a constructor C and subterms ti:
C(t1, t2, ..., tn)
defines a congruence operator
C(s1, s2, ..., sn)
This is an operator that first matches a term
C(t1, t2,...,tn)
, then
applies
s1
to
t1
,
s2
to
t2
, ...,
sn
to
tn
. This is used
e.g. in conjunction with the recursive traversal operator to define
specific data structure traversals.
For example, using the congruence strategy
FunCall(s1,s2)
is
equivalent to applying
R :
FunCall(a,b) -> FunCall(newa,newb)
where
<s1> a => newa
; <s2> b => newb
which is equivalent to
{a, b, newa, newb :
?FunCall(a,b)
; where(
<s1> a => newa
; <s2> b => newb
)
; !FunCall(newa,newb)
}
This equivalent specification uses
match and
build strategies?, and
variable scopes? indicated by
{}
.
FunCall(s1,s2)
is also equivalent to:
R:
FunCall(a,b) -> FunCall(<s1> a, <s2> b)
This specification uses a rewriting rule and
term projection?.
More exotic congruences
Tuple congruences
(s1,s2,...,sn)
List congruences
[s1,s2,...,sn]
A special list congruence is [] which "visits" the empty list
Distributing congruences
c^D(s1, s2, ..., sn)
c
is term constructor
^D
syntax to denote distributing congruence
s1, ..., sn
are strategies.
The meaning is given by
c^D(s1, ..., sn):
(c(x1, ..., xn), env) -> c(y1, ..., yn)
where
<s1> (x1, env) => y1
; <s2> (x2, env) => y2
; ...
; <sn> (xn, env) => yn
Threading congruences
c^T(s1, s2, ..., sn)
c
is term constructor
^T
is syntax to denote threading congruence
The meaning is given by:
c^T(s1, ..., sn):
(c(x1, ..., xn), e-first) -> (c(y1, ..., yn), e-last))
where
<s1> (x1, e-first) => (y1, e2)
; <s2> (x2, e2) => (y2, e3)
; ...
; <sn> (xn, en) => (yn, e-last)
CategoryGlossary