public class TacletAppIndex
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private SemisequentTacletAppIndex |
antecIndex |
private java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> |
cache |
private Goal |
goal |
private TermTacletAppIndexCacheSet |
indexCaches |
private NewRuleListener |
newRuleListener
Object to which the appearance of new taclet apps is reported
|
private RuleFilter |
ruleFilter
Filter that is used to restrict the set of taclets that are considered as
possible members of this index.
|
private Sequent |
seq
The sequent with the formulas for which taclet indices are hold by
this object.
|
private SemisequentTacletAppIndex |
succIndex |
private TacletIndex |
tacletIndex |
Modifier | Constructor and Description |
---|---|
private |
TacletAppIndex(TacletIndex tacletIndex,
SemisequentTacletAppIndex antecIndex,
SemisequentTacletAppIndex succIndex,
Goal goal,
Sequent seq,
RuleFilter ruleFilter,
TermTacletAppIndexCacheSet indexCaches,
java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache) |
|
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() |
(package private) TacletAppIndex |
copyWithTacletIndex(TacletIndex p_tacletIndex)
returns a new TacletAppIndex with a given TacletIndex
|
private void |
createAllFromGoal() |
private void |
createNewIndexCache() |
(package private) static TacletApp |
createTacletApp(NoPosTacletApp tacletApp,
PosInOccurrence pos,
Services services) |
(package private) static ImmutableList<TacletApp> |
createTacletApps(ImmutableList<NoPosTacletApp> tacletInsts,
PosInOccurrence pos,
Services services)
creates TacletApps out of each single NoPosTacletApp object
|
private void |
ensureIndicesExist() |
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
|
private ImmutableList<TacletApp> |
getFindTacletWithPos(PosInOccurrence pos,
TacletFilter filter,
Services services) |
private Goal |
getGoal() |
private SemisequentTacletAppIndex |
getIndex(PosInOccurrence pos) |
private NewRuleListener |
getNewRulePropagator() |
private Node |
getNode() |
ImmutableList<NoPosTacletApp> |
getNoFindTaclet(TacletFilter filter,
Services services)
collects all NoFindTacletInstantiations
|
private Proof |
getProof() |
ImmutableList<NoPosTacletApp> |
getRewriteTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all RewriteTacletInstantiations in a subterm of the
constrainedFormula described by a PosInOccurrence.
|
private RuleFilter |
getRuleFilter() |
private Sequent |
getSequent() |
private Services |
getServices() |
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.
|
private boolean |
isUpToDateForGoal() |
private static ImmutableList<TacletApp> |
prepend(ImmutableList<TacletApp> l1,
ImmutableList<NoPosTacletApp> l2) |
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() |
private void |
updateIndices(SequentChangeInfo sci) |
private void |
updateIndices(SetRuleFilter newTaclets) |
private final TacletIndex tacletIndex
private SemisequentTacletAppIndex antecIndex
private SemisequentTacletAppIndex succIndex
private TermTacletAppIndexCacheSet indexCaches
private Goal goal
private NewRuleListener newRuleListener
private RuleFilter ruleFilter
TacletAppIndex
s exclusively for automatic or interactive
taclets.private Sequent seq
seq != null
implies that the
indices antecIndex
, succIndex
are up to date
for the sequent seq
private java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache
public TacletAppIndex(TacletIndex tacletIndex, Services services)
private TacletAppIndex(TacletIndex tacletIndex, SemisequentTacletAppIndex antecIndex, SemisequentTacletAppIndex succIndex, Goal goal, Sequent seq, RuleFilter ruleFilter, TermTacletAppIndexCacheSet indexCaches, java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache)
public void setNewRuleListener(NewRuleListener p_newRuleListener)
private NewRuleListener getNewRulePropagator()
public void setRuleFilter(RuleFilter p_ruleFilter)
private RuleFilter getRuleFilter()
TacletAppIndex copyWithTacletIndex(TacletIndex p_tacletIndex)
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()
private void createNewIndexCache()
public void fillCache()
private void createAllFromGoal()
private void ensureIndicesExist()
private boolean isUpToDateForGoal()
private SemisequentTacletAppIndex getIndex(PosInOccurrence pos)
private ImmutableList<TacletApp> getFindTacletWithPos(PosInOccurrence pos, TacletFilter filter, Services services)
public ImmutableList<TacletApp> getTacletAppAt(PosInOccurrence pos, TacletFilter filter, Services services)
pos
- the PosInOccurrence to focusstatic ImmutableList<TacletApp> createTacletApps(ImmutableList<NoPosTacletApp> tacletInsts, PosInOccurrence pos, Services services)
tacletInsts
- the list of NoPosTacletApps the TacletApps are to
be created frompos
- the PosInOccurrence to focusstatic TacletApp createTacletApp(NoPosTacletApp tacletApp, PosInOccurrence pos, Services services)
public 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 sequentprivate void updateIndices(SequentChangeInfo sci)
private void updateIndices(SetRuleFilter newTaclets)
public 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
private static ImmutableList<TacletApp> prepend(ImmutableList<TacletApp> l1, ImmutableList<NoPosTacletApp> l2)
private Goal getGoal()
private Sequent getSequent()
private Services getServices()
private Proof getProof()
private Node getNode()
public TacletIndex tacletIndex()
public void reportRuleApps(NewRuleListener l, Services services)