public class StayOnFormulaTermLabelPolicy extends java.lang.Object implements TermLabelPolicy
TermLabelPolicy
maintains a FormulaTermLabel
on predicates.Constructor and Description |
---|
StayOnFormulaTermLabelPolicy() |
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)
|
static FormulaTermLabel |
searchFormulaTermLabel(ImmutableArray<TermLabel> labels)
Searches the
FormulaTermLabel in the given TermLabel s. |
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)
TermLabel
provided by the application Term
.keepLabel
in interface TermLabelPolicy
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 QuantifiableVariable
s of the Term
to create.newTermJavaBlock
- The optional JavaBlock
of the Term
to create.newTermOriginalLabels
- The original TermLabel
s.label
- The TermLabel
to decide if it should be kept or dropped.TermLabel
to keep which might be a different one (e.g. with changed parameters) or null
if the TermLabel
should be dropped.protected boolean isBelowIfThenElse(java.util.Deque<Term> visitStack)
Term
is a child
of an if-then-else operation.visitStack
- The taclet Term
stack.true
is below if-then-else, false
otherwise.public static FormulaTermLabel searchFormulaTermLabel(ImmutableArray<TermLabel> labels)
FormulaTermLabel
in the given TermLabel
s.labels
- The TermLabel
s to search in.FormulaTermLabel
or null
if not available.protected boolean isTopLevel(Taclet.TacletLabelHint tacletHint, Term tacletTerm)
Term
is top level.tacletHint
- The Taclet.TacletLabelHint
to use.tacletTerm
- The taclet Term
to check.true
is top level, false
is not top level.