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 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 |
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 |
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
|
visitSubtree
public static final java.lang.String SUBSTITUTION_WITH_LABELS_HINT
protected final SVInstantiations svInst
protected final Services services
protected final TermBuilder tb
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 java.util.Stack<java.lang.Object> subStack
private final java.lang.Boolean newMarker
private final java.util.Deque<Term> tacletTermStack
private SyntacticalReplaceVisitor(TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, PosInOccurrence applicationPosInOccurrence, SVInstantiations svInst, Goal goal, Rule rule, RuleApp ruleApp, Services services, TermBuilder termBuilder)
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 ServicestermBuilder
- the TermBuilder to use (allows to use the non cached version)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)
private JavaProgramElement addContext(StatementBlock pe)
private JavaBlock replacePrg(SVInstantiations svInst, JavaBlock jb)
private Term[] neededSubs(int n)
protected void pushNew(java.lang.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.