de.uka.ilkd.key.rule.label

Interface ChildTermLabelPolicy

All Superinterfaces:

RuleSpecificTask

public interface ChildTermLabelPolicy
extends RuleSpecificTask

A ChildTermLabelPolicy is used by TermLabelManager#instantiateLabels( TermLabelState, Services, PosInOccurrence, Term, Term, Rule, Goal, Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock) to decide for each TermLabel on a child or grandchild of the application 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
boolean	addLabel(TermServices 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, Term childTerm, TermLabel label) Decides to add or not to add the given TermLabel on a child or grandchild of the application Term to the new Term which will be created.
boolean	isRuleApplicationSupported(TermServices 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) Decides if the currently active Rule application is supported or not.

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

getSupportedRuleNames

Method Detail

isRuleApplicationSupported

boolean isRuleApplicationSupported(TermServices 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)

Decides if the currently active Rule application is supported or not. If it is not supported no iteration over children will be executed. Only if it returns true #addLabel( TermServices, PosInOccurrence, Term, Rule, Goal, Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock, Term, TermLabel) will be called if a child Term contains a managed label.

Parameters:

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. param label The TermLabel to decide if it should be kept or dropped.

Returns:

true keep TermLabel and add it to the new Term. false drop TermLabel and do not need it to the new Term.

addLabel

boolean addLabel(TermServices 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,
                 Term childTerm,
                 TermLabel label)

Decides to add or not to add the given TermLabel on a child or grandchild of the application Term to the new Term which will be created.

If the child Term is still a child of the new Term the label will still exist independent from the result of this method on the child. To remove it from the child a refacotring has to be used instead.

Parameters:

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.

childTerm - The Term which is a child or grandchild of the application Term that provides the TermLabel.

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

Returns:

true add TermLabel to new Term. false do not add TermLabel to new Term.