fmrisc.ProgramExplorer.Judgements

Class RefSubstitution

java.lang.Object

fmrisc.ProgramExplorer.Syntax.ASTVisitorBase

fmrisc.ProgramExplorer.Syntax.ASTCloner

fmrisc.ProgramExplorer.Judgements.RefSubstitution

All Implemented Interfaces:

ASTVisitor

public final class RefSubstitution
extends ASTCloner

Reference substitution P[T1/I1,...]

Method Summary

Methods

Modifier and Type	Method and Description
static AST	perform(java.util.Map<java.lang.String,Term> map, AST exp) Perform substitution of identifiers by terms.
void	visit(ArrayTerm exp) Process expression
void	visit(ExistsFormula exp) Process expression
void	visit(ForallFormula exp) Process expression
void	visit(LambdaFormula exp) Process expression
void	visit(LambdaTerm exp) Process expression
void	visit(LetExpression exp) Process expression
void	visit(LetFormula exp) Process expression
void	visit(LetTerm exp) Process expression
void	visit(QuantifiedExpression exp) Process expression
void	visit(Reference exp) Process expression

Methods inherited from class fmrisc.ProgramExplorer.Syntax.ASTCloner

clone, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class fmrisc.ProgramExplorer.Syntax.ASTVisitorBase

visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

perform

public static AST perform(java.util.Map<java.lang.String,Term> map,
          AST exp)

Perform substitution of identifiers by terms.

Parameters:

map - the mapping of identifier names (strings) to terms.

exp - the expression where to perform the substitution.

Returns:

the substituted formula (=exp, if substitution map is empty)

visit

public void visit(QuantifiedExpression exp)

Process expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

Parameters:

exp - the expression to be substituted.

visit

public void visit(ExistsFormula exp)

Process expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - the expression to be substituted.

visit

public void visit(ForallFormula exp)

Process expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - the expression to be substituted.

visit

public void visit(ArrayTerm exp)

Process expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - the expression to be substituted.

visit

public void visit(LambdaFormula exp)

Process expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - the expression to be substituted.

visit

public void visit(LambdaTerm exp)

Process expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - the expression to be substituted.

visit

public void visit(LetExpression exp)

Process expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

Parameters:

exp - the expression to be substituted.

visit

public void visit(LetFormula exp)

Process expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - the expression to be substituted.

visit

public void visit(LetTerm exp)

Process expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - the expression to be substituted.

visit

public void visit(Reference exp)

Process expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - the expression to be substituted.