de.uka.ilkd.key.logic.sort

Class GenericSort

java.lang.Object

de.uka.ilkd.key.logic.sort.AbstractSort

de.uka.ilkd.key.logic.sort.GenericSort

All Implemented Interfaces:

Named, Sort

public final class GenericSort
extends AbstractSort

Sort used for generic taclets Within an SVInstantiations-object a generic sort is instantiated by a concrete sort, which has to be a subsort of the instantiations of the supersorts of this sort

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableSet<Sort>	oneOf list of sorts this generic sort may be instantiated with; EMPTY_SORT_SORT means that every sort may be used

Fields inherited from interface de.uka.ilkd.key.logic.sort.Sort

ANY, CAST_NAME, EXACT_INSTANCE_NAME, FORMULA, INSTANCE_NAME, TERMLABEL, UPDATE

Constructor Summary

Constructors

Constructor and Description
GenericSort(Name name)
GenericSort(Name name, ImmutableSet<Sort> ext, ImmutableSet<Sort> oneOf) creates a generic sort

Method Summary

Modifier and Type	Method and Description
protected boolean	checkNonGenericSupersorts(Sort p_s)
private void	checkSupersorts()
ImmutableSet<Sort>	getOneOf()
boolean	isPossibleInstantiation(Sort p_s)

Methods inherited from class de.uka.ilkd.key.logic.sort.AbstractSort

declarationString, extendsSorts, extendsSorts, extendsTrans, getCastSymbol, getExactInstanceofSymbol, getInstanceofSymbol, isAbstract, name, toString

Methods inherited from class java.lang.Object

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

Field Detail

oneOf

private final ImmutableSet<Sort> oneOf

list of sorts this generic sort may be instantiated with; EMPTY_SORT_SORT means that every sort may be used

Constructor Detail

GenericSort

public GenericSort(Name name,
                   ImmutableSet<Sort> ext,
                   ImmutableSet<Sort> oneOf)
            throws GenericSupersortException

creates a generic sort

Parameters:

ext - supersorts of this sort, which have to be either concrete sorts or plain generic sorts (i.e. not collection sorts of generic sorts)

Throws:

GenericSupersortException

GenericSort

public GenericSort(Name name)

Method Detail

checkSupersorts

private void checkSupersorts()
                      throws GenericSupersortException

Throws:

GenericSupersortException

getOneOf

public ImmutableSet<Sort> getOneOf()

Returns:

possible instantiations

isPossibleInstantiation

public boolean isPossibleInstantiation(Sort p_s)

Returns:

true if "p_s" is a possible instantiation of this sort. This method does not check the instantiations of other generic sorts, i.e. the return value true is possible even if "p_s" is not a valid instantiation. Use "GenericSortInstantiations" instead

checkNonGenericSupersorts

protected boolean checkNonGenericSupersorts(Sort p_s)

Returns:

true iff "p_s" is subsort of every non-generic supersort of this sort