de.uka.ilkd.key.rule

Class SyntacticalReplaceVisitor

java.lang.Object

de.uka.ilkd.key.logic.DefaultVisitor

de.uka.ilkd.key.rule.SyntacticalReplaceVisitor

All Implemented Interfaces:

Visitor

Direct Known Subclasses:

ConstraintAwareSyntacticalReplaceVisitor

public class SyntacticalReplaceVisitor
extends DefaultVisitor

Field Summary

Fields

Modifier and Type	Field and Description
protected PosInOccurrence	applicationPosInOccurrence
private Term	computedResult
protected Goal	goal
protected Taclet.TacletLabelHint	labelHint
private java.lang.Boolean	newMarker
protected Rule	rule
protected RuleApp	ruleApp
protected Services	services
private java.util.Stack<java.lang.Object>	subStack the stack contains the subterms that will be added in the next step of execPostOrder in Term in order to build the new term.
static java.lang.String	SUBSTITUTION_WITH_LABELS_HINT
protected SVInstantiations	svInst
private java.util.Deque<Term>	tacletTermStack
protected TermBuilder	tb the termbuilder used to construct terms
protected TermLabelState	termLabelState

Constructor Summary

Constructors

Modifier	Constructor and Description
	SyntacticalReplaceVisitor(TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, PosInOccurrence applicationPosInOccurrence, Goal goal, Rule rule, RuleApp ruleApp, Services services, TermBuilder termBuilder)
	SyntacticalReplaceVisitor(TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, PosInOccurrence applicationPosInOccurrence, SVInstantiations svInst, Goal goal, Rule rule, RuleApp ruleApp, Services services) constructs a term visitor replacing any occurrence of a schemavariable found in svInst by its instantiation
private	SyntacticalReplaceVisitor(TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, PosInOccurrence applicationPosInOccurrence, SVInstantiations svInst, Goal goal, Rule rule, RuleApp ruleApp, Services services, TermBuilder termBuilder) constructs a term visitor replacing any occurrence of a schemavariable found in svInst by its instantiation

Method Summary

Modifier and Type	Method and Description
private JavaProgramElement	addContext(StatementBlock pe)
SVInstantiations	getSVInstantiations()
Term	getTerm() delivers the new built term
private Operator	handleSortDependingSymbol(SortDependingFunction depOp)
private ImmutableArray<QuantifiableVariable>	instantiateBoundVariables(Term visited)
private ElementaryUpdate	instantiateElementaryUpdate(ElementaryUpdate op)
private ImmutableArray<TermLabel>	instantiateLabels(Term tacletTerm, Operator newTermOp, ImmutableArray<Term> newTermSubs, ImmutableArray<QuantifiableVariable> newTermBoundVars, JavaBlock newTermJavaBlock, ImmutableArray<TermLabel> newTermOriginalLabels)
private Operator	instantiateOperator(Operator p_operatorToBeInstantiated)
private Operator	instantiateOperatorSV(ModalOperatorSV op)
private Term[]	neededSubs(int n)
protected void	pushNew(java.lang.Object t)
private JavaBlock	replacePrg(SVInstantiations svInst, JavaBlock jb)
private Term	resolveSubst(Term t)
void	subtreeEntered(Term subtreeRoot) this method is called in execPreOrder and execPostOrder in class Term when entering the subtree rooted in the term subtreeRoot.
void	subtreeLeft(Term subtreeRoot) this method is called in execPreOrder and execPostOrder in class Term when leaving the subtree rooted in the term subtreeRoot.
protected Term	toTerm(Term o) the method is only still invoked to allow the ConstraintAwareSyntacticalReplaceVisitor to recursively replace meta variables
void	visit(Term visited) performs the syntactic replacement of schemavariables with their instantiations

Methods inherited from class de.uka.ilkd.key.logic.DefaultVisitor

visitSubtree

Methods inherited from class java.lang.Object

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

Field Detail

SUBSTITUTION_WITH_LABELS_HINT

public static final java.lang.String SUBSTITUTION_WITH_LABELS_HINT

See Also:

Constant Field Values

svInst

protected final SVInstantiations svInst

services

protected final Services services

tb

protected final TermBuilder tb

the termbuilder used to construct terms

computedResult

private Term computedResult

applicationPosInOccurrence

protected final PosInOccurrence applicationPosInOccurrence

rule

protected final Rule rule

goal

protected final Goal goal

ruleApp

protected final RuleApp ruleApp

termLabelState

protected final TermLabelState termLabelState

labelHint

protected final Taclet.TacletLabelHint labelHint

subStack

private final java.util.Stack<java.lang.Object> subStack

the stack contains the subterms that will be added in the next step of execPostOrder in Term in order to build the new term. A boolean value between or under the subterms on the stack indicate that a term using these subterms should build a new term instead of using the old one, because one of its subterms has been built, too.

newMarker

private final java.lang.Boolean newMarker

tacletTermStack

private final java.util.Deque<Term> tacletTermStack

Constructor Detail

SyntacticalReplaceVisitor

private SyntacticalReplaceVisitor(TermLabelState termLabelState,
                                  Taclet.TacletLabelHint labelHint,
                                  PosInOccurrence applicationPosInOccurrence,
                                  SVInstantiations svInst,
                                  Goal goal,
                                  Rule rule,
                                  RuleApp ruleApp,
                                  Services services,
                                  TermBuilder termBuilder)

constructs a term visitor replacing any occurrence of a schemavariable found in svInst by its instantiation

Parameters:

termLabelState - the termlabel state

labelHint - hints about how to deal with labels

applicationPosInOccurrence - the application position

svInst - mapping of schemavariables to their instantiation

goal - the current goal

rule - the applied rule

ruleApp - the rule application

services - the Services

termBuilder - the TermBuilder to use (allows to use the non cached version)

SyntacticalReplaceVisitor

public SyntacticalReplaceVisitor(TermLabelState termLabelState,
                                 Taclet.TacletLabelHint labelHint,
                                 PosInOccurrence applicationPosInOccurrence,
                                 SVInstantiations svInst,
                                 Goal goal,
                                 Rule rule,
                                 RuleApp ruleApp,
                                 Services services)

constructs a term visitor replacing any occurrence of a schemavariable found in svInst by its instantiation

Parameters:

termLabelState - the termlabel state

labelHint - hints about how to deal with labels

applicationPosInOccurrence - the application position

svInst - mapping of schemavariables to their instantiation

goal - the current goal

rule - the applied rule

ruleApp - the rule application

services - the Services

SyntacticalReplaceVisitor

public SyntacticalReplaceVisitor(TermLabelState termLabelState,
                                 Taclet.TacletLabelHint labelHint,
                                 PosInOccurrence applicationPosInOccurrence,
                                 Goal goal,
                                 Rule rule,
                                 RuleApp ruleApp,
                                 Services services,
                                 TermBuilder termBuilder)

Method Detail

addContext

private JavaProgramElement addContext(StatementBlock pe)

replacePrg

private JavaBlock replacePrg(SVInstantiations svInst,
                             JavaBlock jb)

neededSubs

private Term[] neededSubs(int n)

pushNew

protected void pushNew(java.lang.Object t)

toTerm

protected Term toTerm(Term o)

the method is only still invoked to allow the ConstraintAwareSyntacticalReplaceVisitor to recursively replace meta variables

instantiateElementaryUpdate

private ElementaryUpdate instantiateElementaryUpdate(ElementaryUpdate op)

instantiateOperatorSV

private Operator instantiateOperatorSV(ModalOperatorSV op)

instantiateOperator

private Operator instantiateOperator(Operator p_operatorToBeInstantiated)

instantiateBoundVariables

private ImmutableArray<QuantifiableVariable> instantiateBoundVariables(Term visited)

visit

public void visit(Term visited)

performs the syntactic replacement of schemavariables with their instantiations

Parameters:

visited - the Term to be visited

instantiateLabels

private ImmutableArray<TermLabel> instantiateLabels(Term tacletTerm,
                                                    Operator newTermOp,
                                                    ImmutableArray<Term> newTermSubs,
                                                    ImmutableArray<QuantifiableVariable> newTermBoundVars,
                                                    JavaBlock newTermJavaBlock,
                                                    ImmutableArray<TermLabel> newTermOriginalLabels)

handleSortDependingSymbol

private Operator handleSortDependingSymbol(SortDependingFunction depOp)

resolveSubst

private Term resolveSubst(Term t)

getTerm

public Term getTerm()

delivers the new built term

getSVInstantiations

public SVInstantiations getSVInstantiations()

subtreeEntered

public void subtreeEntered(Term subtreeRoot)

this method is called in execPreOrder and execPostOrder in class Term when entering the subtree rooted in the term subtreeRoot. Default implementation is to do nothing. Subclasses can override this method when the visitor behaviour depends on informations bound to subtrees.

Specified by:

subtreeEntered in interface Visitor

Overrides:

subtreeEntered in class DefaultVisitor

Parameters:

subtreeRoot - root of the subtree which the visitor enters.

subtreeLeft

public void subtreeLeft(Term subtreeRoot)

this method is called in execPreOrder and execPostOrder in class Term when leaving the subtree rooted in the term subtreeRoot. Default implementation is to do nothing. Subclasses can override this method when the visitor behaviour depends on informations bound to subtrees.

Specified by:

subtreeLeft in interface Visitor

Overrides:

subtreeLeft in class DefaultVisitor

Parameters:

subtreeRoot - root of the subtree which the visitor leaves.