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: package de.uka.ilkd.key.java.abstraction;
011:
012: import java.util.Comparator;
013:
014: import de.uka.ilkd.key.java.expression.Literal;
015: import de.uka.ilkd.key.java.reference.PackageReference;
016: import de.uka.ilkd.key.logic.ProgramElementName;
017: import de.uka.ilkd.key.logic.sort.*;
018:
019: /**
020: * The KeY java type realises a tuple (sort, type) of a logic sort and
021: * the java type (for example a class declaration).
022: * In contrast to other classes the KeYJavaType is <emph>not</emph>
023: * immutable, so use it with care.
024: */
025: public class KeYJavaType implements Type {
026:
027: /** the AST type */
028: private Type javaType = null;
029: /** the logic sort */
030: private Sort sort = null;
031:
032: /** creates a new KeYJavaType */
033: public KeYJavaType() {
034: }
035:
036: /** creates a new KeYJavaType */
037: public KeYJavaType(Type javaType, Sort sort) {
038: this .javaType = javaType;
039: this .sort = sort;
040: ensureTypeSortConformance();
041: }
042:
043: /** creates a new KeYJavaType */
044: public KeYJavaType(Sort sort) {
045: this .sort = sort;
046: }
047:
048: /** creates a new KeYJavaType */
049: public KeYJavaType(Type type) {
050: this .javaType = type;
051: }
052:
053: private void ensureTypeSortConformance() {
054: if (javaType != null && sort != null) {
055:
056: if (javaType instanceof NullType
057: && sort instanceof NullSort) {
058: return;
059: }
060:
061: final boolean b = (javaType instanceof ClassType == sort instanceof ObjectSort);
062:
063: if (!b) {
064: throw new IllegalStateException(
065: "A primitive sort/type cannot be mapped "
066: + "for a reference type/sort (type:"
067: + javaType + "," + sort + ")");
068: }
069:
070: boolean arrayTypeSort = (javaType instanceof ArrayType == sort instanceof ArraySort);
071:
072: if (!arrayTypeSort) {
073: throw new IllegalStateException(
074: "A non-array sort/type cannot be mapped "
075: + "to an array type/sort (type:"
076: + javaType + "," + sort + ")");
077: }
078:
079: if (javaType instanceof ClassType) {
080: final ObjectSort os = (ObjectSort) sort;
081: if (os instanceof ClassInstanceSort) {
082: boolean conform = ((ClassInstanceSort) os)
083: .representAbstractClassOrInterface() == (((ClassType) javaType)
084: .isAbstract() || ((ClassType) javaType)
085: .isInterface());
086: if (!conform) {
087: throw new IllegalStateException("Java type "
088: + javaType
089: + " cannot be mapped to sort " + os);
090: }
091: }
092: }
093: }
094: }
095:
096: public void setJavaType(Type type) {
097: javaType = type;
098: ensureTypeSortConformance();
099: }
100:
101: public void setSort(Sort s) {
102: sort = s;
103: ensureTypeSortConformance();
104: }
105:
106: public Type getJavaType() {
107: return javaType;
108: }
109:
110: public Sort getSort() {
111: return sort;
112: }
113:
114: /**
115: * returns the default value of the given type
116: * according to JLS ???4.5.5
117: * @return the default value of the given type
118: * according to JLS ???4.5.5
119: */
120: public Literal getDefaultValue() {
121: return javaType.getDefaultValue();
122: }
123:
124: public String toString() {
125: if (javaType == null)
126: return "KeYJavaType:null," + sort;
127: return "(type, sort): (" + javaType.getName() + "," + sort
128: + ")";
129: }
130:
131: public String getFullName() {
132: return getJavaType().getFullName();
133: }
134:
135: public String getName() {
136: return getJavaType().getName();
137: }
138:
139: public PackageReference createPackagePrefix() {
140: PackageReference ref = null;
141: String rest = getFullName();
142: if (rest.indexOf(".") > 0) {
143: rest = rest.substring(0, rest.lastIndexOf(".") + 1);
144: while (rest.indexOf(".") > 0) {
145: String name = rest.substring(0, rest.indexOf("."));
146: rest = rest.substring(rest.indexOf(".") + 1);
147: ref = new PackageReference(
148: new ProgramElementName(name), ref);
149: }
150: }
151: return ref;
152: }
153:
154: public static final class LexicographicalKeYJavaTypeOrder implements
155: Comparator {
156: public int compare(Object arg0, Object arg1) {
157: assert arg0 instanceof KeYJavaType
158: && arg1 instanceof KeYJavaType;
159: return ((KeYJavaType) arg0).getFullName().compareTo(
160: ((KeYJavaType) arg1).getFullName());
161: }
162: }
163: }
|