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

Class AntecTacletExecutor<TacletKind extends AntecTaclet>

java.lang.Object

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

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

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

Type Parameters:

TacletKind - the kind of taclet this executor is responsible for

All Implemented Interfaces:

RuleExecutor

public class AntecTacletExecutor<TacletKind extends AntecTaclet>
extends FindTacletExecutor<TacletKind>

Executes a Taclet which matches on a formula in the antecedent

Author:

Richard Bubel

Field Summary

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

taclet

Constructor Summary

Constructors

Constructor and Description
AntecTacletExecutor(TacletKind taclet)

Method Summary

Modifier and Type	Method and Description
protected 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 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

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

apply

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

AntecTacletExecutor

public AntecTacletExecutor(TacletKind taclet)

Method Detail

applyReplacewith

protected 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

Specified by:

applyReplacewith in class FindTacletExecutor<TacletKind extends AntecTaclet>

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 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

Specified by:

applyAdd in class FindTacletExecutor<TacletKind extends AntecTaclet>

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