001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.logic.sort;
012:
013: import de.uka.ilkd.key.logic.Name;
014:
015: /**
016: * Sort used for generic taclets
017: *
018: * Within an SVInstantiations-object a generic sort is instantiated by
019: * a concrete sort, which has to be a subsort of the instantiations of
020: * the supersorts of this sort
021: */
022: public class GenericSort extends AbstractNonCollectionSort implements
023: ObjectSort {
024:
025: /**
026: * A possible instantiation of this generic sort by a concrete
027: * sort must satisfy each of these conditions:
028: *
029: * - if any generic supersort is to be instantiated simultanously,
030: then this instantiation has to be a supersort of the
031: instantiation of this sort
032: *
033: * - the instantiation of this sort has to be a subsort of every
034: concrete supersort
035: *
036: * - if "oneOf" is not empty, the instantiation must be an element
037: of "oneOf"
038: */
039: private static final SetOfSort EMPTY_SORT_SET = SetAsListOfSort.EMPTY_SET;
040:
041: /** direct supersorts */
042: SetOfSort ext = EMPTY_SORT_SET;
043: /**
044: * list of sorts this generic sort may be instantiated with;
045: * EMPTY_SORT_SORT means that every sort may be used
046: */
047: SetOfSort oneOf = EMPTY_SORT_SET;
048:
049: /**
050: * creates a generic sort (with a new equality symbol for this
051: * sort)
052: */
053: public GenericSort(Name name) {
054: super (name);
055: }
056:
057: /**
058: * creates a generic sort
059: * @param ext supersorts of this sort, which have to be either
060: * concrete sorts or plain generic sorts (i.e. not collection
061: * sorts of generic sorts)
062: */
063: public GenericSort(Name name, SetOfSort ext, SetOfSort oneOf)
064: throws GenericSupersortException {
065:
066: this (name);
067: this .ext = ext;
068: this .oneOf = oneOf;
069: checkSupersorts();
070: }
071:
072: private void checkSupersorts() throws GenericSupersortException {
073: IteratorOfSort it = extendsSorts().iterator();
074: Sort s, t;
075: while (it.hasNext()) {
076: s = it.next();
077: if (s instanceof CollectionSort) {
078: t = ((CollectionSort) s).elementSort();
079: while (t instanceof CollectionSort)
080: t = ((CollectionSort) t).elementSort();
081: if (t instanceof GenericSort)
082: throw new GenericSupersortException(
083: "Illegal supersort " + s
084: + " for generic sort " + name(), s);
085: }
086: }
087: }
088:
089: /**
090: * @return direct supersorts
091: */
092: public SetOfSort extendsSorts() {
093: return ext;
094: }
095:
096: /**
097: * @return possible instantiations or "EMPTY_SORT_SET"
098: */
099: public SetOfSort getOneOf() {
100: return oneOf;
101: }
102:
103: /**
104: * @return true if "p_s" is a possible instantiation of this
105: * sort. This method does not check the instantiations of other
106: * generic sorts, i.e. the return value true is possible even if
107: * "p_s" is not a valid instantiation.
108: *
109: * Use "GenericSortInstantiations" instead
110: */
111: public boolean isPossibleInstantiation(Sort p_s) {
112: return p_s != Sort.FORMULA
113: && (oneOf == EMPTY_SORT_SET || oneOf.contains(p_s))
114: && checkNonGenericSupersorts(p_s);
115: }
116:
117: /**
118: * @return true iff "p_s" is subsort of every non-generic
119: * supersort of this sort
120: */
121: protected boolean checkNonGenericSupersorts(Sort p_s) {
122: IteratorOfSort it = ext.iterator();
123: Sort ss;
124:
125: while (it.hasNext()) {
126: ss = it.next();
127: if (ss instanceof GenericSort) {
128: if (!((GenericSort) ss).checkNonGenericSupersorts(p_s))
129: return false;
130: } else {
131: if (!p_s.extendsTrans(ss))
132: return false;
133: }
134: }
135:
136: return true;
137: }
138: }
|