public class RemoveInCheckBranchesTermLabelRefactoring extends java.lang.Object implements TermLabelRefactoring
TermLabelRefactoring
removes the supported TermLabel
in check branches. These are:
AbstractAuxiliaryContractRule
: PreUseOperationContractRule
: PreUseOperationContractRule
: Null referenceWhileInvariantRule
: Invariant Initially ValidTermLabelRefactoring.RefactoringScope
Modifier and Type | Field and Description |
---|---|
private Name |
termLabelNameToRemove
|
Constructor and Description |
---|
RemoveInCheckBranchesTermLabelRefactoring(Name termLabelNameToRemove)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
TermLabelRefactoring.RefactoringScope |
defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Defines if a refactoring is required and if so in which
TermLabelRefactoring.RefactoringScope . |
ImmutableList<Name> |
getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
void |
refactoreLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels)
This method is used to refactor the labels of the given
Term . |
private final Name termLabelNameToRemove
public ImmutableList<Name> getSupportedRuleNames()
Name
s or null
or an empty
list if all rules are supported.getSupportedRuleNames
in interface RuleSpecificTask
Name
s or null
/empty list if all rules are supported.public TermLabelRefactoring.RefactoringScope defineRefactoringScope(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm)
TermLabelRefactoring.RefactoringScope
.defineRefactoringScope
in interface TermLabelRefactoring
state
- The TermLabelState
of the current rule application.services
- The Services
used by the Proof
on which a Rule
is applied right now.applicationPosInOccurrence
- The PosInOccurrence
in the previous Sequent
which defines the Term
that is rewritten.applicationTerm
- The Term
defined by the PosInOccurrence
in the previous Sequent
.rule
- The Rule
which is applied.goal
- The optional Goal
on which the Term
to create will be used.hint
- An optional hint passed from the active rule to describe the term which should be created.tacletTerm
- The optional taclet Term
.TermLabelRefactoring.RefactoringScope
.public void refactoreLabels(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm, Term term, java.util.List<TermLabel> labels)
Term
.refactoreLabels
in interface TermLabelRefactoring
state
- The TermLabelState
of the current rule application.services
- The Services
used by the Proof
on which a Rule
is applied right now.applicationPosInOccurrence
- The PosInOccurrence
in the previous Sequent
which defines the Term
that is rewritten.applicationTerm
- The Term
defined by the PosInOccurrence
in the previous Sequent
.rule
- The Rule
which is applied.goal
- The optional Goal
on which the Term
to create will be used.hint
- An optional hint passed from the active rule to describe the term which should be created.tacletTerm
- The optional taclet Term
.term
- The Term
which is now refactored.labels
- The new labels the Term
will have after the refactoring.