de.uka.ilkd.key.rule.executor.javadl

Class RewriteTacletExecutor<TacletKind extends RewriteTaclet>

java.lang.Object

de.uka.ilkd.key.rule.executor.javadl.TacletExecutor<TacletKind>

de.uka.ilkd.key.rule.executor.javadl.FindTacletExecutor<TacletKind>

de.uka.ilkd.key.rule.executor.javadl.RewriteTacletExecutor<TacletKind>

All Implemented Interfaces:

RuleExecutor

Direct Known Subclasses:

InfFlowContractAppTacletExecutor

public class RewriteTacletExecutor<TacletKind extends RewriteTaclet>
extends FindTacletExecutor<TacletKind>

Field Summary

Fields inherited from class de.uka.ilkd.key.rule.executor.javadl.TacletExecutor

taclet

Constructor Summary

Constructors

Constructor and Description
RewriteTacletExecutor(TacletKind taclet)

Method Summary

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)

Methods inherited from class de.uka.ilkd.key.rule.executor.javadl.FindTacletExecutor

apply

Methods inherited from class de.uka.ilkd.key.rule.executor.javadl.TacletExecutor

addToAntec, addToSucc, applyAddProgVars, applyAddrule, checkIfGoals, instantiateSemisequent, replaceAtPos, syntacticalReplace

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

RewriteTacletExecutor

public RewriteTacletExecutor(TacletKind taclet)

Method Detail

replace

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)

applyReplacewithHelper

private SequentFormula applyReplacewithHelper(Goal goal,
                                              TermLabelState termLabelState,
                                              RewriteTacletGoalTemplate gt,
                                              PosInOccurrence posOfFind,
                                              Services services,
                                              MatchConditions matchCond,
                                              RuleApp ruleApp)

getRewriteResult

public SequentFormula getRewriteResult(Goal goal,
                                       TermLabelState termLabelState,
                                       Services services,
                                       TacletApp app)

applyReplacewith

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

Specified by:

applyReplacewith in class FindTacletExecutor<TacletKind extends RewriteTaclet>

Parameters:

gt - the TacletGoalTemplate used to get the taclet's replacewith-expression

termLabelState - The TermLabelState of the current rule application.

currentSequent - the SequentChangeInfo which is the current (intermediate) result of applying the taclet

posOfFind - the PosInOccurrence belonging to the find expression

matchCond - the MatchConditions with all required instantiations

goal - the Goal on which the taclet is applied

ruleApp - the TacletApp describing the current ongoing taclet application

services - the Services encapsulating all Java model information

applyAdd

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

Specified by:

applyAdd in class FindTacletExecutor<TacletKind extends RewriteTaclet>

Parameters:

add - the Sequent to be added

termLabelState - The TermLabelState of the current rule application.

currentSequent - the Sequent which is the current (intermediate) result of applying the taclet

posOfFind - describes the application position of the find expression in the original sequent

whereToAdd - the PosInOccurrence describes the place where to add the semisequent

matchCond - the MatchConditions with all required instantiations

goal - the Goal the taclet is applied to

ruleApp - the rule application to apply

services - the Services encapsulating all java information