public class SyntacticalReplaceVisitor extends DefaultVisitor
Modifier and Type | Field and Description |
---|---|
protected PosInOccurrence |
applicationPosInOccurrence |
private Term |
computedResult |
protected Goal |
goal |
protected Taclet.TacletLabelHint |
labelHint |
private Boolean |
newMarker |
protected Rule |
rule |
protected RuleApp |
ruleApp |
protected Services |
services |
private Stack<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 String |
SUBSTITUTION_WITH_LABELS_HINT |
protected SVInstantiations |
svInst |
private Deque<Term> |
tacletTermStack |
protected TermLabelState |
termLabelState |
Constructor and Description |
---|
SyntacticalReplaceVisitor(TermLabelState termLabelState,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Taclet.TacletLabelHint labelHint,
Goal goal) |
SyntacticalReplaceVisitor(TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
SVInstantiations svInst,
Goal goal,
Rule rule,
RuleApp ruleApp,
Services services) |
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(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
|
visitSubtree
public static final String SUBSTITUTION_WITH_LABELS_HINT
protected final SVInstantiations svInst
protected final Services services
private Term computedResult
protected final PosInOccurrence applicationPosInOccurrence
protected final Rule rule
protected final Goal goal
protected final RuleApp ruleApp
protected final TermLabelState termLabelState
protected final Taclet.TacletLabelHint labelHint
private final Stack<Object> subStack
private final Boolean newMarker
public SyntacticalReplaceVisitor(TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, PosInOccurrence applicationPosInOccurrence, SVInstantiations svInst, Goal goal, Rule rule, RuleApp ruleApp, Services services)
public SyntacticalReplaceVisitor(TermLabelState termLabelState, Services services, PosInOccurrence applicationPosInOccurrence, Rule rule, RuleApp ruleApp, Taclet.TacletLabelHint labelHint, Goal goal)
private JavaProgramElement addContext(StatementBlock pe)
private JavaBlock replacePrg(SVInstantiations svInst, JavaBlock jb)
private Term[] neededSubs(int n)
protected void pushNew(Object t)
protected Term toTerm(Term o)
ConstraintAwareSyntacticalReplaceVisitor
to recursively replace meta variablesprivate ElementaryUpdate instantiateElementaryUpdate(ElementaryUpdate op)
private Operator instantiateOperatorSV(ModalOperatorSV op)
private ImmutableArray<QuantifiableVariable> instantiateBoundVariables(Term visited)
public void visit(Term visited)
visited
- the Term to be visitedprivate ImmutableArray<TermLabel> instantiateLabels(Term tacletTerm, Operator newTermOp, ImmutableArray<Term> newTermSubs, ImmutableArray<QuantifiableVariable> newTermBoundVars, JavaBlock newTermJavaBlock, ImmutableArray<TermLabel> newTermOriginalLabels)
private Operator handleSortDependingSymbol(SortDependingFunction depOp)
public Term getTerm()
public SVInstantiations getSVInstantiations()
public void subtreeEntered(Term subtreeRoot)
subtreeEntered
in interface Visitor
subtreeEntered
in class DefaultVisitor
subtreeRoot
- root of the subtree which the visitor enters.public void subtreeLeft(Term subtreeRoot)
subtreeLeft
in interface Visitor
subtreeLeft
in class DefaultVisitor
subtreeRoot
- root of the subtree which the visitor leaves.