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