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: package de.uka.ilkd.key.parser.ocl;
009:
010: import de.uka.ilkd.key.logic.Term;
011: import de.uka.ilkd.key.logic.TermFactory;
012: import de.uka.ilkd.key.logic.op.Function;
013: import de.uka.ilkd.key.logic.op.LogicVariable;
014: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
015: import de.uka.ilkd.key.logic.sort.SequenceSort;
016: import de.uka.ilkd.key.logic.sort.Sort;
017: import de.uka.ilkd.key.util.Debug;
018:
019: class OCLFunctionalCollection {
020:
021: private static final TermFactory tf = TermFactory.DEFAULT;
022: private static final FunctionFactory funcFactory = FunctionFactory.INSTANCE;
023: private final Term restriction;
024:
025: private final int collectionType;
026:
027: /**
028: * Creates a collection of Type <b>collectionType</b> which contains
029: * all values of a sort which satisfy some restriction. (functional)
030: */
031: protected OCLFunctionalCollection(Term restriction,
032: int collectionType) {
033: this .restriction = restriction;
034: this .collectionType = collectionType;
035: }
036:
037: /**
038: * Creates an empty collection.
039: */
040: protected OCLFunctionalCollection() {
041: this (OCLCollection.OCL_SET);
042: }
043:
044: /**
045: * Creates an empty collection.
046: */
047: protected OCLFunctionalCollection(int collectionType) {
048: this .restriction = tf.createFunctionTerm(funcFactory
049: .getEmptySet(Sort.ANY));
050: this .collectionType = collectionType;
051: }
052:
053: /**
054: * Creates a collection which contains all values of a sort.
055: */
056: protected OCLFunctionalCollection(Sort sort, int collectionType) {
057: this .restriction = tf.createFunctionTerm(funcFactory
058: .createAllInstancesConstant(sort));
059: this .collectionType = collectionType;
060: }
061:
062: /**
063: * Creates a collection which contains all values of a sort.
064: */
065: protected OCLFunctionalCollection(Sort sort) {
066: this (sort, OCLCollection.OCL_SET);
067: }
068:
069: /**
070: * Creates a collection which contains a single element.
071: * @throws OCLTranslationError
072: */
073: protected OCLFunctionalCollection(int collectionType, Term element)
074: throws OCLTranslationError {
075: this .restriction = funcFactory.including(tf
076: .createFunctionTerm(funcFactory.getEmptySet(element
077: .sort())), element);
078: this .collectionType = collectionType;
079: }
080:
081: /**
082: * Creates a collection which contains a single element.
083: * @throws OCLTranslationError
084: */
085: protected OCLFunctionalCollection(Term element)
086: throws OCLTranslationError {
087: this (OCLCollection.OCL_SET, element);
088: }
089:
090: /**
091: * Creates a collection which contains all integers between a lower and
092: * an upper bound (described by terms of sort int).
093: * @throws OCLTranslationError
094: */
095: protected OCLFunctionalCollection(Term lowerBound, Term upperBound,
096: Function leq, int collectionType)
097: throws OCLTranslationError {
098: switch (collectionType) {
099: case OCLCollection.OCL_SET:
100: this .restriction = funcFactory.createRangedSet(lowerBound,
101: upperBound, leq);
102: break;
103: case OCLCollection.OCL_BAG:
104: this .restriction = funcFactory.createRangedBag(lowerBound,
105: upperBound, leq);
106: break;
107: case OCLCollection.OCL_SEQUENCE:
108: this .restriction = funcFactory.createRangedSequence(
109: lowerBound, upperBound, leq);
110: break;
111: default:
112: this .restriction = funcFactory.createRangedSet(lowerBound,
113: upperBound, leq);
114: }
115: this .collectionType = collectionType;
116: }
117:
118: /**
119: * Creates a collection which contains all integers between a lower and
120: * an upper bound (described by terms of sort int).
121: * @throws OCLTranslationError
122: */
123: protected OCLFunctionalCollection(Term lowerBound, Term upperBound,
124: Function leq) throws OCLTranslationError {
125: this (lowerBound, upperBound, leq, OCLCollection.OCL_SET);
126: }
127:
128: /**
129: * Creates a collection which contains all values reachable from a receiver
130: * term by applying an association with multiplicity > 1 (described by an
131: * association-function).
132: */
133: protected OCLFunctionalCollection(Term recTerm, Function assocFunc) {
134: Debug.assertTrue(assocFunc != null);
135: Debug.assertTrue(assocFunc.arity() == 1);
136: Debug.assertTrue(assocFunc.argSort(0) == recTerm.sort());
137: this .restriction = tf.createFunctionTerm(assocFunc, recTerm);
138: this .collectionType = (assocFunc.sort() instanceof SequenceSort) ? OCLCollection.OCL_SEQUENCE
139: : OCLCollection.OCL_SET;
140: }
141:
142: public Term getRestriction() {
143: return restriction;
144: }
145:
146: protected int getCollectionType() {
147: return collectionType;
148: }
149:
150: public boolean isSet() {
151: return collectionType == OCLCollection.OCL_SET;
152: }
153:
154: public boolean isBag() {
155: return collectionType == OCLCollection.OCL_BAG;
156: }
157:
158: public boolean isSequence() {
159: return collectionType == OCLCollection.OCL_SEQUENCE;
160: }
161:
162: public String toString() {
163: return "(all elements of " + restriction.sort() + " in "
164: + restriction + ")";
165: }
166:
167: /**
168: * Creates a collection which is the union of this one and another one.
169: * @throws OCLTranslationError
170: */
171: protected OCLFunctionalCollection union(OCLCollection c)
172: throws OCLTranslationError {
173: return new OCLFunctionalCollection(funcFactory
174: .unionAndSimplify(this .restriction, c
175: .getFunctionalRestriction()),
176: this .collectionType);
177: }
178:
179: /**
180: * Creates a functional description of a collection which is produced by
181: * e->collect(b)
182: *
183: * @param collectTerm b
184: * @return new functional description of the appropriate collection
185: * @throws OCLTranslationError
186: */
187: public OCLFunctionalCollection collect(Term collectTerm)
188: throws OCLTranslationError {
189:
190: // is this right?
191: // or are there any collect-expressions which don't have the collectorVar as first subterm?
192: LogicVariable collectVar = (LogicVariable) collectTerm.sub(0)
193: .freeVars().toArray()[0];
194:
195: Function f = funcFactory.createCollectFunction(collectVar,
196: collectTerm, this .collectionType);
197:
198: SetOfQuantifiableVariable vars = collectTerm.freeVars();
199: vars = vars.remove(collectVar);
200:
201: Term[] params = new Term[vars.size() + 1];
202:
203: params[0] = this .restriction;
204:
205: for (int i = 0; i < vars.size(); i++) {
206: params[i + 1] = tf.createVariableTerm((LogicVariable) vars
207: .toArray()[i]);
208: }
209:
210: Term restriction = tf.createFunctionTerm(f, params);
211:
212: int collectionType = (this .collectionType == OCLCollection.OCL_SEQUENCE) ? OCLCollection.OCL_SEQUENCE
213: : OCLCollection.OCL_BAG;
214:
215: return new OCLFunctionalCollection(restriction, collectionType);
216: }
217:
218: /**
219: * Creates a functional description of a collection which is produced by
220: * e->select(x | b)
221: *
222: * @param selectVar x
223: * @param selectTerm b
224: * @return new functional description of the appropriate collection
225: * @throws OCLTranslationError
226: */
227: public OCLFunctionalCollection select(LogicVariable selectVar,
228: Term selectTerm) throws OCLTranslationError {
229:
230: Function f = funcFactory.createSelectFunction(selectVar,
231: selectTerm, this .collectionType);
232:
233: SetOfQuantifiableVariable vars = selectTerm.freeVars();
234: vars = vars.remove(selectVar);
235:
236: Term[] params = new Term[vars.size() + 1];
237:
238: params[0] = this .restriction;
239:
240: for (int i = 0; i < vars.size(); i++) {
241: params[i + 1] = tf.createVariableTerm((LogicVariable) vars
242: .toArray()[i]);
243: }
244:
245: Term restriction = tf.createFunctionTerm(f, params);
246:
247: return new OCLFunctionalCollection(restriction,
248: this.collectionType);
249: }
250:
251: }
|