public class AntecTacletExecutor<TacletKind extends AntecTaclet> extends FindTacletExecutor<TacletKind>
taclet
Constructor and Description |
---|
AntecTacletExecutor(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)
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 |
apply
addToAntec, addToSucc, applyAddProgVars, applyAddrule, checkIfGoals, instantiateSemisequent, replaceAtPos, syntacticalReplace
public AntecTacletExecutor(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 AntecTaclet>
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)
applyAdd
in class FindTacletExecutor<TacletKind extends AntecTaclet>
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
- the PosInOccurrence describes the place where to add
the semisequentmatchCond
- the MatchConditions with all required instantiationsservices
- the Services encapsulating all java informationruleApp
- the TacletApp
describing the current ongoing taclet application