public class TermTacletAppIndex
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ImmutableList<NoPosTacletApp> |
localTacletApps
NoPosTacletApps for this term
|
private RuleFilter |
ruleFilter |
private ImmutableArray<TermTacletAppIndex> |
subtermIndices
indices for subterms
|
private Term |
term
the term for which NoPosTacletApps are kept in this index node
|
Modifier | Constructor and Description |
---|---|
private |
TermTacletAppIndex(Term term,
ImmutableList<NoPosTacletApp> localTacletApps,
ImmutableArray<TermTacletAppIndex> subtermIndices,
RuleFilter ruleFilter)
Create a TermTacletAppIndex
|
Modifier and Type | Method and Description |
---|---|
TermTacletAppIndex |
addTaclets(RuleFilter filter,
PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Create a new tree of indices that additionally contain the taclets that
are selected by
filter |
private TermTacletAppIndex |
addTacletsHelp(RuleFilter filter,
PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener) |
private ImmutableArray<TermTacletAppIndex> |
addTacletsSubIndices(RuleFilter filter,
PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener) |
private static ImmutableList<NoPosTacletApp> |
antecTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services,
TacletIndex tacletIndex)
collects all AntecedentTaclet instantiations for the given
heuristics and SequentFormula
|
private ImmutableList<Pair<PosInOccurrence,ImmutableList<NoPosTacletApp>>> |
collectAllTacletAppsAffectedByModification(PIOPathIterator pathToModification,
ImmutableList<Pair<PosInOccurrence,ImmutableList<NoPosTacletApp>>> collectedApps)
Collects all taclet apps that are affected by a modification of the term
under consideration at place
pathToModification . |
private ImmutableList<Pair<PosInOccurrence,ImmutableList<NoPosTacletApp>>> |
collectAllTacletAppsHereAndBelow(PosInOccurrence pos,
ImmutableList<Pair<PosInOccurrence,ImmutableList<NoPosTacletApp>>> collectedApps)
Collect all
NoPosTacletApp s that are stored by
this (and by the sub-indices of this ). |
private ImmutableList<TacletApp> |
collectTacletApps(PosInOccurrence pos,
RuleFilter p_filter,
Services services)
Collect all taclet apps that are stored by
this (and by
the sub-indices of this ). |
private ImmutableList<TacletApp> |
convert(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos,
RuleFilter filter,
ImmutableList<TacletApp> convertedApps,
Services services) |
static TermTacletAppIndex |
create(PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
RuleFilter filter,
TermTacletAppIndexCacheSet indexCaches)
Create an index for the given term
|
private static TermTacletAppIndex |
createHelp(PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
RuleFilter filter,
ITermTacletAppIndexCache indexCache) |
private static ImmutableArray<TermTacletAppIndex> |
createSubIndices(PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
RuleFilter filter,
ITermTacletAppIndexCache indexCache)
Descend and create indices for each of the direct subterms of
the given term
|
private TermTacletAppIndex |
descend(PosInOccurrence pos) |
private static ITermTacletAppIndexCache |
determineIndexCache(PosInOccurrence pos,
TermTacletAppIndexCacheSet indexCaches) |
static ImmutableList<NoPosTacletApp> |
filter(RuleFilter p_filter,
ImmutableList<NoPosTacletApp> taclets) |
private static void |
fireRulesAdded(NewRuleListener listener,
ImmutableList<NoPosTacletApp> taclets,
PosInOccurrence pos) |
private static ImmutableList<NoPosTacletApp> |
getFindTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services,
TacletIndex tacletIndex)
collects all FindTaclets with instantiations for the given
heuristics and position
|
private static ImmutableList<NoPosTacletApp> |
getRewriteTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services,
TacletIndex tacletIndex)
collects all RewriteTacletInstantiations for the given
heuristics in a subterm of the constrainedFormula described by a
PosInOccurrence
|
private TermTacletAppIndex |
getSubIndex(int subterm) |
ImmutableList<NoPosTacletApp> |
getTacletAppAt(PosInOccurrence pos,
RuleFilter p_filter) |
ImmutableList<TacletApp> |
getTacletAppAtAndBelow(PosInOccurrence pos,
RuleFilter filter,
Services services) |
private ImmutableArray<TermTacletAppIndex> |
replace(ImmutableArray<TermTacletAppIndex> src,
int at,
TermTacletAppIndex newIndex) |
private void |
reportTacletApps(PIOPathIterator pathToModification,
NewRuleListener listener)
Report all taclet apps that are affected by a modification of the term
under consideration at place
pathToModification . |
(package private) void |
reportTacletApps(PosInOccurrence pos,
NewRuleListener listener)
Report all
NoPosTacletApp s that are stored by
this (and by the sub-indices of this ). |
private static ImmutableList<NoPosTacletApp> |
succTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services,
TacletIndex tacletIndex)
collects all SuccedentTaclet instantiations for the given
heuristics and SequentFormula
|
(package private) TermTacletAppIndex |
update(PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
TermTacletAppIndexCacheSet indexCaches)
Updates the TermTacletAppIndex after a change at or below
position
pos |
private TermTacletAppIndex |
updateCompleteRebuild(PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
ITermTacletAppIndexCache indexCache) |
private TermTacletAppIndex |
updateHelp(PIOPathIterator pathToModification,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
ITermTacletAppIndexCache indexCache)
Recursively update the term index, starting at
this and
descending along the given path iterator to the term position below which
a modification was performed |
private ImmutableArray<TermTacletAppIndex> |
updateIUpdateTarget(ImmutableArray<TermTacletAppIndex> oldSubindices,
int updateTarget,
PosInOccurrence targetPos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
ITermTacletAppIndexCache indexCache)
Update the target formula/term of an update (which has position
subtermPos in the complete formula). |
private TermTacletAppIndex |
updateLocalApps(PosInOccurrence pos,
Term newSubterm,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
ImmutableArray<TermTacletAppIndex> newSubIndices) |
private ImmutableArray<TermTacletAppIndex> |
updateOneSubIndex(ImmutableArray<TermTacletAppIndex> oldSubindices,
PIOPathIterator pathToModification,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
ITermTacletAppIndexCache indexCache)
Update the subtree of indices the given iterator
pathToModification descends to |
private ImmutableArray<TermTacletAppIndex> |
updateSubIndexes(PIOPathIterator pathToModification,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
ITermTacletAppIndexCache indexCache) |
private final Term term
private final ImmutableList<NoPosTacletApp> localTacletApps
private final ImmutableArray<TermTacletAppIndex> subtermIndices
private final RuleFilter ruleFilter
private TermTacletAppIndex(Term term, ImmutableList<NoPosTacletApp> localTacletApps, ImmutableArray<TermTacletAppIndex> subtermIndices, RuleFilter ruleFilter)
private TermTacletAppIndex getSubIndex(int subterm)
private static ImmutableList<NoPosTacletApp> getRewriteTaclet(PosInOccurrence pos, RuleFilter filter, Services services, TacletIndex tacletIndex)
pos
- the PosInOccurrence
to focusservices
- the Services
object encapsulating information
about the java datastructures like (static)types etc.private static ImmutableList<NoPosTacletApp> getFindTaclet(PosInOccurrence pos, RuleFilter filter, Services services, TacletIndex tacletIndex)
pos
- the PosInOccurrence to focusservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.private static ImmutableList<NoPosTacletApp> antecTaclet(PosInOccurrence pos, RuleFilter filter, Services services, TacletIndex tacletIndex)
pos
- the PosInOccurrence of the SequentFormula
the taclets have to be connected to
(pos must point to the top level formula, i.e. pos.isTopLevel() must be true)services
- the Services object encapsulating information
about the java datastructures like (static)types etc.private static ImmutableList<NoPosTacletApp> succTaclet(PosInOccurrence pos, RuleFilter filter, Services services, TacletIndex tacletIndex)
pos
- the PosInOccurrence of the SequentFormula
the taclets have to be connected to
(pos must point to the top level formula,
i.e. pos.isTopLevel() must be true)services
- the Services object encapsulating information
about the java datastructures like (static)types etc.private static ImmutableArray<TermTacletAppIndex> createSubIndices(PosInOccurrence pos, Services services, TacletIndex tacletIndex, NewRuleListener listener, RuleFilter filter, ITermTacletAppIndexCache indexCache)
pos
- pointer to the term/formula for whose subterms
indices are to be createdpublic static TermTacletAppIndex create(PosInOccurrence pos, Services services, TacletIndex tacletIndex, NewRuleListener listener, RuleFilter filter, TermTacletAppIndexCacheSet indexCaches)
pos
- Pointer to the term/formula for which an index is to be
created. pos
has to be a top-level term
positionprivate static ITermTacletAppIndexCache determineIndexCache(PosInOccurrence pos, TermTacletAppIndexCacheSet indexCaches)
private static TermTacletAppIndex createHelp(PosInOccurrence pos, Services services, TacletIndex tacletIndex, NewRuleListener listener, RuleFilter filter, ITermTacletAppIndexCache indexCache)
public TermTacletAppIndex addTaclets(RuleFilter filter, PosInOccurrence pos, Services services, TacletIndex tacletIndex, NewRuleListener listener)
filter
filter
- The taclets that are supposed to be addedpos
- Pointer to the term/formula for which an index is to
be created. pos
has to be a top-level term
positionprivate TermTacletAppIndex addTacletsHelp(RuleFilter filter, PosInOccurrence pos, Services services, TacletIndex tacletIndex, NewRuleListener listener)
private ImmutableArray<TermTacletAppIndex> addTacletsSubIndices(RuleFilter filter, PosInOccurrence pos, Services services, TacletIndex tacletIndex, NewRuleListener listener)
private TermTacletAppIndex updateHelp(PIOPathIterator pathToModification, Services services, TacletIndex tacletIndex, NewRuleListener listener, ITermTacletAppIndexCache indexCache)
this
and
descending along the given path iterator to the term position below which
a modification was performedpathToModification
- an iterator that walks from the root of the
formula to the position of modificationprivate TermTacletAppIndex updateCompleteRebuild(PosInOccurrence pos, Services services, TacletIndex tacletIndex, NewRuleListener listener, ITermTacletAppIndexCache indexCache)
private TermTacletAppIndex updateLocalApps(PosInOccurrence pos, Term newSubterm, Services services, TacletIndex tacletIndex, NewRuleListener listener, ImmutableArray<TermTacletAppIndex> newSubIndices)
private ImmutableArray<TermTacletAppIndex> updateSubIndexes(PIOPathIterator pathToModification, Services services, TacletIndex tacletIndex, NewRuleListener listener, ITermTacletAppIndexCache indexCache)
private ImmutableArray<TermTacletAppIndex> updateIUpdateTarget(ImmutableArray<TermTacletAppIndex> oldSubindices, int updateTarget, PosInOccurrence targetPos, Services services, TacletIndex tacletIndex, NewRuleListener listener, ITermTacletAppIndexCache indexCache)
subtermPos
in the complete formula). This is necessary
whenever a part of the update has changed, because this also changes the
update context of taclet apps in the target.private ImmutableArray<TermTacletAppIndex> updateOneSubIndex(ImmutableArray<TermTacletAppIndex> oldSubindices, PIOPathIterator pathToModification, Services services, TacletIndex tacletIndex, NewRuleListener listener, ITermTacletAppIndexCache indexCache)
pathToModification
descends toprivate ImmutableArray<TermTacletAppIndex> replace(ImmutableArray<TermTacletAppIndex> src, int at, TermTacletAppIndex newIndex)
TermTacletAppIndex update(PosInOccurrence pos, Services services, TacletIndex tacletIndex, NewRuleListener listener, TermTacletAppIndexCacheSet indexCaches)
pos
pos
- Pointer to the term/formula where a change occurredservices
- the ServicestacletIndex
- the TacletIndex to access tacletslistener
- the NewRuleListener to be register such that new rules can be reportedindexCaches
- cachesprivate TermTacletAppIndex descend(PosInOccurrence pos)
public ImmutableList<NoPosTacletApp> getTacletAppAt(PosInOccurrence pos, RuleFilter p_filter)
public ImmutableList<TacletApp> getTacletAppAtAndBelow(PosInOccurrence pos, RuleFilter filter, Services services)
private ImmutableList<TacletApp> convert(ImmutableList<? extends RuleApp> rules, PosInOccurrence pos, RuleFilter filter, ImmutableList<TacletApp> convertedApps, Services services)
private ImmutableList<TacletApp> collectTacletApps(PosInOccurrence pos, RuleFilter p_filter, Services services)
this
(and by
the sub-indices of this
). NoPosTacletApp
s are
converted to PosTacletApp
s using the parameter
pos
pos
- The position of this indexvoid reportTacletApps(PosInOccurrence pos, NewRuleListener listener)
NoPosTacletApp
s that are stored by
this
(and by the sub-indices of this
).pos
- The position of this indexlistener
- The listener to which the taclet apps found are supposed to be
reportedprivate ImmutableList<Pair<PosInOccurrence,ImmutableList<NoPosTacletApp>>> collectAllTacletAppsHereAndBelow(PosInOccurrence pos, ImmutableList<Pair<PosInOccurrence,ImmutableList<NoPosTacletApp>>> collectedApps)
NoPosTacletApp
s that are stored by
this
(and by the sub-indices of this
).pos
- The position of this indexcollectedApps
- the ImmutableMap>
to which
to add the found taclet applications; it must not contain
pos
or any position below pos as keyprivate void reportTacletApps(PIOPathIterator pathToModification, NewRuleListener listener)
pathToModification
. These are
the taclet above and below the place of modification, and the taclets
whose update context has changed.private ImmutableList<Pair<PosInOccurrence,ImmutableList<NoPosTacletApp>>> collectAllTacletAppsAffectedByModification(PIOPathIterator pathToModification, ImmutableList<Pair<PosInOccurrence,ImmutableList<NoPosTacletApp>>> collectedApps)
pathToModification
. These are
the taclet above and below the place of modification, and the taclets
whose update context has changed. The map of already collected
apps must not contain any entry for a position on or below the path to
modification.PosInOccurrence
private static void fireRulesAdded(NewRuleListener listener, ImmutableList<NoPosTacletApp> taclets, PosInOccurrence pos)
public static ImmutableList<NoPosTacletApp> filter(RuleFilter p_filter, ImmutableList<NoPosTacletApp> taclets)
p_filter
- the RuleFilter
to be usedtaclets
- the list of Taclet
s to be filtered