de.uka.ilkd.key.rule.label

Class StayOnFormulaTermLabelPolicy

java.lang.Object

de.uka.ilkd.key.rule.label.StayOnFormulaTermLabelPolicy

All Implemented Interfaces:

TermLabelPolicy

public class StayOnFormulaTermLabelPolicy
extends java.lang.Object
implements TermLabelPolicy

This TermLabelPolicy maintains a FormulaTermLabel on predicates.

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
StayOnFormulaTermLabelPolicy()

Method Summary

Modifier and Type	Method and Description
protected boolean	isBelowIfThenElse(java.util.Deque<Term> visitStack) Checks if the currently treated taclet Term is a child of an if-then-else operation.
protected boolean	isTopLevel(Taclet.TacletLabelHint tacletHint, Term tacletTerm) Checks if the given taclet Term is top level.
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.
static FormulaTermLabel	searchFormulaTermLabel(ImmutableArray<TermLabel> labels) Searches the FormulaTermLabel in the given TermLabels.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

StayOnFormulaTermLabelPolicy

public StayOnFormulaTermLabelPolicy()

Method Detail

keepLabel

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

Specified by:

keepLabel in interface TermLabelPolicy

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.

isBelowIfThenElse

protected boolean isBelowIfThenElse(java.util.Deque<Term> visitStack)

Checks if the currently treated taclet Term is a child of an if-then-else operation.

Parameters:

visitStack - The taclet Term stack.

Returns:

true is below if-then-else, false otherwise.

searchFormulaTermLabel

public static FormulaTermLabel searchFormulaTermLabel(ImmutableArray<TermLabel> labels)

Searches the FormulaTermLabel in the given TermLabels.

Parameters:

labels - The TermLabels to search in.

Returns:

The found FormulaTermLabel or null if not available.

isTopLevel

protected boolean isTopLevel(Taclet.TacletLabelHint tacletHint,
                             Term tacletTerm)

Checks if the given taclet Term is top level.

Parameters:

tacletHint - The Taclet.TacletLabelHint to use.

tacletTerm - The taclet Term to check.

Returns:

true is top level, false is not top level.