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 |
---|---|
private SVInstantiations |
instantiations
the instantiations needed for unwind loop constructs
|
protected ImmutableList<SchemaVariable> |
varList
collects all found variables
|
Constructor and Description |
---|
TacletSchemaVariableCollector() |
TacletSchemaVariableCollector(SVInstantiations svInsts) |
Modifier and Type | Method and Description |
---|---|
private ImmutableList<SchemaVariable> |
collectSVInElementaryUpdate(ElementaryUpdate op,
ImmutableList<SchemaVariable> vars)
collects all schema variables occurring on the lhs of an elementary update
|
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() |
private void |
visit(Semisequent semiseq)
collects all variables in a Semisequent
|
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
private SVInstantiations instantiations
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 collectedprivate ImmutableList<SchemaVariable> collectSVInElementaryUpdate(ElementaryUpdate op, ImmutableList<SchemaVariable> vars)
op
- the ElementaryUpdate operator to be scanned for schemavariablesvars
- the ImmutableListvars
together with the schema variables found in op
public java.lang.Iterable<SchemaVariable> vars()
public java.util.Iterator<SchemaVariable> varIterator()
public int size()
public boolean contains(SchemaVariable var)
private void visit(Semisequent semiseq)
semiseq
- the Semisequent to visitpublic 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 to