| java.lang.Object
 de.uka.ilkd.key.rule.inst.GenericSortInstantiations
| GenericSortInstantiations | | public class GenericSortInstantiations (Code) | | This class handles the instantiation of generic sorts (used for
generic taclets), i.e. the class tries to find a solution for the
conditions on the generic sorts given by the type hierarchy and the
chosen SV instantiations
this class is immutable
|
| checkCondition | | public Boolean checkCondition(GenericSortCondition p_condition)(Code) | | Boolean.TRUE if the generic sort instantiations within"this" satisfy "p_condition", null otherwise (this means,"p_condition" could be satisfied by create a new"GenericSortInstantiations"-object) |
| checkSorts | | public Boolean checkSorts(InstantiationEntry p_entry)(Code) | | Boolean.TRUE if the sorts used within "p_entry" arecorrect, Boolean.FALSE if the sorts are definitely incorrect,null if the sorts could (perhaps) be made correct by choosingthe right generic sort instantiations |
| create | | public static GenericSortInstantiations create(IteratorOfEntryOfSchemaVariableAndInstantiationEntry p_instantiations, ListOfGenericSortCondition p_conditions)(Code) | | Create an object that solves the conditions given by the
instantiation iterator, i.e. instantiations of the generic
sorts used within "p_instantiations" are sought for which are
compatible with the instantiations of the SVs
Parameters:
p_instantiations - list of SV instantiations
Parameters:
p_conditions - additional conditions for sort instantiations
throws:
GenericSortException - iff the conditions could not besolved |
| create | | public static GenericSortInstantiations create(ListOfGenericSort p_sorts, ListOfGenericSortCondition p_conditions)(Code) | | Create an object that holds instantiations of the generic sorts
"p_sorts" satisfying the conditions "p_conditions"
Parameters:
p_sorts - generic sorts to instantiate
Parameters:
p_conditions - conditions the instantiations have tosatisfy
throws:
GenericSortException - if no instantiations has beenfound |
| getAllInstantiations | | public MapFromGenericSortToSort getAllInstantiations()(Code) | | ONLY FOR JUNIT TESTS
|
| getRealSort | | public Sort getRealSort(SchemaVariable p_sv, Services services)(Code) | |
Parameters:
services - the Services class p_s iff p_s is not a generic sort, the concrete sortp_s is instantiated with currently otherwise
throws:
GenericSortException - iff p_s is a generic sort which isnot yet instantiated |
| toConditions | | public ListOfGenericSortCondition toConditions()(Code) | | Create a list of conditions establishing the instantiations
stored by this object (not saying anything about further
generic sorts)
|
|
|