de.uka.ilkd.key.rule.label

Interface TermLabelRefactoring

All Superinterfaces:

RuleSpecificTask

All Known Implementing Classes:

FormulaTermLabelRefactoring, RemoveInCheckBranchesTermLabelRefactoring

public interface TermLabelRefactoring
extends RuleSpecificTask

A TermLabelRefactoring is used by TermLabelManager#refactorGoal(TermLabelState, Services, PosInOccurrence, Term, Rule, Goal, Term) to refactor the labels of each visited Term.

For more information about TermLabels and how they are maintained during prove read the documentation of interface TermLabel.

Author:

Martin Hentschel

See Also:

TermLabel, TermLabelManager

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static class	TermLabelRefactoring.RefactoringScope Possible refactoring scopes.

Method Summary

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.
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.

Methods inherited from interface de.uka.ilkd.key.rule.label.RuleSpecificTask

getSupportedRuleNames

Method Detail

defineRefactoringScope

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.

Parameters:

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.

Returns:

The required TermLabelRefactoring.RefactoringScope.

refactoreLabels

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.

Parameters:

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.