de.uka.ilkd.key.rule

Class RewriteTaclet

java.lang.Object

de.uka.ilkd.key.rule.Taclet

de.uka.ilkd.key.rule.FindTaclet

de.uka.ilkd.key.rule.RewriteTaclet

All Implemented Interfaces:

Named, Rule

Direct Known Subclasses:

InfFlowContractAppTaclet

public class RewriteTaclet
extends FindTaclet

A RewriteTaclet represents a taclet, whose find can be matched against any term in the sequent no matter where it occurs. The only constraint to be fulfilled is that the term matches the structure described by the term of the find-part.

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.rule.Taclet

Taclet.TacletLabelHint

Field Summary

Fields

Modifier and Type	Field and Description
static int	ANTECEDENT_POLARITY If the surrounding formula has been decomposed completely, the find-term will NOT appear on the SUCcedent.
private int	applicationRestriction encodes restrictions on the state where a rewrite taclet is applicable If the value is equal to NONE no state restrictions are posed SAME_UPDATE_LEVEL then \assumes must match on a formula within the same state as \find rsp.
static int	IN_SEQUENT_STATE all taclet constituents must be in the same state as the sequent
static int	NONE does not pose state restrictions on valid matchings
static int	SAME_UPDATE_LEVEL all taclet constituents must appear in the same state (and not below a modality (for efficiency reasons))
static int	SUCCEDENT_POLARITY If the surrounding formula has been decomposed completely, the find-term will NOT appear on the ANTEcedent.

Fields inherited from class de.uka.ilkd.key.rule.FindTaclet

find

Fields inherited from class de.uka.ilkd.key.rule.Taclet

choices, executor, prefixMap, ruleSets, tacletAnnotations, tacletAsString

Constructor Summary

Constructors

Constructor and Description
RewriteTaclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> ruleSets, TacletAttributes attrs, Term find, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, int p_applicationRestriction, ImmutableSet<Choice> choices, boolean surviveSymbExec, ImmutableSet<TacletAnnotation> tacletAnnotations)
RewriteTaclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> ruleSets, TacletAttributes attrs, Term find, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, int p_applicationRestriction, ImmutableSet<Choice> choices, ImmutableSet<TacletAnnotation> tacletAnnotations) creates a Schematic Theory Specific Rule (Taclet) with the given parameters that represents a rewrite rule.

Method Summary

Modifier and Type	Method and Description
MatchConditions	checkPrefix(PosInOccurrence p_pos, MatchConditions p_mc) For taclets with getSameUpdatePrefix (), collect the updates above p_pos and add them to the update context of the instantiations object p_mc.
protected void	createAndInitializeExecutor()
int	getApplicationRestriction() returns the int encoding the kind of state restriction this rewrite taclet must obey
RewriteTacletExecutor<? extends RewriteTaclet>	getExecutor()
SequentFormula	getRewriteResult(Goal goal, TermLabelState termLabelState, Services services, TacletApp app)
boolean	ignoreTopLevelUpdates() this method is used to determine if top level updates are allowed to be ignored.
private int	polarity(Operator op, PIOPathIterator it, int polarity) Compute polarity
RewriteTaclet	setName(java.lang.String s)
protected java.lang.StringBuffer	toStringFind(java.lang.StringBuffer sb)
private boolean	veto(Term t) the top level operator has to be a simultaneous update.

Methods inherited from class de.uka.ilkd.key.rule.FindTaclet

equals, find, getBoundVariablesHelper, getIfFindVariables, hashCode, toString

Methods inherited from class de.uka.ilkd.key.rule.Taclet

admissible, admissibleAutomatic, admissibleInteractive, apply, closeGoal, collectSchemaVars, createAndInitializeMatcher, createTacletServices, displayName, getBoundVariables, getChoices, getIfVariables, getMatcher, getNameCorrespondent, getPrefix, getRuleJustification, getRuleSets, getSurviveSymbExec, getTrigger, getVariableConditions, goalTemplates, hasReplaceWith, hasTrigger, ifSequent, isContextInPrefix, name, prefixMap, ruleSets, toStringAttribs, toStringGoalTemplates, toStringIf, toStringRuleSets, toStringVarCond, varDeclaredNew, varsNew, varsNewDependingOn, varsNotFreeIn

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

NONE

public static final int NONE

does not pose state restrictions on valid matchings

See Also:

Constant Field Values

SAME_UPDATE_LEVEL

public static final int SAME_UPDATE_LEVEL

all taclet constituents must appear in the same state (and not below a modality (for efficiency reasons))

See Also:

Constant Field Values

IN_SEQUENT_STATE

public static final int IN_SEQUENT_STATE

all taclet constituents must be in the same state as the sequent

See Also:

Constant Field Values

ANTECEDENT_POLARITY

public static final int ANTECEDENT_POLARITY

If the surrounding formula has been decomposed completely, the find-term will NOT appear on the SUCcedent. The formula "wellformed(h)" in "wellformed(h) ==>" or in "==> wellformed(h) -> (inv(h) = inv(h2))" or in "==> \if(b) \then(!wellformed(h)) \else(!wellformed(h2))" has antecedent polarity. The formula "wellformed(h)" in "wellformed(h) <-> wellformed(h2) ==>" has NO antecedent polarity.

See Also:

Constant Field Values

SUCCEDENT_POLARITY

public static final int SUCCEDENT_POLARITY

If the surrounding formula has been decomposed completely, the find-term will NOT appear on the ANTEcedent. The formula "wellformed(h)" in "==> wellformed(h)" or in "wellformed(h) -> (inv(h) = inv(h2)) ==>" or in "\if(b) \then(!wellformed(h)) \else(!wellformed(h2)) ==>" has succedent polarity. The formula "wellformed(h)" in "wellformed(h) <-> wellformed(h2) ==>" has NO succedent polarity.

See Also:

Constant Field Values

applicationRestriction

private int applicationRestriction

encodes restrictions on the state where a rewrite taclet is applicable If the value is equal to

• NONE no state restrictions are posed
• SAME_UPDATE_LEVEL then \assumes must match on a formula within the same state as \find rsp. \add. For efficiency no modalities are allowed above the \find position
• IN_SEQUENT_STATE the \find part is only allowed to match on formulas which are evaluated in the same state as the sequent

Constructor Detail

RewriteTaclet

public RewriteTaclet(Name name,
                     TacletApplPart applPart,
                     ImmutableList<TacletGoalTemplate> goalTemplates,
                     ImmutableList<RuleSet> ruleSets,
                     TacletAttributes attrs,
                     Term find,
                     ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
                     int p_applicationRestriction,
                     ImmutableSet<Choice> choices,
                     ImmutableSet<TacletAnnotation> tacletAnnotations)

creates a Schematic Theory Specific Rule (Taclet) with the given parameters that represents a rewrite rule.

Parameters:

name - the Name of the Taclet

applPart - the TacletApplPart that contains the application part of an Taclet that is the if-sequent, the variable conditions

goalTemplates - a list of goal descriptions.

ruleSets - a list of rule sets for the Taclet

attrs - the TacletAttributes; these are boolean values indicating a noninteractive or recursive use of the Taclet.

find - the find term of the Taclet

prefixMap - a ImmMap that contains the prefix for each SchemaVariable in the Taclet

p_applicationRestriction - an int defining state restrictions of the taclet (required for location check)

choices - the SetOf to which this taclet belongs to

RewriteTaclet

public RewriteTaclet(Name name,
                     TacletApplPart applPart,
                     ImmutableList<TacletGoalTemplate> goalTemplates,
                     ImmutableList<RuleSet> ruleSets,
                     TacletAttributes attrs,
                     Term find,
                     ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
                     int p_applicationRestriction,
                     ImmutableSet<Choice> choices,
                     boolean surviveSymbExec,
                     ImmutableSet<TacletAnnotation> tacletAnnotations)

Method Detail

createAndInitializeExecutor

protected void createAndInitializeExecutor()

Specified by:

createAndInitializeExecutor in class Taclet

ignoreTopLevelUpdates

public boolean ignoreTopLevelUpdates()

this method is used to determine if top level updates are allowed to be ignored. This is the case if we have an Antec or SuccTaclet but not for a RewriteTaclet

Specified by:

ignoreTopLevelUpdates in class FindTaclet

Returns:

true if top level updates shall be ignored

getApplicationRestriction

public int getApplicationRestriction()

returns the int encoding the kind of state restriction this rewrite taclet must obey

Returns:

the int encoding the kind of state restriction this rewrite taclet must obey

veto

private boolean veto(Term t)

the top level operator has to be a simultaneous update. This method checks if the assignment pairs of the update contain free logic variables and gives a veto if positive

Parameters:

t - the Term to check

Returns:

false if vetoing

checkPrefix

public MatchConditions checkPrefix(PosInOccurrence p_pos,
                                   MatchConditions p_mc)

For taclets with getSameUpdatePrefix (), collect the updates above p_pos and add them to the update context of the instantiations object p_mc.

Returns:

the new instantiations with the additional updates, or null, if program modalities appear above p_pos

polarity

private int polarity(Operator op,
                     PIOPathIterator it,
                     int polarity)

Compute polarity

See Also:

seems to reimplement this.

toStringFind

protected java.lang.StringBuffer toStringFind(java.lang.StringBuffer sb)

Overrides:

toStringFind in class FindTaclet

getExecutor

public RewriteTacletExecutor<? extends RewriteTaclet> getExecutor()

Overrides:

getExecutor in class Taclet

getRewriteResult

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

setName

public RewriteTaclet setName(java.lang.String s)

Specified by:

setName in class Taclet