Package | Description |
---|---|
de.uka.ilkd.key.logic.label |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<Name,ChildTermLabelPolicy> |
TermLabelManager.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. |
ImmutableList<ChildTermLabelPolicy> |
TermLabelManager.TermLabelConfiguration.getChildAndGrandchildTermLabelPolicies()
Returns the child and grandchild
ChildTermLabelPolicy instances to use. |
ImmutableList<ChildTermLabelPolicy> |
TermLabelManager.TermLabelConfiguration.getDirectChildTermLabelPolicies()
Returns the direct
ChildTermLabelPolicy instances to use. |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<Name,ChildTermLabelPolicy> |
TermLabelManager.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 java.util.Map<Name,ChildTermLabelPolicy> |
TermLabelManager.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 void |
TermLabelManager.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 |
TermLabelManager.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. |
Constructor and Description |
---|
TermLabelConfiguration(Name termLabelName,
TermLabelFactory<?> factory,
ImmutableList<TermLabelPolicy> applicationTermPolicies,
ImmutableList<TermLabelPolicy> modalityTermPolicies,
ImmutableList<ChildTermLabelPolicy> directChildTermLabelPolicies,
ImmutableList<ChildTermLabelPolicy> childAndGrandchildTermLabelPolicies,
ImmutableList<TermLabelUpdate> termLabelUpdates,
ImmutableList<TermLabelRefactoring> termLabelRefactorings,
TermLabelMerger termLabelMerger)
Constructor.
|
TermLabelConfiguration(Name termLabelName,
TermLabelFactory<?> factory,
ImmutableList<TermLabelPolicy> applicationTermPolicies,
ImmutableList<TermLabelPolicy> modalityTermPolicies,
ImmutableList<ChildTermLabelPolicy> directChildTermLabelPolicies,
ImmutableList<ChildTermLabelPolicy> childAndGrandchildTermLabelPolicies,
ImmutableList<TermLabelUpdate> termLabelUpdates,
ImmutableList<TermLabelRefactoring> termLabelRefactorings,
TermLabelMerger termLabelMerger)
Constructor.
|
Copyright © 2003-2019 The KeY-Project.