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 |
---|---|
protected ImmutableSet<Choice> |
choices
the set of taclet options for this taclet
|
protected TacletExecutor<? extends Taclet> |
executor
The taclet executor
|
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
|
protected ImmutableSet<TacletAnnotation> |
tacletAnnotations |
protected java.lang.String |
tacletAsString |
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() |
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"
|
java.lang.String |
getOrigin()
Information about the origin of the rule.
|
TacletPrefix |
getPrefix(SchemaVariable sv)
returns the computed prefix for the given schemavariable.
|
RuleJustification |
getRuleJustification() |
ImmutableList<RuleSet> |
getRuleSets() |
boolean |
getSurviveSymbExec() |
ImmutableSet<Choice> |
getTacletOptions() |
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) |
void |
setOrigin(java.lang.String origin) |
void |
setTacletOptions(ImmutableSet<Choice> tacletOptions) |
java.lang.String |
toString()
returns a representation of the Taclet as String
|
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
protected final ImmutableSet<Choice> choices
protected final ImmutableList<RuleSet> ruleSets
protected final ImmutableMap<SchemaVariable,TacletPrefix> prefixMap
protected java.lang.String tacletAsString
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)
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()
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)
@Nonnull public ImmutableSet<Choice> getTacletOptions()
public void setTacletOptions(@Nonnull ImmutableSet<Choice> tacletOptions)
@Nullable public java.lang.String getOrigin()
Rule
public void setOrigin(@Nullable java.lang.String origin)
Copyright © 2003-2019 The KeY-Project.