public interface TermLabelUpdate extends RuleSpecificTask
A TermLabelUpdate
is used by
TermLabelManager#instantiateLabels(Services, PosInOccurrence, Term, Term, Rule, Goal, Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
to add or remove maintained TermLabel
s which will be added to the new Term
.
For more information about TermLabel
s and how they are maintained
during prove read the documentation of interface TermLabel
.
TermLabel
,
TermLabelManager
Modifier and Type | Method and Description |
---|---|
void |
updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
Goal goal,
Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
Set<TermLabel> labels)
|
getSupportedRuleNames
void updateLabels(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Term modalityTerm, Rule rule, RuleApp ruleApp, Goal goal, Object hint, Term tacletTerm, Operator newTermOp, ImmutableArray<Term> newTermSubs, ImmutableArray<QuantifiableVariable> newTermBoundVars, JavaBlock newTermJavaBlock, Set<TermLabel> labels)
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
.modalityTerm
- The optional modality Term
.rule
- The Rule
which is applied.ruleApp
- The RuleApp
which is currently performed.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.labels
- The Set
of TermLabel
s to modify.state
- The TermLabelState
of the current rule application.