TacletKind
- the kind of taclet this executor is responsible forpublic 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 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 |
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 whereToAdd, PosInOccurrence posOfFind, MatchConditions matchCond, Goal goal, RuleApp ruleApp, Services services)
add
-expressions of taclet goal descriptionsapplyAdd
in class FindTacletExecutor<TacletKind extends AntecTaclet>
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 tacletwhereToAdd
- 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 placematchCond
- the MatchConditions
with all required instantiationsgoal
- the Goal where the taclet is applied toruleApp
- the TacletApp
describing the current ongoing taclet applicationservices
- the Services
encapsulating all Java model information