public class SyntacticalReplaceVisitor extends DefaultVisitor
Modifier and Type | Field and Description |
---|---|
protected PosInOccurrence |
applicationPosInOccurrence |
protected Goal |
goal |
protected Taclet.TacletLabelHint |
labelHint |
protected Rule |
rule |
protected RuleApp |
ruleApp |
protected Services |
services |
static java.lang.String |
SUBSTITUTION_WITH_LABELS_HINT |
protected SVInstantiations |
svInst |
protected TermBuilder |
tb
the termbuilder used to construct terms
|
protected TermLabelState |
termLabelState |
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 |
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
getSVInstantiations() |
Term |
getTerm()
delivers the new built term
|
protected void |
pushNew(java.lang.Object 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 java.lang.String SUBSTITUTION_WITH_LABELS_HINT
protected final SVInstantiations svInst
protected final Services services
protected final TermBuilder tb
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
public SyntacticalReplaceVisitor(TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, PosInOccurrence applicationPosInOccurrence, SVInstantiations svInst, Goal goal, Rule rule, RuleApp ruleApp, Services services)
svInst
by its instantiationtermLabelState
- the termlabel statelabelHint
- hints about how to deal with labelsapplicationPosInOccurrence
- the application positionsvInst
- mapping of schemavariables to their instantiationgoal
- the current goalrule
- the applied ruleruleApp
- the rule applicationservices
- the Servicespublic SyntacticalReplaceVisitor(TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, PosInOccurrence applicationPosInOccurrence, Goal goal, Rule rule, RuleApp ruleApp, Services services, TermBuilder termBuilder)
protected void pushNew(java.lang.Object t)
protected Term toTerm(Term o)
ConstraintAwareSyntacticalReplaceVisitor
to recursively replace meta variablespublic void visit(Term visited)
visited
- the Term to be visitedpublic 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.Copyright © 2003-2019 The KeY-Project.