public class SemisequentTacletAppIndex
extends java.lang.Object
TermTacletAppIndex
s for all formulas of
a semisequent.Modifier and Type | Field and Description |
---|---|
private boolean |
antec |
private TermTacletAppIndexCacheSet |
indexCaches |
private RuleFilter |
ruleFilter |
private Sequent |
seq |
private ImmutableMap<SequentFormula,TermTacletAppIndex> |
termIndices |
Modifier | Constructor and Description |
---|---|
private |
SemisequentTacletAppIndex(SemisequentTacletAppIndex orig) |
(package private) |
SemisequentTacletAppIndex(Sequent s,
boolean antec,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
RuleFilter ruleFilter,
TermTacletAppIndexCacheSet indexCaches)
Create an index object for the semisequent determined by
s and antec that contains term
indices for each formula. |
Modifier and Type | Method and Description |
---|---|
private void |
addTaclets(RuleFilter filter,
SequentFormula cfma,
Sequent s,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Update the index for the given formula, which is supposed to be an
element of the map
termIndices , by adding the taclets that
are selected by filter
Note: destructive, use only when constructing new index |
SemisequentTacletAppIndex |
addTaclets(RuleFilter filter,
Sequent s,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Create an index that additionally contains the taclets that are selected
by
filter |
private void |
addTermIndex(SequentFormula cfma,
Sequent s,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Add an index for the given formula to the map
termIndices . |
private void |
addTermIndices(ImmutableList<SequentFormula> cfmas,
Sequent s,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Add indices for the given formulas to the map
termIndices . |
SemisequentTacletAppIndex |
copy() |
ImmutableList<NoPosTacletApp> |
getTacletAppAt(PosInOccurrence pos,
RuleFilter filter) |
ImmutableList<TacletApp> |
getTacletAppAtAndBelow(PosInOccurrence pos,
RuleFilter filter,
Services services) |
private TermTacletAppIndex |
getTermIndex(PosInOccurrence pos)
Get term index for the formula to which position
pos points |
private ImmutableList<TermTacletAppIndex> |
removeFormulas(ImmutableList<FormulaChangeInfo> infos)
Remove the formulas that are listed as modified by
infos |
private void |
removeTermIndex(SequentFormula cfma)
Remove the index for the given formula from the map
termIndices . |
private void |
removeTermIndices(ImmutableList<SequentFormula> cfmas)
Remove the indices for the given formulas from the map
termIndices . |
(package private) void |
reportRuleApps(NewRuleListener l)
Reports all cached rule apps.
|
SemisequentTacletAppIndex |
sequentChanged(SequentChangeInfo sci,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
called if a formula has been replaced
|
(package private) void |
setIndexCache(TermTacletAppIndexCacheSet indexCaches) |
private void |
updateTermIndices(ImmutableList<FormulaChangeInfo> infos,
Sequent newSeq,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener) |
private void |
updateTermIndices(ImmutableList<TermTacletAppIndex> oldIndices,
ImmutableList<FormulaChangeInfo> infos,
Sequent newSeq,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Update the given list of term indices according to the list
infos of modification information. |
private ImmutableMap<SequentFormula,TermTacletAppIndex> termIndices
private TermTacletAppIndexCacheSet indexCaches
private final RuleFilter ruleFilter
private final Sequent seq
private final boolean antec
SemisequentTacletAppIndex(Sequent s, boolean antec, Services services, TacletIndex tacletIndex, NewRuleListener listener, RuleFilter ruleFilter, TermTacletAppIndexCacheSet indexCaches)
s
and antec
that contains term
indices for each formula.antec
- iff true create an index for the antecedent of
s
, otherwise for the succedentprivate SemisequentTacletAppIndex(SemisequentTacletAppIndex orig)
private void addTermIndices(ImmutableList<SequentFormula> cfmas, Sequent s, Services services, TacletIndex tacletIndex, NewRuleListener listener)
termIndices
. Existing entries are replaced with
the new indices.
Note: destructive, use only when constructing new indexprivate void addTermIndex(SequentFormula cfma, Sequent s, Services services, TacletIndex tacletIndex, NewRuleListener listener)
termIndices
. An existing entry is replaced with
the new one.
Note: destructive, use only when constructing new indexprivate void addTaclets(RuleFilter filter, SequentFormula cfma, Sequent s, Services services, TacletIndex tacletIndex, NewRuleListener listener)
termIndices
, by adding the taclets that
are selected by filter
Note: destructive, use only when constructing new indexprivate void removeTermIndices(ImmutableList<SequentFormula> cfmas)
termIndices
.
Note: destructive, use only when constructing new indexprivate void removeTermIndex(SequentFormula cfma)
termIndices
.
Note: destructive, use only when constructing new indexprivate ImmutableList<TermTacletAppIndex> removeFormulas(ImmutableList<FormulaChangeInfo> infos)
infos
infos
Note: destructive, use only when constructing new indexprivate void updateTermIndices(ImmutableList<TermTacletAppIndex> oldIndices, ImmutableList<FormulaChangeInfo> infos, Sequent newSeq, Services services, TacletIndex tacletIndex, NewRuleListener listener)
infos
of modification information. Both lists have
to be compatible, i.e. same length and same order. The new
indices are inserted in the map termIndices
.
Note: destructive, use only when constructing new indexprivate void updateTermIndices(ImmutableList<FormulaChangeInfo> infos, Sequent newSeq, Services services, TacletIndex tacletIndex, NewRuleListener listener)
public SemisequentTacletAppIndex copy()
private TermTacletAppIndex getTermIndex(PosInOccurrence pos)
pos
pointspublic ImmutableList<NoPosTacletApp> getTacletAppAt(PosInOccurrence pos, RuleFilter filter)
public ImmutableList<TacletApp> getTacletAppAtAndBelow(PosInOccurrence pos, RuleFilter filter, Services services)
public SemisequentTacletAppIndex sequentChanged(SequentChangeInfo sci, Services services, TacletIndex tacletIndex, NewRuleListener listener)
sci
- SequentChangeInfo describing the change of the sequentpublic SemisequentTacletAppIndex addTaclets(RuleFilter filter, Sequent s, Services services, TacletIndex tacletIndex, NewRuleListener listener)
filter
filter
- The taclets that are supposed to be addedvoid reportRuleApps(NewRuleListener l)
void setIndexCache(TermTacletAppIndexCacheSet indexCaches)