fmrisc.Proving
Class Substitute

java.lang.Object
  extended by fmrisc.Syntax.ASTVisitorBase
      extended by fmrisc.Proving.Substitute
All Implemented Interfaces:
ASTVisitor

public final class Substitute
extends ASTVisitorBase

Substitute in an expression all free occurences of denoted variables.


Method Summary
 boolean isCloned()
          Signal that visitor shall clone tree.
static Expression substitute(Expression exp, ValueDeclIdentifier[] ident, Expression[] subst, boolean repeat)
          Return expression with simultaneous variable substitutions performed.
 
Methods inherited from class fmrisc.Syntax.ASTVisitorBase
visit
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Method Detail

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.