public class TermLabelManager
extends java.lang.Object
This class provides access to the functionality of term labels.
A TermLabelManager
is associated to a Profile
object using
Profile.getTermLabelManager()
. It allows:
TermLabel
Name
s via getSupportedTermLabelNames()
.TermLabel
via
#parseLabel(String, List, TermServices)
.TermLabel
s of a Term
to be created via
#instantiateLabels(TermLabelState, Services, PosInOccurrence,
Term, Rule, Goal, Object, Term, Operator,
ImmutableArray, ImmutableArray, JavaBlock)
during rule application.Term
s during rule application via:
#refactorGoal(TermLabelState, Services, PosInOccurrence,
Term, Rule, Goal, Term)
: The full sequentrefactorSequentFormula(TermLabelState, Services, Term,
PosInOccurrence, Rule, Goal,
Object, Term)
:
The sequent formula which contains the application term on
which the rule is appliedrefactorTerm(TermLabelState, Services, PosInOccurrence,
Term, Rule, Goal, Object, Term)
:
The current term.
For more information about TermLabel
s and how they are maintained
during prove read the documentation of interface TermLabel
.
TermLabel
Modifier and Type | Class and Description |
---|---|
protected static class |
TermLabelManager.RefactoringsContainer
Utility class used by
TermLabelManager#computeRefactorings(
TermLabelState, TermServices, PosInOccurrence, Term, Rule, Goal,
Term) . |
static class |
TermLabelManager.TermLabelConfiguration
Instances of this class are used to group everything which is required
to support one specific
TermLabel . |
Constructor and Description |
---|
TermLabelManager(ImmutableList<TermLabelManager.TermLabelConfiguration> configurations)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
private void |
analyzeChildTermPolicies(Name termLabelName,
ImmutableList<ChildTermLabelPolicy> policies,
java.util.Map<Name,ChildTermLabelPolicy> allRulesPolicyMap,
java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificPolicyMap)
Analyzes the given
ChildTermLabelPolicy and adds it to the given policy Map s. |
private void |
analyzeMerger(Name termLabelName,
TermLabelMerger termLabelMerger)
Analyzes the given
TermLabelMerger and adds it to mergerMap . |
private void |
analyzeRefactorings(ImmutableList<TermLabelRefactoring> refactorings)
Analyzes the given
TermLabelRefactoring and updates allRulesRefactorings and ruleSpecificRefactorings . |
private void |
analyzeTermPolicies(Name termLabelName,
ImmutableList<TermLabelPolicy> policies,
java.util.Map<Name,TermLabelPolicy> policyMap)
Analyzes the given
TermLabelPolicy and adds it to the given policy Map . |
private void |
analyzeUpdates(ImmutableList<TermLabelUpdate> updates)
|
protected java.util.Map<Name,ChildTermLabelPolicy> |
computeActiveChildPolicies(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,
java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificPolicies,
java.util.Map<Name,ChildTermLabelPolicy> ruleIndependentPolicies)
Computes active
ChildTermLabelPolicy instances which have to be executed during the given rule application. |
protected TermLabelManager.RefactoringsContainer |
computeRefactorings(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Computes the
TermLabelRefactoring to consider. |
static TermLabel |
findInnerMostParentLabel(PosInOccurrence pio,
Name termLabelName)
Searches the inner most
TermLabel wit the given Name in the parent hierarchy of the PosInOccurrence . |
ImmutableList<Name> |
getSupportedTermLabelNames()
|
static ImmutableList<Name> |
getSupportedTermLabelNames(Services services)
|
static TermLabelManager |
getTermLabelManager(Services services)
|
static ImmutableArray<TermLabel> |
instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
ImmutableArray<TermLabel> |
instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static ImmutableArray<TermLabel> |
instantiateLabels(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static Term |
label(Services services,
TermLabelState state,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp, Goal, Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object, Rule, Term) . |
static Term |
label(Services services,
TermLabelState state,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp, Goal, Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object, Rule, Term) . |
Term |
label(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp, Goal, Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object, Rule, Term) . |
static void |
mergeLabels(SequentChangeInfo currentSequent,
Services services)
|
protected void |
mergeLabels(SequentChangeInfo currentSequent,
Services services,
SequentFormula rejectedSF,
boolean inAntecedent)
|
void |
mergeLabels(Services services,
SequentChangeInfo currentSequent)
|
TermLabel |
parseLabel(java.lang.String name,
java.util.List<java.lang.String> args,
TermServices services)
Get a term label for string parameters.
|
protected void |
performChildAndGrandchildPolicies(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,
java.util.Map<Name,ChildTermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
ChildTermLabelPolicy instances. |
protected void |
performDirectChildPolicies(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,
java.util.Map<Name,ChildTermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given direct
ChildTermLabelPolicy instances. |
protected ImmutableArray<TermLabel> |
performRefactoring(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
ImmutableList<TermLabelRefactoring> activeRefactorings)
Computes the new labels as part of the refactoring for the given
Term . |
protected void |
performTacletTerm(Term tacletTerm,
java.util.Set<TermLabel> newLabels)
|
protected void |
performTermLabelPolicies(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,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given
TermLabelPolicy instances. |
protected void |
performTermLabelPolicies(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,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels,
TermLabel label)
Performs the given
TermLabelPolicy instances. |
protected void |
performUpdater(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableList<TermLabelUpdate> updater,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
TermLabelUpdate instances. |
protected Term |
refactorApplicationTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
TermLabelManager.RefactoringsContainer refactorings,
TermFactory tf)
Refactors the labels of the application term.
|
static void |
refactorGoal(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
void |
refactorGoal(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
protected Term |
refactorLabelsRecursive(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
ImmutableList<TermLabelRefactoring> activeRefactorings)
|
protected void |
refactorSemisequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Semisequent semisequent,
boolean inAntec,
ImmutableList<TermLabelRefactoring> activeRefactorings)
Performs a
TermLabel refactoring on the given Semisequent . |
static void |
refactorSequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
void |
refactorSequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
Term |
refactorSequentFormula(TermLabelState state,
Services services,
Term sequentFormula,
PosInOccurrence applicationPosInOccurrence,
Goal goal,
java.lang.Object hint,
Rule rule,
Term tacletTerm)
|
static Term |
refactorSequentFormula(TermLabelState state,
Services services,
Term sequentFormula,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
|
Term |
refactorTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Goal goal,
java.lang.Object hint,
Rule rule,
Term tacletTerm)
Refactors all labels in the given application
Term . |
static Term |
refactorTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
protected Term |
replaceTerm(TermLabelState state,
PosInOccurrence pio,
Term newTerm,
TermFactory tf,
ImmutableList<TermLabelRefactoring> parentRefactorings,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Replaces the
Term at the specified PosInOccurrence . |
private final java.util.Map<Name,TermLabelFactory<?>> factoryMap
private final java.util.Map<Name,TermLabelPolicy> applicationTermPolicyMap
private final java.util.Map<Name,TermLabelPolicy> modalityTermPolicyMap
private final java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificDirectChildTermLabelPolicies
ChildTermLabelPolicy
s.private final java.util.Map<Name,ChildTermLabelPolicy> allRulesDirectChildTermLabelPolicies
ChildTermLabelPolicy
s.private final java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificChildAndGrandchildTermLabelPolicies
ChildTermLabelPolicy
s.private final java.util.Map<Name,ChildTermLabelPolicy> allRulesChildAndGrandchildTermLabelPolicies
ChildTermLabelPolicy
s.private final java.util.Map<Name,ImmutableList<TermLabelUpdate>> ruleSpecificUpdates
TermLabelUpdate
s.private ImmutableList<TermLabelUpdate> allRulesUpdates
TermLabelUpdate
s.private final java.util.Map<Name,ImmutableList<TermLabelRefactoring>> ruleSpecificRefactorings
TermLabelRefactoring
s.private ImmutableList<TermLabelRefactoring> allRulesRefactorings
TermLabelRefactoring
s.private ImmutableList<Name> supportedTermLabelnames
private final java.util.Map<Name,TermLabelMerger> mergerMap
public TermLabelManager(ImmutableList<TermLabelManager.TermLabelConfiguration> configurations)
configurations
- The TermLabelManager.TermLabelConfiguration
which defines how to support each TermLabel
.private void analyzeMerger(Name termLabelName, TermLabelMerger termLabelMerger)
TermLabelMerger
and adds it to mergerMap
.termLabelName
- The name of the supported TermLabel
.termLabelMerger
- The TermLabelMerger
to use.private void analyzeTermPolicies(Name termLabelName, ImmutableList<TermLabelPolicy> policies, java.util.Map<Name,TermLabelPolicy> policyMap)
Analyzes the given TermLabelPolicy
and adds it to the given policy Map
.
This is a helper Map
of TermLabelManager(ImmutableList)
.
termLabelName
- The name of the supported TermLabel
.policies
- The TermLabelPolicy
instances to analyze.policyMap
- The policy Map
to update.private void analyzeChildTermPolicies(Name termLabelName, ImmutableList<ChildTermLabelPolicy> policies, java.util.Map<Name,ChildTermLabelPolicy> allRulesPolicyMap, java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificPolicyMap)
Analyzes the given ChildTermLabelPolicy
and adds it to the given policy Map
s.
This is a helper Map
of TermLabelManager(ImmutableList)
.
termLabelName
- The name of the supported TermLabel
.policies
- The ChildTermLabelPolicy
instances to analyze.allRulesPolicyMap
- The policy Map
with all rules to update.ruleSpecificPolicyMap
- The rule specific policy Map
to update.private void analyzeUpdates(ImmutableList<TermLabelUpdate> updates)
Analyzes the given TermLabelUpdate
and updates allRulesUpdates
and ruleSpecificUpdates
.
This is a helper Map
of TermLabelManager(ImmutableList)
.
updates
- The TermLabelUpdate
s to analyze.private void analyzeRefactorings(ImmutableList<TermLabelRefactoring> refactorings)
Analyzes the given TermLabelRefactoring
and updates allRulesRefactorings
and ruleSpecificRefactorings
.
This is a helper Map
of TermLabelManager(ImmutableList)
.
TermLabelUpdate
s to analyze.public static TermLabelManager getTermLabelManager(Services services)
services
- The Services
which provides the TermLabelManager
.TermLabelManager
s or null
if not available.public static ImmutableList<Name> getSupportedTermLabelNames(Services services)
public ImmutableList<Name> getSupportedTermLabelNames()
public TermLabel parseLabel(java.lang.String name, java.util.List<java.lang.String> args, TermServices services) throws TermLabelException
Get a term label for string parameters.
Parses the string arguments and returns the term label of name
name
with the corresponding parameters.
The name must be associated with a TermLabelFactory
. Otherwise a
TermLabelException
is thrown to indicate that an unknown term
label kind has been asked for.
name
- The name of the term label, not null
args
- The arguments, not null
, no entry null
services
- a non-null
services object to look up symbolsname
with parameters as parsed.TermLabelException
- if name is not a registered label name or the arguments cannot be parsed.public static Term label(Services services, TermLabelState state, PosInOccurrence applicationPosInOccurrence, Rule rule, RuleApp ruleApp, Goal goal, java.lang.Object hint, Term tacletTerm, Term newTerm)
TermLabel
s for the new Term
via
instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp, Goal, Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock, ImmutableArray)
and refactors the labels below the new Term
in addition via
refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object, Rule, Term)
.services
- The Services
used by the Proof
on which a Rule
is applied right now.state
- The TermLabelState
of the current rule application.applicationPosInOccurrence
- The PosInOccurrence
in the previous Sequent
which defines the Term
that is rewritten.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.newTerm
- The new Term
to update its labels.Term
with updates labels.public static Term label(Services services, TermLabelState state, Term applicationTerm, PosInOccurrence applicationPosInOccurrence, Rule rule, RuleApp ruleApp, Goal goal, java.lang.Object hint, Term tacletTerm, Term newTerm)
TermLabel
s for the new Term
via
instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp, Goal, Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock, ImmutableArray)
and refactors the labels below the new Term
in addition via
refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object, Rule, Term)
.services
- The Services
used by the Proof
on which a Rule
is applied right now.state
- The TermLabelState
of the current rule application.applicationTerm
- The Term
defined by the PosInOccurrence
in the previous Sequent
.applicationPosInOccurrence
- The PosInOccurrence
in the previous Sequent
which defines the Term
that is rewritten.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.newTerm
- The new Term
to update its labels.Term
with updates labels.public Term label(TermLabelState state, Services services, Term applicationTerm, PosInOccurrence applicationPosInOccurrence, Rule rule, RuleApp ruleApp, Goal goal, java.lang.Object hint, Term tacletTerm, Term newTerm)
TermLabel
s for the new Term
via
instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp, Goal, Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock, ImmutableArray)
and refactors the labels below the new Term
in addition via
refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object, Rule, Term)
.state
- The TermLabelState
of the current rule application.services
- The Services
used by the Proof
on which a Rule
is applied right now.applicationTerm
- The Term
defined by the PosInOccurrence
in the previous Sequent
.applicationPosInOccurrence
- The PosInOccurrence
in the previous Sequent
which defines the Term
that is rewritten.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.newTerm
- The new Term
to update its labels.Term
with updates labels.public static ImmutableArray<TermLabel> instantiateLabels(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Rule rule, RuleApp ruleApp, Goal goal, java.lang.Object hint, Term tacletTerm, Operator newTermOp, ImmutableArray<Term> newTermSubs, ImmutableArray<QuantifiableVariable> newTermBoundVars, JavaBlock newTermJavaBlock, ImmutableArray<TermLabel> newTermOriginalLabels)
Computes the TermLabel
to add to a new Term
while
a Rule
is currently active. The labels of the new Term
are computed just before the term is created.
This method delegates the request to the TermLabelManager
of the given Services
if possible. Otherwise no labels are returned.
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.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.newTermOriginalLabels
- The original TermLabel
s.TermLabel
s to add to the new Term
which should be created.public static ImmutableArray<TermLabel> instantiateLabels(TermLabelState state, Services services, Term applicationTerm, PosInOccurrence applicationPosInOccurrence, Rule rule, RuleApp ruleApp, Goal goal, java.lang.Object hint, Term tacletTerm, Operator newTermOp, ImmutableArray<Term> newTermSubs, ImmutableArray<QuantifiableVariable> newTermBoundVars, JavaBlock newTermJavaBlock, ImmutableArray<TermLabel> newTermOriginalLabels)
Computes the TermLabel
to add to a new Term
while
a Rule
is currently active. The labels of the new Term
are computed just before the term is created.
This method delegates the request to the TermLabelManager
of the given Services
if possible. Otherwise no labels are returned.
state
- The TermLabelState
of the current rule application.services
- The Services
used by the Proof
on which a Rule
is applied right now.applicationTerm
- The Term
defined by the PosInOccurrence
in the previous Sequent
.applicationPosInOccurrence
- The PosInOccurrence
in the previous Sequent
which defines the Term
that is rewritten.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.newTermOriginalLabels
- The original TermLabel
s.TermLabel
s to add to the new Term
which should be created.public ImmutableArray<TermLabel> instantiateLabels(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, RuleApp ruleApp, Goal goal, java.lang.Object hint, Term tacletTerm, Operator newTermOp, ImmutableArray<Term> newTermSubs, ImmutableArray<QuantifiableVariable> newTermBoundVars, JavaBlock newTermJavaBlock, ImmutableArray<TermLabel> newTermOriginalLabels)
TermLabel
to add to a new Term
while
a Rule
is currently active. The labels of the new Term
are computed just before the term is created in the following way:
List
is created.List
.List
if TermLabelPolicy
wants to keep it.List
if TermLabelPolicy
wants to keep it.TermLabelUpdate
are asked to add or remove labels from result List
List
is returned.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.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.newTermOriginalLabels
- The original TermLabel
s.TermLabel
s to add to the new Term
which should be created.protected void performTacletTerm(Term tacletTerm, java.util.Set<TermLabel> newLabels)
protected void performTermLabelPolicies(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, java.util.Map<Name,TermLabelPolicy> policies, java.util.Set<TermLabel> newLabels)
Performs the given TermLabelPolicy
instances.
This is a helper method of #instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Rule, Goal, Object,
Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
.
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.policies
- The TermLabelPolicy
instances to perform.newLabels
- The result Set
with the TermLabel
s of the new Term
.protected void performTermLabelPolicies(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, java.util.Map<Name,TermLabelPolicy> policies, java.util.Set<TermLabel> newLabels, TermLabel label)
Performs the given TermLabelPolicy
instances.
This is a helper method of #performTermLabelPolicies(
TermLabelState, Services, PosInOccurrence, Term, Rule, Goal, Object,
Term, Operator, ImmutableArray, ImmutableArray, JavaBlock,
ImmutableArray, Map, List)
.
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.policies
- The TermLabelPolicy
instances to perform.newLabels
- The result Set
with the TermLabel
s of the new Term
.label
- The current TermLabel
to ask its TermLabelPolicy
.protected java.util.Map<Name,ChildTermLabelPolicy> computeActiveChildPolicies(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, java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificPolicies, java.util.Map<Name,ChildTermLabelPolicy> ruleIndependentPolicies)
Computes active ChildTermLabelPolicy
instances which have to be executed during the given rule application.
This is a helper Map
of #instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Rule, Goal, Object,
Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
.
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.ruleSpecificPolicies
- Rule specific ChildTermLabelPolicy
instances.ruleIndependentPolicies
- All rules ChildTermLabelPolicy
instances.ChildTermLabelPolicy
which have to be performed.protected void performDirectChildPolicies(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, java.util.Map<Name,ChildTermLabelPolicy> policies, java.util.Set<TermLabel> newLabels)
Performs the given direct ChildTermLabelPolicy
instances.
This is a helper Map
of #instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Rule, Goal, Object,
Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
.
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.policies
- The ChildTermLabelPolicy
instances to perform.newLabels
- The result Set
with the TermLabel
s of the new Term
.protected void performChildAndGrandchildPolicies(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, java.util.Map<Name,ChildTermLabelPolicy> policies, java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild ChildTermLabelPolicy
instances.
This is a helper Map
of #instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Rule, Goal, Object,
Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
.
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.policies
- The ChildTermLabelPolicy
instances to perform.newLabels
- The result Set
with the TermLabel
s of the new Term
.protected void performUpdater(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Term modalityTerm, Rule rule, RuleApp ruleApp, java.lang.Object hint, Term tacletTerm, Operator newTermOp, ImmutableArray<Term> newTermSubs, ImmutableArray<QuantifiableVariable> newTermBoundVars, JavaBlock newTermJavaBlock, ImmutableList<TermLabelUpdate> updater, java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild TermLabelUpdate
instances.
This is a helper Map
of #instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Rule, Goal, Object,
Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
.
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
.modalityTerm
- The optional modality Term
.rule
- The Rule
which is applied.ruleApp
- The RuleApp
which is currently performed.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.updater
- The TermLabelUpdate
instances to perform.newLabels
- The result Set
with the TermLabel
s of the new Term
.public static Term refactorSequentFormula(TermLabelState state, Services services, Term sequentFormula, PosInOccurrence applicationPosInOccurrence, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm)
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.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 taclet Term
.Term
.public Term refactorSequentFormula(TermLabelState state, Services services, Term sequentFormula, PosInOccurrence applicationPosInOccurrence, Goal goal, java.lang.Object hint, Rule rule, Term tacletTerm)
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.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.rule
- The Rule
which is applied.tacletTerm
- The optional taclet Term
.Term
.public static Term refactorTerm(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm)
Refactors all labels in the complete Sequent
. This is the last
step of each rule application.
This method delegates the request to the TermLabelManager
of the given Services
if possible. Otherwise no labels are returned.
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.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 taclet Term
.Term
.public Term refactorTerm(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Goal goal, java.lang.Object hint, Rule rule, Term tacletTerm)
Term
.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
.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.rule
- The Rule
which is applied.tacletTerm
- The optional taclet Term
.Term
.public static void refactorGoal(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm)
Refactors all labels in the complete Sequent
. This is the last
step of each rule application.
This method delegates the request to the TermLabelManager
of the given Services
if possible. Otherwise no labels are returned.
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.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 taclet Term
.public void refactorGoal(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm)
Refactors all labels in the complete Sequent
. This is the last
step of each rule application.
This method delegates the request to the TermLabelManager
of the given Services
if possible. Otherwise no labels are returned.
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 taclet Term
.public static void refactorSequent(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm)
Refactors all labels in the complete Sequent
. This is the last
step of each rule application. Only refactorings with scope
TermLabelRefactoring.RefactoringScope.SEQUENT
are performed!
This method delegates the request to the TermLabelManager
of the given Services
if possible. Otherwise no labels are returned.
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.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 taclet Term
.public void refactorSequent(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm)
Refactors all labels in the complete Sequent
. This is the last
step of each rule application. Only refactorings with scope
TermLabelRefactoring.RefactoringScope.SEQUENT
are performed!
This method delegates the request to the TermLabelManager
of the given Services
if possible. Otherwise no labels are returned.
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 taclet Term
.protected Term replaceTerm(TermLabelState state, PosInOccurrence pio, Term newTerm, TermFactory tf, ImmutableList<TermLabelRefactoring> parentRefactorings, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm)
Term
at the specified PosInOccurrence
.state
- The TermLabelState
of the current rule application.pio
- The PosInOccurrence
to replace Term
at.newTerm
- The new Term
to set.tf
- The TermFactory
to use.parentRefactorings
- The TermLabelManager.RefactoringsContainer
to consider.PosInOccurrence
containing the new Term
at the specified PosInOccurrence
.protected TermLabelManager.RefactoringsContainer computeRefactorings(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm)
TermLabelRefactoring
to consider.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 taclet Term
.TermLabelManager.RefactoringsContainer
with the TermLabelRefactoring
s to consider.protected Term refactorApplicationTerm(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm, TermLabelManager.RefactoringsContainer refactorings, TermFactory tf)
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 taclet Term
.refactorings
- The TermLabelManager.RefactoringsContainer
with the TermLabelRefactoring
s to consider.Term
or null
if no refactoring was performed.protected void refactorSemisequent(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm, Semisequent semisequent, boolean inAntec, ImmutableList<TermLabelRefactoring> activeRefactorings)
TermLabel
refactoring on the given Semisequent
.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 taclet Term
.semisequent
- The Semisequent
to refactor.inAntec
- true
antecedent, false
succedent.activeRefactorings
- The active TermLabelRefactoring
s to execute.protected Term refactorLabelsRecursive(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm, Term term, ImmutableList<TermLabelRefactoring> activeRefactorings)
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 taclet Term
.term
- The Term
to refactor.activeRefactorings
- The active TermLabelRefactoring
s to execute.Term
in which the TermLabel
s may have changed.protected ImmutableArray<TermLabel> performRefactoring(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm, Term term, ImmutableList<TermLabelRefactoring> activeRefactorings)
Term
.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 taclet Term
.term
- The Term
to refactor.activeRefactorings
- The active TermLabelRefactoring
s to execute.TermLabel
which should be used for the given Term
.public static TermLabel findInnerMostParentLabel(PosInOccurrence pio, Name termLabelName)
TermLabel
wit the given Name
in the parent hierarchy of the PosInOccurrence
.pio
- The PosInOccurrence
to search in.termLabelName
- The Name
of the TermLabel
to search.TermLabel
or null
if not available.public static void mergeLabels(SequentChangeInfo currentSequent, Services services)
currentSequent
- The SequentChangeInfo
which lists the rejected SequentFormula
s.services
- The Services
to use.public void mergeLabels(Services services, SequentChangeInfo currentSequent)
services
- The Services
to use.currentSequent
- The SequentChangeInfo
which lists the rejected SequentFormula
s.protected void mergeLabels(SequentChangeInfo currentSequent, Services services, SequentFormula rejectedSF, boolean inAntecedent)
currentSequent
- The SequentChangeInfo
which lists the rejected SequentFormula
s.services
- The Services
to use.rejectedSF
- The rejected SequentFormula
to work with.inAntecedent
- true
rejected SequentFormula
is in antecedent, false
it is in succedent.