de.uka.ilkd.key.rule.executor.javadl

Class FindTacletExecutor<TacletKind extends FindTaclet>

java.lang.Object

de.uka.ilkd.key.rule.executor.javadl.TacletExecutor<TacletKind>

de.uka.ilkd.key.rule.executor.javadl.FindTacletExecutor<TacletKind>

All Implemented Interfaces:

RuleExecutor

Direct Known Subclasses:

AntecTacletExecutor, RewriteTacletExecutor, SuccTacletExecutor

public abstract class FindTacletExecutor<TacletKind extends FindTaclet>
extends TacletExecutor<TacletKind>

Field Summary

Fields inherited from class de.uka.ilkd.key.rule.executor.javadl.TacletExecutor

taclet

Constructor Summary

Constructors

Constructor and Description
FindTacletExecutor(TacletKind taclet)

Method Summary

Modifier and Type	Method and Description
ImmutableList<Goal>	apply(Goal goal, Services services, RuleApp ruleApp) the rule is applied on the given goal using the information of rule application.
protected abstract void	applyAdd(Sequent add, TermLabelState termLabelState, SequentChangeInfo currentSequent, PosInOccurrence whereToAdd, PosInOccurrence posOfFind, MatchConditions matchCond, Goal goal, RuleApp ruleApp, Services services) applies the add-expressions of taclet goal descriptions
protected abstract void	applyReplacewith(TacletGoalTemplate gt, TermLabelState termLabelState, SequentChangeInfo currentSequent, PosInOccurrence posOfFind, MatchConditions matchCond, Goal goal, RuleApp ruleApp, Services services) applies the replacewith-expression of taclet goal descriptions
private PosInOccurrence	updatePositionInformation(TacletApp tacletApp, TacletGoalTemplate gt, SequentChangeInfo currentSequent) creates a new position information object, describing where to add the formulas or null if it should just be added to the beginning

Methods inherited from class de.uka.ilkd.key.rule.executor.javadl.TacletExecutor

addToAntec, addToSucc, applyAddProgVars, applyAddrule, checkIfGoals, instantiateSemisequent, replaceAtPos, syntacticalReplace

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

FindTacletExecutor

public FindTacletExecutor(TacletKind taclet)

Method Detail

applyReplacewith

protected abstract void applyReplacewith(TacletGoalTemplate gt,
                                         TermLabelState termLabelState,
                                         SequentChangeInfo currentSequent,
                                         PosInOccurrence posOfFind,
                                         MatchConditions matchCond,
                                         Goal goal,
                                         RuleApp ruleApp,
                                         Services services)

applies the replacewith-expression of taclet goal descriptions

Parameters:

gt - the TacletGoalTemplate used to get the taclet's replacewith-expression

termLabelState - The TermLabelState of the current rule application.

currentSequent - the SequentChangeInfo which is the current (intermediate) result of applying the taclet

posOfFind - the PosInOccurrence belonging to the find expression

matchCond - the MatchConditions with all required instantiations

goal - the Goal on which the taclet is applied

ruleApp - the TacletApp describing the current ongoing taclet application

services - the Services encapsulating all Java model information

applyAdd

protected abstract void applyAdd(Sequent add,
                                 TermLabelState termLabelState,
                                 SequentChangeInfo currentSequent,
                                 PosInOccurrence whereToAdd,
                                 PosInOccurrence posOfFind,
                                 MatchConditions matchCond,
                                 Goal goal,
                                 RuleApp ruleApp,
                                 Services services)

applies the add-expressions of taclet goal descriptions

Parameters:

add - the Sequent with the uninstantiated SequentFormula's to be added to the goal's sequent

termLabelState - The TermLabelState of the current rule application.

currentSequent - the SequentChangeInfo which is the current (intermediate) result of applying the taclet

whereToAdd - the PosInOccurrence where to add the sequent or null if it should just be added to the head of the sequent (otherwise it will be tried to add the new formulas close to that position)

posOfFind - the PosInOccurrence providing the position information where the match took place

matchCond - the MatchConditions with all required instantiations

goal - the Goal where the taclet is applied to

ruleApp - the TacletApp describing the current ongoing taclet application

services - the Services encapsulating all Java model information

apply

public final ImmutableList<Goal> apply(Goal goal,
                                       Services services,
                                       RuleApp ruleApp)

the rule is applied on the given goal using the information of rule application.

Specified by:

apply in interface RuleExecutor

Specified by:

apply in class TacletExecutor<TacletKind extends FindTaclet>

Parameters:

goal - the goal that the rule application should refer to.

services - the Services encapsulating all java information

ruleApp - the taclet application that is executed.

Returns:

List of the goals created by the rule which have to be proved. If this is a close-goal-taclet ( this.closeGoal () ), the first goal of the return list is the goal that should be closed (with the constraint this taclet is applied under).

updatePositionInformation

private PosInOccurrence updatePositionInformation(TacletApp tacletApp,
                                                  TacletGoalTemplate gt,
                                                  SequentChangeInfo currentSequent)

creates a new position information object, describing where to add the formulas or null if it should just be added to the beginning

Parameters:

tacletApp - a TacletApp with application information

gt - the TacletGoalTemplate to be applied

currentSequent - the current sequent (the one of the new goal)

Returns:

the PosInOccurrence object describing where to add the formula