de.uka.ilkd.key.logic.label

Class TermLabelManager

java.lang.Object

de.uka.ilkd.key.logic.label.TermLabelManager

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:

• To list all supported TermLabel Names via getSupportedTermLabelNames().
• To instantiate a TermLabel via #parseLabel(String, List, TermServices).
• To compute the TermLabels of a Term to be created via #instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, Goal, Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock) during rule application.
• To refactor existing Terms during rule application via:
  • #refactorGoal(TermLabelState, Services, PosInOccurrence, Term, Rule, Goal, Term) : The full sequent
  • refactorSequentFormula(TermLabelState, Services, Term, PosInOccurrence, Rule, Goal, Object, Term) : The sequent formula which contains the application term on which the rule is applied
  • refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Rule, Goal, Object, Term) : The current term.

For more information about TermLabels and how they are maintained during prove read the documentation of interface TermLabel.

Author:

Mattias Ulbrich

See Also:

TermLabel

Nested Class Summary

Nested Classes

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.

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<Name,ChildTermLabelPolicy>	allRulesChildAndGrandchildTermLabelPolicies All rule independent child and grandchild ChildTermLabelPolicys.
private java.util.Map<Name,ChildTermLabelPolicy>	allRulesDirectChildTermLabelPolicies All rule independent direct ChildTermLabelPolicys.
private ImmutableList<TermLabelRefactoring>	allRulesRefactorings All rule independent TermLabelRefactorings.
private ImmutableList<TermLabelUpdate>	allRulesUpdates All rule independent TermLabelUpdates.
private java.util.Map<Name,TermLabelPolicy>	applicationTermPolicyMap Maps the Name of a TermLabel to its TermLabelPolicy applied on the application Term.
private java.util.Map<Name,TermLabelFactory<?>>	factoryMap Maps the Name of a TermLabel to its TermLabelFactory.
private java.util.Map<Name,TermLabelMerger>	mergerMap Maps the Name of a TermLabel to its TermLabelMerger.
private java.util.Map<Name,TermLabelPolicy>	modalityTermPolicyMap Maps the Name of a TermLabel to its TermLabelPolicy applied on the modality Term.
private java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>>	ruleSpecificChildAndGrandchildTermLabelPolicies All rule specific child and grandchild ChildTermLabelPolicys.
private java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>>	ruleSpecificDirectChildTermLabelPolicies All rule specific direct ChildTermLabelPolicys.
private java.util.Map<Name,ImmutableList<TermLabelRefactoring>>	ruleSpecificRefactorings All rule specific TermLabelRefactorings.
private java.util.Map<Name,ImmutableList<TermLabelUpdate>>	ruleSpecificUpdates All rule independent TermLabelUpdates.
private ImmutableList<Name>	supportedTermLabelnames The Names of all supported TermLabels.

Constructor Summary

Constructors

Constructor and Description
TermLabelManager(ImmutableList<TermLabelManager.TermLabelConfiguration> configurations) Constructor.

Method Summary

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 Maps.
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) Analyzes the given TermLabelUpdate and updates allRulesUpdates and ruleSpecificUpdates.
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() Returns the Names of all supported TermLabels.
static ImmutableList<Name>	getSupportedTermLabelNames(Services services) Returns the Names of the supported TermLabels.
static TermLabelManager	getTermLabelManager(Services services) Returns the TermLabelManager defined by the Profile of the given 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) Computes the TermLabel to add to a new Term while a Rule is currently active.
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) Computes the TermLabel to add to a new Term while a Rule is currently active.
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.
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 TermLabels 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 TermLabels 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 TermLabels 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) Merges the TermLabels of the rejected SequentFormulas into the resulting Sequent.
protected void	mergeLabels(SequentChangeInfo currentSequent, Services services, SequentFormula rejectedSF, boolean inAntecedent) Merges the TermLabels of the given SequentFormula into the resulting Sequent.
void	mergeLabels(Services services, SequentChangeInfo currentSequent) Merges the TermLabels of the rejected SequentFormulas into the resulting Sequent.
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) Performs the TermLabels provided by the taclet 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) 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) Performs a TermLabel refactoring recursively on the given Term.
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) Refactors all labels on the PosInOccurrence in the given Term of a SequentFormula.
static Term	refactorSequentFormula(TermLabelState state, Services services, Term sequentFormula, PosInOccurrence applicationPosInOccurrence, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm) Refactors all labels on the PosInOccurrence in the given Term of a SequentFormula.
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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

factoryMap

private final java.util.Map<Name,TermLabelFactory<?>> factoryMap

Maps the Name of a TermLabel to its TermLabelFactory.

applicationTermPolicyMap

private final java.util.Map<Name,TermLabelPolicy> applicationTermPolicyMap

Maps the Name of a TermLabel to its TermLabelPolicy applied on the application Term.

modalityTermPolicyMap

private final java.util.Map<Name,TermLabelPolicy> modalityTermPolicyMap

Maps the Name of a TermLabel to its TermLabelPolicy applied on the modality Term.

ruleSpecificDirectChildTermLabelPolicies

private final java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificDirectChildTermLabelPolicies

All rule specific direct ChildTermLabelPolicys.

allRulesDirectChildTermLabelPolicies

private final java.util.Map<Name,ChildTermLabelPolicy> allRulesDirectChildTermLabelPolicies

All rule independent direct ChildTermLabelPolicys.

ruleSpecificChildAndGrandchildTermLabelPolicies

private final java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificChildAndGrandchildTermLabelPolicies

All rule specific child and grandchild ChildTermLabelPolicys.

allRulesChildAndGrandchildTermLabelPolicies

private final java.util.Map<Name,ChildTermLabelPolicy> allRulesChildAndGrandchildTermLabelPolicies

All rule independent child and grandchild ChildTermLabelPolicys.

ruleSpecificUpdates

private final java.util.Map<Name,ImmutableList<TermLabelUpdate>> ruleSpecificUpdates

All rule independent TermLabelUpdates.

allRulesUpdates

private ImmutableList<TermLabelUpdate> allRulesUpdates

All rule independent TermLabelUpdates.

ruleSpecificRefactorings

private final java.util.Map<Name,ImmutableList<TermLabelRefactoring>> ruleSpecificRefactorings

All rule specific TermLabelRefactorings.

allRulesRefactorings

private ImmutableList<TermLabelRefactoring> allRulesRefactorings

All rule independent TermLabelRefactorings.

supportedTermLabelnames

private ImmutableList<Name> supportedTermLabelnames

The Names of all supported TermLabels.

mergerMap

private final java.util.Map<Name,TermLabelMerger> mergerMap

Maps the Name of a TermLabel to its TermLabelMerger.

Constructor Detail

TermLabelManager

public TermLabelManager(ImmutableList<TermLabelManager.TermLabelConfiguration> configurations)

Constructor.

Parameters:

configurations - The TermLabelManager.TermLabelConfiguration which defines how to support each TermLabel.

Method Detail

analyzeMerger

private void analyzeMerger(Name termLabelName,
                           TermLabelMerger termLabelMerger)

Analyzes the given TermLabelMerger and adds it to mergerMap.

Parameters:

termLabelName - The name of the supported TermLabel.

termLabelMerger - The TermLabelMerger to use.

analyzeTermPolicies

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).

Parameters:

termLabelName - The name of the supported TermLabel.

policies - The TermLabelPolicy instances to analyze.

policyMap - The policy Map to update.

analyzeChildTermPolicies

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 Maps.

This is a helper Map of TermLabelManager(ImmutableList).

Parameters:

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.

analyzeUpdates

private void analyzeUpdates(ImmutableList<TermLabelUpdate> updates)

Analyzes the given TermLabelUpdate and updates allRulesUpdates and ruleSpecificUpdates.

This is a helper Map of TermLabelManager(ImmutableList).

Parameters:

updates - The TermLabelUpdates to analyze.

analyzeRefactorings

private void analyzeRefactorings(ImmutableList<TermLabelRefactoring> refactorings)

Analyzes the given TermLabelRefactoring and updates allRulesRefactorings and ruleSpecificRefactorings.

This is a helper Map of TermLabelManager(ImmutableList).

param updates The TermLabelUpdates to analyze.

getTermLabelManager

public static TermLabelManager getTermLabelManager(Services services)

Returns the TermLabelManager defined by the Profile of the given Services.

Parameters:

services - The Services which provides the TermLabelManager.

Returns:

The TermLabelManagers or null if not available.

getSupportedTermLabelNames

public static ImmutableList<Name> getSupportedTermLabelNames(Services services)

Returns the Names of the supported TermLabels.

Parameters:

services - The Services used by the Proof on which the Names of supported TermLabels are requested.

Returns:

The Names of the supported TermLabels.

getSupportedTermLabelNames

public ImmutableList<Name> getSupportedTermLabelNames()

Returns the Names of all supported TermLabels.

Returns:

The Names of all supported TermLabels.

parseLabel

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.

Parameters:

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 symbols

Returns:

term label of kind name with parameters as parsed.

Throws:

TermLabelException - if name is not a registered label name or the arguments cannot be parsed.

label

public 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 TermLabels 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).

Parameters:

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.

Returns:

The Term with updates labels.

label

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)

Computes the TermLabels 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).

Parameters:

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.

Returns:

The Term with updates labels.

label

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)

Computes the TermLabels 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).

Parameters:

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.

Returns:

The Term with updates labels.

instantiateLabels

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.

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.

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 QuantifiableVariables of the Term to create.

newTermJavaBlock - The optional JavaBlock of the Term to create.

newTermOriginalLabels - The original TermLabels.

Returns:

The TermLabels to add to the new Term which should be created.

instantiateLabels

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.

Parameters:

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 QuantifiableVariables of the Term to create.

newTermJavaBlock - The optional JavaBlock of the Term to create.

newTermOriginalLabels - The original TermLabels.

Returns:

The TermLabels to add to the new Term which should be created.

instantiateLabels

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)

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 in the following way:

1. An empty result List is created.
2. All labels from taclet term are added to the result List.
3. Existing labels on application term are added to result List if TermLabelPolicy wants to keep it.
4. Existing labels on modality term are added to result List if TermLabelPolicy wants to keep it.
5. All TermLabelUpdate are asked to add or remove labels from result List
6. Result List is returned.

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.

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 QuantifiableVariables of the Term to create.

newTermJavaBlock - The optional JavaBlock of the Term to create.

newTermOriginalLabels - The original TermLabels.

Returns:

The TermLabels to add to the new Term which should be created.

performTacletTerm

protected void performTacletTerm(Term tacletTerm,
                                 java.util.Set<TermLabel> newLabels)

Performs the TermLabels provided by the taclet Term.

This is a helper Map of #instantiateLabels( TermLabelState, Services, PosInOccurrence, Term, Rule, Goal, Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock).

Parameters:

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.

newLabels - The result Set with the TermLabels of the new Term.

performTermLabelPolicies

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).

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 QuantifiableVariables of the Term to create.

newTermJavaBlock - The optional JavaBlock of the Term to create.

newTermOriginalLabels - The original TermLabels.

policies - The TermLabelPolicy instances to perform.

newLabels - The result Set with the TermLabels of the new Term.

performTermLabelPolicies

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).

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 QuantifiableVariables of the Term to create.

newTermJavaBlock - The optional JavaBlock of the Term to create.

newTermOriginalLabels - The original TermLabels.

policies - The TermLabelPolicy instances to perform.

newLabels - The result Set with the TermLabels of the new Term.

label - The current TermLabel to ask its TermLabelPolicy.

computeActiveChildPolicies

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).

Parameters:

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 QuantifiableVariables of the Term to create.

newTermJavaBlock - The optional JavaBlock of the Term to create.

ruleSpecificPolicies - Rule specific ChildTermLabelPolicy instances.

ruleIndependentPolicies - All rules ChildTermLabelPolicy instances.

Returns:

The active ChildTermLabelPolicy which have to be performed.

performDirectChildPolicies

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).

Parameters:

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 QuantifiableVariables 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 TermLabels of the new Term.

performChildAndGrandchildPolicies

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).

Parameters:

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 QuantifiableVariables 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 TermLabels of the new Term.

performUpdater

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).

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.

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 QuantifiableVariables 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 TermLabels of the new Term.

refactorSequentFormula

public static Term refactorSequentFormula(TermLabelState state,
                                          Services services,
                                          Term sequentFormula,
                                          PosInOccurrence applicationPosInOccurrence,
                                          Rule rule,
                                          Goal goal,
                                          java.lang.Object hint,
                                          Term tacletTerm)

Refactors all labels on the PosInOccurrence in the given Term of a SequentFormula.

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.

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.

Returns:

The updated application Term.

refactorSequentFormula

public Term refactorSequentFormula(TermLabelState state,
                                   Services services,
                                   Term sequentFormula,
                                   PosInOccurrence applicationPosInOccurrence,
                                   Goal goal,
                                   java.lang.Object hint,
                                   Rule rule,
                                   Term tacletTerm)

Refactors all labels on the PosInOccurrence in the given Term of a SequentFormula.

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.

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.

Returns:

The updated application Term.

refactorTerm

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.

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.

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.

Returns:

The updated application Term.

refactorTerm

public 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.

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.

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.

Returns:

The updated application Term.

refactorGoal

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.

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.

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.

refactorGoal

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.

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 taclet Term.

refactorSequent

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.

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.

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.

refactorSequent

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.

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 taclet Term.

replaceTerm

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.

Parameters:

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.

Returns:

The root of the PosInOccurrence containing the new Term at the specified PosInOccurrence.

computeRefactorings

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.

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 taclet Term.

Returns:

The TermLabelManager.RefactoringsContainer with the TermLabelRefactorings to consider.

refactorApplicationTerm

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.

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 taclet Term.

refactorings - The TermLabelManager.RefactoringsContainer with the TermLabelRefactorings to consider.

Returns:

The new application Term or null if no refactoring was performed.

refactorSemisequent

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.

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 taclet Term.

semisequent - The Semisequent to refactor.

inAntec - true antecedent, false succedent.

activeRefactorings - The active TermLabelRefactorings to execute.

refactorLabelsRecursive

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)

Performs a TermLabel refactoring recursively on the given Term.

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 taclet Term.

term - The Term to refactor.

activeRefactorings - The active TermLabelRefactorings to execute.

Returns:

The refactored Term in which the TermLabels may have changed.

performRefactoring

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.

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 taclet Term.

term - The Term to refactor.

activeRefactorings - The active TermLabelRefactorings to execute.

Returns:

The new TermLabel which should be used for the given Term.

findInnerMostParentLabel

public static TermLabel findInnerMostParentLabel(PosInOccurrence pio,
                                                 Name termLabelName)

Searches the inner most TermLabel wit the given Name in the parent hierarchy of the PosInOccurrence.

Parameters:

pio - The PosInOccurrence to search in.

termLabelName - The Name of the TermLabel to search.

Returns:

The found TermLabel or null if not available.

mergeLabels

public static void mergeLabels(SequentChangeInfo currentSequent,
                               Services services)

Merges the TermLabels of the rejected SequentFormulas into the resulting Sequent.

Parameters:

currentSequent - The SequentChangeInfo which lists the rejected SequentFormulas.

services - The Services to use.

mergeLabels

public void mergeLabels(Services services,
                        SequentChangeInfo currentSequent)

Merges the TermLabels of the rejected SequentFormulas into the resulting Sequent.

Parameters:

services - The Services to use.

currentSequent - The SequentChangeInfo which lists the rejected SequentFormulas.

mergeLabels

protected void mergeLabels(SequentChangeInfo currentSequent,
                           Services services,
                           SequentFormula rejectedSF,
                           boolean inAntecedent)

Merges the TermLabels of the given SequentFormula into the resulting Sequent.

Parameters:

currentSequent - The SequentChangeInfo which lists the rejected SequentFormulas.

services - The Services to use.

rejectedSF - The rejected SequentFormula to work with.

inAntecedent - true rejected SequentFormula is in antecedent, false it is in succedent.