Package | Description |
---|---|
de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
Modifier and Type | Method and Description |
---|---|
static GenericSortCondition |
GenericSortCondition.createCondition(SchemaVariable sv,
InstantiationEntry<?> p_entry)
Create the condition that needs to be fulfilled for the given
instantiation of a metavariable to be correct, i.e.
|
static GenericSortCondition |
GenericSortCondition.createCondition(SortDependingFunction p0,
SortDependingFunction p1)
Create a condition ensuring that the two given symbols become
identical; "p0" may be of generic sort, "p1" not
|
protected static GenericSortCondition |
GenericSortCondition.createCondition(Sort s0,
Sort s1,
boolean p_identity)
Create the condition to make a generic sort (s0) (or a
collection sort of a generic sort) and a concrete sort (s1)
equal
|
static GenericSortCondition |
GenericSortCondition.createForceInstantiationCondition(GenericSort p_gs,
boolean p_maximum) |
static GenericSortCondition |
GenericSortCondition.createIdentityCondition(GenericSort p_gs,
Sort p_s) |
static GenericSortCondition |
GenericSortCondition.createSupersortCondition(GenericSort p_gs,
Sort p_s) |
static GenericSortCondition |
GenericSortCondition.forceInstantiation(Sort p_s,
boolean p_maximum)
Create the condition to force the instantiation of a given
(possibly generic) sort
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<GenericSortCondition> |
SVInstantiations.getGenericSortConditions() |
ImmutableList<GenericSortCondition> |
GenericSortInstantiations.toConditions()
Create a list of conditions establishing the instantiations
stored by this object (not saying anything about further
generic sorts)
|
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.add(GenericSortCondition p_c,
Services services)
Add the given additional condition for the generic sort instantiations
|
java.lang.Boolean |
GenericSortInstantiations.checkCondition(GenericSortCondition p_condition) |
Modifier and Type | Method and Description |
---|---|
static GenericSortInstantiations |
GenericSortInstantiations.create(ImmutableList<GenericSort> p_sorts,
ImmutableList<GenericSortCondition> p_conditions,
Services services)
Create an object that holds instantiations of the generic sorts
"p_sorts" satisfying the conditions "p_conditions"
|
static GenericSortInstantiations |
GenericSortInstantiations.create(java.util.Iterator<ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>>> p_instantiations,
ImmutableList<GenericSortCondition> p_conditions,
Services services)
Create an object that solves the conditions given by the
instantiation iterator, i.e.
|
void |
GenericSortException.setConditions(ImmutableList<GenericSortCondition> pConditions) |
Constructor and Description |
---|
GenericSortException(java.lang.String description,
ImmutableList<GenericSortCondition> pConditions) |
Copyright © 2003-2019 The KeY-Project.