/** * Renaming of bound variables is determined by the shape of * variables and binding constructs. Three generic strategies * are defined that cater for different complexities of binding * constructs. * * Variable binding constructs protect variables from clashing * with variables in other parts of a program when their names * are the same. To prevent the introduction of name clashes * during program transformation it can be useful to give * all variable bindings a unique name. This module defines three * generic strategies for bound variable renaming all based on * the same idea, but dealing with increasingly complex variable * binding models. * * Renaming depends \emph{only} on the shape of variable bindings * and variable occurences. Other language constructs are irrelevant. * * In the generic strategies the following assumptions about * binding constructs are made: (1) * There is a subtree that covers the scope in which the * variables are bound. (2) variables are atomic, i.e., do not * contain subterms that are * variables or binding constructs. * * Approach: indicate shape of variable occurences and variable * binders */ module strategy/general/rename imports strategy/traversal/simple collection/tuple/common collection/list/- strategy/traversal/environment rules RnVar(isvar : (name -> env) * name -> term) : (t, env) -> <isvar(split(id, !env); lookup)> t RnBinding(bndvrs) : (t, env1) -> (t, env1, env2) where <bndvrs> t => xs; map(new) => ys; <conc>(<zip(id)>(xs,ys), env1) => env2 DistBinding(s) : (t, env1, env2) -> <all( \x -> <s>(x, env2)\ )> t strategies /** * renaming bound variables assuming that variables are bound * in all subterms of a binding construct * variable declarations in binding constructs are assumed to * have the same shape as variable uses */ rename(isvar : (name -> env) * name -> term , bndvars) = \ t -> (t, []) \ ; rec x(env-alltd(RnVar(isvar) <+ RnBinding(bndvars); DistBinding(x))) rules DistBinding(s, boundin : (term -> term) * (term -> term) * (term -> term) * term -> term): (t, env1, env2) -> <boundin(\x -> <s>(x, env2)\ ,\x -> <s>(x, env1)\ ,id)> t strategies /** * The strategy \verb|rename(isvar, mkvar, bnd)| renames all * bound variables in a term to fresh variables; * * Parameters: * * isvar: Succeeds if applied to a variable * newvar: Takes a string and builds a variable * bnd: Maps a binding construct to the list of bound variables * * renaming while making a distinction between subterms * in which the variables are bound or not * variables at binding sites are assumed to have * the same shape as other variable occurences */ rename(isvar : (name -> env) * name -> term , bndvars , boundin : (term -> term) * (term -> term) * (term -> term) * term -> term) = \ t -> (t, []) \ ; rec x(env-alltd(RnVar(isvar) <+ RnBinding(bndvars); DistBinding(x, boundin))) rules RnBinding(bndvrs, paste : (term -> vars) * term -> term) : (t, env1) -> (<paste(!ys)> t, env1, env2) where <bndvrs> t => xs; map(new) => ys; <conc>(<zip(id)>(xs,ys), env1) => env2 strategies rename(isvar : (name -> env) * name -> term , bndvars , boundin : (term -> term) * (term -> term) * (term -> term) * term -> term , paste : (term -> vars) * term -> term ) = \ t -> (t, []) \ ; rec x(env-alltd(RnVar(isvar) <+ RnBinding(bndvars, paste); DistBinding(x, boundin)))