fmrisc.ProofNavigator.Proving

Class Substitute

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTVisitorBase

fmrisc.ProofNavigator.Proving.Substitute

All Implemented Interfaces:

ASTVisitor

public final class Substitute
extends ASTVisitorBase

Substitute in an expression all free occurences of denoted variables.

Method Summary

Modifier and Type	Method and Description
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.ProofNavigator.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.