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 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.
- Returns:
- The
TermLabel
to keep which might be a different one (e.g. with changed parameters) or null
if the TermLabel
should be dropped.