public class LightweightSyntacticalReplaceVisitor extends DefaultVisitor
SyntacticalReplaceVisitor
which does not
replace labels. This saves a lot of dependencies to Goal
,
RuleApp
, PosInOccurrence
etc. and is therefore useful for
internal computations not having access to all these objects. Since labels
are not refactored, this class is *not* useful for rule applications etc.
Note that this class is basically a stripped-down copy of
SyntacticalReplaceVisitor
, so problems in that class would carry over
to this one...Constructor and Description |
---|
LightweightSyntacticalReplaceVisitor(Services services) |
LightweightSyntacticalReplaceVisitor(SVInstantiations svInst,
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 LightweightSyntacticalReplaceVisitor(SVInstantiations svInst, Services services)
svInst
by its instantiationsvInst
- mapping of schemavariables to their instantiationlocalSpecRepo
- TODOservices
- the Servicespublic LightweightSyntacticalReplaceVisitor(Services services)
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.