Source Code Cross Referenced for GenericSortInstantiations.java in  » Testing » KeY » de » uka » ilkd » key » rule » inst » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.rule.inst 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


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 java.util.HashSet;
014:        import java.util.Iterator;
015:        import java.util.Set;
016:
017:        import de.uka.ilkd.key.java.Services;
018:        import de.uka.ilkd.key.logic.Term;
019:        import de.uka.ilkd.key.logic.op.IteratorOfEntryOfSchemaVariableAndInstantiationEntry;
020:        import de.uka.ilkd.key.logic.op.SchemaVariable;
021:        import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
022:        import de.uka.ilkd.key.logic.sort.*;
023:
024:        /**
025:         * This class handles the instantiation of generic sorts (used for
026:         * generic taclets), i.e. the class tries to find a solution for the
027:         * conditions on the generic sorts given by the type hierarchy and the
028:         * chosen SV instantiations
029:         *
030:         * this class is immutable
031:         */
032:
033:        public class GenericSortInstantiations {
034:
035:            public static final GenericSortInstantiations EMPTY_INSTANTIATIONS = new GenericSortInstantiations(
036:                    MapAsListFromGenericSortToSort.EMPTY_MAP);
037:
038:            private final MapFromGenericSortToSort insts;
039:
040:            private GenericSortInstantiations(MapFromGenericSortToSort p_insts) {
041:                insts = p_insts;
042:            }
043:
044:            /**
045:             * Create an object that solves the conditions given by the
046:             * instantiation iterator, i.e. instantiations of the generic
047:             * sorts used within "p_instantiations" are sought for which are
048:             * compatible with the instantiations of the SVs
049:             * @param p_instantiations list of SV instantiations
050:             * @param p_conditions additional conditions for sort instantiations
051:             * @throws GenericSortException iff the conditions could not be
052:             * solved
053:             */
054:            public static GenericSortInstantiations create(
055:                    IteratorOfEntryOfSchemaVariableAndInstantiationEntry p_instantiations,
056:                    ListOfGenericSortCondition p_conditions) {
057:
058:                ListOfGenericSort sorts = SLListOfGenericSort.EMPTY_LIST;
059:                GenericSortCondition c;
060:
061:                final IteratorOfGenericSortCondition it;
062:
063:                // Find the generic sorts within "p_instantiations" and
064:                // "p_conditions", create the conditions
065:
066:                for (it = p_conditions.iterator(); it.hasNext();)
067:                    sorts = sorts.prepend(it.next().getGenericSort());
068:
069:                while (p_instantiations.hasNext()) {
070:                    c = GenericSortCondition.createCondition(p_instantiations
071:                            .next().value());
072:                    if (c != null) {
073:                        p_conditions = p_conditions.prepend(c);
074:                        sorts = sorts.prepend(c.getGenericSort());
075:                    }
076:                }
077:                return create(sorts, p_conditions);
078:            }
079:
080:            /**
081:             * Create an object that holds instantiations of the generic sorts
082:             * "p_sorts" satisfying the conditions "p_conditions"
083:             * @param p_sorts generic sorts to instantiate
084:             * @param p_conditions conditions the instantiations have to
085:             * satisfy
086:             * @throws GenericSortException if no instantiations has been
087:             * found
088:             */
089:            public static GenericSortInstantiations create(
090:                    ListOfGenericSort p_sorts,
091:                    ListOfGenericSortCondition p_conditions) {
092:
093:                if (p_sorts.isEmpty())
094:                    return EMPTY_INSTANTIATIONS;
095:
096:                return new GenericSortInstantiations(solve(p_sorts,
097:                        p_conditions));
098:            }
099:
100:            /**
101:             * @return Boolean.TRUE if the sorts used within "p_entry" are
102:             * correct, Boolean.FALSE if the sorts are definitely incorrect,
103:             * null if the sorts could (perhaps) be made correct by choosing
104:             * the right generic sort instantiations
105:             */
106:            public Boolean checkSorts(InstantiationEntry p_entry) {
107:                if (!(p_entry instanceof  TermInstantiation)
108:                        || p_entry.getSchemaVariable().isProgramSV())
109:                    return Boolean.TRUE;
110:
111:                final GenericSortCondition c = GenericSortCondition
112:                        .createCondition(p_entry);
113:                if (c != null)
114:                    return checkCondition(c);
115:
116:                final SortedSchemaVariable sv = (SortedSchemaVariable) p_entry
117:                        .getSchemaVariable();
118:                final Term term = ((TermInstantiation) p_entry).getTerm();
119:
120:                if (GenericSortCondition.subSortsAllowed(sv))
121:                    return term.sort().extendsTrans(sv.sort()) ? Boolean.TRUE
122:                            : Boolean.FALSE;
123:
124:                return sv.sort() == term.sort() ? Boolean.TRUE : Boolean.FALSE;
125:            }
126:
127:            /**
128:             * @return Boolean.TRUE if the generic sort instantiations within
129:             * "this" satisfy "p_condition", null otherwise (this means,
130:             * "p_condition" could be satisfied by create a new
131:             * "GenericSortInstantiations"-object)
132:             */
133:            public Boolean checkCondition(GenericSortCondition p_condition) {
134:                Sort s = insts.get(p_condition.getGenericSort());
135:
136:                if (s == null) {
137:                    return null;
138:                }
139:
140:                return p_condition.check(s, this ) ? Boolean.TRUE : null;
141:            }
142:
143:            public boolean isInstantiated(GenericSort p_gs) {
144:                return insts.containsKey(p_gs);
145:            }
146:
147:            public Sort getInstantiation(GenericSort p_gs) {
148:                return insts.get(p_gs);
149:            }
150:
151:            /**
152:             * Create a list of conditions establishing the instantiations
153:             * stored by this object (not saying anything about further
154:             * generic sorts)
155:             */
156:            public ListOfGenericSortCondition toConditions() {
157:                ListOfGenericSortCondition res = SLListOfGenericSortCondition.EMPTY_LIST;
158:                IteratorOfEntryOfGenericSortAndSort it = insts.entryIterator();
159:                EntryOfGenericSortAndSort entry;
160:
161:                while (it.hasNext()) {
162:                    entry = it.next();
163:                    res = res
164:                            .prepend(GenericSortCondition
165:                                    .createIdentityCondition(entry.key(), entry
166:                                            .value()));
167:                }
168:
169:                return res;
170:            }
171:
172:            /**
173:             * @param services the Services class
174:             * @return p_s iff p_s is not a generic sort, the concrete sort
175:             * p_s is instantiated with currently otherwise 
176:             * @throws GenericSortException iff p_s is a generic sort which is
177:             * not yet instantiated
178:             */
179:            public Sort getRealSort(SchemaVariable p_sv, Services services) {
180:                return getRealSort(((SortedSchemaVariable) p_sv).sort(),
181:                        services);
182:            }
183:
184:            public Sort getRealSort(Sort p_s, Services services) {
185:                if (p_s instanceof  GenericSort) {
186:                    p_s = getInstantiation((GenericSort) p_s);
187:                    if (p_s == null) {
188:                        throw GenericSortException.UNINSTANTIATED_GENERIC_SORT;
189:                    }
190:                } else if (p_s instanceof  IntersectionSort) {
191:                    final IntersectionSort inter = (IntersectionSort) p_s;
192:
193:                    SetOfSort sos = SetAsListOfSort.EMPTY_SET;
194:
195:                    for (int i = 0, sz = inter.memberCount(); i < sz; i++) {
196:                        sos = sos.add(getRealSort(inter.getComponent(i),
197:                                services));
198:                    }
199:                    return IntersectionSort.getIntersectionSort(sos, services);
200:                } else if (p_s instanceof  CollectionSort) {
201:                    Sort s = getRealSort(((CollectionSort) p_s).elementSort(),
202:                            services);
203:
204:                    s = ((CollectionSort) p_s).cloneFor(s);
205:
206:                    if (s == null)
207:                        throw new GenericSortException(
208:                                "Generic collection sort is instantiated with a sort"
209:                                        + " without collections");
210:
211:                    return s;
212:                }
213:
214:                return p_s;
215:            }
216:
217:            /**
218:             * Really solve the conditions given
219:             * @param p_sorts generic sorts that must be instantiated
220:             * @param p_conditions conditions to be solved
221:             * @throws GenericSortException no solution could be found
222:             * @return the/a found solution
223:             */
224:            private static MapFromGenericSortToSort solve(
225:                    ListOfGenericSort p_sorts,
226:                    ListOfGenericSortCondition p_conditions) {
227:
228:                MapFromGenericSortToSort res;
229:
230:                // the generic sorts are sorted topologically, i.e. if sort A
231:                // is a supersort of sort B, then A appears behind B within
232:                // "topologicalSorts"
233:                ListOfGenericSort topologicalSorts = topology(p_sorts);
234:
235:                res = solveHelp(topologicalSorts,
236:                        MapAsListFromGenericSortToSort.EMPTY_MAP, p_conditions,
237:                        SLListOfGenericSort.EMPTY_LIST);
238:
239:                if (res == null)
240:                    throw new GenericSortException(
241:                            "Conditions for generic sorts could not be solved: "
242:                                    + p_conditions);
243:
244:                return res;
245:            }
246:
247:            private static final class FailException extends Exception {
248:                private static final long serialVersionUID = 5291022478863582449L;
249:            }
250:
251:            private final static FailException FAIL_EXCEPTION = new FailException();
252:
253:            /**
254:             * Method which is called recursively and tries to instantiate one
255:             * (the first) generic sort from the "p_remainingSorts"-list
256:             * @param p_remainingSorts generic sorts which needs to be
257:             * instantiated (topologically sorted)
258:             * @param p_curRes instantiations so far
259:             * @param p_conditions conditions (see above)
260:             * @return a solution if one could be found, null otherwise
261:             */
262:            private static MapFromGenericSortToSort solveHelp(
263:                    ListOfGenericSort p_remainingSorts,
264:                    MapFromGenericSortToSort p_curRes,
265:                    ListOfGenericSortCondition p_conditions,
266:                    ListOfGenericSort p_pushedBack) {
267:
268:                if (p_remainingSorts == SLListOfGenericSort.EMPTY_LIST)
269:                    return solveForcedInst(p_pushedBack, p_curRes, p_conditions);
270:
271:                // next generic sort to seek an instantiation for
272:                final GenericSort gs = p_remainingSorts.head();
273:                p_remainingSorts = p_remainingSorts.tail();
274:
275:                // Find the sorts "gs" has to be a supersort of and the
276:                // identity conditions
277:                ListOfSort subsorts = SLListOfSort.EMPTY_LIST;
278:                ListOfGenericSortCondition idConditions = SLListOfGenericSortCondition.EMPTY_LIST;
279:
280:                // subsorts given by the conditions (could be made faster
281:                // by using a hash map for storing the conditions)
282:                {
283:                    final IteratorOfGenericSortCondition itC = p_conditions
284:                            .iterator();
285:                    while (itC.hasNext()) {
286:                        final GenericSortCondition c = itC.next();
287:                        if (c.getGenericSort() == gs) {
288:                            if (c instanceof  GenericSortCondition.GSCSupersort)
289:                                subsorts = subsorts
290:                                        .prepend(((GenericSortCondition.GSCSupersort) c)
291:                                                .getSubsort());
292:                            else if (c instanceof  GenericSortCondition.GSCIdentity)
293:                                idConditions = idConditions.prepend(c);
294:                        }
295:                    }
296:                }
297:
298:                // add the subsorts given by the already instantiated
299:                // generic sorts
300:                subsorts = addChosenInstantiations(p_curRes, gs, subsorts);
301:
302:                // Solve the conditions
303:                final ListOfSort chosenList;
304:                try {
305:                    chosenList = chooseResults(gs, idConditions);
306:                } catch (FailException e) {
307:                    return null;
308:                }
309:
310:                if (chosenList != null) {
311:                    return descend(p_remainingSorts, p_curRes, p_conditions,
312:                            p_pushedBack, gs, subsorts, chosenList);
313:                } else if (subsorts != SLListOfSort.EMPTY_LIST) {
314:                    // if anything else has failed, construct minimal
315:                    // supersorts of the found subsorts and try them
316:                    final ListOfSort super Sorts = minimalSupersorts(subsorts);
317:
318:                    return descend(p_remainingSorts, p_curRes, p_conditions,
319:                            p_pushedBack, gs, subsorts, super Sorts);
320:                } else {
321:                    // and if even that did not work, remove the generic
322:                    // sort from the list and try again later
323:                    return solveHelp(p_remainingSorts, p_curRes, p_conditions,
324:                            p_pushedBack.prepend(gs));
325:                }
326:            }
327:
328:            private static MapFromGenericSortToSort descend(
329:                    ListOfGenericSort p_remainingSorts,
330:                    MapFromGenericSortToSort p_curRes,
331:                    ListOfGenericSortCondition p_conditions,
332:                    ListOfGenericSort p_pushedBack, GenericSort p_gs,
333:                    ListOfSort p_subsorts, ListOfSort p_chosenList) {
334:                final IteratorOfSort itChosen = p_chosenList.iterator();
335:                while (itChosen.hasNext()) {
336:                    final Sort chosen = itChosen.next();
337:                    if (!isSupersortOf(chosen, p_subsorts) // this test is unnecessary in some cases
338:                            || !p_gs.isPossibleInstantiation(chosen))
339:                        continue;
340:
341:                    final MapFromGenericSortToSort res = solveHelp(
342:                            p_remainingSorts, p_curRes.put(p_gs, chosen),
343:                            p_conditions, p_pushedBack);
344:                    if (res != null)
345:                        return res;
346:                }
347:                return null;
348:            }
349:
350:            private static ListOfSort chooseResults(GenericSort p_gs,
351:                    ListOfGenericSortCondition p_idConditions)
352:                    throws FailException {
353:                if (p_idConditions != SLListOfGenericSortCondition.EMPTY_LIST) {
354:                    // then the instantiation is completely determined by
355:                    // an identity condition
356:                    final IteratorOfGenericSortCondition itC = p_idConditions
357:                            .iterator();
358:                    final Sort chosen = condSort(itC);
359:
360:                    // other identity conditions must lead to the same
361:                    // instantiation
362:                    while (itC.hasNext()) {
363:                        if (chosen != condSort(itC))
364:                            throw FAIL_EXCEPTION;
365:                    }
366:
367:                    return SLListOfSort.EMPTY_LIST.prepend(chosen);
368:                } else {
369:                    // if a list of possible instantiations of the generic
370:                    // sort has been given, use it
371:                    final ListOfSort res = toList(p_gs.getOneOf());
372:                    if (res.isEmpty())
373:                        return null;
374:                    return res;
375:                }
376:            }
377:
378:            private static ListOfSort toList(SetOfSort p_set) {
379:                ListOfSort res;
380:                res = SLListOfSort.EMPTY_LIST;
381:                final IteratorOfSort it = p_set.iterator();
382:                while (it.hasNext())
383:                    res = res.prepend(it.next());
384:                return res;
385:            }
386:
387:            private static Sort condSort(IteratorOfGenericSortCondition itC) {
388:                return ((GenericSortCondition.GSCIdentity) itC.next())
389:                        .getSort();
390:            }
391:
392:            private static ListOfSort addChosenInstantiations(
393:                    MapFromGenericSortToSort p_curRes, GenericSort p_gs,
394:                    ListOfSort p_subsorts) {
395:                final IteratorOfEntryOfGenericSortAndSort it = p_curRes
396:                        .entryIterator();
397:                while (it.hasNext()) {
398:                    final EntryOfGenericSortAndSort entry = it.next();
399:                    if (entry.key().extendsTrans(p_gs))
400:                        p_subsorts = p_subsorts.prepend(entry.value());
401:                }
402:                return p_subsorts;
403:            }
404:
405:            /**
406:             * Method which is called by solveHelp and tries to instantiate
407:             * the generic sorts for which GSCForceInstantiation-conditions
408:             * (with "maximum" parameter) are contained within "p_conditions"
409:             * @param p_curRes instantiations so far
410:             * @param p_conditions conditions (see above)
411:             * @return a solution if one could be found, null otherwise
412:             */
413:            private static MapFromGenericSortToSort solveForcedInst(
414:                    ListOfGenericSort p_remainingSorts,
415:                    MapFromGenericSortToSort p_curRes,
416:                    ListOfGenericSortCondition p_conditions) {
417:
418:                if (p_remainingSorts == SLListOfGenericSort.EMPTY_LIST)
419:                    return p_curRes; // nothing further to be done
420:
421:                IteratorOfGenericSort it = topology(p_remainingSorts)
422:                        .iterator();
423:                p_remainingSorts = SLListOfGenericSort.EMPTY_LIST;
424:
425:                // reverse the order of the sorts, to start with the most
426:                // general one
427:                while (it.hasNext())
428:                    p_remainingSorts = p_remainingSorts.prepend(it.next());
429:
430:                return solveForcedInstHelp(p_remainingSorts, p_curRes);
431:            }
432:
433:            /**
434:             * Method which is called recursively and tries to instantiate one
435:             * (the first) generic sort from the "p_remainingSorts"-list
436:             * @param p_remainingSorts generic sorts which needs to be
437:             * instantiated (topologically sorted, starting with the most
438:             * general sort)
439:             * @param p_curRes instantiations so far
440:             * @return a solution if one could be found, null otherwise
441:             */
442:            private static MapFromGenericSortToSort solveForcedInstHelp(
443:                    ListOfGenericSort p_remainingSorts,
444:                    MapFromGenericSortToSort p_curRes) {
445:                if (p_remainingSorts == SLListOfGenericSort.EMPTY_LIST) {
446:                    // we're done
447:                    return p_curRes;
448:                } else {
449:                    // next generic sort to seek an instantiation for
450:                    GenericSort gs = p_remainingSorts.head();
451:                    p_remainingSorts = p_remainingSorts.tail();
452:
453:                    IteratorOfSort it;
454:                    Sort cur;
455:                    MapFromGenericSortToSort res;
456:                    HashSet todo = new HashSet();
457:                    HashSet done = new HashSet();
458:                    Sort cand;
459:
460:                    // search for instantiated supersorts of gs (the method
461:                    // below is neither fast nor complete, but should find a
462:                    // solution for relevant situations)
463:
464:                    // insert into the working list (set)
465:                    it = gs.extendsSorts().iterator();
466:                    while (it.hasNext())
467:                        todo.add(it.next());
468:
469:                    while (!todo.isEmpty()) {
470:                        it = null;
471:                        cur = (Sort) todo.iterator().next();
472:                        todo.remove(cur);
473:                        done.add(cur);
474:
475:                        if (cur instanceof  GenericSort) {
476:                            cand = p_curRes.get((GenericSort) cur);
477:                            if (cand == null)
478:                                it = cur.extendsSorts().iterator();
479:                        } else {
480:                            it = cur.extendsSorts().iterator();
481:                            cand = cur;
482:                        }
483:
484:                        if (cand != null
485:                                && isPossibleInstantiation(gs, cand, p_curRes)) {
486:                            res = solveForcedInstHelp(p_remainingSorts,
487:                                    p_curRes.put(gs, cand));
488:                            if (res != null)
489:                                return res;
490:                        }
491:
492:                        if (it != null) {
493:                            while (it.hasNext()) {
494:                                cur = it.next();
495:                                if (!done.contains(cur))
496:                                    todo.add(cur);
497:                            }
498:                        }
499:                    }
500:                }
501:
502:                return null;
503:            }
504:
505:            /**
506:             * Sort generic sorts topologically, i.e. if sort A is a supersort
507:             * of sort B, then A appears behind B within the return value
508:             * @return sorted sorts
509:             */
510:            private static ListOfGenericSort topology(ListOfGenericSort p_sorts) {
511:                ListOfGenericSort res = SLListOfGenericSort.EMPTY_LIST;
512:                IteratorOfGenericSort it;
513:                GenericSort curMax;
514:                GenericSort tMax;
515:                ListOfGenericSort tList;
516:
517:                while (p_sorts != SLListOfGenericSort.EMPTY_LIST) {
518:                    // search for a maximal element
519:                    it = p_sorts.iterator();
520:                    curMax = it.next();
521:
522:                    if (res.contains(curMax)) {
523:                        p_sorts = p_sorts.tail();
524:                        continue;
525:                    }
526:
527:                    tList = SLListOfGenericSort.EMPTY_LIST;
528:
529:                    while (it.hasNext()) {
530:                        tMax = it.next();
531:                        if (!res.contains(tMax)) {
532:                            if (curMax.extendsTrans(tMax)) {
533:                                tList = tList.prepend(curMax);
534:                                curMax = tMax;
535:                            } else
536:                                tList = tList.prepend(tMax);
537:                        }
538:                    }
539:
540:                    res = res.prepend(curMax);
541:                    p_sorts = tList;
542:                }
543:
544:                return res;
545:            }
546:
547:            /**
548:             * Find all minimal common supersorts of "p_itSorts"
549:             *
550:             * PRECONDITION: !p_sorts.isEmpty ()
551:             */
552:            private static ListOfSort minimalSupersorts(ListOfSort p_sorts) {
553:                // if the list only consists of a single sort, return this sort
554:                if (p_sorts.size() == 1)
555:                    return p_sorts;
556:
557:                final IteratorOfSort p_itSorts = p_sorts.iterator();
558:                HashSet inside = new HashSet();
559:                HashSet outside = new HashSet();
560:                HashSet todo = new HashSet();
561:
562:                // the null sort has to be handled separately, as it doesn't
563:                // provide a list of direct supersorts
564:                final boolean checkNULL = insertFirstSort(p_itSorts, inside);
565:
566:                // Find a set "inside" of common supersorts of "p_itSorts"
567:                // that contains all minimal common supersorts
568:                while (!inside.isEmpty() && p_itSorts.hasNext()) {
569:                    final Sort condition = p_itSorts.next();
570:
571:                    // At this point todo.isEmpty ()
572:                    final HashSet t = todo;
573:                    todo = inside;
574:                    inside = t;
575:
576:                    while (!todo.isEmpty()) {
577:                        final Sort nextTodo = getOneOf(todo);
578:
579:                        if (!inside.contains(nextTodo)
580:                                && !outside.contains(nextTodo)) {
581:                            if (condition.extendsTrans(nextTodo))
582:                                inside.add(nextTodo);
583:                            else {
584:                                outside.add(nextTodo);
585:                                addSortsToSet(todo, nextTodo.extendsSorts());
586:                            }
587:                        }
588:                    }
589:                }
590:
591:                if (checkNULL) {
592:                    // At this point todo.isEmpty ()
593:                    treatNullSorts(inside, todo);
594:                    inside = todo;
595:                }
596:
597:                // Find the minimal elements of "inside"
598:                return findMinimalElements(inside);
599:            }
600:
601:            /**
602:             * Find all minimal elements of the given set <code>p_inside</code>
603:             */
604:            private static ListOfSort findMinimalElements(Set p_inside) {
605:                if (p_inside.size() == 1)
606:                    return SLListOfSort.EMPTY_LIST.prepend((Sort) p_inside
607:                            .iterator().next());
608:
609:                ListOfSort res = SLListOfSort.EMPTY_LIST;
610:                final Iterator it = p_inside.iterator();
611:
612:                mainloop: while (it.hasNext()) {
613:                    final Sort sort = (Sort) it.next();
614:
615:                    ListOfSort res2 = SLListOfSort.EMPTY_LIST;
616:                    final IteratorOfSort itSort = res.iterator();
617:                    while (itSort.hasNext()) {
618:                        final Sort oldMinimal = itSort.next();
619:
620:                        if (oldMinimal.extendsTrans(sort))
621:                            continue mainloop;
622:                        else if (!sort.extendsTrans(oldMinimal))
623:                            res2 = res2.prepend(oldMinimal);
624:                    }
625:
626:                    res = res2.prepend(sort);
627:                }
628:
629:                return res;
630:            }
631:
632:            /**
633:             * Remove all sorts that are not supersorts of the null sort, add the found
634:             * sorts to the set <code>p_emptySet</code>
635:             */
636:            private static void treatNullSorts(HashSet p_inside,
637:                    HashSet p_emptySet) {
638:                final Iterator it = p_inside.iterator();
639:
640:                while (it.hasNext()) {
641:                    final Sort sort = (Sort) it.next();
642:                    if (Sort.NULL.extendsTrans(sort))
643:                        p_emptySet.add(sort);
644:                }
645:            }
646:
647:            private static Sort getOneOf(Set p_set) {
648:                final Sort nextTodo = (Sort) p_set.iterator().next();
649:                p_set.remove(nextTodo);
650:                return nextTodo;
651:            }
652:
653:            private static void addSortsToSet(Set p_set, SetOfSort p_sorts) {
654:                final IteratorOfSort itSort = p_sorts.iterator();
655:                while (itSort.hasNext())
656:                    p_set.add(itSort.next());
657:            }
658:
659:            /**
660:             * Add the first non-NULL sort given by the iterator <code>p_itSorts</code>
661:             * to the set <code>inside</code>, return true iff NULL sorts have been
662:             * found and omitted doing this. If <code>p_itSorts</code> does only
663:             * deliver the sort NULL, add NULL to the set <code>inside</code>
664:             */
665:            private static boolean insertFirstSort(IteratorOfSort p_itSorts,
666:                    HashSet inside) {
667:                boolean checkNULL = false;
668:                Sort cand = p_itSorts.next();
669:                while (cand == Sort.NULL && p_itSorts.hasNext()) {
670:                    cand = p_itSorts.next();
671:                    checkNULL = true;
672:                }
673:                inside.add(cand);
674:                return checkNULL;
675:            }
676:
677:            /**
678:             * @return true iff "p_s" is supersort of every sort of
679:             * "p_subsorts"
680:             */
681:            private static boolean isSupersortOf(Sort p_s, ListOfSort p_subsorts) {
682:                final IteratorOfSort it = p_subsorts.iterator();
683:
684:                while (it.hasNext()) {
685:                    if (!it.next().extendsTrans(p_s))
686:                        return false;
687:                }
688:
689:                return true;
690:            }
691:
692:            /**
693:             * @return true iff "p_s" is a valid instantiation of the generic
694:             * sort "p_gs", and this instantiation is consistent with
695:             * previously chosen instantiations
696:             */
697:            private static boolean isPossibleInstantiation(GenericSort p_gs,
698:                    Sort p_s, MapFromGenericSortToSort p_curRes) {
699:
700:                if (!p_gs.isPossibleInstantiation(p_s))
701:                    return false;
702:
703:                // check whether the new instantiation is consistent with the
704:                // already chosen instantiations
705:                final IteratorOfEntryOfGenericSortAndSort itEntry = p_curRes
706:                        .entryIterator();
707:                while (itEntry.hasNext()) {
708:                    final EntryOfGenericSortAndSort entry = itEntry.next();
709:
710:                    if (entry.key().extendsTrans(p_gs)
711:                            && !entry.value().extendsTrans(p_s)
712:                            || p_gs.extendsTrans(entry.key())
713:                            && !p_s.extendsTrans(entry.value()))
714:                        return false;
715:                }
716:                return true;
717:            }
718:
719:            /** toString */
720:            public String toString() {
721:                IteratorOfEntryOfGenericSortAndSort it = insts.entryIterator();
722:                EntryOfGenericSortAndSort entry;
723:                String res = "";
724:
725:                while (it.hasNext()) {
726:                    if (!"".equals(res))
727:                        res += ", ";
728:                    entry = it.next();
729:                    res += entry.key() + "=" + entry.value();
730:                }
731:
732:                return res;
733:            }
734:
735:            /**
736:             * ONLY FOR JUNIT TESTS
737:             */
738:
739:            public MapFromGenericSortToSort getAllInstantiations() {
740:                return insts;
741:            }
742:
743:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.