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 whereToAdd,
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 |
private PosInOccurrence |
updatePositionInformation(TacletApp tacletApp,
TacletGoalTemplate gt,
SequentChangeInfo currentSequent)
creates a new position information object, describing where to add the formulas or
null if it should just be added to the beginning |
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 whereToAdd, 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 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 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.private PosInOccurrence updatePositionInformation(TacletApp tacletApp, TacletGoalTemplate gt, SequentChangeInfo currentSequent)
null
if it should just be added to the beginningtacletApp
- a TacletApp with application informationgt
- the TacletGoalTemplate to be appliedcurrentSequent
- the current sequent (the one of the new goal)