public class RewriteTacletExecutor<TacletKind extends RewriteTaclet> extends FindTacletExecutor<TacletKind>
taclet
Constructor and Description |
---|
RewriteTacletExecutor(TacletKind taclet) |
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)
adds the sequent of the add part of the Taclet to the goal sequent
|
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 |
SequentFormula |
getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
apply
addToAntec, addToSucc, applyAddProgVars, applyAddrule, checkIfGoals, instantiateSemisequent, replaceAtPos, syntacticalReplace
public RewriteTacletExecutor(TacletKind taclet)
public SequentFormula getRewriteResult(Goal goal, TermLabelState termLabelState, Services services, TacletApp app)
protected void applyReplacewith(TacletGoalTemplate gt, TermLabelState termLabelState, SequentChangeInfo currentSequent, PosInOccurrence posOfFind, MatchConditions matchCond, Goal goal, RuleApp ruleApp, Services services)
replacewith
-expression of taclet goal descriptionsapplyReplacewith
in class FindTacletExecutor<TacletKind extends RewriteTaclet>
gt
- the TacletGoalTemplate
used to get the taclet's
replacewith
-expressiontermLabelState
- The TermLabelState
of the current rule application.currentSequent
- the SequentChangeInfo
which is the current (intermediate)
result of applying the tacletposOfFind
- the PosInOccurrence
belonging to the find expressionmatchCond
- the MatchConditions
with all required instantiationsgoal
- the Goal
on which the taclet is appliedruleApp
- the TacletApp
describing the current ongoing taclet applicationservices
- the Services
encapsulating all Java model informationprotected void applyAdd(Sequent add, TermLabelState termLabelState, SequentChangeInfo currentSequent, PosInOccurrence whereToAdd, PosInOccurrence posOfFind, MatchConditions matchCond, Goal goal, RuleApp ruleApp, Services services)
applyAdd
in class FindTacletExecutor<TacletKind extends RewriteTaclet>
add
- the Sequent to be addedtermLabelState
- The TermLabelState
of the current rule application.currentSequent
- the Sequent which is the current (intermediate) result of
applying the tacletposOfFind
- describes the application position of the find expression
in the original sequentwhereToAdd
- the PosInOccurrence describes the place where to add the
semisequentmatchCond
- the MatchConditions with all required instantiationsgoal
- the Goal the taclet is applied toruleApp
- the rule application to applyservices
- the Services encapsulating all java informationCopyright © 2003-2019 The KeY-Project.