public class SVNameCorrespondenceCollector extends DefaultVisitor
Modifier and Type | Field and Description |
---|---|
private HeapLDT |
heapLDT |
private ImmutableMap<SchemaVariable,SchemaVariable> |
nameCorrespondences
This map contains (a, b) if there is a substitution {b a}
somewhere in the taclet
|
Constructor and Description |
---|
SVNameCorrespondenceCollector(HeapLDT heapLDT) |
Modifier and Type | Method and Description |
---|---|
private void |
addNameCorrespondence(SchemaVariable nameReceiver,
SchemaVariable nameProvider) |
ImmutableMap<SchemaVariable,SchemaVariable> |
getCorrespondences() |
private void |
visit(Semisequent semiseq)
collects all correspondences in a semisequent
|
void |
visit(Sequent seq)
collects all correspondences in a sequent
|
void |
visit(Taclet taclet,
boolean visitAddrules)
collects all correspondences in a taclet
|
void |
visit(Term t)
is called by the execPostOrder-method of a term
|
subtreeEntered, subtreeLeft, visitSubtree
private ImmutableMap<SchemaVariable,SchemaVariable> nameCorrespondences
private final HeapLDT heapLDT
SVNameCorrespondenceCollector(HeapLDT heapLDT)
public void visit(Term t)
t
- the Term if the toplevel operator of this term is a
substitution of schema variables, then this pair is added to
the map "nameCorrespondences"private void addNameCorrespondence(SchemaVariable nameReceiver, SchemaVariable nameProvider)
public ImmutableMap<SchemaVariable,SchemaVariable> getCorrespondences()
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 correspondences have to be
collectedvisitAddrules
- a boolean that contols if the addrule sections are
to be ignored (iff false) or if the visitor descends into them (iff true)