01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.logic.sort;
12:
13: import de.uka.ilkd.key.logic.Name;
14:
15: public class PrimitiveSort extends AbstractNonCollectionSort {
16:
17: private static final SetOfSort EMPTY_SORT_SET = SetAsListOfSort.EMPTY_SET;
18:
19: /** direct supersorts */
20: SetOfSort ext = EMPTY_SORT_SET;
21:
22: /** creates a Sort (with a new equality symbol for this sort) */
23: public PrimitiveSort(Name name) {
24: super (name);
25: }
26:
27: public PrimitiveSort(Name name, SetOfSort ext) {
28: super (name);
29: this .ext = ext;
30: }
31:
32: public SetOfSort extendsSorts() {
33: return ext;
34: }
35:
36: /**
37: * @return the sorts of the predecessors of this sort
38: */
39: public boolean extendsTrans(Sort sort) {
40: if (sort == this || sort == Sort.ANY) {
41: return true;
42: }
43:
44: if (!(sort instanceof PrimitiveSort)) {
45: return false;
46: }
47:
48: final IteratorOfSort it = extendsSorts().iterator();
49: while (it.hasNext()) {
50: final Sort s = it.next();
51: assert s != null;
52: if (s == sort || s.extendsTrans(sort)) {
53: return true;
54: }
55: }
56: return false;
57: }
58: }
|