| java.lang.Object
 de.uka.ilkd.key.proof.TacletAppIndex
| TacletAppIndex | | public class TacletAppIndex (Code) | | the class manages the available TacletApps. This index has to be
used if one wants to ask for the available taclet application at a
specific position (or the whole sequent if taclet is a nofind
rule). This means all taclet applications that have a position
information are managed by this index. For all others the class
TacletIndex is used. This index uses also the TacletIndex to
calculate new TacletApps.
|
| Method Summary | |
| public void | addedNoPosTacletApp(NoPosTacletApp tacletApp)
updates the internal caches after a new Taclet with instantiation
information has been added to the TacletIndex. | | public void | clearAndDetachCache()
Delete all cached information about taclet apps. | | public void | clearIndexes()
| | TacletAppIndex | copyWithTacletIndex(TacletIndex p_tacletIndex)
| | static TacletApp | createTacletApp(NoPosTacletApp tacletApp, PosInOccurrence pos)
| | static ListOfTacletApp | createTacletApps(ListOfNoPosTacletApp tacletInsts, PosInOccurrence pos)
| | public void | fillCache()
| | public ListOfNoPosTacletApp | getFindTaclet(PosInOccurrence pos, TacletFilter filter, Services services, Constraint userConstraint)
collects all FindTaclets with instantiations and position
Parameters:
pos - the PosInOccurrence to focus
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc. | | public ListOfNoPosTacletApp | getNoFindTaclet(TacletFilter filter, Services services, Constraint userConstraint)
collects all NoFindTacletInstantiations
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc. | | public ListOfNoPosTacletApp | getRewriteTaclet(PosInOccurrence pos, TacletFilter filter, Services services, Constraint userConstraint)
collects all RewriteTacletInstantiations in a subterm of the
constrainedFormula described by a
PosInOccurrence
Parameters:
pos - the PosInOccurrence to focus
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc. | | public ListOfTacletApp | getTacletAppAt(PosInOccurrence pos, TacletFilter filter, Services services, Constraint userConstraint)
returns the set of rule applications
at the given position of the given sequent. | | public ListOfTacletApp | getTacletAppAtAndBelow(PosInOccurrence pos, TacletFilter filter, Services services, Constraint userConstraint)
returns the rule applications at the given PosInOccurrence and at all
Positions below this. | | public void | removedNoPosTacletApp(NoPosTacletApp tacletApp)
updates the internal caches after a Taclet with instantiation
information has been removed from the TacletIndex. | | public void | reportRuleApps(NewRuleListener l, Services services, Constraint userConstraint)
Reports all cached rule apps. | | public void | sequentChanged(Goal goal, SequentChangeInfo sci)
| | public void | setNewRuleListener(NewRuleListener p_newRuleListener)
| | public void | setRuleFilter(RuleFilter p_ruleFilter)
| | public void | setup(Goal p_goal)
Set the goal association of this index to the given object
p_goal. | | public TacletIndex | tacletIndex()
returns the Taclet index for this ruleAppIndex. | | public String | toString()
|
| addedNoPosTacletApp | | public void addedNoPosTacletApp(NoPosTacletApp tacletApp)(Code) | | updates the internal caches after a new Taclet with instantiation
information has been added to the TacletIndex.
Parameters:
tacletApp - the partially instantiated Taclet to add |
| clearAndDetachCache | | public void clearAndDetachCache()(Code) | | Delete all cached information about taclet apps. This also makes the
index cache of this index independent from the caches of other indexes
(expensive)
|
| clearIndexes | | public void clearIndexes()(Code) | | |
| createTacletApps | | static ListOfTacletApp createTacletApps(ListOfNoPosTacletApp tacletInsts, PosInOccurrence pos)(Code) | | creates TacletApps out of each single NoPosTacletApp object
Parameters:
tacletInsts - the list of NoPosTacletApps the TacletApps are tobe created from
Parameters:
pos - the PosInOccurrence to focus list of all created TacletApps |
| fillCache | | public void fillCache()(Code) | | Forces all delayed computations to be performed, so that
the cache is fully up-to-date (NewRuleListener gets informed)
|
| getFindTaclet | | public ListOfNoPosTacletApp getFindTaclet(PosInOccurrence pos, TacletFilter filter, Services services, Constraint userConstraint)(Code) | | collects all FindTaclets with instantiations and position
Parameters:
pos - the PosInOccurrence to focus
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc. list of all possible instantiations |
| getNoFindTaclet | | public ListOfNoPosTacletApp getNoFindTaclet(TacletFilter filter, Services services, Constraint userConstraint)(Code) | | collects all NoFindTacletInstantiations
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc. list of all possible instantiations |
| getRewriteTaclet | | public ListOfNoPosTacletApp getRewriteTaclet(PosInOccurrence pos, TacletFilter filter, Services services, Constraint userConstraint)(Code) | | collects all RewriteTacletInstantiations in a subterm of the
constrainedFormula described by a
PosInOccurrence
Parameters:
pos - the PosInOccurrence to focus
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc. list of all possible instantiations |
| getTacletAppAt | | public ListOfTacletApp getTacletAppAt(PosInOccurrence pos, TacletFilter filter, Services services, Constraint userConstraint)(Code) | | returns the set of rule applications
at the given position of the given sequent.
Parameters:
pos - the PosInOccurrence to focus |
| getTacletAppAtAndBelow | | public ListOfTacletApp getTacletAppAtAndBelow(PosInOccurrence pos, TacletFilter filter, Services services, Constraint userConstraint)(Code) | | returns the rule applications at the given PosInOccurrence and at all
Positions below this. The method calls getTacletAppAt for all the
Positions below.
Parameters:
pos - the position where to start from
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc. the possible rule applications |
| removedNoPosTacletApp | | public void removedNoPosTacletApp(NoPosTacletApp tacletApp)(Code) | | updates the internal caches after a Taclet with instantiation
information has been removed from the TacletIndex.
Parameters:
tacletApp - the partially instantiated Taclet to remove |
| reportRuleApps | | public void reportRuleApps(NewRuleListener l, Services services, Constraint userConstraint)(Code) | | Reports all cached rule apps.
Calls ruleAdded on the given NewRuleListener for
every cached taclet app.
|
| sequentChanged | | public void sequentChanged(Goal goal, SequentChangeInfo sci)(Code) | | called if a formula has been replaced
Parameters:
sci - SequentChangeInfo describing the change of the sequent |
| setup | | public void setup(Goal p_goal)(Code) | | Set the goal association of this index to the given object
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.
|
| tacletIndex | | public TacletIndex tacletIndex()(Code) | | returns the Taclet index for this ruleAppIndex.
|
|
|