TacletKind
- The kind of taclet that is executed.public abstract class TacletExecutor<TacletKind extends Taclet> extends java.lang.Object implements RuleExecutor
Modifier and Type | Field and Description |
---|---|
protected TacletKind |
taclet |
Constructor and Description |
---|
TacletExecutor(TacletKind taclet) |
Modifier and Type | Method and Description |
---|---|
protected void |
addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
adds SequentFormula to antecedent depending on
position information (if none is handed over it is added at the
head of the antecedent).
|
protected void |
addToSucc(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds SequentFormula to succedent depending on
position information (if none is handed over it is added at the
head of the succedent).
|
abstract ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp tacletApp)
applies the given rule application to the specified goal
|
protected void |
applyAddProgVars(ImmutableSet<SchemaVariable> pvs,
SequentChangeInfo currentSequent,
Goal goal,
PosInOccurrence posOfFind,
Services services,
MatchConditions matchCond) |
protected void |
applyAddrule(ImmutableList<Taclet> rules,
Goal goal,
Services services,
MatchConditions matchCond)
adds the given rules (i.e.
|
protected ImmutableList<SequentChangeInfo> |
checkIfGoals(Goal p_goal,
ImmutableList<IfFormulaInstantiation> p_list,
MatchConditions p_matchCond,
int p_numberOfNewGoals)
Search for formulas within p_list that have to be proved by an
explicit assumes-goal, i.e.
|
protected ImmutableList<SequentFormula> |
instantiateSemisequent(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
instantiates the given semisequent with the instantiations found in
Matchconditions
|
protected void |
replaceAtPos(Semisequent semi,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
MatchConditions matchCond,
Taclet.TacletLabelHint labelHint,
Goal goal,
RuleApp ruleApp,
Services services)
replaces the constrained formula at the given position with the first
formula in the given semisequent and adds possible other formulas of the
semisequent starting at the position
|
protected Term |
syntacticalReplace(Term term,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions mc,
Goal goal,
RuleApp ruleApp,
Services services)
a new term is created by replacing variables of term whose replacement is
found in the given SVInstantiations
|
protected final TacletKind extends Taclet taclet
public TacletExecutor(TacletKind taclet)
public abstract ImmutableList<Goal> apply(Goal goal, Services services, RuleApp tacletApp)
apply
in interface RuleExecutor
goal
- the goal that the rule application should refer to.services
- the Services encapsulating all java informationtacletApp
- the rule application that is executed.protected Term syntacticalReplace(Term term, TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, PosInOccurrence applicationPosInOccurrence, MatchConditions mc, Goal goal, RuleApp ruleApp, Services services)
term
- the Term
the syntactical replacement is performed ontermLabelState
- The TermLabelState
of the current rule application.labelHint
- the hint used to maintain TermLabel
s.applicationPosInOccurrence
- the PosInOccurrence
of the find term
in the sequent this taclet is applied tomc
- the MatchConditions
with all instantiations and
the constraintgoal
- the Goal
on which this taclet is appliedruleApp
- the RuleApp
with application informationservices
- the Services
with the Java model informationprotected ImmutableList<SequentFormula> instantiateSemisequent(Semisequent semi, TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, PosInOccurrence applicationPosInOccurrence, MatchConditions matchCond, Goal goal, RuleApp tacletApp, Services services)
semi
- the Semisequent to be instantiatedtermLabelState
- The TermLabelState
of the current rule application.labelHint
- The hint used to maintain TermLabel
s.applicationPosInOccurrence
- The PosInOccurrence
of the Term
which is rewrittenmatchCond
- the MatchConditions including the mapping
Schemavariables to concrete logic elementsservices
- the Servicesprotected void replaceAtPos(Semisequent semi, TermLabelState termLabelState, SequentChangeInfo currentSequent, PosInOccurrence pos, MatchConditions matchCond, Taclet.TacletLabelHint labelHint, Goal goal, RuleApp ruleApp, Services services)
semi
- the Semisequent with the the ConstrainedFormulae to be addedtermLabelState
- The TermLabelState
of the current rule application.currentSequent
- the Sequent which is the current (intermediate) result of applying the tacletpos
- the PosInOccurrence describing the place in the sequentmatchCond
- the MatchConditions containing in particularlabelHint
- The hint used to maintain TermLabel
s.
the instantiations of the schemavariablesservices
- the Services encapsulating all java informationprotected void addToAntec(Semisequent semi, TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, SequentChangeInfo currentSequent, PosInOccurrence pos, PosInOccurrence applicationPosInOccurrence, MatchConditions matchCond, Goal goal, RuleApp tacletApp, Services services)
semi
- the Semisequent with the the ConstrainedFormulae to be addedtermLabelState
- The TermLabelState
of the current rule application.labelHint
- The hint used to maintain TermLabel
s.currentSequent
- the Sequent which is the current (intermediate) result of applying the tacletpos
- the PosInOccurrence describing the place in the
sequent or null for head of antecedentapplicationPosInOccurrence
- The PosInOccurrence
of the Term
which is rewrittenmatchCond
- the MatchConditions containing in particular
the instantiations of the schemavariablesservices
- the Services encapsulating all java informationprotected void addToSucc(Semisequent semi, TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, SequentChangeInfo currentSequent, PosInOccurrence pos, PosInOccurrence applicationPosInOccurrence, MatchConditions matchCond, Goal goal, RuleApp ruleApp, Services services)
semi
- the Semisequent with the the ConstrainedFormulae to be addedtermLabelState
- The TermLabelState
of the current rule application.labelHint
- The hint used to maintain TermLabel
s.pos
- the PosInOccurrence describing the place in the
sequent or null for head of antecedentapplicationPosInOccurrence
- The PosInOccurrence
of the Term
which is rewrittenmatchCond
- the MatchConditions containing in particular
the instantiations of the schemavariablesgoal
- the Goal that knows the node the formulae have to be addedservices
- the Services encapsulating all java informationprotected void applyAddrule(ImmutableList<Taclet> rules, Goal goal, Services services, MatchConditions matchCond)
rules
- the rules to be addedgoal
- the goal describing the node where the rules should be addedservices
- the Services encapsulating all java informationmatchCond
- the MatchConditions containing in particular
the instantiations of the schemavariablesprotected void applyAddProgVars(ImmutableSet<SchemaVariable> pvs, SequentChangeInfo currentSequent, Goal goal, PosInOccurrence posOfFind, Services services, MatchConditions matchCond)
protected ImmutableList<SequentChangeInfo> checkIfGoals(Goal p_goal, ImmutableList<IfFormulaInstantiation> p_list, MatchConditions p_matchCond, int p_numberOfNewGoals)
p_goal
- the Goal
on which the taclet is appliedp_list
- the list of IfFormulaInstantiation
containing
the instantiations for the assumes formulasp_matchCond
- the MatchConditions
with the instantiations of the
schema variablesp_numberOfNewGoals
- the number of new goals the Taclet
creates in
any case because of existing TacletGoalTemplate
sCopyright © 2003-2019 The KeY-Project.