fmrisc.Proving
Class Substitute
java.lang.Object
fmrisc.Syntax.ASTVisitorBase
fmrisc.Proving.Substitute
- All Implemented Interfaces:
- ASTVisitor
public final class Substitute
- extends ASTVisitorBase
Substitute in an expression all free occurences of denoted variables.
Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
substitute
public static Expression substitute(Expression exp,
ValueDeclIdentifier[] ident,
Expression[] subst,
boolean repeat)
- Return expression with simultaneous variable substitutions performed.
- Parameters:
exp
- an expression.ident
- an array of identifiers.subst
- an array of expressions of the same length as ident;
if repeat is true, none of the expressions contains a free
occurence of any identifier in ident.repeat
- true iff the substitution is to be iterated until
no more applicable.
- Returns:
- exp[subst/ident], i.e., a version of exp where all free
occurences of any element of ident have been substituted by the
corresponding expression in subst with some locally bound variables in
exp possibly renamed to avoid name capture.
isCloned
public boolean isCloned()
- Signal that visitor shall clone tree.
- Specified by:
isCloned
in interface ASTVisitor
- Overrides:
isCloned
in class ASTVisitorBase
- Returns:
- false, signalling that the tree is not to be cloned.