public class TacletSchemaVariableCollector extends DefaultVisitor
\find, \assumes
part or goal description of a taclet.
The addrule section is scanned optionally.
Duplicates are not removed because the use of persistent
datastructure and up to now we just have a SetAsList-implementaion
causing to have O(sqr(n)) if it would used.
For example, TacletApp
uses this class
to determine all uninstantiated schemavariables.Modifier and Type | Field and Description |
---|---|
protected ImmutableList<SchemaVariable> |
varList
collects all found variables
|
Constructor and Description |
---|
TacletSchemaVariableCollector() |
TacletSchemaVariableCollector(SVInstantiations svInsts) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<SchemaVariable> |
collectSVInProgram(JavaBlock jb,
ImmutableList<SchemaVariable> vars)
collects all SchemVariables that occur in the JavaBlock
|
boolean |
contains(SchemaVariable var) |
int |
size() |
java.util.Iterator<SchemaVariable> |
varIterator() |
java.lang.Iterable<SchemaVariable> |
vars() |
void |
visit(Sequent seq)
goes through the given sequent an collects all vars found
|
void |
visit(Taclet taclet,
boolean visitAddrules)
collects all schema variables of a taclet
|
void |
visit(Term t)
visits the Term in post order
Term.execPostOrder(Visitor) and
collects all found schema variables |
protected void |
visitFindPart(Taclet taclet) |
protected void |
visitGoalTemplates(Taclet taclet,
boolean visitAddrules) |
void |
visitWithoutAddrule(Taclet taclet)
collects all variables in a Taclet but ignores the variables that appear
only in the addrule sections of the Taclet
|
subtreeEntered, subtreeLeft, visitSubtree
protected ImmutableList<SchemaVariable> varList
public TacletSchemaVariableCollector()
public TacletSchemaVariableCollector(SVInstantiations svInsts)
svInsts
- the SVInstantiations that have been already found
(needed by unwind loop constructs to determine which labels are needed)protected ImmutableList<SchemaVariable> collectSVInProgram(JavaBlock jb, ImmutableList<SchemaVariable> vars)
jb
- the JavaBlock where to look for Schemavariablesvars
- the IListpublic void visit(Term t)
Term.execPostOrder(Visitor)
and
collects all found schema variablest
- the Term whose schema variables are collectedpublic java.lang.Iterable<SchemaVariable> vars()
public java.util.Iterator<SchemaVariable> varIterator()
public int size()
public boolean contains(SchemaVariable var)
public void visit(Sequent seq)
seq
- the Sequent to visitpublic void visit(Taclet taclet, boolean visitAddrules)
taclet
- the Taclet where the variables have to be collected tovisitAddrules
- a boolean that contols if the addrule sections are
to be ignored (iff false) or if the visitor descends into them (iff true)protected void visitFindPart(Taclet taclet)
protected void visitGoalTemplates(Taclet taclet, boolean visitAddrules)
public void visitWithoutAddrule(Taclet taclet)
taclet
- the Taclet where the variables have to be collected toCopyright © 2003-2019 The KeY-Project.