public final class RuleAppIndex
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private TacletAppIndex |
automatedTacletAppIndex |
private boolean |
autoMode
The current mode of the index: For
autoMode==true , the index
interactiveTacletAppIndex is not updated |
private BuiltInRuleAppIndex |
builtInRuleAppIndex |
private Goal |
goal |
private TacletAppIndex |
interactiveTacletAppIndex
Two
TacletAppIndex objects, one of which only contains rules
that have to be applied interactively, and the other one for rules that
can also be applied automatic. |
private java.util.List<NewRuleListener> |
listenerList |
private TacletIndex |
tacletIndex |
Modifier | Constructor and Description |
---|---|
|
RuleAppIndex(TacletAppIndex p_tacletAppIndex,
BuiltInRuleAppIndex p_builtInRuleAppIndex,
Services services) |
|
RuleAppIndex(TacletIndex p_tacletIndex,
BuiltInRuleAppIndex p_builtInRuleAppIndex,
Services services) |
private |
RuleAppIndex(TacletIndex tacletIndex,
TacletAppIndex interactiveTacletAppIndex,
TacletAppIndex automatedTacletAppIndex,
BuiltInRuleAppIndex builtInRuleAppIndex,
boolean autoMode) |
Modifier and Type | Method and Description |
---|---|
void |
addNewRuleListener(NewRuleListener l)
adds a change listener to the index
|
void |
addNoPosTacletApp(java.lang.Iterable<NoPosTacletApp> tacletApps)
adds a new Taclet with instantiation information to the Taclet Index
of this TacletAppIndex.
|
void |
addNoPosTacletApp(NoPosTacletApp tacletApp)
adds a new Taclet with instantiation information to the Taclet Index
of this TacletAppIndex.
|
void |
autoModeStarted()
Currently the rule app index can either operate in interactive mode (and
contain applications of all existing taclets) or in automatic mode (and
only contain a restricted set of taclets that can possibly be applied
automated).
|
void |
autoModeStopped() |
BuiltInRuleAppIndex |
builtInRuleAppIndex()
returns the built-in rule application index for this
ruleAppIndex.
|
void |
clearAndDetachCache()
Empties all caches
|
void |
clearIndexes()
Empties all caches
|
RuleAppIndex |
copy()
returns a new RuleAppIndex with a copied TacletIndex.
|
void |
fillCache()
Ensures that all caches are fully up-to-date
|
ImmutableList<IBuiltInRuleApp> |
getBuiltInRules(Goal g,
PosInOccurrence pos)
returns a list of built-in rule applications applicable
for the given goal, user defined constraint and position
|
ImmutableList<NoPosTacletApp> |
getFindTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all FindTacletInstantiations for the given
heuristics and position
|
ImmutableList<NoPosTacletApp> |
getNoFindTaclet(TacletFilter filter,
Services services)
collects all NoFindTacletInstantiations for the given
heuristics
|
ImmutableList<NoPosTacletApp> |
getRewriteTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all RewriteTacletInstantiations for the given
heuristics in a subterm of the constraintformula described by a
PosInOccurrence
|
ImmutableList<TacletApp> |
getTacletAppAt(TacletFilter filter,
PosInOccurrence pos,
Services services)
returns the set of rule applications for
the given heuristics
at the given position of the given sequent.
|
ImmutableList<TacletApp> |
getTacletAppAtAndBelow(TacletFilter filter,
PosInOccurrence pos,
Services services)
returns the rule applications at the given PosInOccurrence and at all
Positions below this.
|
private void |
informNewRuleListener(ImmutableList<? extends RuleApp> p_apps,
PosInOccurrence p_pos)
informs all observers, if a formula has been added, changed or
removed
|
private void |
informNewRuleListener(RuleApp p_app,
PosInOccurrence p_pos)
informs all observers, if a formula has been added, changed or
removed
|
void |
removeNewRuleListener(NewRuleListener l)
removes a change listener to the index
|
void |
removeNoPosTacletApp(NoPosTacletApp tacletApp)
remove a Taclet with instantiation information from the Taclet
Index of this TacletAppIndex.
|
void |
reportAutomatedRuleApps(NewRuleListener l,
Services services)
Report all rule applications that are supposed to be applied
automatically, and that are currently stored by the index
|
void |
scanBuiltInRules(Goal p_goal)
Report builtin rules to all registered NewRuleListener instances.
|
void |
sequentChanged(Goal g,
SequentChangeInfo sci)
called if a formula has been replaced
|
private void |
setNewRuleListeners() |
void |
setup(Goal p_goal) |
TacletIndex |
tacletIndex()
returns the Taclet index for this ruleAppIndex.
|
java.lang.String |
toString() |
private Goal goal
private TacletIndex tacletIndex
private TacletAppIndex interactiveTacletAppIndex
TacletAppIndex
objects, one of which only contains rules
that have to be applied interactively, and the other one for rules that
can also be applied automatic. This is used as an optimization, as only
the latter index has to be kept up to date while applying rules automatedprivate TacletAppIndex automatedTacletAppIndex
private BuiltInRuleAppIndex builtInRuleAppIndex
private java.util.List<NewRuleListener> listenerList
private boolean autoMode
autoMode==true
, the index
interactiveTacletAppIndex
is not updatedpublic RuleAppIndex(TacletAppIndex p_tacletAppIndex, BuiltInRuleAppIndex p_builtInRuleAppIndex, Services services)
public RuleAppIndex(TacletIndex p_tacletIndex, BuiltInRuleAppIndex p_builtInRuleAppIndex, Services services)
private RuleAppIndex(TacletIndex tacletIndex, TacletAppIndex interactiveTacletAppIndex, TacletAppIndex automatedTacletAppIndex, BuiltInRuleAppIndex builtInRuleAppIndex, boolean autoMode)
private void setNewRuleListeners()
public void setup(Goal p_goal)
public void autoModeStarted()
public void autoModeStopped()
public TacletIndex tacletIndex()
public BuiltInRuleAppIndex builtInRuleAppIndex()
public void addNewRuleListener(NewRuleListener l)
l
- the AppIndexListener to addpublic void removeNewRuleListener(NewRuleListener l)
l
- the AppIndexListener to removepublic ImmutableList<TacletApp> getTacletAppAt(TacletFilter filter, PosInOccurrence pos, Services services)
filter
- the TacletFiler filtering the taclets of interestpos
- the PosInOccurrence to focusservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<TacletApp> getTacletAppAtAndBelow(TacletFilter filter, PosInOccurrence pos, Services services)
filter
- the TacletFiler filtering the taclets of interestpos
- the position where to start fromservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<NoPosTacletApp> getFindTaclet(TacletFilter filter, PosInOccurrence pos, TermServices services)
filter
- the TacletFiler filtering the taclets of interestpos
- the PosInOccurrence to focusservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<NoPosTacletApp> getNoFindTaclet(TacletFilter filter, Services services)
filter
- the TacletFiler filtering the taclets of interestservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<NoPosTacletApp> getRewriteTaclet(TacletFilter filter, PosInOccurrence pos, TermServices services)
filter
- the TacletFiler filtering the taclets of interestpos
- the PosInOccurrence to focusservices
- the Services object encapsulating information
about the java datastructures like (static)types etc.public ImmutableList<IBuiltInRuleApp> getBuiltInRules(Goal g, PosInOccurrence pos)
public void addNoPosTacletApp(java.lang.Iterable<NoPosTacletApp> tacletApps)
tacletApp
- the NoPosTacletApp describing a partial instantiated Taclet to addpublic void addNoPosTacletApp(NoPosTacletApp tacletApp)
tacletApp
- the NoPosTacletApp describing a partial instantiated Taclet to addpublic void removeNoPosTacletApp(NoPosTacletApp tacletApp)
tacletApp
- the NoPosTacletApp to removepublic void sequentChanged(Goal g, SequentChangeInfo sci)
g
- the Goal which sequent has been changedsci
- SequentChangeInfo describing the change of the sequentpublic void clearAndDetachCache()
public void clearIndexes()
public void fillCache()
public void reportAutomatedRuleApps(NewRuleListener l, Services services)
l
- the NewRuleListenerservices
- the Servicespublic void scanBuiltInRules(Goal p_goal)
p_goal
- the Goal which to scanprivate void informNewRuleListener(RuleApp p_app, PosInOccurrence p_pos)
private void informNewRuleListener(ImmutableList<? extends RuleApp> p_apps, PosInOccurrence p_pos)
public RuleAppIndex copy()
public java.lang.String toString()
toString
in class java.lang.Object