/*

	Substituting terms for variables depends mainly on
	the shape of variables.
	This module implements several generic strategies for different
	styles of parallel substitution, including ones that rename
	bound variables to prevent name capture.

	\end{abstract}


	A substitution is a mapping from variables to terms. Given a
	substitution the strategy \verb|substitute(...)| traverses
	a term and replaces variables in the domain of the mapping by
	their associated term.
	The strategy can be applied in two ways; (1) to a pair of a
	substitution and a term
\verb|<substitute(...)> (sbs, t)|
	and (2) to a triple of a list of variables, a list of (equal
	length) of terms and a term
\verb|<substitute(...)> (xs, ts, t)|. This entails that the type of
	\verb|substitute(...)| is either 
\verb|Prod([List(Prod([a,b])),b]) -> b|
	or
\verb|Prod([List(a),List(b),b]) -> b|, with \verb|a| the type of variables
	and \verb|b| the type of terms.

	There are four versions of the substitution strategy that
	depend on two factors; (1) renaming of bound variables in
	terms substituted for variables (2) renaming of bound
	variables in the context of substituted variables.

	All versions are parameterized with a strategy \verb|isvar|
	recognizing variables and mapping them to a substitution key,
	which can be the entire variable structure or just its
	name. That is, \verb|isvar| should have type \verb|b -> a|.

	The substitution strategy can be parameterized with a variable
	renaming strategy \verb|ren| (of type \verb|b -> b|) that will
	be applied to each term after it is substituted for a
	variable. This
	can be used to ensure that all bound variables are unique throughout
	an abstract syntax tree and thus prevent free variable
	capture.

	A better way to ensure that free variables are not captured
	when substituting under bindings requires renaming the bound variables
	in the context of the variables that are substituted for. This
	is achieved by combining the generic bound variable renaming techniques
	from module \verb|rename| with replacing a variable by a term.
	For this purpose there are two variants of the
	substitution strategy that are parameterized with strategies indicating
	shape of variables, the bound variables, the arguments
	that they are binding in and a replacement strategy.
	See module \verb|rename| for an explanation of these parameters.

*/

module strategy/general/substitution
imports 
  strategy/traversal/simple
  collection/tuple/common 
  collection/list/-
  strategy/general/rename

strategies

  // substitutions accept two types of input 
  // 1) a pair of a substitution (is list of pairs) and a term
  // 2) a triple of a list of variables, a list of terms that should
  //    replace them, and a term

  subs-args = 
    ?(sbs, t) <+ \ (xs, ys, t) -> (<zip(id)> (xs, ys), t) \

rules

  // replacing a variable with its value in the substitution

  SubsVar(isvar, mksbs) :
    t -> <lookup> (x, sbs)
    where <isvar> t => x; mksbs => sbs

strategies  

  // substitute variables, no regard for variable bindings, and
  // rename bound variables in substituted terms

  substitute(isvar, ren) =
    subs-args => (sbs,t); !t;
    alltd(SubsVar(isvar, !sbs); ren)

  // substitute variables, no regard for variable bindings

  substitute(isvar) =
    substitute(isvar, id)

  // substitute all variables, rename bound variables on the way down,
  // and rename the bound variables in the terms that are substituted
  // for variables using the renaming strategy ren

  substitute(isvar
            , varshape: (name -> env) * name -> term
            , bndvars
            , boundin: (term -> term) * (term -> term) * (term -> term) * term -> term
            , paste: (term -> vars) * term -> term
            , ren) 
  = subs-args => (sbs,t); !(t, []);
    rec x(env-alltd(RnVar(varshape)
                    <+ Fst; SubsVar(isvar, !sbs); ren
                    <+ RnBinding(bndvars, paste);
                       DistBinding(x,boundin)))

  // substitute variables and rename bound variables encountered
  // on the way to prevent variable capture, don't rename
  // substituted terms

  substitute(isvar
            , varshape: (name -> env) * name -> term
            , bndvars
            , boundin: (term -> term) * (term -> term) * (term -> term) * term -> term
            , paste: (term -> vars) * term -> term )
  = substitute(isvar, varshape, bndvars, boundin, paste, id)