de.uka.ilkd.key.rule.label

Interface TermLabelPolicy

All Known Implementing Classes:

StayOnFormulaTermLabelPolicy, StayOnOperatorTermLabelPolicy

public interface TermLabelPolicy

A TermLabelPolicy is used by TermLabelManager#instantiateLabels( TermLabelState, Services, PosInOccurrence, Term, Term, Rule, Goal, Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock) to decide for each TermLabel of an old Term if it should be re-added to the new Term or not.

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

Method Summary

Modifier and Type

Method and Description

TermLabel

keepLabel(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm, Operator newTermOp, ImmutableArray<Term> newTermSubs, ImmutableArray<QuantifiableVariable> newTermBoundVars, JavaBlock newTermJavaBlock, ImmutableArray<TermLabel> newTermOriginalLabels, TermLabel label) Decides to keep (add to term which will be created) or to drop (do not add label to new term) the given TermLabel provided by the application Term.

Method Detail

keepLabel

TermLabel keepLabel(TermLabelState state,
                    Services services,
                    PosInOccurrence applicationPosInOccurrence,
                    Term applicationTerm,
                    Rule rule,
                    Goal goal,
                    java.lang.Object hint,
                    Term tacletTerm,
                    Operator newTermOp,
                    ImmutableArray<Term> newTermSubs,
                    ImmutableArray<QuantifiableVariable> newTermBoundVars,
                    JavaBlock newTermJavaBlock,
                    ImmutableArray<TermLabel> newTermOriginalLabels,
                    TermLabel label)

Decides to keep (add to term which will be created) or to drop (do not add label to new term) the given TermLabel provided by the application 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 Term in the taclet which is responsible to instantiate the new Term for the new proof node or null in case of built in rules.

newTermOp - The new Operator of the Term to create.

newTermSubs - The optional children of the Term to create.

newTermBoundVars - The optional QuantifiableVariables of the Term to create.

newTermJavaBlock - The optional JavaBlock of the Term to create.

newTermOriginalLabels - The original TermLabels.

label - The TermLabel to decide if it should be kept or dropped.

Returns:

The TermLabel to keep which might be a different one (e.g. with changed parameters) or null if the TermLabel should be dropped.