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: import de.uka.ilkd.key.logic.Namespace;
015: import de.uka.ilkd.key.logic.op.*;
016: import de.uka.ilkd.key.util.Debug;
017:
018: public abstract class AbstractSort implements Sort, SortDefiningSymbols {
019:
020: public static final Name OBJECT_REPOSITORY_NAME = new Name("<get>");
021:
022: /** name of the Sort */
023: protected Name name;
024:
025: /**
026: * equality symbol for this sort
027: */
028: protected final Equality equality = Op.EQUALS;
029:
030: /**
031: * cast symbol casting any sort to <em>this</em> one
032: */
033: private CastFunctionSymbol castSymbol;
034:
035: protected MapFromNameToSortDependingSymbol definedSymbols = MapAsListFromNameToSortDependingSymbol.EMPTY_MAP;
036:
037: protected boolean symbolsCreated = false;
038:
039: /** creates a Sort (with a new equality symbol for this sort) */
040: public AbstractSort(Name name) {
041: this .name = name;
042: }
043:
044: /**
045: * @return the sorts of the successors of this sort
046: */
047: public abstract SetOfSort extendsSorts();
048:
049: /**
050: * returns true iff given sort is a part of the transitive closure of the
051: * supersorts of this sort. One might optimize by hashing %%
052: */
053: public boolean extendsTrans(Sort sort) {
054: if (sort == this || sort == Sort.ANY) {
055: return true;
056: }
057:
058: if (!(sort instanceof ObjectSort || sort instanceof GenericSort)) {
059: return false;
060: }
061:
062: if (sort instanceof IntersectionSort) {
063: final IntersectionSort intersect = (IntersectionSort) sort;
064: for (int i = 0, sz = intersect.memberCount(); i < sz; i++) {
065: final Sort s = intersect.getComponent(i);
066: Debug.assertTrue(s != null);
067: if (!this .extendsTrans(s)) {
068: return false;
069: }
070: }
071: return true;
072: } else {
073: final IteratorOfSort it = extendsSorts().iterator();
074: while (it.hasNext()) {
075: final Sort s = it.next();
076: assert s != null;
077: if (s == sort || s.extendsTrans(sort)) {
078: return true;
079: }
080: }
081: }
082: return false;
083: }
084:
085: /** @return name of the Sort as String */
086: public Name name() {
087: return name;
088: }
089:
090: /** @return equality symbol of this sort */
091: public Equality getEqualitySymbol() {
092: return (this == Sort.FORMULA ? Op.EQV : equality);
093: }
094:
095: /**
096: * returns the cast symbol of this Sort
097: *
098: * @return the cast function of this sort
099: * @throws IllegalStateException
100: * if the symbols have not been created yet
101: */
102: public CastFunctionSymbol getCastSymbol() {
103: if (castSymbol == null) {
104: throw new IllegalStateException(this + ":"
105: + "Symbols have to be created before "
106: + "trying to access a sort depending function.");
107: }
108: return castSymbol;
109: }
110:
111: /**
112: * This method returns a cast into this sort.
113: */
114: private SortDependingSymbol createCastSymbol(Namespace sort_ns) {
115: Debug.assertTrue(castSymbol == null);
116: castSymbol = new CastFunctionSymbol(Sort.ANY, this );
117: return castSymbol;
118: }
119:
120: /**
121: * Creates the functions depening on this sort and adds them to the functions
122: * namespace. If the functions have been already created nothing is done.
123: */
124: protected void createSymbols(Namespace p_func_ns, Namespace sort_ns) {
125: if (!symbolsCreated) {
126: final Sort booleanSort = (Sort) sort_ns.lookup(new Name(
127: "boolean"));
128: final Sort intSort = (Sort) sort_ns.lookup(new Name("int"));
129: if (booleanSort == null || intSort == null) {
130: return; //create symbols later
131: }
132: ListOfSortDependingSymbol l0 = SLListOfSortDependingSymbol.EMPTY_LIST;
133: l0 = l0.prepend(createCastSymbol(sort_ns)).prepend(
134: new InstanceofSymbol(this , booleanSort)).prepend(
135: new ExactInstanceSymbol(this , booleanSort))
136: .prepend(
137: new InstanceofSymbol(new Name("contains"),
138: this ));
139:
140: /**
141: * this is a hack. Solution: Create a class Signature which is repsobsible to
142: * build the required sort depending functions after all sorts have been read.
143: */
144: if (!(this instanceof NullSort)
145: && (this instanceof ArraySort
146: || this instanceof GenericSort || (this instanceof ClassInstanceSortImpl && !((ClassInstanceSort) this )
147: .representAbstractClassOrInterface()))) {
148: l0 = l0.prepend(createInstanceRepository(intSort));
149: }
150:
151: addSymbols(l0);
152: symbolsCreated = true;
153: }
154: }
155:
156: private SortDependingFunction createInstanceRepository(
157: Sort integerSort) {
158: return new SortDependingFunction(new Name(this .name.toString()
159: + "::" + OBJECT_REPOSITORY_NAME.toString()), this ,
160: new Sort[] { integerSort }, OBJECT_REPOSITORY_NAME,
161: this );
162: }
163:
164: /**
165: * Lookup the symbol of kind "p_name", which is a sort independent
166: * identifier for this symbol
167: *
168: * @return Symbol with (kind) name "p_name"
169: * ("ret.getKind().equals(p_name)"), null if no such object exists
170: */
171: public SortDependingSymbol lookupSymbol(Name p_name) {
172: return definedSymbols.get(p_name);
173: }
174:
175: protected void addSymbols(ListOfSortDependingSymbol p) {
176: final IteratorOfSortDependingSymbol it = p.iterator();
177: while (it.hasNext()) {
178: final SortDependingSymbol s = it.next();
179: definedSymbols = definedSymbols.put(s.getKind(), s);
180: }
181: }
182:
183: /**
184: * Adds the sort depending functions to the given function namespace if
185: * possible. Functions are created if not already done
186: */
187: public void addDefinedSymbols(Namespace functions, Namespace sorts) {
188: if (!symbolsCreated) {
189: createSymbols(functions, sorts);
190: }
191: final IteratorOfSortDependingSymbol it = definedSymbols
192: .valueIterator();
193: while (it.hasNext()) {
194: final SortDependingSymbol sds = it.next();
195: //if (functions.lookup(sds.name()) == null) {
196: functions.add(sds);
197: //}
198: }
199: }
200:
201: public String toString() {
202: return name().toString();
203: }
204: }
|