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