public class TacletAppIndex
extends java.lang.Object
Constructor and Description |
---|
TacletAppIndex(TacletIndex tacletIndex,
Services services) |
Modifier and Type | Method and Description |
---|---|
void |
addedNoPosTacletApp(NoPosTacletApp tacletApp)
updates the internal caches after a new Taclet with instantiation
information has been added to the TacletIndex.
|
void |
addedNoPosTacletApps(java.lang.Iterable<NoPosTacletApp> tacletApps)
updates the internal caches after a new Taclet with instantiation
information has been added to the TacletIndex.
|
void |
clearAndDetachCache()
Delete all cached information about taclet apps.
|
void |
clearIndexes() |
void |
fillCache()
Forces all delayed computations to be performed, so that
the cache is fully up-to-date (NewRuleListener gets informed)
|
ImmutableList<NoPosTacletApp> |
getFindTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all FindTaclets with instantiations and position
|
ImmutableList<NoPosTacletApp> |
getNoFindTaclet(TacletFilter filter,
Services services)
collects all NoFindTacletInstantiations
|
ImmutableList<NoPosTacletApp> |
getRewriteTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all RewriteTacletInstantiations in a subterm of the
constrainedFormula described by a PosInOccurrence.
|
ImmutableList<TacletApp> |
getTacletAppAt(PosInOccurrence pos,
TacletFilter filter,
Services services)
returns the set of rule applications
at the given position of the given sequent.
|
ImmutableList<TacletApp> |
getTacletAppAtAndBelow(PosInOccurrence pos,
TacletFilter filter,
Services services)
returns the rule applications at the given PosInOccurrence and at all
Positions below this.
|
void |
removedNoPosTacletApp(NoPosTacletApp tacletApp)
updates the internal caches after a Taclet with instantiation
information has been removed from the TacletIndex.
|
void |
reportRuleApps(NewRuleListener l,
Services services)
Reports all cached rule apps.
|
void |
sequentChanged(Goal goal,
SequentChangeInfo sci)
called if a formula has been replaced
|
void |
setNewRuleListener(NewRuleListener p_newRuleListener) |
void |
setRuleFilter(RuleFilter p_ruleFilter) |
void |
setup(Goal p_goal)
Set the goal association of this index to the given object
p_goal . |
TacletIndex |
tacletIndex()
returns the Taclet index for this ruleAppIndex.
|
java.lang.String |
toString() |
public TacletAppIndex(TacletIndex tacletIndex, Services services)
public void setNewRuleListener(NewRuleListener p_newRuleListener)
public void setRuleFilter(RuleFilter p_ruleFilter)
public void setup(Goal p_goal)
p_goal
. If the sequent of the new goal differs from the
former one (attribute seq
), the index will be rebuilt as
soon as data is requested from it.public void clearAndDetachCache()
public void clearIndexes()
public void fillCache()
public ImmutableList<TacletApp> getTacletAppAt(PosInOccurrence pos, TacletFilter filter, Services services)
pos
- the PosInOccurrence to focuspublic ImmutableList<NoPosTacletApp> getNoFindTaclet(TacletFilter filter, Services services)
services
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<NoPosTacletApp> getRewriteTaclet(PosInOccurrence pos, TacletFilter filter, TermServices services)
pos
- the PosInOccurrence to focusservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<NoPosTacletApp> getFindTaclet(PosInOccurrence pos, TacletFilter filter, TermServices services)
pos
- the PosInOccurrence to focusservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<TacletApp> getTacletAppAtAndBelow(PosInOccurrence pos, TacletFilter filter, Services services)
pos
- the position where to start fromservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public void sequentChanged(Goal goal, SequentChangeInfo sci)
sci
- SequentChangeInfo describing the change of the sequentpublic void addedNoPosTacletApp(NoPosTacletApp tacletApp)
tacletApp
- the partially instantiated Taclet to addpublic void addedNoPosTacletApps(java.lang.Iterable<NoPosTacletApp> tacletApps)
tacletApps
- set of partially instantiated Taclet
s to addpublic void removedNoPosTacletApp(NoPosTacletApp tacletApp)
tacletApp
- the partially instantiated Taclet to removepublic java.lang.String toString()
toString
in class java.lang.Object
public TacletIndex tacletIndex()
public void reportRuleApps(NewRuleListener l, Services services)
Copyright © 2003-2019 The KeY-Project.