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.rule.inst;
012:
013: import junit.framework.TestCase;
014: import de.uka.ilkd.key.logic.Name;
015: import de.uka.ilkd.key.logic.TermFactory;
016: import de.uka.ilkd.key.logic.sort.*;
017: import de.uka.ilkd.key.rule.TacletForTests;
018:
019: public class TestGenericSortInstantiations extends TestCase {
020:
021: TermFactory tf = TermFactory.DEFAULT;
022: static final SetOfSort emptySortSet = SetAsListOfSort.EMPTY_SET;
023:
024: /**
025: *
026: * A4
027: * |
028: * A3
029: * / \
030: * A6 A1 A2
031: * \ |
032: * A5
033: *
034: *
035: * B4
036: * / \
037: * B2 B3
038: * / \ /
039: * B5 B1
040: *
041: *
042: * D4 (the same with array sorts)
043: * / \
044: * D2 D3
045: * / \ /
046: * D5 D1
047: *
048: *
049: * G3
050: * / \
051: * G1 G2
052: * |
053: * G4
054: *
055: *
056: * A3
057: * H1 /
058: * / \ /
059: * H2 H3
060: * |
061: * H4
062: *
063: * H2 oneof { A2, A3 }
064: */
065:
066: {
067: // this ensures that necessary Java types are loaded
068: TacletForTests.services().getJavaInfo().readJavaBlock("{}");
069: }
070:
071: Sort object = TacletForTests.services().getJavaInfo()
072: .getJavaLangObjectAsSort();
073: Sort cloneable = TacletForTests.services().getJavaInfo()
074: .getJavaLangCloneableAsSort();
075: Sort serializable = TacletForTests.services().getJavaInfo()
076: .getJavaIoSerializableAsSort();
077:
078: Sort objectArray = ArraySortImpl.getArraySort(object, object,
079: cloneable, serializable);
080: // these sorts are supposed to have no relations to other (object) sorts;
081: // probably in this place primitive sorts should be used, but these sorts
082: // do currently not support sort hierarchies
083: ObjectSort A4 = new ClassInstanceSortImpl(new Name("A4"),
084: emptySortSet, false);
085: ObjectSort A3 = new ClassInstanceSortImpl(new Name("A3"),
086: emptySortSet.add(A4), false);
087: ObjectSort A1 = new ClassInstanceSortImpl(new Name("A1"),
088: emptySortSet.add(A3), false);
089: ObjectSort A2 = new ClassInstanceSortImpl(new Name("A2"),
090: emptySortSet.add(A3), false);
091: ObjectSort A6 = new ClassInstanceSortImpl(new Name("A6"),
092: emptySortSet, false);
093: ObjectSort A5 = new ClassInstanceSortImpl(new Name("A5"),
094: emptySortSet.add(A1).add(A6), false);
095:
096: ObjectSort B4 = new ClassInstanceSortImpl(new Name("B4"),
097: emptySortSet.add(object), false);
098: ObjectSort B2 = new ClassInstanceSortImpl(new Name("B2"),
099: emptySortSet.add(B4), false);
100: ObjectSort B3 = new ClassInstanceSortImpl(new Name("B3"),
101: emptySortSet.add(B4), false);
102: ObjectSort B1 = new ClassInstanceSortImpl(new Name("B1"),
103: emptySortSet.add(B2).add(B3), false);
104: ObjectSort B5 = new ClassInstanceSortImpl(new Name("B5"),
105: emptySortSet.add(B2), false);
106:
107: // This setup resembles the code of <code>Recoder2KeY</code>
108: ObjectSort D4 = ArraySortImpl.getArraySort(B4, object, cloneable,
109: serializable);
110: ObjectSort D2 = ArraySortImpl.getArraySort(B2, object, cloneable,
111: serializable);
112: ObjectSort D3 = ArraySortImpl.getArraySort(B3, object, cloneable,
113: serializable);
114: ObjectSort D1 = ArraySortImpl.getArraySort(B1, object, cloneable,
115: serializable);
116: ObjectSort D5 = ArraySortImpl.getArraySort(B5, object, cloneable,
117: serializable);
118:
119: Sort C1 = new PrimitiveSort(new Name("C1"));
120:
121: GenericSort G3;
122: GenericSort G1;
123: GenericSort G2;
124: GenericSort G4;
125:
126: GenericSort H1;
127: GenericSort H2;
128: GenericSort H3;
129: GenericSort H4;
130:
131: /*
132: Function fa1 = new Function ( new Name ( "fa1" ), A1, new Sort [0] );
133: Term a1 = tf.createFunctionTerm ( fa1 );
134: Function fa2 = new Function ( new Name ( "fa2" ), A2, new Sort [0] );
135: Term a2 = tf.createFunctionTerm ( fa2 );
136: Function fa3 = new Function ( new Name ( "fa3" ), A3, new Sort [0] );
137: Term a3 = tf.createFunctionTerm ( fa3 );
138: Function fa4 = new Function ( new Name ( "fa4" ), A4, new Sort [0] );
139: Term a4 = tf.createFunctionTerm ( fa4 );
140: Function fa5 = new Function ( new Name ( "fa5" ), A5, new Sort [0] );
141: Term a5 = tf.createFunctionTerm ( fa5 );
142: Function fa6 = new Function ( new Name ( "fa6" ), A6, new Sort [0] );
143: Term a6 = tf.createFunctionTerm ( fa6 );
144:
145: Function fb1 = new Function ( new Name ( "fb1" ), B1, new Sort [0] );
146: Term b1 = tf.createFunctionTerm ( fb1 );
147: Function fb2 = new Function ( new Name ( "fb2" ), B2, new Sort [0] );
148: Term b2 = tf.createFunctionTerm ( fb2 );
149: Function fb3 = new Function ( new Name ( "fb3" ), B3, new Sort [0] );
150: Term b3 = tf.createFunctionTerm ( fb3 );
151: Function fb4 = new Function ( new Name ( "fb4" ), B4, new Sort [0] );
152: Term b4 = tf.createFunctionTerm ( fb4 );
153: Function fb5 = new Function ( new Name ( "fb5" ), B5, new Sort [0] );
154: Term b5 = tf.createFunctionTerm ( fb5 );
155:
156:
157: SchemaVariable svg1 = SchemaVariableFactory.createTermSV ( new Name ( "svg1" ), G1 );
158: SchemaVariable svg1b = SchemaVariableFactory.createTermSV ( new Name ( "svg1b" ), G1 );
159: SchemaVariable svg1c = SchemaVariableFactory.createTermSV ( new Name ( "svg1c" ), G1 );
160: SchemaVariable svg2 = SchemaVariableFactory.createTermSV ( new Name ( "svg2" ), G2 );
161: SchemaVariable svg2b = SchemaVariableFactory.createTermSV ( new Name ( "svg2b" ), G2 );
162: SchemaVariable svg3 = SchemaVariableFactory.createTermSV ( new Name ( "svg3" ), G3 );
163: SchemaVariable svg4 = SchemaVariableFactory.createTermSV ( new Name ( "svg4" ), G4 );
164:
165:
166: SchemaVariable sva4 = SchemaVariableFactory.createTermSV ( new Name ( "sva4" ), A4 );
167: */
168:
169: public TestGenericSortInstantiations(String name)
170: throws GenericSupersortException {
171: super (name);
172:
173: G3 = new GenericSort(new Name("G3"));
174: G1 = new GenericSort(new Name("G1"), emptySortSet.add(G3),
175: emptySortSet);
176: G2 = new GenericSort(new Name("G2"), emptySortSet.add(G3),
177: emptySortSet);
178: G4 = new GenericSort(new Name("G4"), emptySortSet.add(G1),
179: emptySortSet);
180:
181: H1 = new GenericSort(new Name("H1"));
182: H2 = new GenericSort(new Name("H2"), emptySortSet.add(H1),
183: emptySortSet.add(A2).add(A3));
184: H3 = new GenericSort(new Name("H3"), emptySortSet.add(A3).add(
185: H1), emptySortSet);
186: H4 = new GenericSort(new Name("H4"), emptySortSet.add(H3),
187: emptySortSet);
188: }
189:
190: public static ListOfGenericSort sorts(
191: ListOfGenericSortCondition p_conditions) {
192: IteratorOfGenericSortCondition it = p_conditions.iterator();
193: ListOfGenericSort res = SLListOfGenericSort.EMPTY_LIST;
194:
195: while (it.hasNext())
196: res = res.prepend(it.next().getGenericSort());
197:
198: return res;
199: }
200:
201: /*
202: public void testGeneric0 () {
203: SVInstantiations svi = SVInstantiations.EMPTY_SVINSTANTIATIONS;
204: svi = svi.add ( sva4, a4 );
205:
206: assertTrue ( "Instantiations should be equal",
207: gsi ==
208: GenericSortInstantiations.EMPTY_INSTANTIATIONS );
209: }
210: */
211:
212: public void testGeneric1() {
213: ListOfGenericSortCondition cs;
214: GenericSortInstantiations gsi;
215:
216: cs = SLListOfGenericSortCondition.EMPTY_LIST;
217: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
218: G1, A4));
219:
220: gsi = GenericSortInstantiations.create(sorts(cs), cs);
221: assertEquals(
222: "Instantiations should be equal",
223: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
224: .put(G1, A4), gsi.getAllInstantiations());
225:
226: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
227: G1, A3));
228:
229: gsi = GenericSortInstantiations.create(sorts(cs), cs);
230: assertEquals(
231: "Instantiations should be equal",
232: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
233: .put(G1, A4), gsi.getAllInstantiations());
234:
235: cs = SLListOfGenericSortCondition.EMPTY_LIST;
236: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
237: G1, A1));
238: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
239: G1, A2));
240:
241: gsi = GenericSortInstantiations.create(sorts(cs), cs);
242: assertEquals(
243: "Instantiations should be equal",
244: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
245: .put(G1, A3), gsi.getAllInstantiations());
246:
247: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
248: G1, A4));
249:
250: gsi = GenericSortInstantiations.create(sorts(cs), cs);
251: assertEquals(
252: "Instantiations should be equal",
253: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
254: .put(G1, A4), gsi.getAllInstantiations());
255:
256: cs = SLListOfGenericSortCondition.EMPTY_LIST;
257: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
258: G1, A1));
259: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
260: G1, A6));
261:
262: try {
263: gsi = GenericSortInstantiations.create(sorts(cs), cs);
264: fail("Expected GenericSortException");
265: } catch (GenericSortException e) {
266: }
267:
268: cs = SLListOfGenericSortCondition.EMPTY_LIST;
269: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
270: G1, B1));
271: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
272: G1, B5));
273:
274: gsi = GenericSortInstantiations.create(sorts(cs), cs);
275: assertEquals(
276: "Instantiations should be equal",
277: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
278: .put(G1, B2), gsi.getAllInstantiations());
279: }
280:
281: public void testGeneric2() {
282: ListOfGenericSortCondition cs;
283: GenericSortInstantiations gsi;
284:
285: cs = SLListOfGenericSortCondition.EMPTY_LIST;
286: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
287: G1, A1));
288: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
289: G2, A2));
290:
291: gsi = GenericSortInstantiations.create(sorts(cs), cs);
292: assertEquals(
293: "Instantiations should be equal",
294: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
295: .put(G1, A1).put(G2, A2), gsi
296: .getAllInstantiations());
297:
298: cs = SLListOfGenericSortCondition.EMPTY_LIST;
299: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
300: G1, A1));
301: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
302: G2, B3));
303:
304: gsi = GenericSortInstantiations.create(sorts(cs), cs);
305: assertEquals(
306: "Instantiations should be equal",
307: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
308: .put(G1, A1).put(G2, B3), gsi
309: .getAllInstantiations());
310:
311: cs = SLListOfGenericSortCondition.EMPTY_LIST;
312: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
313: G1, A1));
314: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
315: G1, A2));
316: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
317: G2, B3));
318: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
319: G2, B5));
320:
321: gsi = GenericSortInstantiations.create(sorts(cs), cs);
322: assertEquals(
323: "Instantiations should be equal",
324: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
325: .put(G1, A3).put(G2, B4), gsi
326: .getAllInstantiations());
327:
328: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
329: G4, A5));
330:
331: gsi = GenericSortInstantiations.create(sorts(cs), cs);
332: assertEquals(
333: "Instantiations should be equal",
334: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
335: .put(G1, A3).put(G2, B4).put(G4, A5), gsi
336: .getAllInstantiations());
337:
338: cs = cs.tail();
339: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
340: G4, A4));
341:
342: gsi = GenericSortInstantiations.create(sorts(cs), cs);
343: assertEquals(
344: "Instantiations should be equal",
345: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
346: .put(G1, A4).put(G2, B4).put(G4, A4), gsi
347: .getAllInstantiations());
348:
349: cs = cs.tail();
350: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
351: G4, B1));
352:
353: try {
354: gsi = GenericSortInstantiations.create(sorts(cs), cs);
355: fail("Expected GenericSortException");
356: } catch (GenericSortException e) {
357: }
358: }
359:
360: public void testGeneric2Array() {
361: ListOfGenericSortCondition cs;
362: GenericSortInstantiations gsi;
363:
364: cs = SLListOfGenericSortCondition.EMPTY_LIST;
365: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
366: G1, A1));
367: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
368: G2, A2));
369:
370: gsi = GenericSortInstantiations.create(sorts(cs), cs);
371: assertEquals(
372: "Instantiations should be equal",
373: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
374: .put(G1, A1).put(G2, A2), gsi
375: .getAllInstantiations());
376:
377: cs = SLListOfGenericSortCondition.EMPTY_LIST;
378: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
379: G1, A1));
380: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
381: G2, D3));
382:
383: gsi = GenericSortInstantiations.create(sorts(cs), cs);
384: assertEquals(
385: "Instantiations should be equal",
386: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
387: .put(G1, A1).put(G2, D3), gsi
388: .getAllInstantiations());
389:
390: cs = SLListOfGenericSortCondition.EMPTY_LIST;
391: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
392: G1, A1));
393: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
394: G1, A2));
395: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
396: G2, D3));
397: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
398: G2, D5));
399:
400: gsi = GenericSortInstantiations.create(sorts(cs), cs);
401: assertEquals(
402: "Instantiations should be equal",
403: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
404: .put(G1, A3).put(G2, D4), gsi
405: .getAllInstantiations());
406:
407: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
408: G4, A5));
409:
410: gsi = GenericSortInstantiations.create(sorts(cs), cs);
411: assertEquals(
412: "Instantiations should be equal",
413: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
414: .put(G1, A3).put(G2, D4).put(G4, A5), gsi
415: .getAllInstantiations());
416:
417: cs = cs.tail();
418: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
419: G4, A4));
420:
421: gsi = GenericSortInstantiations.create(sorts(cs), cs);
422: assertEquals(
423: "Instantiations should be equal",
424: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
425: .put(G1, A4).put(G2, D4).put(G4, A4), gsi
426: .getAllInstantiations());
427:
428: cs = cs.tail();
429: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
430: G4, D1));
431:
432: try {
433: gsi = GenericSortInstantiations.create(sorts(cs), cs);
434: fail("Expected GenericSortException");
435: } catch (GenericSortException e) {
436: }
437: }
438:
439: public void testGeneric3() {
440: ListOfGenericSortCondition cs;
441: GenericSortInstantiations gsi;
442:
443: cs = SLListOfGenericSortCondition.EMPTY_LIST;
444: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
445: G1, A1));
446: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
447: G2, A2));
448: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
449: G3, A5));
450:
451: gsi = GenericSortInstantiations.create(sorts(cs), cs);
452: assertEquals(
453: "Instantiations should be equal",
454: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
455: .put(G1, A1).put(G2, A2).put(G3, A3), gsi
456: .getAllInstantiations());
457:
458: cs = SLListOfGenericSortCondition.EMPTY_LIST;
459: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
460: G1, A5));
461: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
462: G2, A2));
463: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
464: G3, A5));
465:
466: gsi = GenericSortInstantiations.create(sorts(cs), cs);
467: assertEquals(
468: "Instantiations should be equal",
469: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
470: .put(G1, A5).put(G2, A2).put(G3, A3), gsi
471: .getAllInstantiations());
472:
473: cs = SLListOfGenericSortCondition.EMPTY_LIST;
474: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
475: G1, A5));
476: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
477: G2, A2));
478: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
479: G3, A5));
480: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
481: G4, A1));
482:
483: gsi = GenericSortInstantiations.create(sorts(cs), cs);
484: assertEquals(
485: "Instantiations should be equal",
486: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
487: .put(G1, A1).put(G2, A2).put(G3, A3)
488: .put(G4, A1), gsi.getAllInstantiations());
489:
490: cs = SLListOfGenericSortCondition.EMPTY_LIST;
491: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
492: G1, A5));
493: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
494: G2, A2));
495: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
496: G3, A5));
497: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
498: G4, B1));
499:
500: try {
501: gsi = GenericSortInstantiations.create(sorts(cs), cs);
502: fail("Expected GenericSortException");
503: } catch (GenericSortException e) {
504: }
505:
506: cs = SLListOfGenericSortCondition.EMPTY_LIST;
507: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
508: G1, A2));
509: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
510: G2, B2));
511: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
512: G4, A5));
513:
514: gsi = GenericSortInstantiations.create(sorts(cs), cs);
515: assertEquals(
516: "Instantiations should be equal",
517: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
518: .put(G1, A3).put(G2, B2).put(G4, A5), gsi
519: .getAllInstantiations());
520: }
521:
522: public void testGeneric4() {
523: ListOfGenericSortCondition cs;
524: GenericSortInstantiations gsi;
525:
526: cs = SLListOfGenericSortCondition.EMPTY_LIST;
527: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
528: G1, A4));
529:
530: gsi = GenericSortInstantiations.create(sorts(cs), cs);
531: assertEquals(
532: "Instantiations should be equal",
533: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
534: .put(G1, A4), gsi.getAllInstantiations());
535:
536: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
537: G1, A3));
538:
539: gsi = GenericSortInstantiations.create(sorts(cs), cs);
540: assertEquals(
541: "Instantiations should be equal",
542: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
543: .put(G1, A4), gsi.getAllInstantiations());
544:
545: cs = SLListOfGenericSortCondition.EMPTY_LIST;
546: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
547: G1, A1));
548: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
549: G1, A2));
550:
551: try {
552: gsi = GenericSortInstantiations.create(sorts(cs), cs);
553: fail("Expected GenericSortException");
554: } catch (GenericSortException e) {
555: }
556:
557: cs = SLListOfGenericSortCondition.EMPTY_LIST;
558: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
559: G1, A1));
560: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
561: G1, A2));
562:
563: try {
564: gsi = GenericSortInstantiations.create(sorts(cs), cs);
565: fail("Expected GenericSortException");
566: } catch (GenericSortException e) {
567: }
568:
569: cs = SLListOfGenericSortCondition.EMPTY_LIST;
570: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
571: H2, A3));
572:
573: gsi = GenericSortInstantiations.create(sorts(cs), cs);
574: assertEquals(
575: "Instantiations should be equal",
576: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
577: .put(H2, A3), gsi.getAllInstantiations());
578:
579: cs = SLListOfGenericSortCondition.EMPTY_LIST;
580: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
581: H2, A5));
582:
583: gsi = GenericSortInstantiations.create(sorts(cs), cs);
584: assertEquals(
585: "Instantiations should be equal",
586: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
587: .put(H2, A3), gsi.getAllInstantiations());
588:
589: cs = SLListOfGenericSortCondition.EMPTY_LIST;
590: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
591: H2, A4));
592:
593: try {
594: gsi = GenericSortInstantiations.create(sorts(cs), cs);
595: fail("Expected GenericSortException");
596: } catch (GenericSortException e) {
597: }
598:
599: cs = SLListOfGenericSortCondition.EMPTY_LIST;
600: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
601: H3, A1));
602:
603: gsi = GenericSortInstantiations.create(sorts(cs), cs);
604: assertEquals(
605: "Instantiations should be equal",
606: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
607: .put(H3, A1), gsi.getAllInstantiations());
608:
609: cs = SLListOfGenericSortCondition.EMPTY_LIST;
610: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
611: H3, A1));
612:
613: gsi = GenericSortInstantiations.create(sorts(cs), cs);
614: assertEquals(
615: "Instantiations should be equal",
616: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
617: .put(H3, A1), gsi.getAllInstantiations());
618:
619: cs = SLListOfGenericSortCondition.EMPTY_LIST;
620: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
621: H3, A6));
622:
623: try {
624: gsi = GenericSortInstantiations.create(sorts(cs), cs);
625: fail("Expected GenericSortException");
626: } catch (GenericSortException e) {
627: }
628:
629: }
630:
631: public void testGeneric5() {
632: ListOfGenericSortCondition cs;
633: GenericSortInstantiations gsi;
634:
635: cs = SLListOfGenericSortCondition.EMPTY_LIST;
636: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
637: H1, A4));
638: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
639: H2, A3));
640:
641: gsi = GenericSortInstantiations.create(sorts(cs), cs);
642: assertEquals(
643: "Instantiations should be equal",
644: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
645: .put(H1, A4).put(H2, A3), gsi
646: .getAllInstantiations());
647:
648: cs = SLListOfGenericSortCondition.EMPTY_LIST;
649: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
650: H1, A6));
651: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
652: H2, A5));
653:
654: try {
655: gsi = GenericSortInstantiations.create(sorts(cs), cs);
656: fail("Expected GenericSortException");
657: } catch (GenericSortException e) {
658: }
659:
660: cs = SLListOfGenericSortCondition.EMPTY_LIST;
661: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
662: H1, A2));
663: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
664: H2, A5));
665:
666: gsi = GenericSortInstantiations.create(sorts(cs), cs);
667: assertEquals(
668: "Instantiations should be equal",
669: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
670: .put(H1, A3).put(H2, A3), gsi
671: .getAllInstantiations());
672:
673: cs = SLListOfGenericSortCondition.EMPTY_LIST;
674: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
675: H1, A2));
676: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
677: H3, A5));
678:
679: gsi = GenericSortInstantiations.create(sorts(cs), cs);
680: assertEquals(
681: "Instantiations should be equal",
682: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
683: .put(H1, A3).put(H3, A5), gsi
684: .getAllInstantiations());
685:
686: cs = SLListOfGenericSortCondition.EMPTY_LIST;
687: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
688: H1, A2));
689: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
690: H3, A5));
691:
692: try {
693: gsi = GenericSortInstantiations.create(sorts(cs), cs);
694: fail("Expected GenericSortException");
695: } catch (GenericSortException e) {
696: }
697:
698: cs = SLListOfGenericSortCondition.EMPTY_LIST;
699: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
700: H4, A6));
701:
702: try {
703: gsi = GenericSortInstantiations.create(sorts(cs), cs);
704: fail("Expected GenericSortException");
705: } catch (GenericSortException e) {
706: }
707:
708: }
709:
710: public void testGeneric6() {
711: ListOfGenericSortCondition cs;
712: GenericSortInstantiations gsi;
713:
714: cs = SLListOfGenericSortCondition.EMPTY_LIST;
715: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
716: G1, A4));
717: cs = cs.prepend(GenericSortCondition
718: .createForceInstantiationCondition(G4, true));
719: cs = cs.prepend(GenericSortCondition
720: .createForceInstantiationCondition(G3, false));
721:
722: gsi = GenericSortInstantiations.create(sorts(cs), cs);
723: assertEquals(
724: "Instantiations should be equal",
725: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
726: .put(G1, A4).put(G4, A4).put(G3, A4), gsi
727: .getAllInstantiations());
728:
729: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
730: G1, A3));
731:
732: gsi = GenericSortInstantiations.create(sorts(cs), cs);
733: assertEquals(
734: "Instantiations should be equal",
735: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
736: .put(G1, A4).put(G4, A4).put(G3, A4), gsi
737: .getAllInstantiations());
738:
739: cs = SLListOfGenericSortCondition.EMPTY_LIST;
740: cs = cs.prepend(GenericSortCondition.createIdentityCondition(
741: G1, A5));
742: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
743: G2, A2));
744: cs = cs.prepend(GenericSortCondition
745: .createForceInstantiationCondition(G3, false));
746:
747: gsi = GenericSortInstantiations.create(sorts(cs), cs);
748: assertEquals(
749: "Instantiations should be equal",
750: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
751: .put(G1, A5).put(G2, A2).put(G3, A3), gsi
752: .getAllInstantiations());
753:
754: cs = cs.prepend(GenericSortCondition
755: .createForceInstantiationCondition(G4, true));
756:
757: gsi = GenericSortInstantiations.create(sorts(cs), cs);
758: assertEquals(
759: "Instantiations should be equal",
760: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
761: .put(G1, A5).put(G2, A2).put(G3, A3)
762: .put(G4, A5), gsi.getAllInstantiations());
763:
764: cs = SLListOfGenericSortCondition.EMPTY_LIST;
765: cs = cs.prepend(GenericSortCondition
766: .createForceInstantiationCondition(H3, true));
767:
768: gsi = GenericSortInstantiations.create(sorts(cs), cs);
769: assertEquals(
770: "Instantiations should be equal",
771: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
772: .put(H3, A3), gsi.getAllInstantiations());
773:
774: }
775:
776: public void testNullsort() {
777: ListOfGenericSortCondition cs;
778: GenericSortInstantiations gsi;
779:
780: cs = SLListOfGenericSortCondition.EMPTY_LIST;
781: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
782: G1, A1));
783: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
784: G1, Sort.NULL));
785:
786: gsi = GenericSortInstantiations.create(sorts(cs), cs);
787: assertEquals(
788: "Instantiations should be equal",
789: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
790: .put(G1, A1), gsi.getAllInstantiations());
791:
792: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
793: G1, A2));
794:
795: gsi = GenericSortInstantiations.create(sorts(cs), cs);
796: assertEquals(
797: "Instantiations should be equal",
798: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
799: .put(G1, A3), gsi.getAllInstantiations());
800:
801: cs = SLListOfGenericSortCondition.EMPTY_LIST;
802: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
803: G1, Sort.NULL));
804: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
805: G1, A1));
806:
807: gsi = GenericSortInstantiations.create(sorts(cs), cs);
808: assertEquals(
809: "Instantiations should be equal",
810: ((MapFromGenericSortToSort) MapAsListFromGenericSortToSort.EMPTY_MAP)
811: .put(G1, A1), gsi.getAllInstantiations());
812:
813: cs = SLListOfGenericSortCondition.EMPTY_LIST;
814: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
815: G1, C1));
816: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
817: G1, Sort.NULL));
818:
819: try {
820: gsi = GenericSortInstantiations.create(sorts(cs), cs);
821: fail("Expected GenericSortException");
822: } catch (GenericSortException e) {
823: }
824:
825: cs = SLListOfGenericSortCondition.EMPTY_LIST;
826: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
827: G1, Sort.NULL));
828: cs = cs.prepend(GenericSortCondition.createSupersortCondition(
829: G1, C1));
830:
831: try {
832: gsi = GenericSortInstantiations.create(sorts(cs), cs);
833: fail("Expected GenericSortException");
834: } catch (GenericSortException e) {
835: }
836: }
837:
838: }
|