Package: TypeComparator

TypeComparator

nameinstructionbranchcomplexitylinemethod
TypeComparator(ITypeCheckerAssistantFactory)
M: 0 C: 15
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
allCompatible(List, List, boolean)
M: 0 C: 32
100%
M: 0 C: 6
100%
M: 0 C: 4
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
allSubTypes(List, List, boolean)
M: 2 C: 30
94%
M: 1 C: 5
83%
M: 1 C: 3
75%
M: 1 C: 5
83%
M: 0 C: 1
100%
checkComposeTypes(PType, Environment, boolean)
M: 76 C: 114
60%
M: 12 C: 16
57%
M: 9 C: 6
40%
M: 12 C: 27
69%
M: 0 C: 1
100%
compatible(List, List)
M: 0 C: 14
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
compatible(PType, PType)
M: 0 C: 14
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
compatible(PType, PType, boolean)
M: 0 C: 14
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
getCurrentModule()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
intersect(PType, PType)
M: 22 C: 145
87%
M: 5 C: 27
84%
M: 4 C: 13
76%
M: 7 C: 42
86%
M: 0 C: 1
100%
isSubType(PType, PType)
M: 0 C: 6
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
isSubType(PType, PType, boolean)
M: 0 C: 14
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
narrowest(List, List)
M: 1 C: 10
91%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 1
100%
M: 0 C: 1
100%
narrowest(PType, PType)
M: 1 C: 8
89%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 1
100%
M: 0 C: 1
100%
searchCompatible(PType, PType, boolean)
M: 0 C: 35
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 7
100%
M: 0 C: 1
100%
searchSubType(PType, PType, boolean)
M: 0 C: 35
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 7
100%
M: 0 C: 1
100%
setCurrentModule(String)
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
subtest(PType, PType, boolean)
M: 77 C: 482
86%
M: 24 C: 124
84%
M: 21 C: 54
72%
M: 12 C: 123
91%
M: 0 C: 1
100%
test(PType, PType, boolean)
M: 40 C: 617
94%
M: 18 C: 150
89%
M: 15 C: 70
82%
M: 11 C: 136
93%
M: 0 C: 1
100%

Coverage

1: /*******************************************************************************
2: *
3: *        Copyright (C) 2008 Fujitsu Services Ltd.
4: *
5: *        Author: Nick Battle
6: *
7: *        This file is part of VDMJ.
8: *
9: *        VDMJ is free software: you can redistribute it and/or modify
10: *        it under the terms of the GNU General Public License as published by
11: *        the Free Software Foundation, either version 3 of the License, or
12: *        (at your option) any later version.
13: *
14: *        VDMJ is distributed in the hope that it will be useful,
15: *        but WITHOUT ANY WARRANTY; without even the implied warranty of
16: *        MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17: *        GNU General Public License for more details.
18: *
19: *        You should have received a copy of the GNU General Public License
20: *        along with VDMJ. If not, see <http://www.gnu.org/licenses/>.
21: *
22: ******************************************************************************/
23:
24: package org.overture.typechecker;
25:
26: import java.util.HashSet;
27: import java.util.List;
28: import java.util.Set;
29: import java.util.Vector;
30:
31: import org.overture.ast.analysis.AnalysisException;
32: import org.overture.ast.assistant.pattern.PTypeList;
33: import org.overture.ast.definitions.ATypeDefinition;
34: import org.overture.ast.definitions.PDefinition;
35: import org.overture.ast.factory.AstFactory;
36: import org.overture.ast.lex.LexNameList;
37: import org.overture.ast.types.ABracketType;
38: import org.overture.ast.types.AClassType;
39: import org.overture.ast.types.AFunctionType;
40: import org.overture.ast.types.AInMapMapType;
41: import org.overture.ast.types.ANamedInvariantType;
42: import org.overture.ast.types.AOperationType;
43: import org.overture.ast.types.AOptionalType;
44: import org.overture.ast.types.AParameterType;
45: import org.overture.ast.types.AProductType;
46: import org.overture.ast.types.ARecordInvariantType;
47: import org.overture.ast.types.ASeq1SeqType;
48: import org.overture.ast.types.ASet1SetType;
49: import org.overture.ast.types.SInvariantType;
50: import org.overture.ast.types.SSetType;
51: import org.overture.ast.types.AUndefinedType;
52: import org.overture.ast.types.AUnionType;
53: import org.overture.ast.types.AUnknownType;
54: import org.overture.ast.types.AUnresolvedType;
55: import org.overture.ast.types.AVoidReturnType;
56: import org.overture.ast.types.AVoidType;
57: import org.overture.ast.types.PType;
58: import org.overture.ast.types.SMapType;
59: import org.overture.ast.types.SNumericBasicType;
60: import org.overture.ast.types.SSeqType;
61: import org.overture.typechecker.assistant.ITypeCheckerAssistantFactory;
62: import org.overture.typechecker.utilities.type.ParameterFinder;
63:
64: /**
65: * A class for static type checking comparisons.
66: */
67:
68: public class TypeComparator
69: {
70:         /**
71:          * A vector of type pairs that have already been compared. This is to allow recursive type definitions to be
72:          * compared without infinite regress.
73:          */
74:
75:         private Vector<TypePair> done = new Vector<TypePair>(256);
76:
77:         private final ITypeCheckerAssistantFactory assistantFactory;
78:
79:         public TypeComparator(ITypeCheckerAssistantFactory assistantFactory)
80:         {
81:                 this.assistantFactory = assistantFactory;
82:         }
83:
84:         /**
85:          * A result value for comparison of types. The "Maybe" value is needed so that the fact that a type's subtypes are
86:          * being actively compared in a recursive call can be recorded. For example, if a MySetType contains references to
87:          * MySetType in its element's type, the comparison of those types will see the "Maybe" result of the original call
88:          * and not recurse. That will not fail the lower level comparison, but the overall "yes" will not be recorded until
89:          * the recursive calls return (assuming there are no "no" votes of course).
90:          */
91:
92:         private static enum Result
93:         {
94:                 Yes, No, Maybe
95:         }
96:
97:         private static class TypePair
98:         {
99:                 public PType a;
100:                 public PType b;
101:                 public Result result;
102:
103:                 public TypePair(PType a, PType b)
104:                 {
105:                         this.a = a;
106:                         this.b = b;
107:                         this.result = Result.Maybe;
108:                 }
109:
110:                 @Override
111:                 public boolean equals(Object other)
112:                 {
113:                         if (other instanceof TypePair)
114:                         {
115:                                 TypePair to = (TypePair) other;
116:                                 return a.equals(to.a) && b.equals(to.b);
117:                         }
118:
119:                         return false;
120:                 }
121:
122:                 @Override
123:                 public int hashCode()
124:                 {
125:                         return a.hashCode() + b.hashCode();
126:                 }
127:         }
128:
129:         /**
130:          * The current module name. This is set as the type checker goes from module
131:          * to module, and is used to affect the processing of opaque "non-struct"
132:          * type exports.
133:          */
134:
135:         private String currentModule = null;
136:
137:         public String getCurrentModule()
138:         {
139:                 return currentModule;
140:         }
141:
142:         public void setCurrentModule(String module)
143:         {
144:                 currentModule = module;
145:         }
146:
147:         /**
148:          * Test whether the two types are compatible. This means that, at runtime, it is possible that the two types are the
149:          * same, or sufficiently similar that the "from" value can be assigned to the "to" value.
150:          *
151:          * @param to
152:          * @param from
153:          * @return True if types "a" and "b" are compatible.
154:          */
155:
156:         public synchronized boolean compatible(PType to, PType from)
157:         {
158:                 done.clear();
159:•                return searchCompatible(to, from, false) == Result.Yes;
160:         }
161:
162:         public synchronized boolean compatible(PType to, PType from,
163:                         boolean paramOnly)
164:         {
165:                 done.clear();
166:•                return searchCompatible(to, from, paramOnly) == Result.Yes;
167:         }
168:
169:         /**
170:          * Compare two type lists for placewise compatibility. , assistantFactory @param to
171:          *
172:          * @param to
173:          * @param from
174:          * @return True if all types compatible.
175:          */
176:
177:         public synchronized boolean compatible(List<PType> to, List<PType> from)
178:         {
179:                 done.clear();
180:•                return allCompatible(to, from, false) == Result.Yes;
181:         }
182:
183:         /**
184:          * Compare two type lists for placewise compatibility. This is used to check ordered lists of types such as those in
185:          * a ProductType or parameters to a function or operation.
186:          *
187:          * @param to
188:          * @param from
189:          * @return Yes or No.
190:          */
191:
192:         private Result allCompatible(List<PType> to, List<PType> from,
193:                         boolean paramOnly)
194:         {
195:•                if (to.size() != from.size())
196:                 {
197:                         return Result.No;
198:                 } else
199:                 {
200:•                        for (int i = 0; i < to.size(); i++)
201:                         {
202:•                                if (searchCompatible(to.get(i), from.get(i), paramOnly) == Result.No)
203:                                 {
204:                                         return Result.No;
205:                                 }
206:                         }
207:                 }
208:
209:                 return Result.Yes;
210:         }
211:
212:         /**
213:          * Search the {@link #done} vector for an existing comparison of two types before either returning the previous
214:          * result, or making a new comparison and adding that result to the vector.
215:          *
216:          * @param to
217:          * @param from
218:          * @return Yes or No.
219:          */
220:
221:         private Result searchCompatible(PType to, PType from, boolean paramOnly)
222:         {
223:                 TypePair pair = new TypePair(to, from);
224:                 int i = done.indexOf(pair);
225:
226:•                if (i >= 0)
227:                 {
228:                         return done.get(i).result; // May be "Maybe".
229:                 } else
230:                 {
231:                         done.add(pair);
232:                 }
233:
234:                 // The pair.result is "Maybe" until this call returns.
235:                 pair.result = test(to, from, paramOnly);
236:
237:                 return pair.result;
238:         }
239:
240:         /**
241:          * The main implementation of the compatibility checker. If "a" and "b" are the same object the result is "yes"; if
242:          * either is an {@link UnknownType}, we are dealing with earlier parser errors and so "yes" is returned to avoid too
243:          * many errors; if either is a {@link ParameterType} the result is also "yes" on the grounds that the type cannot be
244:          * tested at compile time. If either type is a {@link BracketType} or a {@link NamedType} the types are reduced to
245:          * their underlying type before proceeding; if either is an {@link OptionalType} and the other is optional also, the
246:          * result is "yes", otherwise the underlying type of the optional type is taken before proceeding; the last two
247:          * steps are repeated until the types will not reduce further. To compare the reduced types, if "a" is a union type,
248:          * then all the component types of "a" are compared to "b" (or b's components, if it too is a union type) until a
249:          * match is found; otherwise basic type comparisons are made, involving any subtypes - for example, if they are both
250:          * sets, then the result depends on whether their "set of" subtypes are compatible, by a recursive call. Similarly
251:          * with maps and sequences, function/operation parameter types, and record field types. Lastly, a simple
252:          * {@link org.overture.vdmj.types.Type#equals} operation is performed on two basic types to decide the result.
253:          *
254:          * @param to
255:          * @param from
256:          * @param paramOnly
257:          * @return Yes or No.
258:          */
259:
260:         private Result test(PType to, PType from, boolean paramOnly)
261:         {
262:•                if (to instanceof AUnresolvedType)
263:                 {
264:                         throw new TypeCheckException("Unknown type: " + to, to.getLocation(), to);
265:                 }
266:
267:•                if (from instanceof AUnresolvedType)
268:                 {
269:                         throw new TypeCheckException("Unknown type: " + from, from.getLocation(), from);
270:                 }
271:
272:•                if (to == from) // (assistantFactory.createPTypeAssistant().equals(to, from))
273:                 {
274:                         return Result.Yes; // Same object!
275:                 }
276:
277:•                if (to instanceof AUnknownType || from instanceof AUnknownType)
278:                 {
279:                         return Result.Yes; // Hmmm... too many errors otherwise
280:                 }
281:
282:•                if (to instanceof AUndefinedType || from instanceof AUndefinedType)
283:                 {
284:                         return Result.Yes; // Not defined "yet"...?
285:                 }
286:
287:                 // Correct for one-type unions
288:•                if (to instanceof AUnionType && ((AUnionType)to).getTypes().size() == 1)
289:                 {
290:                         to = ((AUnionType)to).getTypes().get(0);
291:                 }
292:
293:•                if (from instanceof AUnionType && ((AUnionType)from).getTypes().size() == 1)
294:                 {
295:                         from = ((AUnionType)from).getTypes().get(0);
296:                 }
297:
298:                 // Obtain the fundamental type of BracketTypes, NamedTypes and
299:                 // OptionalTypes.
300:
301:                 boolean resolved = false;
302:
303:•                while (!resolved)
304:                 {
305:•                        if (to instanceof ABracketType)
306:                         {
307:                                 to = ((ABracketType) to).getType();
308:                                 continue;
309:                         }
310:
311:•                        if (from instanceof ABracketType)
312:                         {
313:                                 from = ((ABracketType) from).getType();
314:                                 continue;
315:                         }
316:
317:•                 if (to instanceof SInvariantType)
318:                 {
319:                         SInvariantType ito =(SInvariantType)to;
320:
321:•                         if (to instanceof ANamedInvariantType && !TypeChecker.isOpaque(ito, currentModule))
322:                          {
323:                                  to = ((ANamedInvariantType)to).getType();
324:                                  continue;
325:                          }
326:                 }
327:
328:•                 if (from instanceof SInvariantType)
329:                 {
330:                         SInvariantType ifrom =(SInvariantType)from;
331:
332:•                         if (from instanceof ANamedInvariantType && !TypeChecker.isOpaque(ifrom, currentModule))
333:                          {
334:                                  from = ((ANamedInvariantType)from).getType();
335:                                  continue;
336:                          }
337:                 }
338:
339:•                        if (to instanceof AOptionalType)
340:                         {
341:•                                if (from instanceof AOptionalType)
342:                                 {
343:                                         return Result.Yes;
344:                                 }
345:
346:                                 to = ((AOptionalType) to).getType();
347:                                 continue;
348:                         }
349:
350:•                        if (from instanceof AOptionalType)
351:                         {
352:                                 // Can't assign nil to a non-optional type? This should maybe
353:                                 // generate a warning here?
354:
355:•                                if (to instanceof AOptionalType)
356:                                 {
357:                                         return Result.Yes;
358:                                 }
359:
360:                                 from = ((AOptionalType) from).getType();
361:                                 continue;
362:                         }
363:
364:                         resolved = true;
365:                 }
366:
367:•                if (from instanceof AParameterType)
368:                 {
369:                         try
370:                         {
371:                                 String fstr = from.apply(new ParameterFinder()).get(0);
372:                                 List<String> tstr = to.apply(new ParameterFinder());
373:
374:•                                if (tstr.contains(fstr) && !(to instanceof AParameterType))
375:                                 {
376:                                         TypeChecker.warning(5031, "Type " + from + " must be a union", from.getLocation());        // See bug #562
377:                                 }
378:                         }
379:                         catch (AnalysisException e)
380:                         {
381:                                 // Can't happen
382:                         }
383:
384:                         return Result.Yes;        // Runtime checked...
385:                 }
386:
387:                 // OK... so we have fully resolved the basic types...
388:
389:•                if (to instanceof AUnionType)
390:                 {
391:                         AUnionType ua = (AUnionType) to;
392:
393:•                        for (PType ta : ua.getTypes())
394:                         {
395:•                                if (searchCompatible(ta, from, paramOnly) == Result.Yes)
396:                                 {
397:                                         return Result.Yes;
398:                                 }
399:                         }
400:                 } else
401:                 {
402:•                        if (from instanceof AUnionType)
403:                         {
404:                                 AUnionType ub = (AUnionType) from;
405:
406:•                                for (PType tb : ub.getTypes())
407:                                 {
408:•                                        if (searchCompatible(to, tb, paramOnly) == Result.Yes)
409:                                         {
410:                                                 return Result.Yes;
411:                                         }
412:                                 }
413:•                        } else if (to instanceof SNumericBasicType)
414:                         {
415:•                                return from instanceof SNumericBasicType ? Result.Yes
416:                                                 : Result.No;
417:•                        } else if (to instanceof AProductType)
418:                         {
419:•                                if (!(from instanceof AProductType))
420:                                 {
421:                                         return Result.No;
422:                                 }
423:
424:                                 List<PType> ta = ((AProductType) to).getTypes();
425:                                 List<PType> tb = ((AProductType) from).getTypes();
426:                                 return allCompatible(ta, tb, paramOnly);
427:•                        } else if (to instanceof SMapType)
428:                         {
429:•                                if (!(from instanceof SMapType))
430:                                 {
431:                                         return Result.No;
432:                                 }
433:
434:                                 SMapType ma = (SMapType) to;
435:                                 SMapType mb = (SMapType) from;
436:
437:•                                return ma.getEmpty()
438:•                                                || mb.getEmpty()
439:•                                                || searchCompatible(ma.getFrom(), mb.getFrom(), paramOnly) == Result.Yes
440:•                                                && searchCompatible(ma.getTo(), mb.getTo(), paramOnly) == Result.Yes ? Result.Yes
441:                                                 : Result.No;
442:•                        } else if (to instanceof SSetType)        // Includes set1
443:                         {
444:•                                if (!(from instanceof SSetType))
445:                                 {
446:                                         return Result.No;
447:                                 }
448:
449:                                 SSetType sa = (SSetType) to;
450:                                 SSetType sb = (SSetType) from;
451:
452:•                                if (to instanceof ASet1SetType && sb.getEmpty())
453:                                 {
454:                                         return Result.No;
455:                                 }
456:
457:•                                return sa.getEmpty()
458:•                                                || sb.getEmpty()
459:•                                                || searchCompatible(sa.getSetof(), sb.getSetof(), paramOnly) == Result.Yes ? Result.Yes
460:                                                 : Result.No;
461:•                        } else if (to instanceof SSeqType) // Includes seq1
462:                         {
463:•                                if (!(from instanceof SSeqType))
464:                                 {
465:                                         return Result.No;
466:                                 }
467:
468:                                 SSeqType sa = (SSeqType) to;
469:                                 SSeqType sb = (SSeqType) from;
470:
471:•                                if (to instanceof ASeq1SeqType && sb.getEmpty())
472:                                 {
473:                                         return Result.No;
474:                                 }
475:
476:•                                return sa.getEmpty()
477:•                                                || sb.getEmpty()
478:•                                                || searchCompatible(sa.getSeqof(), sb.getSeqof(), paramOnly) == Result.Yes ? Result.Yes
479:                                                 : Result.No;
480:•                        } else if (to instanceof AFunctionType)
481:                         {
482:•                                if (!(from instanceof AFunctionType))
483:                                 {
484:                                         return Result.No;
485:                                 }
486:
487:                                 AFunctionType fa = (AFunctionType) to;
488:                                 AFunctionType fb = (AFunctionType) from;
489:
490:•                                return allCompatible(fa.getParameters(), fb.getParameters(), paramOnly) == Result.Yes
491:•                                                && (paramOnly || searchCompatible(fa.getResult(), fb.getResult(), paramOnly) == Result.Yes) ? Result.Yes
492:                                                 : Result.No;
493:•                        } else if (to instanceof AOperationType)
494:                         {
495:•                                if (!(from instanceof AOperationType))
496:                                 {
497:                                         return Result.No;
498:                                 }
499:
500:                                 AOperationType fa = (AOperationType) to;
501:                                 AOperationType fb = (AOperationType) from;
502:
503:•                                return allCompatible(fa.getParameters(), fb.getParameters(), paramOnly) == Result.Yes
504:•                                                && (paramOnly || searchCompatible(fa.getResult(), fb.getResult(), paramOnly) == Result.Yes) ? Result.Yes
505:                                                 : Result.No;
506:•                        } else if (to instanceof ARecordInvariantType)
507:                         {
508:•                                if (!(from instanceof ARecordInvariantType))
509:                                 {
510:                                         return Result.No;
511:                                 }
512:
513:                                 ARecordInvariantType rf = (ARecordInvariantType) from;
514:                                 ARecordInvariantType rt = (ARecordInvariantType) to;
515:
516:•                                return assistantFactory.createPTypeAssistant().equals(rf, rt) ? Result.Yes
517:                                                 : Result.No;
518:•                        } else if (to instanceof AClassType)
519:                         {
520:•                                if (!(from instanceof AClassType))
521:                                 {
522:                                         return Result.No;
523:                                 }
524:
525:                                 AClassType cfrom = (AClassType) from;
526:                                 AClassType cto = (AClassType) to;
527:
528:                                 // VDMTools doesn't seem to worry about sub/super type
529:                                 // assignments. This was "cfrom.equals(cto)".
530:
531:•                                if (assistantFactory.createPTypeAssistant().hasSupertype(cfrom, cto)
532:•                                                || assistantFactory.createPTypeAssistant().hasSupertype(cto, cfrom))
533:                                 {
534:                                         return Result.Yes;
535:                                 }
536:•                        } else if (from instanceof AVoidReturnType)
537:                         {
538:•                                if (to instanceof AVoidType || to instanceof AVoidReturnType)
539:                                 {
540:                                         return Result.Yes;
541:                                 } else
542:                                 {
543:                                         return Result.No;
544:                                 }
545:•                        } else if (to instanceof AVoidReturnType)
546:                         {
547:•                                if (from instanceof AVoidType
548:                                                 || from instanceof AVoidReturnType)
549:                                 {
550:                                         return Result.Yes;
551:                                 } else
552:                                 {
553:                                         return Result.No;
554:                                 }
555:                         }
556:•                        else if (to instanceof AParameterType)
557:                         {
558:                                 try
559:                                 {
560:                                         String tstr = to.apply(new ParameterFinder()).get(0);
561:                                         List<String> fstr = from.apply(new ParameterFinder());
562:
563:•                                        if (fstr.contains(tstr) && !(from instanceof AParameterType))
564:                                         {
565:                                                 TypeChecker.warning(5031, "Type " + to + " must be a union", to.getLocation());        // See bug #562
566:                                         }
567:                                 }
568:                                 catch (AnalysisException e)
569:                                 {
570:                                         // Can't happen
571:                                 }
572:
573:                                 return Result.Yes;        // Runtime checked...
574:                         }
575:                         else
576:                         {
577:•                                return assistantFactory.createPTypeAssistant().equals(to, from) ? Result.Yes
578:                                                 : Result.No;
579:                         }
580:                 }
581:
582:                 return Result.No;
583:         }
584:
585:         /**
586:          * Test whether one type is a subtype of another.
587:          *
588:          * @param sub
589:          * @param sup
590:          * @return True if sub is a subtype of sup.
591:          */
592:
593:         public synchronized boolean isSubType(PType sub, PType sup)
594:         {
595:                 return isSubType(sub, sup, false);
596:         }
597:
598:         public synchronized boolean isSubType(PType sub, PType sup,
599:                         boolean invignore)
600:         {
601:                 done.clear();
602:•                return searchSubType(sub, sup, invignore) == Result.Yes;
603:         }
604:
605:         /**
606:          * Compare two type lists for placewise subtype compatibility. This is used to check ordered lists of types such as
607:          * those in a ProductType or parameters to a function or operation.
608:          *
609:          * @param sub
610:          * @param sup
611:          * @return Yes or No.
612:          */
613:
614:         private Result allSubTypes(List<PType> sub, List<PType> sup,
615:                         boolean invignore)
616:         {
617:•                if (sub.size() != sup.size())
618:                 {
619:                         return Result.No;
620:                 } else
621:                 {
622:•                        for (int i = 0; i < sub.size(); i++)
623:                         {
624:•                                if (searchSubType(sub.get(i), sup.get(i), invignore) == Result.No)
625:                                 {
626:                                         return Result.No;
627:                                 }
628:                         }
629:                 }
630:
631:                 return Result.Yes;
632:         }
633:
634:         /**
635:          * Search the {@link #done} vector for an existing subtype comparison of two types before either returning the
636:          * previous result, or making a new comparison and adding that result to the vector.
637:          *
638:          * @param sub
639:          * @param sup
640:          * @param invignore
641:          * @return Yes or No, if sub is a subtype of sup.
642:          */
643:
644:         private Result searchSubType(PType sub, PType sup, boolean invignore)
645:         {
646:                 TypePair pair = new TypePair(sub, sup);
647:                 int i = done.indexOf(pair);
648:
649:•                if (i >= 0)
650:                 {
651:                         return done.get(i).result; // May be "Maybe".
652:                 } else
653:                 {
654:                         done.add(pair);
655:                 }
656:
657:                 // The pair.result is "Maybe" until this call returns.
658:                 pair.result = subtest(sub, sup, invignore);
659:
660:                 return pair.result;
661:         }
662:
663:         /**
664:          * The main implementation of the subtype checker. If "a" and "b" are the same object the result is "yes"; if either
665:          * is an {@link UnknownType}, we are dealing with earlier parser errors and so "yes" is returned to avoid too many
666:          * errors; if either is a {@link ParameterType} the result is also "yes" on the grounds that the type cannot be
667:          * tested at compile time. If either type is a {@link BracketType} or a {@link NamedType} the types are reduced to
668:          * their underlying type before proceeding; if either is an {@link OptionalType} and the other is optional also, the
669:          * result is "yes", otherwise the underlying type of the optional type is taken before proceeding; the last two
670:          * steps are repeated until the types will not reduce further. To compare the reduced types, if "a" is a union type,
671:          * then all the component types of "a" are compared to "b" (or b's components, if it too is a union type); otherwise
672:          * basic type comparisons are made, involving any subtypes - for example, if they are both sets, then the result
673:          * depends on whether their "set of" subtypes are subtypes, by a recursive call. Similarly with maps and sequences,
674:          * function/operation parameter types, and record field types. Lastly, a simple
675:          * {@link org.overture.vdmj.types.Type#equals} operation is performed on two basic types to decide the result.
676:          *
677:          * @param sub
678:          * @param sup
679:          * @param invignore
680:          * @return Yes or No.
681:          */
682:
683:         private Result subtest(PType sub, PType sup, boolean invignore)
684:         {
685:•                if (sub instanceof AUnresolvedType)
686:                 {
687:                         throw new TypeCheckException("Unknown type: " + sub, sub.getLocation(), sub);
688:                 }
689:
690:•                if (sup instanceof AUnresolvedType)
691:                 {
692:                         throw new TypeCheckException("Unknown type: " + sup, sup.getLocation(), sup);
693:                 }
694:
695:•                if (sub instanceof AUnknownType || sup instanceof AUnknownType)
696:                 {
697:                         return Result.Yes; // Hmmm... too many errors otherwise
698:                 }
699:
700:•                if (sub instanceof AParameterType || sup instanceof AParameterType)
701:                 {
702:                         return Result.Yes; // Runtime checked...
703:                 }
704:
705:•                if (sub instanceof AUndefinedType || sup instanceof AUndefinedType)
706:                 {
707:                         return Result.Yes; // Usually uninitialized variables etc.
708:                 }
709:
710:                 // Obtain the fundamental type of BracketTypes, NamedTypes and
711:                 // OptionalTypes.
712:
713:                 boolean resolved = false;
714:
715:•                while (!resolved)
716:                 {
717:•                        if (sub instanceof ABracketType)
718:                         {
719:                                 sub = ((ABracketType) sub).getType();
720:                                 continue;
721:                         }
722:
723:•                        if (sup instanceof ABracketType)
724:                         {
725:                                 sup = ((ABracketType) sup).getType();
726:                                 continue;
727:                         }
728:
729:•                        if (sub instanceof ANamedInvariantType)
730:                         {
731:                                 ANamedInvariantType nt = (ANamedInvariantType) sub;
732:
733:•                                if (nt.getInvDef() == null || invignore)
734:                                 {
735:                                         sub = nt.getType();
736:                                         continue;
737:                                 }
738:                         }
739:
740:•                        if (sup instanceof ANamedInvariantType)
741:                         {
742:                                 ANamedInvariantType nt = (ANamedInvariantType) sup;
743:
744:•                                if (nt.getInvDef() == null || invignore)
745:                                 {
746:                                         sup = nt.getType();
747:                                         continue;
748:                                 }
749:                         }
750:
751:•                        if (sub instanceof AOptionalType && sup instanceof AOptionalType)
752:                         {
753:                                 sub = ((AOptionalType) sub).getType();
754:                                 sup = ((AOptionalType) sup).getType();
755:                                 continue;
756:                         }
757:
758:                         resolved = true;
759:                 }
760:
761:•                if (sub instanceof AUnknownType || sup instanceof AUnknownType)
762:                 {
763:                         return Result.Yes; // Hmmm... too many errors otherwise
764:                 }
765:
766:                 // TODO: When nodes are cloned this 'if(sub == sup)' will not work,
767:                 // but this might not be the best way to solve it
768:                 // if(sub == sup)
769:
770:•                if (sub.equals(sup))
771:                 {
772:                         return Result.Yes;
773:                 }
774:
775:                 // OK... so we have fully resolved the basic types...
776:
777:•                if (sub instanceof AUnionType)
778:                 {
779:                         AUnionType subu = (AUnionType) sub;
780:
781:•                        for (PType suba : subu.getTypes())
782:                         {
783:•                                if (searchSubType(suba, sup, invignore) == Result.No)
784:                                 {
785:                                         return Result.No;
786:                                 }
787:                         }
788:
789:                         return Result.Yes; // Must be all of them
790:                 } else
791:                 {
792:•                        if (sup instanceof AUnionType)
793:                         {
794:                                 AUnionType supu = (AUnionType) sup;
795:
796:•                                for (PType supt : supu.getTypes())
797:                                 {
798:•                                        if (searchSubType(sub, supt, invignore) == Result.Yes)
799:                                         {
800:                                                 return Result.Yes; // Can be any of them
801:                                         }
802:                                 }
803:
804:                                 return Result.No;
805:•                        } else if (sub instanceof ANamedInvariantType)
806:                         {
807:                                 ANamedInvariantType subn = (ANamedInvariantType) sub;
808:                                 return searchSubType(subn.getType(), sup, invignore);
809:•                        } else if (sup instanceof AOptionalType)
810:                         {
811:                                 // Supertype includes a nil value, and the subtype is not
812:                                 // optional (stripped above), so we test the optional's type.
813:
814:                                 AOptionalType op = (AOptionalType) sup;
815:                                 return searchSubType(sub, op.getType(), invignore);
816:•                        } else if (sub instanceof SNumericBasicType)
817:                         {
818:•                                if (sup instanceof SNumericBasicType)
819:                                 {
820:                                         SNumericBasicType subn = (SNumericBasicType) sub;
821:                                         SNumericBasicType supn = (SNumericBasicType) sup;
822:
823:•                                        return assistantFactory.createSNumericBasicTypeAssistant().getWeight(subn) <= assistantFactory.createSNumericBasicTypeAssistant().getWeight(supn) ? Result.Yes
824:                                                         : Result.No;
825:                                 }
826:•                        } else if (sub instanceof AProductType)
827:                         {
828:•                                if (!(sup instanceof AProductType))
829:                                 {
830:                                         return Result.No;
831:                                 }
832:
833:                                 List<PType> subl = ((AProductType) sub).getTypes();
834:                                 List<PType> supl = ((AProductType) sup).getTypes();
835:
836:                                 return allSubTypes(subl, supl, invignore);
837:•                        } else if (sub instanceof SMapType)
838:                         {
839:•                                if (!(sup instanceof SMapType))
840:                                 {
841:                                         return Result.No;
842:                                 }
843:
844:                                 SMapType subm = (SMapType) sub;
845:                                 SMapType supm = (SMapType) sup;
846:
847:•                                if (subm.getEmpty() || supm.getEmpty())
848:                                 {
849:                                         return Result.Yes;
850:                                 }
851:
852:•                                if (searchSubType(subm.getFrom(), supm.getFrom(), invignore) == Result.Yes
853:•                                                && searchSubType(subm.getTo(), supm.getTo(), invignore) == Result.Yes)
854:                                 {
855:
856:•                                        if (!(sub instanceof AInMapMapType)
857:                                                         && sup instanceof AInMapMapType)
858:                                         {
859:                                                 return Result.No;
860:                                         }
861:
862:                                         return Result.Yes;
863:                                 } else
864:                                 {
865:                                         return Result.No;
866:                                 }
867:
868:•                        } else if (sub instanceof SSetType)
869:                         {
870:•                                if (!(sup instanceof SSetType))
871:                                 {
872:                                         return Result.No;
873:                                 }
874:
875:                                 SSetType subs = (SSetType) sub;
876:                                 SSetType sups = (SSetType) sup;
877:
878:•                                if ((subs.getEmpty() && !(sup instanceof ASet1SetType)) || sups.getEmpty())
879:                                 {
880:                                         return Result.Yes;
881:                                 }
882:
883:•                                if (searchSubType(subs.getSetof(), sups.getSetof(), invignore) == Result.Yes)
884:                                 {
885:•                                        if (!(sub instanceof ASet1SetType) && (sup instanceof ASet1SetType))
886:                                         {
887:                                                 return Result.No;
888:                                         }
889:
890:                                         return Result.Yes;
891:                                 }
892:                                 else
893:                                 {
894:                                         return Result.No;
895:                                 }
896:
897:•                        } else if (sub instanceof SSeqType) // Includes seq1
898:                         {
899:•                                if (!(sup instanceof SSeqType))
900:                                 {
901:                                         return Result.No;
902:                                 }
903:
904:                                 SSeqType subs = (SSeqType) sub;
905:                                 SSeqType sups = (SSeqType) sup;
906:
907:•                                if ((subs.getEmpty() && !(sup instanceof ASeq1SeqType)) || sups.getEmpty())
908:                                 {
909:                                         return Result.Yes;
910:                                 }
911:
912:•                                if (searchSubType(subs.getSeqof(), sups.getSeqof(), invignore) == Result.Yes)
913:                                 {
914:•                                        if (!(sub instanceof ASeq1SeqType) && sup instanceof ASeq1SeqType)
915:                                         {
916:                                                 return Result.No;
917:                                         }
918:
919:                                         return Result.Yes;
920:                                 } else
921:                                 {
922:                                         return Result.No;
923:                                 }
924:•                        } else if (sub instanceof AFunctionType)
925:                         {
926:•                                if (!(sup instanceof AFunctionType))
927:                                 {
928:                                         return Result.No;
929:                                 }
930:
931:                                 AFunctionType subf = (AFunctionType) sub;
932:                                 AFunctionType supf = (AFunctionType) sup;
933:
934:•                                return allSubTypes(subf.getParameters(), supf.getParameters(), invignore) == Result.Yes
935:•                                                && searchSubType(subf.getResult(), supf.getResult(), invignore) == Result.Yes ? Result.Yes
936:                                                 : Result.No;
937:•                        } else if (sub instanceof AOperationType)
938:                         {
939:•                                if (!(sup instanceof AOperationType))
940:                                 {
941:                                         return Result.No;
942:                                 }
943:
944:                                 AOperationType subo = (AOperationType) sub;
945:                                 AOperationType supo = (AOperationType) sup;
946:
947:•                                return allSubTypes(subo.getParameters(), supo.getParameters(), invignore) == Result.Yes
948:•                                                && searchSubType(subo.getResult(), supo.getResult(), invignore) == Result.Yes ? Result.Yes
949:                                                 : Result.No;
950:•                        } else if (sub instanceof ARecordInvariantType)
951:                         {
952:•                                if (!(sup instanceof ARecordInvariantType))
953:                                 {
954:                                         return Result.No;
955:                                 }
956:
957:                                 ARecordInvariantType subr = (ARecordInvariantType) sub;
958:                                 ARecordInvariantType supr = (ARecordInvariantType) sup;
959:
960:•                                return assistantFactory.createPTypeAssistant().equals(subr, supr) ? Result.Yes
961:                                                 : Result.No;
962:•                        } else if (sub instanceof AClassType)
963:                         {
964:•                                if (!(sup instanceof AClassType))
965:                                 {
966:                                         return Result.No;
967:                                 }
968:
969:                                 AClassType supc = (AClassType) sup;
970:                                 AClassType subc = (AClassType) sub;
971:
972:•                                if (assistantFactory.createPTypeAssistant().hasSupertype(subc, supc))
973:                                 {
974:                                         return Result.Yes;
975:                                 }
976:                         } else
977:                         {
978:•                                return assistantFactory.createPTypeAssistant().equals(sub, sup) ? Result.Yes
979:                                                 : Result.No;
980:                         }
981:                 }
982:
983:                 return Result.No;
984:         }
985:
986:         /**
987:          * Check that the compose types that are referred to in a type have a matching definition in the environment. The
988:          * method returns a list of types that do not exist if the newTypes parameter is passed.
989:          *
990:          * @param type
991:          * @param env
992:          * @param newTypes
993:          * @return
994:          */
995:         public PTypeList checkComposeTypes(PType type, Environment env,
996:                         boolean newTypes)
997:         {
998:                 PTypeList undefined = new PTypeList();
999:
1000:•                for (PType compose : env.af.createPTypeAssistant().getComposeTypes(type))
1001:                 {
1002:                         ARecordInvariantType composeType = (ARecordInvariantType) compose;
1003:                         PDefinition existing = env.findType(composeType.getName(), null);
1004:
1005:•                        if (existing != null)
1006:                         {
1007:                                 // If the type is already defined, check that it has the same shape and
1008:                                 // does not have an invariant (which cannot match a compose definition).
1009:                                 boolean matches = false;
1010:
1011:•                                if (existing instanceof ATypeDefinition)
1012:                                 {
1013:                                         ATypeDefinition edef = (ATypeDefinition) existing;
1014:                                         PType etype = existing.getType();
1015:
1016:•                                        if (edef.getInvExpression() == null
1017:                                                         && etype instanceof ARecordInvariantType)
1018:                                         {
1019:                                                 ARecordInvariantType retype = (ARecordInvariantType) etype;
1020:
1021:•                                                if (retype.getFields().equals(composeType.getFields()))
1022:                                                 {
1023:                                                         matches = true;
1024:                                                 }
1025:                                         }
1026:                                 }
1027:
1028:•                                if (!matches)
1029:                                 {
1030:                                         TypeChecker.report(3325, "Mismatched compose definitions for "
1031:                                                         + composeType.getName(), composeType.getLocation());
1032:                                         TypeChecker.detail2(composeType.getName().getName(), composeType.getLocation(), existing.getName().getName(), existing.getLocation());
1033:                                 }
1034:                         } else
1035:                         {
1036:•                                if (newTypes)
1037:                                 {
1038:                                         undefined.add(composeType);
1039:                                 } else
1040:                                 {
1041:                                         TypeChecker.report(3113, "Unknown type name '"
1042:                                                         + composeType.getName() + "'", composeType.getLocation());
1043:                                 }
1044:                         }
1045:                 }
1046:
1047:                 // Lastly, check that the compose types extracted are compatible
1048:                 LexNameList done = new LexNameList();
1049:
1050:•                for (PType c1 : undefined)
1051:                 {
1052:•                        for (PType c2 : undefined)
1053:                         {
1054:•                                if (c1 != c2)
1055:                                 {
1056:                                         ARecordInvariantType r1 = (ARecordInvariantType) c1;
1057:                                         ARecordInvariantType r2 = (ARecordInvariantType) c2;
1058:
1059:•                                        if (r1.getName().equals(r2.getName())
1060:•                                                        && !done.contains(r1.getName())
1061:•                                                        && !r1.getFields().equals(r2.getFields()))
1062:                                         {
1063:                                                 TypeChecker.report(3325, "Mismatched compose definitions for "
1064:                                                                 + r1.getName(), r1.getLocation());
1065:                                                 TypeChecker.detail2(r1.getName().getName(), r1.getLocation(), r2.getName().getName(), r2.getLocation());
1066:                                                 done.add(r1.getName());
1067:                                         }
1068:                                 }
1069:                         }
1070:                 }
1071:
1072:                 return undefined;
1073:         }
1074:
1075:         /**
1076:          * Calculate the intersection of two types.
1077:          *
1078:          * @param a
1079:          * @param b
1080:          * @return
1081:          */
1082:         public PType intersect(PType a, PType b)
1083:         {
1084:                 Set<PType> tsa = new HashSet<PType>();
1085:                 Set<PType> tsb = new HashSet<PType>();
1086:
1087:                 // Obtain the fundamental type of BracketTypes, NamedTypes and OptionalTypes.
1088:                 boolean resolved = false;
1089:
1090:•                while (!resolved)
1091:                 {
1092:•                        if (a instanceof ABracketType)
1093:                         {
1094:                                 a = ((ABracketType) a).getType();
1095:                                 continue;
1096:                         }
1097:
1098:•                        if (b instanceof ABracketType)
1099:                         {
1100:                                 b = ((ABracketType) b).getType();
1101:                                 continue;
1102:                         }
1103:
1104:•                        if (a instanceof ANamedInvariantType)
1105:                         {
1106:                                 ANamedInvariantType nt = (ANamedInvariantType) a;
1107:
1108:•                                if (nt.getInvDef() == null)
1109:                                 {
1110:                                         a = nt.getType();
1111:                                         continue;
1112:                                 }
1113:                         }
1114:
1115:•                        if (b instanceof ANamedInvariantType)
1116:                         {
1117:                                 ANamedInvariantType nt = (ANamedInvariantType) b;
1118:
1119:•                                if (nt.getInvDef() == null)
1120:                                 {
1121:                                         b = nt.getType();
1122:                                         continue;
1123:                                 }
1124:                         }
1125:
1126:•                        if (a instanceof AOptionalType && b instanceof AOptionalType)
1127:                         {
1128:                                 a = ((AOptionalType) a).getType();
1129:                                 b = ((AOptionalType) b).getType();
1130:                                 continue;
1131:                         }
1132:
1133:                         resolved = true;
1134:                 }
1135:
1136:•                if (a instanceof AUnionType)
1137:                 {
1138:                         AUnionType uta = (AUnionType) a;
1139:                         tsa.addAll(uta.getTypes());
1140:                 } else
1141:                 {
1142:                         tsa.add(a);
1143:                 }
1144:
1145:•                if (b instanceof AUnionType)
1146:                 {
1147:                         AUnionType utb = (AUnionType) b;
1148:                         tsb.addAll(utb.getTypes());
1149:                 } else
1150:                 {
1151:                         tsb.add(b);
1152:                 }
1153:
1154:                 // Keep largest types which are compatible (eg. nat and int choses int)
1155:                 Set<PType> result = new HashSet<PType>();
1156:
1157:•                for (PType atype : tsa)
1158:                 {
1159:•                        for (PType btype : tsb)
1160:                         {
1161:•                                if (isSubType(atype, btype))
1162:                                 {
1163:                                         result.add(btype);
1164:•                                } else if (isSubType(btype, atype))
1165:                                 {
1166:                                         result.add(atype);
1167:                                 }
1168:                         }
1169:                 }
1170:
1171:•                if (result.isEmpty())
1172:                 {
1173:                         return null;
1174:                 } else
1175:                 {
1176:                         List<PType> list = new Vector<PType>();
1177:                         list.addAll(result);
1178:                         return AstFactory.newAUnionType(a.getLocation(), list);
1179:                 }
1180:         }
1181:
1182:         /**
1183:          * Return the narrowest of two types/type lists.
1184:          */
1185:         public synchronized List<PType> narrowest(List<PType> t1, List<PType> t2)
1186:         {
1187:•                return allSubTypes(t1, t2, false) == Result.Yes ? t1 : t2;
1188:         }
1189:
1190:         public synchronized PType narrowest(PType t1, PType t2)
1191:         {
1192:•                return isSubType(t1, t2) ? t1 : t2;
1193:         }
1194: }