Rewriting modifier example

 

We'll use the following example, extracted from a query optimizer for a subset of the relational calculus, to demonstrate the use of the rewriting modifiers.

The query optimizer transforms the following abstract syntax, defined as a set of Prop's datatypes.

datatype List<T> = #[] | #[ T ... List<T> ];
datatype Literal = INT int
                 | STRING const char *
                 | BOOL Bool

and      Exp     = OP Id, Exps
                 | APP Id, Exps
                 | LIT Literal
                 | ID Id
                 | TUPLE Exps                  // [ E1, E2, ... En ]
                 | FORALL Id, Exp, Exp         // forall x in E1 . E2
                 | EXISTS Id, Exp, Exp         // exists x in E1 . E2
                 | GUARD (Exp, Exp)            //
                 | GENERATOR (Ids, Exps, Exp)  // [x_1,...,x_n] in X_1*...*X_n
                 | LET  (Id, Exp, Exp)

law inline Int  i    = LIT(INT i)
|   inline Boolean b = LIT(BOOL b)
|          True      = Boolean true
|          False     = Boolean false
|   inline And a,b   = OP("and",#[a,b])
|   inline Or  a,b   = OP("or", #[a,b])
|   inline Not a     = OP("not",#[a])
|   inline Eq a,b    = OP("=",  #[a,b])
|   inline Ne a,b    = OP("/=", #[a,b])
|   inline Gt a,b    = OP(">",  #[a,b])
|   inline Ge a,b    = OP(">=", #[a,b])
|   inline Lt a,b    = OP("<",  #[a,b])
|   inline Le a,b    = OP("<=", #[a,b])
|   inline In a,b    = OP("in", #[a,b])
|   inline Union a,b = OP("union", #[a,b])
|   inline Count a   = OP("#", #[a])

where type Id         = const char *
and        Ids        = List<Id>
and        Exps       = List<Exp>
;

Note that existential and universal quantifiers are represented by the constructors FORALL and EXISTS respectively. For example, $x Î A.p is presented as the term EXISTS(x,A,p). Here x is a binding occurrence for x; note that the variable x may occur within the predicate p. In addition, a list comprehension expression such as
is represented as the compound term

Suppose we'll like to rename all variables in a query Q so that no two binding occurrences are given the same name. This can be easily accomplished using a combination of preorder: and postorder: rules in the following manner:

(i) Use preorder rules to check for new variable bindings, for example in EXISTS(x,A,p). For each new binding occurrence for x, create a new name for x. These will be performed before the subterms A and p are traversed.
(ii) Whenever a variable x is found during the sub-traversal of A and p, rename the variable by looking up its new name.
(iii) Finally, use postorder rules to remove the current variable substitution whenever we're exiting a binding occurrence.

For example, the following set of rewriting rules accomplish this renaming task for our query language using exactly this method.

rewrite RemoveDuplicateNames
{
   // We use before and after rules to remove duplicates from variable names.
   // As each new binding occurrence is found, we enter a new binding
   // into the current environment.  Identifiers found within
   // the binding occurrence are then renamed.

preorder: // insert new bindings
   EXISTS(x,_,_):     { new_binding(x); }
|  FORALL(x,_,_):     { new_binding(x); }
|  GENERATOR(xs,_,_): { new_binding(xs); }
|  LET(x,_,_):        { new_binding(x); }

         // rename variables
|  ID x:             { rename(x); }

postorder: // removes the binding
|  EXISTS(x,A,_):      { old_binding(x); }
|  FORALL(x,A,_):      { old_binding(x); }
|  GENERATOR(xs,As,_): { old_binding(xs); }
|  LET(x,_,_):         { old_binding(x); }
};

Note that we have accomplished a depth first traversal using rewriting without writing any traversal code! As a side benefit, since the traversal is automatically determined by the structure of the datatypes, we do not have to rewrite this renaming code even if the abstract syntax of the query language is extended, as long as no additional binding operators are added.