de.uka.ilkd.key.rule.inst

Class GenericSortCondition

java.lang.Object

de.uka.ilkd.key.rule.inst.GenericSortCondition

Direct Known Subclasses:

GenericSortCondition.GSCForceInstantiation, GenericSortCondition.GSCIdentity, GenericSortCondition.GSCSupersort

public abstract class GenericSortCondition
extends java.lang.Object

Abstract superclass for conditions controlling the instantiations of generic sorts

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	GenericSortCondition.GSCForceInstantiation
(package private) static class	GenericSortCondition.GSCIdentity
(package private) static class	GenericSortCondition.GSCSupersort

Field Summary

Fields

Modifier and Type	Field and Description
private GenericSort	gs

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	GenericSortCondition(GenericSort p_gs)

Method Summary

Modifier and Type	Method and Description
abstract boolean	check(Sort s, GenericSortInstantiations insts) returns true if the given sort s satisfies this generic sort condition
static 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. if the schemavariable is of generic sort, the instantiation of that sort has to match the sort of the schemavariable's instantiation
static 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	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	createForceInstantiationCondition(GenericSort p_gs, boolean p_maximum)
static GenericSortCondition	createIdentityCondition(GenericSort p_gs, Sort p_s)
static GenericSortCondition	createSupersortCondition(GenericSort p_gs, Sort p_s)
static GenericSortCondition	forceInstantiation(Sort p_s, boolean p_maximum) Create the condition to force the instantiation of a given (possibly generic) sort
GenericSort	getGenericSort()
(package private) static boolean	subSortsAllowed(SchemaVariable p_sv)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

gs

private GenericSort gs

Constructor Detail

GenericSortCondition

protected GenericSortCondition(GenericSort p_gs)

Method Detail

createCondition

public static 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. if the schemavariable is of generic sort, the instantiation of that sort has to match the sort of the schemavariable's instantiation

Returns:

the resulting condition, if the schemavariable is of generic sort; null, if the sorts are either always compatible (no generic sorts) or never compatible (non generic sorts that don't match)

createCondition

public static 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

Returns:

the resulting condition; null if the symbols are either incompatible or equal

subSortsAllowed

static boolean subSortsAllowed(SchemaVariable p_sv)

Returns:

true iff the variable p_sv is allowed to be instantiated with expressions that have a real subtype of the type of p_sv. Otherwise the sorts have to match exactly

createCondition

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 be generated (otherwise: a supersort condition is generated)

Returns:

the resulting condition, if "s0" is of generic sort; null, if the sorts are either always compatible (no generic sorts) or never compatible (e.g. non generic sorts that don't match)

forceInstantiation

public static GenericSortCondition forceInstantiation(Sort p_s,
                                                      boolean p_maximum)

Create the condition to force the instantiation of a given (possibly generic) sort

Parameters:

p_maximum - hint whether the generic sort should be instantiated with the maximum or mimimum possible concrete sort (this hint is currently not used by GenericSortInstantiations)

Returns:

the resulting condition, or null if "p_s" is not generic

createSupersortCondition

public static GenericSortCondition createSupersortCondition(GenericSort p_gs,
                                                            Sort p_s)

Returns:

a condition that specifies the given generic sort to be instantiated with a supersort of the given concrete sort

createIdentityCondition

public static GenericSortCondition createIdentityCondition(GenericSort p_gs,
                                                           Sort p_s)

Returns:

a condition that specifies the given generic sort to be instantiated (exactly) with the given concrete sort

createForceInstantiationCondition

public static GenericSortCondition createForceInstantiationCondition(GenericSort p_gs,
                                                                     boolean p_maximum)

Parameters:

p_maximum - hint whether the generic sort should be instantiated with the maximum or mimimum possible concrete sort (this hint is currently not used by GenericSortInstantiations)

Returns:

a condition that specifies the given generic sort to be instantiated

getGenericSort

public GenericSort getGenericSort()

check

public abstract boolean check(Sort s,
                              GenericSortInstantiations insts)

returns true if the given sort s satisfies this generic sort condition

Parameters:

s - the Sort to check

insts - a map containing already found instantiations

Returns:

true if the given sort s satisfies this generic sort condition