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 |
---|---|
private static java.lang.String |
AUTONAME |
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).
|
private void |
addToPos(Semisequent semi,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
boolean antec,
Taclet.TacletLabelHint labelHint,
MatchConditions matchCond,
Goal goal,
Services services,
RuleApp tacletApp)
instantiates the constrained formulas of semisequent
semi and adds the instantiatied formulas at the specified
position to goal |
private void |
addToPosWithoutInst(SequentFormula frm,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
boolean antec)
adds SequentFormula to antecedent or succedent depending on
position information or the boolean antec
contrary to "addToPos" frm will not be modified
|
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. the rules to add according to the Taclet goal
template to the node of the given goal
|
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. elements of type IfFormulaInstDirect.
|
private SequentFormula |
instantiateReplacement(TermLabelState termLabelState,
SequentFormula schemaFormula,
Services services,
MatchConditions matchCond,
PosInOccurrence applicationPosInOccurrence,
Taclet.TacletLabelHint labelHint,
Goal goal,
RuleApp tacletApp)
the given constrained formula is instantiated and then
the result (usually a complete instantiated formula) is returned.
|
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
|
private static final java.lang.String AUTONAME
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 informationprivate void addToPosWithoutInst(SequentFormula frm, SequentChangeInfo currentSequent, PosInOccurrence pos, boolean antec)
frm
- the SequentFormula
that should be addedcurrentSequent
- the SequentChangeInfo
which is the current (intermediate) result of applying the tacletpos
- the PosInOccurrence
describing the place in the sequentantec
- boolean true(false) if elements have to be added to the
antecedent(succedent) (only looked at if pos == null)private SequentFormula instantiateReplacement(TermLabelState termLabelState, SequentFormula schemaFormula, Services services, MatchConditions matchCond, PosInOccurrence applicationPosInOccurrence, Taclet.TacletLabelHint labelHint, Goal goal, RuleApp tacletApp)
termLabelState
- The TermLabelState
of the current rule application.schemaFormula
- the SequentFormula to be instantiatedservices
- the Services object carrying ja related informationmatchCond
- the MatchConditions object with the instantiations of
the schemavariables, constraints etc.applicationPosInOccurrence
- The PosInOccurrence
of the Term
which is rewrittenlabelHint
- The hint used to maintain TermLabel
s.protected 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 informationprivate void addToPos(Semisequent semi, TermLabelState termLabelState, SequentChangeInfo currentSequent, PosInOccurrence pos, PosInOccurrence applicationPosInOccurrence, boolean antec, Taclet.TacletLabelHint labelHint, MatchConditions matchCond, Goal goal, Services services, RuleApp tacletApp)
semi
and adds the instantiatied formulas at the specified
position to goal
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 sequentapplicationPosInOccurrence
- The PosInOccurrence
of the Term
which is rewrittenantec
- boolean true(false) if elements have to be added to the
antecedent(succedent) (only looked at if pos == null)labelHint
- The hint used to maintain TermLabel
s.
the instantiations of the schemavariablesmatchCond
- the MatchConditions containing in particularservices
- 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
s