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.oclsort;
012:
013: import de.uka.ilkd.key.logic.Name;
014: import de.uka.ilkd.key.logic.op.Equality;
015: import de.uka.ilkd.key.logic.op.Op;
016: import de.uka.ilkd.key.logic.sort.*;
017:
018: public class CollectionSort implements OclSort {
019:
020: public static final int COLLECTION = 0;
021: public static final int SET = 1;
022: public static final int BAG = 2;
023: public static final int SEQUENCE = 3;
024:
025: private int collectionKind;
026: private OclSort elemSort;
027: private Name name;
028: private int hashcode = 0;
029:
030: public CollectionSort(int collectionKind, OclSort elemSort) {
031: this .collectionKind = collectionKind;
032: this .elemSort = elemSort;
033:
034: switch (this .collectionKind) {
035: case COLLECTION:
036: name = new Name("OclCollectionOf" + elemSort.name());
037: break;
038: case SET:
039: name = new Name("OclSetOf" + elemSort.name());
040: break;
041: case BAG:
042: name = new Name("OclBagOf" + elemSort.name());
043: break;
044: case SEQUENCE:
045: name = new Name("OclSequenceOf" + elemSort.name());
046: break;
047: }
048: }
049:
050: /** @return name of the Sort */
051: public Name name() {
052: return name;
053: }
054:
055: public int getCollectionKind() {
056: return collectionKind;
057: }
058:
059: public OclSort getElemSort() {
060: return elemSort;
061: }
062:
063: public static CollectionSort getCollectionSort(int collectionKind,
064: OclSort elemSort) {
065: switch (collectionKind) {
066: case SET:
067: return getSetSort(elemSort);
068: case BAG:
069: return getBagSort(elemSort);
070: case SEQUENCE:
071: return getSequenceSort(elemSort);
072: default:
073: return getSetSort(elemSort);
074: }
075: }
076:
077: private static CollectionSort getSetSort(OclSort elemSort) {
078:
079: if (elemSort == OclSort.OCLGENERIC) {
080: return OclSort.SET_OF_OCLGENERIC;
081: } else if (elemSort == OclSort.OCLANY) {
082: return OclSort.SET_OF_OCLANY;
083: } else if (elemSort == OclSort.OCLTYPE) {
084: return OclSort.SET_OF_OCLTYPE;
085: } else if (elemSort == OclSort.BOOLEAN) {
086: return OclSort.SET_OF_BOOLEAN;
087: } else if (elemSort == OclSort.REAL) {
088: return OclSort.SET_OF_REAL;
089: } else if (elemSort == OclSort.INTEGER) {
090: return OclSort.SET_OF_INTEGER;
091: } else if (elemSort == OclSort.STRING) {
092: return OclSort.SET_OF_STRING;
093: } else {
094: return OclSort.SET_OF_CLASSIFIER;
095: }
096: }
097:
098: private static CollectionSort getBagSort(OclSort elemSort) {
099:
100: if (elemSort == OclSort.OCLGENERIC) {
101: return OclSort.BAG_OF_OCLGENERIC;
102: } else if (elemSort == OclSort.OCLANY) {
103: return OclSort.BAG_OF_OCLANY;
104: } else if (elemSort == OclSort.OCLTYPE) {
105: return OclSort.BAG_OF_OCLTYPE;
106: } else if (elemSort == OclSort.BOOLEAN) {
107: return OclSort.BAG_OF_BOOLEAN;
108: } else if (elemSort == OclSort.REAL) {
109: return OclSort.BAG_OF_REAL;
110: } else if (elemSort == OclSort.INTEGER) {
111: return OclSort.BAG_OF_INTEGER;
112: } else if (elemSort == OclSort.STRING) {
113: return OclSort.BAG_OF_STRING;
114: } else {
115: return OclSort.BAG_OF_CLASSIFIER;
116: }
117: }
118:
119: private static CollectionSort getSequenceSort(OclSort elemSort) {
120:
121: if (elemSort == OclSort.OCLGENERIC) {
122: return OclSort.SEQUENCE_OF_OCLGENERIC;
123: } else if (elemSort == OclSort.OCLANY) {
124: return OclSort.SEQUENCE_OF_OCLANY;
125: } else if (elemSort == OclSort.OCLTYPE) {
126: return OclSort.SEQUENCE_OF_OCLTYPE;
127: } else if (elemSort == OclSort.BOOLEAN) {
128: return OclSort.SEQUENCE_OF_BOOLEAN;
129: } else if (elemSort == OclSort.REAL) {
130: return OclSort.SEQUENCE_OF_REAL;
131: } else if (elemSort == OclSort.INTEGER) {
132: return OclSort.SEQUENCE_OF_INTEGER;
133: } else if (elemSort == OclSort.STRING) {
134: return OclSort.SEQUENCE_OF_STRING;
135: } else {
136: return OclSort.SEQUENCE_OF_CLASSIFIER;
137: }
138: }
139:
140: /**
141: * For finding out whether a certain sort is super- or subsort of another
142: * sort or not, please use <code>extendsTrans</code>.
143: * Using <code>extendsSorts()</code> for this purpose may lead to
144: * undesired results when dealing with arraysorts!
145: * @return the sorts of the predecessors of this sort
146: */
147: public SetOfSort extendsSorts() {
148: return SetAsListOfSort.EMPTY_SET;
149: }
150:
151: /**
152: * returns true iff the given sort is a transitive supersort of this sort
153: * or it is the same.
154: */
155: public boolean extendsTrans(Sort sort) {
156: if (sort instanceof OclGenericSort) {
157: return true;
158: } else if (sort instanceof GenericSort) {
159: if (((GenericSort) sort).getOneOf().size() == 0) {
160: return true;
161: } else {
162: IteratorOfSort iter = ((GenericSort) sort).getOneOf()
163: .iterator();
164: while (iter.hasNext()) {
165: if (this .extendsTrans(iter.next())) {
166: return true;
167: }
168: }
169: return false;
170: }
171: } else {
172: if (!(sort instanceof CollectionSort)) {
173: return false;
174: }
175: if (((CollectionSort) sort).getCollectionKind() != COLLECTION
176: && this .getCollectionKind() != ((CollectionSort) sort)
177: .getCollectionKind()) {
178: return false;
179: }
180: return this .getElemSort().extendsTrans(
181: ((CollectionSort) sort).getElemSort());
182: }
183: }
184:
185: /** @return equality symbol of this sort */
186: public Equality getEqualitySymbol() {
187: return Op.EQUALS;
188: }
189:
190: public boolean equals(Object obj) {
191: if (!(obj instanceof CollectionSort)) {
192: return false;
193: }
194: CollectionSort cSort = (CollectionSort) obj;
195: if (this .collectionKind == cSort.collectionKind
196: && this .elemSort == cSort.elemSort) {
197: return true;
198: } else {
199: return false;
200: }
201: }
202:
203: public int hashCode() {
204: if (hashcode == 0) {
205: hashcode = calculateHash();
206: }
207: return hashcode;
208: }
209:
210: protected int calculateHash() {
211: int hashValue = 5;
212: hashValue = hashValue * 17 + collectionKind * 5;
213: hashValue = hashValue * 17 + elemSort.hashCode();
214: return hashValue;
215: }
216:
217: public String toString() {
218: return name.toString();
219: }
220: }
|