Package | Description |
---|---|
de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
Modifier and Type | Class and Description |
---|---|
class |
ContextInstantiationEntry
This class is used to store the information about a matched
context of a dl formula.
|
class |
ListInstantiation |
class |
NameInstantiationEntry
This class is used to store the instantiation of a schemavarible
if it is a name.
|
class |
OperatorInstantiation
This class is used to store the instantiation of a schemavarible
if it is an operator.
|
class |
ProgramInstantiation
This class is used to store the instantiation of a schemavarible
if it is a ProgramElement.
|
class |
ProgramListInstantiation
This class is used to store the instantiation of a schemavariable
if it is a ProgramElement.
|
class |
TermInstantiation
This class is used to store the instantiation of a schemavarible
if it is a term.
|
class |
TermLabelInstantiationEntry |
Modifier and Type | Method and Description |
---|---|
InstantiationEntry<?> |
SVInstantiations.getInstantiationEntry(SchemaVariable sv)
returns the instantiation of the given SchemaVariable
|
Modifier and Type | Method and Description |
---|---|
ImmutableMap<SchemaVariable,InstantiationEntry<?>> |
SVInstantiations.interesting() |
ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>> |
SVInstantiations.lookupEntryForSV(Name name) |
java.util.Iterator<ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>>> |
SVInstantiations.pairIterator()
returns iterator of the mapped pair (SchemaVariables, InstantiationEntry>)
|
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services) |
java.lang.Boolean |
GenericSortInstantiations.checkSorts(SchemaVariable sv,
InstantiationEntry<?> p_entry) |
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.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services)
replaces the given pair in the instantiations.
|
Modifier and Type | Method and Description |
---|---|
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.
|
Copyright © 2003-2019 The KeY-Project.