public class SuccTacletExecutor<TacletKind extends SuccTaclet> extends FindTacletExecutor<TacletKind>
taclet
Constructor and Description |
---|
SuccTacletExecutor(TacletKind taclet) |
Modifier and Type | Method and Description |
---|---|
protected void |
applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
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 |
apply
addToAntec, addToSucc, applyAddProgVars, applyAddrule, checkIfGoals, instantiateSemisequent, replaceAtPos, syntacticalReplace
public SuccTacletExecutor(TacletKind taclet)
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 SuccTaclet>
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 posOfFind, MatchConditions matchCond, Goal goal, RuleApp ruleApp, Services services)
add
-expressions of taclet goal descriptionsapplyAdd
in class FindTacletExecutor<TacletKind extends SuccTaclet>
add
- the Sequent
with the uninstantiated SequentFormula
's to be added to the goal's sequenttermLabelState
- The TermLabelState
of the current rule application.currentSequent
- the SequentChangeInfo
which is the current (intermediate) result of applying the tacletposOfFind
- the PosInOccurrence
providing the position information where the match took place
(it will be tried to add the new formulas close to that position)matchCond
- the MatchConditions
with all required instantiationsruleApp
- the TacletApp
describing the current ongoing taclet applicationservices
- the Services
encapsulating all Java model information