| java.lang.Object
 de.uka.ilkd.key.rule.inst.GenericSortCondition
| GenericSortCondition | | abstract public class GenericSortCondition (Code) | | Abstract superclass for conditions controlling the instantiations
of generic sorts
|
| Method Summary | |
| abstract public boolean | check(Sort s, GenericSortInstantiations insts)
| | public static GenericSortCondition | createCondition(InstantiationEntry p_entry)
Create the condition that needs to be fulfilled for the given
instantiation of a metavariable to be correct, i.e. | | public static GenericSortCondition | createCondition(SortDependingSymbol p0, SortDependingSymbol p1)
| | protected static 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
Parameters:
p_identity - true iff an identity condition should begenerated (otherwise: a supersort condition is generated) the resulting condition, if "s0" is of generic sort;null, if the sorts are either always compatible (no genericsorts) or never compatible (e.g. | | public static GenericSortCondition | createForceInstantiationCondition(GenericSort p_gs, boolean p_maximum)
| | public static GenericSortCondition | createIdentityCondition(GenericSort p_gs, Sort p_s)
| | public static GenericSortCondition | createSupersortCondition(GenericSort p_gs, Sort p_s)
| | public static GenericSortCondition | forceInstantiation(Sort p_s, boolean p_maximum)
| | public GenericSort | getGenericSort()
| | static boolean | subSortsAllowed(SortedSchemaVariable p_sv)
true iff the variable p_sv isallowed to be instantiated with expressions that have a realsubtype of the type of p_sv. |
| check | | abstract public boolean check(Sort s, GenericSortInstantiations insts)(Code) | | returns true if the given sort s satisfies this generic sort
condition
Parameters:
s - the Sort to check
Parameters:
insts - a map containing already found instantiations true if the given sort s satisfies this generic sortcondition |
| createCondition | | public static GenericSortCondition createCondition(InstantiationEntry p_entry)(Code) | | Create the condition that needs to be fulfilled for the given
instantiation of a metavariable to be correct, i.e. if the
schemavariable is of generic sort, the instantiation of that
sort has to match the sort of the schemavariable's
instantiation
the resulting condition, if the schemavariable is ofgeneric sort; null, if the sorts are either always compatible(no generic sorts) or never compatible (non generic sorts thatdon't match) |
| createCondition | | protected static GenericSortCondition createCondition(Sort s0, Sort s1, boolean p_identity)(Code) | | Create the condition to make a generic sort (s0) (or a
collection sort of a generic sort) and a concrete sort (s1)
equal
Parameters:
p_identity - true iff an identity condition should begenerated (otherwise: a supersort condition is generated) the resulting condition, if "s0" is of generic sort;null, if the sorts are either always compatible (no genericsorts) or never compatible (e.g. non generic sorts that don'tmatch) |
| createForceInstantiationCondition | | public static GenericSortCondition createForceInstantiationCondition(GenericSort p_gs, boolean p_maximum)(Code) | | a condition that specifies the given generic sort to beinstantiated
Parameters:
p_maximum - hint whether the generic sort should beinstantiated with the maximum or mimimum possible concrete sort(this hint is currently not used by GenericSortInstantiations) |
| createIdentityCondition | | public static GenericSortCondition createIdentityCondition(GenericSort p_gs, Sort p_s)(Code) | | a condition that specifies the given generic sort to beinstantiated (exactly) with the given concrete sort |
| createSupersortCondition | | public static GenericSortCondition createSupersortCondition(GenericSort p_gs, Sort p_s)(Code) | | a condition that specifies the given generic sort to beinstantiated with a supersort of the given concrete sort |
| forceInstantiation | | public static GenericSortCondition forceInstantiation(Sort p_s, boolean p_maximum)(Code) | | Create the condition to force the instantiation of a given
(possibly generic) sort
Parameters:
p_maximum - hint whether the generic sort should beinstantiated with the maximum or mimimum possible concrete sort(this hint is currently not used by GenericSortInstantiations) the resulting condition, or null if "p_s" is notgeneric |
| subSortsAllowed | | static boolean subSortsAllowed(SortedSchemaVariable p_sv)(Code) | | true iff the variable p_sv isallowed to be instantiated with expressions that have a realsubtype of the type of p_sv. Otherwise the sortshave to match exactly |
|
|