public abstract class Taclet extends java.lang.Object implements Rule, Named
taclet_name { if ( ... ) find ( ... ) goal_descriptions }
The find part of a taclet is used to attached the rule to a term in the
sequent of the current goal. Therefore the term of the sequent has to match
the schema as found in the taclet's find part. The taclet is then attached to
this term, more precise not the taclet itself, but an application object of
this taclet (see TacletApp
. When
this attached taclet application object is applied, the new goals are
constructed as described by the goal descriptions. For example
find (A | B ==>) replacewith ( A ==> ); replacewith(B ==>)
creates
two new goals, where the first has been built by replacing A | B
with A
and the second one by replacing A | B
with
B
. For a complete description of the syntax and semantics of
taclets consult the KeY-Manual. The objects of this class serve different
purposes: First they represent the syntactical structure of a taclet, but
they also include the taclet interpreter isself. The taclet interpreter
knows two modes: the match and the execution mode. The match mode tries to
find a a mapping from schemavariables to a given term or formula. In the
execution mode, a given goal is manipulated in the manner as described by the
goal descriptions.
But an object of this class neither copies or split the goal, nor it
iterates through a sequent looking where it can be applied, these tasks have
to be done in advance. For example by one of the following classes
RuleAppIndex
or
TacletAppIndex
or
TacletApp
Modifier and Type | Class and Description |
---|---|
static class |
Taclet.TacletLabelHint
Instances of this class are used as hints to maintain
TermLabel s. |
Modifier and Type | Field and Description |
---|---|
private ImmutableSet<QuantifiableVariable> |
boundVariables
cache; contains set of all bound variables
|
protected ImmutableSet<Choice> |
choices
the set of taclet options for this taclet
|
private boolean |
contextInfoComputed
tracks state of pre-computation
|
private boolean |
contextIsInPrefix |
private java.lang.String |
displayName
name displayed by the pretty printer
|
protected TacletExecutor<? extends Taclet> |
executor
The taclet executor
|
private ImmutableList<TacletGoalTemplate> |
goalTemplates
the list of taclet goal descriptions
|
private int |
hashcode
Integer to cache the hashcode
|
private Sequent |
ifSequent
the if sequent of the taclet
|
private ImmutableSet<SchemaVariable> |
ifVariables
Set of schemavariables of the if part
|
private TacletMatcher |
matcher
The taclet matcher
|
private Name |
name
name of the taclet
|
protected ImmutableMap<SchemaVariable,TacletPrefix> |
prefixMap
map from a schemavariable to its prefix.
|
protected ImmutableList<RuleSet> |
ruleSets
list of rulesets (formerly known as heuristics) the taclet belongs to
|
private boolean |
surviveSymbExec |
private ImmutableMap<SchemaVariable,SchemaVariable> |
svNameCorrespondences
This map contains (a, b) if there is a substitution {b a}
somewhere in this taclet
|
protected ImmutableSet<TacletAnnotation> |
tacletAnnotations |
protected java.lang.String |
tacletAsString |
private Trigger |
trigger |
private ImmutableList<VariableCondition> |
variableConditions
Additional generic conditions for schema variable instantiations.
|
private ImmutableList<NewVarcond> |
varsNew
Variables that have to be created each time the taclet is applied.
|
private ImmutableList<NewDependingOn> |
varsNewDependingOn
Deprecated.
|
private ImmutableList<NotFreeIn> |
varsNotFreeIn
variables with a "x not free in y" variable condition.
|
Modifier | Constructor and Description |
---|---|
protected |
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSmbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Taclet (originally known as Schematic Theory Specific Rules)
|
protected |
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
Modifier and Type | Method and Description |
---|---|
boolean |
admissible(boolean interactive,
ImmutableList<RuleSet> p_ruleSets) |
protected boolean |
admissibleAutomatic(ImmutableList<RuleSet> admissibleRuleSets) |
protected boolean |
admissibleInteractive(ImmutableList<RuleSet> notAdmissibleRuleSets) |
ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp tacletApp)
applies the given rule application to the specified goal
|
boolean |
closeGoal()
returns true iff the taclet contains a "close goal"-statement
|
java.util.Set<SchemaVariable> |
collectSchemaVars() |
private void |
collectSchemaVarsHelper(Sequent s,
OpCollector oc) |
protected abstract void |
createAndInitializeExecutor() |
protected void |
createAndInitializeMatcher() |
protected void |
createTacletServices()
creates and initializes the taclet matching and execution engines
has to be called at the end of initialization
|
java.lang.String |
displayName()
returns the display name of the taclet, or, if not specified --
the canonical name
|
boolean |
equals(java.lang.Object o)
return true if
o is a taclet of the same name and
o and this contain no mutually exclusive
taclet options. |
ImmutableSet<QuantifiableVariable> |
getBoundVariables()
computes and returns all variables that occur bound in the taclet
including the taclets defined in addrules sections.
|
protected abstract ImmutableSet<QuantifiableVariable> |
getBoundVariablesHelper()
collects bound variables in taclet entities others than goal templates
|
ImmutableSet<Choice> |
getChoices() |
TacletExecutor<? extends Taclet> |
getExecutor() |
abstract ImmutableSet<SchemaVariable> |
getIfFindVariables() |
protected ImmutableSet<SchemaVariable> |
getIfVariables()
returns the set of schemavariables of the taclet's if-part
|
TacletMatcher |
getMatcher() |
SchemaVariable |
getNameCorrespondent(SchemaVariable p,
Services services)
Find a schema variable that could be used to choose a name for
an instantiation (a new variable or constant) of "p"
|
TacletPrefix |
getPrefix(SchemaVariable sv)
returns the computed prefix for the given schemavariable.
|
RuleJustification |
getRuleJustification() |
ImmutableList<RuleSet> |
getRuleSets() |
boolean |
getSurviveSymbExec() |
Trigger |
getTrigger() |
ImmutableList<VariableCondition> |
getVariableConditions() |
ImmutableList<TacletGoalTemplate> |
goalTemplates()
returns an iterator over the goal descriptions.
|
int |
hashCode() |
boolean |
hasReplaceWith()
returns true if one of the goal templates is a replacewith.
|
boolean |
hasTrigger() |
Sequent |
ifSequent()
returns the if-sequence of the application part of the Taclet.
|
boolean |
isContextInPrefix()
returns true iff a context flag is set in one of the entries in
the prefix map.
|
Name |
name()
returns the name of the Taclet
|
ImmutableMap<SchemaVariable,TacletPrefix> |
prefixMap() |
java.util.Iterator<RuleSet> |
ruleSets()
returns an iterator over the rule sets.
|
abstract Taclet |
setName(java.lang.String s) |
java.lang.String |
toString()
returns a representation of the Taclet as String
|
(package private) java.lang.StringBuffer |
toStringAttribs(java.lang.StringBuffer sb) |
(package private) java.lang.StringBuffer |
toStringGoalTemplates(java.lang.StringBuffer sb) |
(package private) java.lang.StringBuffer |
toStringIf(java.lang.StringBuffer sb) |
(package private) java.lang.StringBuffer |
toStringRuleSets(java.lang.StringBuffer sb) |
(package private) java.lang.StringBuffer |
toStringVarCond(java.lang.StringBuffer sb) |
NewVarcond |
varDeclaredNew(SchemaVariable var)
looks if a variable is declared as new and returns its sort to match
with or the schema variable it shares the match-sort with.
|
ImmutableList<NewVarcond> |
varsNew()
returns an iterator over the variables that are new in the Taclet.
|
ImmutableList<NewDependingOn> |
varsNewDependingOn() |
ImmutableList<NotFreeIn> |
varsNotFreeIn()
returns an iterator over the variable pairs that indicate that are
new in the Taclet.
|
protected final ImmutableSet<TacletAnnotation> tacletAnnotations
private final Name name
private final java.lang.String displayName
protected final ImmutableSet<Choice> choices
private final Sequent ifSequent
private final ImmutableList<NewVarcond> varsNew
private final ImmutableList<NotFreeIn> varsNotFreeIn
@Deprecated private final ImmutableList<NewDependingOn> varsNewDependingOn
private final ImmutableList<VariableCondition> variableConditions
private final ImmutableList<TacletGoalTemplate> goalTemplates
protected final ImmutableList<RuleSet> ruleSets
protected final ImmutableMap<SchemaVariable,TacletPrefix> prefixMap
private ImmutableSet<QuantifiableVariable> boundVariables
private boolean contextInfoComputed
private boolean contextIsInPrefix
protected java.lang.String tacletAsString
private ImmutableSet<SchemaVariable> ifVariables
private ImmutableMap<SchemaVariable,SchemaVariable> svNameCorrespondences
private int hashcode
private final Trigger trigger
private final boolean surviveSymbExec
private TacletMatcher matcher
protected TacletExecutor<? extends Taclet> executor
protected Taclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> ruleSets, TacletAttributes attrs, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, ImmutableSet<Choice> choices, boolean surviveSmbExec, ImmutableSet<TacletAnnotation> tacletAnnotations)
name
- the name of the TacletapplPart
- contains the application part of an Taclet that is
the if-sequence, the variable conditionsgoalTemplates
- a list of goal descriptions.ruleSets
- a list of rule sets for the Tacletattrs
- attributes for the Taclet; these are boolean values
indicating a noninteractive or recursive use of the Taclet.protected Taclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> ruleSets, TacletAttributes attrs, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, ImmutableSet<Choice> choices, ImmutableSet<TacletAnnotation> tacletAnnotations)
name
- the name of the TacletapplPart
- contains the application part of an Taclet that is the
if-sequence, the variable conditionsgoalTemplates
- a list of goal descriptions.ruleSets
- a list of rule sets for the Tacletattrs
- attributes for the Taclet; these are boolean values
indicating a noninteractive or recursive use of the Taclet.public RuleJustification getRuleJustification()
public boolean hasTrigger()
public Trigger getTrigger()
public final TacletMatcher getMatcher()
protected void createTacletServices()
protected void createAndInitializeMatcher()
protected abstract void createAndInitializeExecutor()
public ImmutableSet<QuantifiableVariable> getBoundVariables()
protected abstract ImmutableSet<QuantifiableVariable> getBoundVariablesHelper()
public boolean closeGoal()
public NewVarcond varDeclaredNew(SchemaVariable var)
var
- the SchemaVariable to look forpublic ImmutableList<VariableCondition> getVariableConditions()
public Name name()
public java.lang.String displayName()
displayName
in interface Rule
public Sequent ifSequent()
public ImmutableList<NewVarcond> varsNew()
public ImmutableList<NotFreeIn> varsNotFreeIn()
public ImmutableList<NewDependingOn> varsNewDependingOn()
public ImmutableList<TacletGoalTemplate> goalTemplates()
public ImmutableSet<Choice> getChoices()
public java.util.Iterator<RuleSet> ruleSets()
public ImmutableList<RuleSet> getRuleSets()
public ImmutableMap<SchemaVariable,TacletPrefix> prefixMap()
public boolean hasReplaceWith()
public TacletPrefix getPrefix(SchemaVariable sv)
sv
- the Schemavariablepublic boolean isContextInPrefix()
public boolean equals(java.lang.Object o)
o
is a taclet of the same name and
o
and this
contain no mutually exclusive
taclet options.equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
protected ImmutableSet<SchemaVariable> getIfVariables()
public abstract ImmutableSet<SchemaVariable> getIfFindVariables()
public SchemaVariable getNameCorrespondent(SchemaVariable p, Services services)
java.lang.StringBuffer toStringIf(java.lang.StringBuffer sb)
java.lang.StringBuffer toStringVarCond(java.lang.StringBuffer sb)
java.lang.StringBuffer toStringGoalTemplates(java.lang.StringBuffer sb)
java.lang.StringBuffer toStringRuleSets(java.lang.StringBuffer sb)
java.lang.StringBuffer toStringAttribs(java.lang.StringBuffer sb)
public java.lang.String toString()
toString
in class java.lang.Object
public boolean admissible(boolean interactive, ImmutableList<RuleSet> p_ruleSets)
this
taclet may be applied for the
given mode (interactive/non-interactive, activated rule sets)protected boolean admissibleInteractive(ImmutableList<RuleSet> notAdmissibleRuleSets)
protected boolean admissibleAutomatic(ImmutableList<RuleSet> admissibleRuleSets)
public boolean getSurviveSymbExec()
public java.util.Set<SchemaVariable> collectSchemaVars()
private void collectSchemaVarsHelper(Sequent s, OpCollector oc)
public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp tacletApp)
apply
in interface Rule
goal
- the goal that the rule application should refer to.services
- the Services encapsulating all java informationtacletApp
- the rule application that is executed.public TacletExecutor<? extends Taclet> getExecutor()
public abstract Taclet setName(java.lang.String s)