public abstract class FindTacletExecutor<TacletKind extends FindTaclet> extends TacletExecutor<TacletKind>
taclet
Constructor and Description |
---|
FindTacletExecutor(TacletKind taclet) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
protected abstract 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 abstract 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 |
addToAntec, addToSucc, applyAddProgVars, applyAddrule, checkIfGoals, instantiateSemisequent, replaceAtPos, syntacticalReplace
public FindTacletExecutor(TacletKind taclet)
protected abstract void applyReplacewith(TacletGoalTemplate gt, TermLabelState termLabelState, SequentChangeInfo currentSequent, PosInOccurrence posOfFind, MatchConditions matchCond, Goal goal, RuleApp ruleApp, Services services)
replacewith
-expression of taclet goal descriptionsgt
- 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 abstract void applyAdd(Sequent add, TermLabelState termLabelState, SequentChangeInfo currentSequent, PosInOccurrence posOfFind, MatchConditions matchCond, Goal goal, RuleApp ruleApp, Services services)
add
-expressions of taclet goal descriptionsadd
- 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 informationpublic final ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
apply
in interface RuleExecutor
apply
in class TacletExecutor<TacletKind extends FindTaclet>
goal
- the goal that the rule application should refer to.services
- the Services encapsulating all java informationruleApp
- the taclet application that is executed.