public interface TermLabel extends Named
The interface for term labels. Term labels are annotations that can be attached
to Term
s and carry additional information.
They must not be soundness relevant. But they may be used in strategies
to compute the order in which rules are applied.
Term
s with or without term labels are still unmodifiable.
It is recommended to implement TermLabel
s including their parameters also unmodifiable.
For new TermLabel
s without parameters class ParameterlessTermLabel
can be used.
A term label can have parameters accessible via getChild(int)
and
getChildCount()
. Such parameters can be any Object
.
But keep in mind that it is required to parse String
s into Term
s,
e.g. if it is used in a Taclet definition or if a cut rule is applied.
For convenience parameters are always printed as String
s
and have to be parsed individually into the required Object
instances
via a TermLabelFactory
.
Which TermLabel
s are available is defined by the Profile
or
more precise by its TermLabelManager
available via Profile.getTermLabelManager()
.
The TermLabelManager
provides also the functionality to parse and maintain them during prove.
The TermLabelManager
is responsible during prove to maintain term labels.
This means that labels of new Term
s created during rule application are computed
via TermLabelManager#instantiateLabels(
de.uka.ilkd.key.logic.label.TermLabelState, de.uka.ilkd.key.java.Services,
de.uka.ilkd.key.logic.PosInOccurrence, Term, de.uka.ilkd.key.rule.Rule,
de.uka.ilkd.key.proof.Goal, Object, Term, de.uka.ilkd.key.logic.op.Operator,
de.uka.ilkd.key.collection.ImmutableArray,
de.uka.ilkd.key.collection.ImmutableArray,
de.uka.ilkd.key.logic.JavaBlock)
and of existing Term
s are refactored (added or removed) via
TermLabelManager#refactorGoal(
de.uka.ilkd.key.logic.label.TermLabelState, de.uka.ilkd.key.java.Services,
de.uka.ilkd.key.logic.PosInOccurrence, Term, de.uka.ilkd.key.rule.Rule,
de.uka.ilkd.key.proof.Goal, Term)
.
Antecedent and succedent of a Sequent
are sets. The equality check
if a SequentFormula
is already contained ignores TermLabel
s.
To ensure that TermLabel
s are not lost,
TermLabelManager.mergeLabels(de.uka.ilkd.key.java.Services, de.uka.ilkd.key.logic.SequentChangeInfo)
merges the labels of the existing SequentFormula
with those of the rejected SequentFormula
.
How this is done in detail is implemented by a TermLabelMerger
.
If no TermLabelMerger
is available, the TermLabel
of the rejected SequentFormula
are lost.
To implement a new TermLabel
follow the following steps:
TermLabel
implementation.
Name
and one with the instance to ParameterlessTermLabel
.TermLabel
.TermLabelFactory
which will be used during the parse process.
SingletonLabelFactory
with the instance added as constant to ParameterlessTermLabel
.TermLabelFactory
.TermLabel
is maintained during prove.
This may have to be done for different rules in different ways.
Orienteer yourself for each rule on the examples provided in the following.
They are ordered with the less to the most performance impact during prove.
Try to treat as many rules as possible with the same solution, but
choose always the solution with the less performance impact!
a(b<<l>>) ~~> c(b<<l>>)
: b
is a constant which is never rewritten by rules. The label stays on the Term
and will be dropped when the Term
is dropped. Nothing to be done.a ~~> b<<l>>
: The taclet rewrites a
into b<<l>>
. TermLabel
s defined by taclets are automatically considered during rule application. Nothing to be done.a<<l>> ~~> b<<l>>
The application Term
a
contains the label before. Use an application TermLabelPolicy
to ensure that it is maintained.Update[...]<<l>> ~~> Update[...new...]<<l>>
The application Term
Update
contains a Modality
. Use a modality TermLabelPolicy
to ensure that it is maintained.2 + 3 ~~> 5<>a>>
: A new label has to be added which is not provided by the rule. Implement a TermLabelUpdate
which adds, sorts or removes TermLabel
before a new Term
is created.2<<a>> + 3<<b>> ~~> 5<<a>>
: A direct child of the application Term
a
contains the label before. Use a direct ChildTermLabelPolicy
to ensure that it is added also to the new term.2 + (3<<a>> - 1<<b>>) ~~> 4<<a>>
: A child or grandchild of the application Term
a
contains the label before. Use a direct ChildTermLabelPolicy
to ensure that it is added also to the new term.2<<a>> + 3<<b>> ~~> 2<<a>> - 3
: Implement a TermLabelRefactoring
which works on TermLabelRefactoring.RefactoringScope.APPLICATION_DIRECT_CHILDREN
to freely add or remove TermLabel
s on direct children of the application Term
.2 + (3<<a>> - 1<<b>>) ~~> 2 * (3<<a>> - 1)
: Implement a TermLabelRefactoring
which works on TermLabelRefactoring.RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE
to freely add or remove TermLabel
s on children and grandchildren of the application Term
.Sequent
: Implement a TermLabelRefactoring
which works on TermLabelRefactoring.RefactoringScope.SEQUENT
to freely add or remove TermLabel
s on any Term
of the Sequent
.TermLabelMerger
to ensure that TermLabel
s are maintained in case of rejected SequentFormula
s.Profile
supports the new TermLabel
.
All implementations from the previous have to be bundled in a
TermLabelManager.TermLabelConfiguration
instance. This instance has to be
created and returned in AbstractProfile.computeTermLabelConfiguration()
.
BuiltInRule
, the
functionality of TermLabelManager
to maintain TermLabel
s
is only called for newly created Term
s labeled up to now. If
your TermLabelPolicy
, TermLabelUpdate
or TermLabelRefactoring
is not called on the right Term
, it is your task to call
TermLabelManager#instantiateLabels(
de.uka.ilkd.key.logic.label.TermLabelState, de.uka.ilkd.key.java.Services,
de.uka.ilkd.key.logic.PosInOccurrence, de.uka.ilkd.key.rule.Rule,
de.uka.ilkd.key.proof.Goal, Object, Term, de.uka.ilkd.key.logic.op.Operator,
de.uka.ilkd.key.collection.ImmutableArray, de.uka.ilkd.key.collection.ImmutableArray,
de.uka.ilkd.key.logic.JavaBlock)
and
TermLabelManager#refactorLabels(
de.uka.ilkd.key.logic.label.TermLabelState, de.uka.ilkd.key.java.Services,
de.uka.ilkd.key.logic.PosInOccurrence, de.uka.ilkd.key.rule.Rule,
de.uka.ilkd.key.proof.Goal, Term)
on the right place in the rule implementation.
TermLabelManager
Modifier and Type | Method and Description |
---|---|
java.lang.Object |
getChild(int i)
Retrieves the i-th parameter object of this term label.
|
int |
getChildCount()
Gets the number of parameters of this term label.
|
java.lang.Object getChild(int i)
A term label may have structure, i.e. can be parameterized.
i
- the number of the parameter to retrieve (
0 <= i < getChildCount()
)java.lang.IndexOutOfBoundsException
- if the given parameter number
i is negative or greater-or-equal the number of
parameters returned by getChildCount()
int getChildCount()