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 TermLabel
s and how they are maintained
during prove read the documentation of interface TermLabel
.
TermLabel
,
TermLabelManager
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)
|
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. |
getSupportedRuleNames
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)
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.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.
param label The TermLabel
to decide if it should be kept or dropped.true
keep TermLabel
and add it to the new Term
. false
drop TermLabel
and do not need it to the new Term
.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.
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.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.true
add TermLabel
to new Term
. false
do not add TermLabel
to new Term
.