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:

    sorts AsFixTerm
      layout : Sort
      lit   : String -> Sort
      sort   : String -> Sort
      lex   : Sort ->; Sort
      prod   : List(Sort) * Sort * List(Attr) -> Prod
      appl   : Prod * List(AsFixTerm) -> AsFixTer
    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:

    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:

    Add(x, y) = BinExp(x, "+", y)
    Mul(x, y) = BinExp(x, "*", y)

So that we can write

    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:

    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])