/* Extraction of free variables from an expression is governed by the shape of variables and the shape of variable bindings. */ module strategy/general/free-variables imports collection/list/- /* \paragraph{Parameters of Free Variable Extraction} the following aspects determine the extraction of free variables from expressions \begin{itemize} \item shape of variables \item variables bound by a binding construct \item arguments of the binding constructs where variables are bound \end{itemize} In addition can variable constructs contain other variables, or in other words, whether variables are leaves or non-leaves. \paragraph{Variables are Leaves} In the first style of free variable extraction, variables are leaves of abstract syntax trees. Free variables of a term; The first argument s1 is a strategy that transforms variables into lists of variables, e.g., \verb|Var(x) -> [x]|; The second argument s2 is a strategy that maps binding constructs to the list of bound variables, e.g., \verb|Scope(xs, s) -> xs|; */ strategies free-vars(getvars, boundvars) = rec x(getvars <+ split(crush(![],union,x), boundvars <+ ![]); diff) free-vars(getvars, boundvars , boundin : (term -> term) * (term -> term) * (term -> term) * term -> term) = rec x(getvars <+ {vs: where(boundvars => vs); boundin(split(x, !vs); diff, x, ![])}; crush(![],union,id) <+ crush(![],union,x)) /* // if we had strategy abstraction /\(x1,...,xn) -> s free-vars(getvars, boundvars, boundin) = collect(getvars ,/\ (x,nil) -> {vs: where(boundvars => vs); boundin(split(x, !vs); diff, x, nil)}) */ free-vars(getvars, boundvars , boundin : (term -> term) * (term -> term) * (term -> term) * term -> term , eq) = rec x(getvars <+ {vs: where(boundvars => vs); boundin(split(x, !vs); diff(eq), x, ![])}; crush(![],union,id) <+ crush(![],union,x)) /* \paragraph{Variables are not Leafs} In a more complicated style of free variable extraction, variables are not leaves of abstract syntax trees, but can contain subterms that again contain variables. */ strategies free-vars2(getvars, boundvars) = rec x(split(getvars <+ ![], split(crush(![],union,x), boundvars <+ ![]); diff); union) free-vars2(getvars, boundvars , boundin : (term -> term) * (term -> term) * (term -> term) * term -> term) = rec x(split(getvars <+ ![], ({vs: where(boundvars => vs); boundin(split(x, !vs); diff, x, ![])}; crush(![],union,id) <+ crush(![],union,x))); union) free-vars2(getvars, boundvars , boundin : (term -> term) * (term -> term) * (term -> term) * term -> term , eq) = rec x(split(getvars <+ ![] ,{vs: where(boundvars => vs); boundin(split(x, !vs); diff(eq), x, ![]); crush(![],union,id)} <+ crush(![],union,x) ); union)