public class OriginTermLabelRefactoring extends java.lang.Object implements TermLabelRefactoring
OriginTermLabel
s.
This ensures that OriginTermLabel.getSubtermOrigins()
always returns an up-to-date value.TermLabelRefactoring.RefactoringScope
Constructor and Description |
---|
OriginTermLabelRefactoring() |
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 |
refactorLabels(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 . |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
shouldRefactorOnBuiltInRule
public ImmutableList<Name> getSupportedRuleNames()
RuleSpecificTask
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
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 refactorLabels(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)
TermLabelRefactoring
Term
.refactorLabels
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.Copyright © 2003-2019 The KeY-Project.