public class RewriteTacletExecutor<TacletKind extends RewriteTaclet> extends FindTacletExecutor<TacletKind>
taclet
Constructor and Description |
---|
RewriteTacletExecutor(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)
adds the sequent of the add part of the Taclet to the goal sequent
|
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 |
private SequentFormula |
applyReplacewithHelper(Goal goal,
TermLabelState termLabelState,
RewriteTacletGoalTemplate gt,
PosInOccurrence posOfFind,
Services services,
MatchConditions matchCond,
RuleApp ruleApp) |
SequentFormula |
getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
private Term |
replace(Term term,
Term with,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence posOfFind,
IntIterator it,
MatchConditions mc,
Sort maxSort,
Goal goal,
Services services,
RuleApp ruleApp)
does the work for applyReplacewith (wraps recursion)
|
apply
addToAntec, addToSucc, applyAddProgVars, applyAddrule, checkIfGoals, instantiateSemisequent, replaceAtPos, syntacticalReplace
public RewriteTacletExecutor(TacletKind taclet)
private Term replace(Term term, Term with, TermLabelState termLabelState, Taclet.TacletLabelHint labelHint, PosInOccurrence posOfFind, IntIterator it, MatchConditions mc, Sort maxSort, Goal goal, Services services, RuleApp ruleApp)
private SequentFormula applyReplacewithHelper(Goal goal, TermLabelState termLabelState, RewriteTacletGoalTemplate gt, PosInOccurrence posOfFind, Services services, MatchConditions matchCond, RuleApp ruleApp)
public SequentFormula getRewriteResult(Goal goal, TermLabelState termLabelState, Services services, TacletApp app)
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 RewriteTaclet>
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)
applyAdd
in class FindTacletExecutor<TacletKind extends RewriteTaclet>
add
- the Sequent to be addedtermLabelState
- The TermLabelState
of the current rule application.currentSequent
- the Sequent which is the current (intermediate) result of
applying the tacletposOfFind
- describes the application position of the find expression
in the original sequentwhereToAdd
- the PosInOccurrence describes the place where to add the
semisequentmatchCond
- the MatchConditions with all required instantiationsgoal
- the Goal the taclet is applied toruleApp
- the rule application to applyservices
- the Services encapsulating all java information