de.uka.ilkd.key.rule

Class AntecTaclet

java.lang.Object

de.uka.ilkd.key.rule.Taclet

de.uka.ilkd.key.rule.FindTaclet

de.uka.ilkd.key.rule.AntecTaclet

All Implemented Interfaces:

Named, Rule

public class AntecTaclet
extends FindTaclet

An AntecTaclet represents a taclet whose find part has to match a top level formula in the antecedent of the sequent.

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
private boolean	ignoreTopLevelUpdates

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

AntecTaclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> heuristics, TacletAttributes attrs, Term find, boolean ignoreTopLevelUpdates, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, ImmutableSet<Choice> choices, ImmutableSet<TacletAnnotation> tacletAnnotations) creates a Schematic Theory Specific Rule (Taclet) with the given parameters.

Method Summary

Modifier and Type	Method and Description
protected void	createAndInitializeExecutor()
boolean	ignoreTopLevelUpdates() this method is used to determine if top level updates are allowed to be ignored.
AntecTaclet	setName(java.lang.String s)
protected java.lang.StringBuffer	toStringFind(java.lang.StringBuffer sb) toString for the find part

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, getExecutor, 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

ignoreTopLevelUpdates

private final boolean ignoreTopLevelUpdates

Constructor Detail

AntecTaclet

public AntecTaclet(Name name,
                   TacletApplPart applPart,
                   ImmutableList<TacletGoalTemplate> goalTemplates,
                   ImmutableList<RuleSet> heuristics,
                   TacletAttributes attrs,
                   Term find,
                   boolean ignoreTopLevelUpdates,
                   ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
                   ImmutableSet<Choice> choices,
                   ImmutableSet<TacletAnnotation> tacletAnnotations)

creates a Schematic Theory Specific Rule (Taclet) with the given parameters.

Parameters:

name - the name of the Taclet

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

goalTemplates - a list of goal descriptions.

heuristics - a list of heurisics for the Taclet

attrs - attributes for the Taclet; 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

Method Detail

ignoreTopLevelUpdates

public boolean ignoreTopLevelUpdates()

this method is used to determine if top level updates are allowed to be ignored. This may be 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

toStringFind

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

toString for the find part

Overrides:

toStringFind in class FindTaclet

createAndInitializeExecutor

protected void createAndInitializeExecutor()

Specified by:

createAndInitializeExecutor in class Taclet

setName

public AntecTaclet setName(java.lang.String s)

Specified by:

setName in class Taclet