Method: caseARealLiteralExp(ARealLiteralExp, TypeCheckInfo)

1: /*
2: * #%~
3: * The VDM Type Checker
4: * %%
5: * Copyright (C) 2008 - 2014 Overture
6: * %%
7: * This program is free software: you can redistribute it and/or modify
8: * it under the terms of the GNU General Public License as
9: * published by the Free Software Foundation, either version 3 of the
10: * License, or (at your option) any later version.
11: *
12: * This program is distributed in the hope that it will be useful,
13: * but WITHOUT ANY WARRANTY; without even the implied warranty of
14: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15: * GNU General Public License for more details.
16: *
17: * You should have received a copy of the GNU General Public
18: * License along with this program. If not, see
19: * <http://www.gnu.org/licenses/gpl-3.0.html>.
20: * #~%
21: */
22: package org.overture.typechecker.visitor;
23:
24: import java.util.ArrayList;
25: import java.util.Iterator;
26: import java.util.LinkedList;
27: import java.util.List;
28: import java.util.Map.Entry;
29: import java.util.Vector;
30:
31: import org.overture.ast.analysis.AnalysisException;
32: import org.overture.ast.analysis.intf.IQuestion;
33: import org.overture.ast.analysis.intf.IQuestionAnswer;
34: import org.overture.ast.definitions.ABusClassDefinition;
35: import org.overture.ast.definitions.ACpuClassDefinition;
36: import org.overture.ast.definitions.AExplicitFunctionDefinition;
37: import org.overture.ast.definitions.AImplicitFunctionDefinition;
38: import org.overture.ast.definitions.AMultiBindListDefinition;
39: import org.overture.ast.definitions.AStateDefinition;
40: import org.overture.ast.definitions.ASystemClassDefinition;
41: import org.overture.ast.definitions.ATypeDefinition;
42: import org.overture.ast.definitions.PDefinition;
43: import org.overture.ast.definitions.SClassDefinition;
44: import org.overture.ast.expressions.*;
45: import org.overture.ast.factory.AstFactory;
46: import org.overture.ast.intf.lex.ILexNameToken;
47: import org.overture.ast.intf.lex.ILexRealToken;
48: import org.overture.ast.lex.LexNameToken;
49: import org.overture.ast.patterns.AExpressionPattern;
50: import org.overture.ast.patterns.AIdentifierPattern;
51: import org.overture.ast.patterns.ASeqBind;
52: import org.overture.ast.patterns.ASetBind;
53: import org.overture.ast.patterns.ATypeBind;
54: import org.overture.ast.patterns.PBind;
55: import org.overture.ast.patterns.PMultipleBind;
56: import org.overture.ast.patterns.PPattern;
57: import org.overture.ast.typechecker.NameScope;
58: import org.overture.ast.types.*;
59: import org.overture.ast.util.PTypeSet;
60: import org.overture.ast.util.Utils;
61: import org.overture.config.Release;
62: import org.overture.config.Settings;
63: import org.overture.typechecker.Environment;
64: import org.overture.typechecker.FlatCheckedEnvironment;
65: import org.overture.typechecker.RecursiveLoops;
66: import org.overture.typechecker.TypeCheckException;
67: import org.overture.typechecker.TypeCheckInfo;
68: import org.overture.typechecker.TypeChecker;
69: import org.overture.typechecker.TypeCheckerErrors;
70: import org.overture.typechecker.assistant.definition.PDefinitionAssistantTC;
71: import org.overture.typechecker.assistant.definition.SClassDefinitionAssistantTC;
72: import org.overture.typechecker.assistant.type.AClassTypeAssistantTC;
73: import org.overture.typechecker.assistant.type.PTypeAssistantTC;
74: import org.overture.typechecker.utilities.type.QualifiedDefinition;
75:
76: public class TypeCheckerExpVisitor extends AbstractTypeCheckVisitor
77: {
78:
79:         public TypeCheckerExpVisitor(
80:                         IQuestionAnswer<TypeCheckInfo, PType> typeCheckVisitor)
81:         {
82:                 super(typeCheckVisitor);
83:         }
84:
85:         @Override public PType caseAApplyExp(AApplyExp node, TypeCheckInfo question)
86:                         throws AnalysisException
87:         {
88:                 TypeCheckInfo noConstraint = question.newConstraint(null);
89:                 noConstraint.qualifiers = null;
90:                 node.setArgtypes(new ArrayList<PType>());
91:
92:                 for (PExp a : node.getArgs())
93:                 {
94:                         question.qualifiers = null;
95:                         node.getArgtypes().add(a.apply(THIS, noConstraint));
96:                 }
97:
98:                 node.setType(node.getRoot().apply(THIS, new TypeCheckInfo(question.assistantFactory, question.env, question.scope, node.getArgtypes())));
99:
100:                 if (question.assistantFactory.createPTypeAssistant().isUnknown(node.getType()))
101:                 {
102:                         return node.getType();
103:                 }
104:
105:                 PDefinition enclfunc = question.env.getEnclosingDefinition();
106:                 boolean inFunction = question.env.isFunctional();
107:                 boolean inOperation = !inFunction;
108:                 boolean inReserved = (enclfunc == null || enclfunc.getName() == null) ?
109:                                 false :
110:                                 enclfunc.getName().isReserved();
111:
112:                 if (inFunction)
113:                 {
114:                         PDefinition calling = getRecursiveDefinition(node, question);
115:
116:                         if (calling instanceof AExplicitFunctionDefinition)
117:                         {
118:
119:                                 AExplicitFunctionDefinition def = (AExplicitFunctionDefinition) calling;
120:
121:                                 if (def.getIsCurried())
122:                                 {
123:                                         // Only recursive if this apply is the last - so our type is not a function.
124:
125:                                         if (node.getType() instanceof AFunctionType
126:                                                         && ((AFunctionType) node.getType()).getResult() instanceof AFunctionType)
127:                                         {
128:                                                 calling = null;
129:                                         }
130:                                 }
131:
132:                         }
133:
134:                         if (enclfunc != null && calling != null)
135:                         {
136:                                 RecursiveLoops.getInstance().addApplyExp(enclfunc, node, calling);
137:                         }
138:                 }
139:
140:                 boolean isSimple = !question.assistantFactory.createPTypeAssistant().isUnion(node.getType(), question.fromModule);
141:                 PTypeSet results = new PTypeSet(question.assistantFactory);
142:
143:                 if (question.assistantFactory.createPTypeAssistant().isFunction(node.getType(), question.fromModule))
144:                 {
145:                         AFunctionType ft = question.assistantFactory.createPTypeAssistant().getFunction(node.getType());
146:
147:                         if (ft.getInstantiated() != null && !ft.getInstantiated())
148:                         {
149:                                 // Something like f(x) rather than f[nat](x)
150:                                 TypeCheckerErrors.report(3350, "Polymorphic function has not been instantiated", node.getRoot().getLocation(), node);
151:                         }
152:
153:                         question.assistantFactory.createPTypeAssistant().typeResolve(ft, null, THIS, question);
154:                         results.add(functionApply(node, isSimple, ft, question));
155:                 }
156:
157:                 if (question.assistantFactory.createPTypeAssistant().isOperation(node.getType(), question.fromModule))
158:                 {
159:                         if (node.getRoot() instanceof AVariableExp)
160:                         {
161:                                 AVariableExp exp = (AVariableExp) node.getRoot();
162:                                 PDefinition opdef = question.env.findName(exp.getName(), question.scope);
163:                                 AClassTypeAssistantTC assist = question.assistantFactory.createAClassTypeAssistant();
164:
165:                                 if (opdef != null && assist.isConstructor(opdef)
166:                                                 && !assist.inConstructor(question.env))
167:                                 {
168:                                         TypeCheckerErrors.report(3337, "Cannot call a constructor from here", node.getLocation(), node);
169:                                         results.add(AstFactory.newAUnknownType(node.getLocation()));
170:                                 }
171:                         }
172:
173:                         AOperationType ot = question.assistantFactory.createPTypeAssistant().getOperation(node.getType(), question.fromModule);
174:                         question.assistantFactory.createPTypeAssistant().typeResolve(ot, null, THIS, question);
175:
176:                         if (inFunction && Settings.release == Release.VDM_10
177:                                         && !ot.getPure())
178:                         {
179:                                 TypeCheckerErrors.report(3300,
180:                                                 "Impure operation '" + node.getRoot()
181:                                                                 + "' cannot be called from here", node.getLocation(), node);
182:                                 results.add(AstFactory.newAUnknownType(node.getLocation()));
183:                         } else if (inOperation && Settings.release == Release.VDM_10
184:                                         && enclfunc != null && enclfunc.getAccess().getPure()
185:                                         && !ot.getPure())
186:                         {
187:                                 TypeCheckerErrors.report(3339,
188:                                                 "Cannot call impure operation '" + node.getRoot()
189:                                                                 + "' from a pure operation", node.getLocation(), node);
190:                                 results.add(AstFactory.newAUnknownType(node.getLocation()));
191:                         } else
192:                         {
193:                                 results.add(operationApply(node, isSimple, ot, question));
194:                         }
195:
196:                         if (inFunction && Settings.release == Release.VDM_10 && ot.getPure()
197:                                         && !inReserved)
198:                         {
199:                                 TypeCheckerErrors.warning(5017, "Pure operation call may not be referentially transparent", node.getLocation(), node);
200:                         }
201:                 }
202:
203:                 if (question.assistantFactory.createPTypeAssistant().isSeq(node.getType(), question.fromModule))
204:                 {
205:                         SSeqType seq = question.assistantFactory.createPTypeAssistant().getSeq(node.getType(), question.fromModule);
206:                         results.add(sequenceApply(node, isSimple, seq, question));
207:                 }
208:
209:                 if (question.assistantFactory.createPTypeAssistant().isMap(node.getType(), question.fromModule))
210:                 {
211:                         SMapType map = question.assistantFactory.createPTypeAssistant().getMap(node.getType(), question.fromModule);
212:                         results.add(mapApply(node, isSimple, map, question));
213:                 }
214:
215:                 if (results.isEmpty())
216:                 {
217:                         TypeCheckerErrors.report(3054, "Type " + node.getType()
218:                                         + " cannot be applied", node.getLocation(), node);
219:                         return AstFactory.newAUnknownType(node.getLocation());
220:                 }
221:
222:                 node.setType(results.getType(node.getLocation()));
223:                 return question.assistantFactory.createPTypeAssistant().possibleConstraint(question.constraint, node.getType(), node.getLocation());
224:         }
225:
226:         @Override public PType defaultSBooleanBinaryExp(SBooleanBinaryExp node,
227:                         TypeCheckInfo question) throws AnalysisException
228:         {
229:                 node.setType(binaryCheck(node, AstFactory.newABooleanBasicType(node.getLocation()), THIS, question));
230:
231:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
232:         }
233:
234:         @Override public PType caseAAndBooleanBinaryExp(AAndBooleanBinaryExp node,
235:                         TypeCheckInfo question) throws AnalysisException
236:         {
237:                 List<QualifiedDefinition> qualified = node.getLeft().apply(question.assistantFactory.getQualificationVisitor(), question);
238:
239:                 for (QualifiedDefinition qdef : qualified)
240:                 {
241:                         qdef.qualifyType();
242:                 }
243:
244:                 PType result = defaultSBooleanBinaryExp(node, question);
245:
246:                 for (QualifiedDefinition qdef : qualified)
247:                 {
248:                         qdef.resetType();
249:                 }
250:
251:                 return result;
252:         }
253:
254:         @Override public PType caseACompBinaryExp(ACompBinaryExp node,
255:                         TypeCheckInfo question) throws AnalysisException
256:         {
257:                 TypeCheckInfo noConstraint = question.newConstraint(null);
258:                 noConstraint.qualifiers = null;
259:
260:                 node.getLeft().apply(THIS, noConstraint);
261:                 node.getRight().apply(THIS, noConstraint);
262:
263:                 PTypeSet results = new PTypeSet(question.assistantFactory);
264:
265:                 if (question.assistantFactory.createPTypeAssistant().isMap(node.getLeft().getType(), question.fromModule))
266:                 {
267:                         if (!question.assistantFactory.createPTypeAssistant().isMap(node.getRight().getType(), question.fromModule))
268:                         {
269:                                 TypeCheckerErrors.report(3068, "Right hand of map 'comp' is not a map", node.getLocation(), node);
270:                                 TypeCheckerErrors.detail("Type", node.getRight().getType());
271:                                 node.setType(AstFactory.newAMapMapType(node.getLocation())); // Unknown
272:                                 // types
273:                                 // types
274:                                 return node.getType();
275:                         }
276:
277:                         SMapType lm = question.assistantFactory.createPTypeAssistant().getMap(node.getLeft().getType(), question.fromModule);
278:                         SMapType rm = question.assistantFactory.createPTypeAssistant().getMap(node.getRight().getType(), question.fromModule);
279:
280:                         if (!question.assistantFactory.getTypeComparator().compatible(lm.getFrom(), rm.getTo()))
281:                         {
282:                                 TypeCheckerErrors.report(3069, "Domain of left should equal range of right in map 'comp'", node.getLocation(), node);
283:                                 TypeCheckerErrors.detail2("Dom", lm.getFrom(), "Rng", rm.getTo());
284:                         }
285:
286:                         results.add(AstFactory.newAMapMapType(node.getLocation(), rm.getFrom(), lm.getTo()));
287:                 }
288:
289:                 if (question.assistantFactory.createPTypeAssistant().isFunction(node.getLeft().getType(), question.fromModule))
290:                 {
291:                         if (!question.assistantFactory.createPTypeAssistant().isFunction(node.getRight().getType(), question.fromModule))
292:                         {
293:                                 TypeCheckerErrors.report(3070, "Right hand of function 'comp' is not a function", node.getLocation(), node);
294:                                 TypeCheckerErrors.detail("Type", node.getRight().getType());
295:                                 node.setType(AstFactory.newAUnknownType(node.getLocation()));
296:                                 return node.getType();
297:                         } else
298:                         {
299:                                 AFunctionType lf = question.assistantFactory.createPTypeAssistant().getFunction(node.getLeft().getType());
300:                                 AFunctionType rf = question.assistantFactory.createPTypeAssistant().getFunction(node.getRight().getType());
301:
302:                                 if (lf.getParameters().size() != 1)
303:                                 {
304:                                         TypeCheckerErrors.report(3071, "Left hand function must have a single parameter", node.getLocation(), node);
305:                                         TypeCheckerErrors.detail("Type", lf);
306:                                 } else if (rf.getParameters().size() != 1)
307:                                 {
308:                                         TypeCheckerErrors.report(3072, "Right hand function must have a single parameter", node.getLocation(), node);
309:                                         TypeCheckerErrors.detail("Type", rf);
310:                                 } else if (!question.assistantFactory.getTypeComparator().compatible(lf.getParameters().get(0), rf.getResult()))
311:                                 {
312:                                         TypeCheckerErrors.report(3073, "Parameter of left should equal result of right in function 'comp'", node.getLocation(), node);
313:                                         TypeCheckerErrors.detail2("Parameter", lf.getParameters().get(0), "Result", rf.getResult());
314:                                 }
315:
316:                                 results.add(AstFactory.newAFunctionType(node.getLocation(), true, rf.getParameters(), lf.getResult()));
317:
318:                         }
319:                 }
320:
321:                 if (results.isEmpty())
322:                 {
323:                         TypeCheckerErrors.report(3074, "Left hand of 'comp' is neither a map nor a function", node.getLocation(), node);
324:                         TypeCheckerErrors.detail("Type", node.getLeft().getType());
325:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
326:                         return node.getType();
327:                 }
328:
329:                 node.setType(results.getType(node.getLocation()));
330:                 return node.getType();
331:         }
332:
333:         @Override public PType caseADomainResByBinaryExp(ADomainResByBinaryExp node,
334:                         TypeCheckInfo question) throws AnalysisException
335:         {
336:                 TypeCheckInfo domConstraint = question;
337:
338:                 if (question.constraint != null
339:                                 && question.assistantFactory.createPTypeAssistant().isMap(question.constraint, question.fromModule))
340:                 {
341:                         PType stype = question.assistantFactory.createPTypeAssistant().getMap(question.constraint, question.fromModule).getFrom();
342:                         domConstraint = question.newConstraint(AstFactory.newASetSetType(node.getLocation(), stype));
343:                 }
344:
345:                 node.getLeft().apply(THIS, domConstraint);
346:                 node.getRight().apply(THIS, question);
347:
348:                 if (!question.assistantFactory.createPTypeAssistant().isSet(node.getLeft().getType(), question.fromModule))
349:                 {
350:                         TypeCheckerErrors.report(3079, "Left of '<-:' is not a set", node.getLocation(), node);
351:                 } else if (!question.assistantFactory.createPTypeAssistant().isMap(node.getRight().getType(), question.fromModule))
352:                 {
353:                         TypeCheckerErrors.report(3080, "Right of '<-:' is not a map", node.getLocation(), node);
354:                 } else
355:                 {
356:                         SSetType set = question.assistantFactory.createPTypeAssistant().getSet(node.getLeft().getType(), question.fromModule);
357:                         SMapType map = question.assistantFactory.createPTypeAssistant().getMap(node.getRight().getType(), question.fromModule);
358:
359:                         if (!question.assistantFactory.getTypeComparator().compatible(set.getSetof(), map.getFrom()))
360:                         {
361:                                 TypeCheckerErrors.report(3081,
362:                                                 "Restriction of map should be set of "
363:                                                                 + map.getFrom(), node.getLocation(), node);
364:                         }
365:                 }
366:
367:                 node.setType(node.getRight().getType());
368:                 return node.getType();
369:         }
370:
371:         @Override public PType caseADomainResToBinaryExp(ADomainResToBinaryExp node,
372:                         TypeCheckInfo question) throws AnalysisException
373:         {
374:                 TypeCheckInfo domConstraint = question;
375:
376:                 if (question.constraint != null
377:                                 && question.assistantFactory.createPTypeAssistant().isMap(question.constraint, question.fromModule))
378:                 {
379:                         PType stype = question.assistantFactory.createPTypeAssistant().getMap(question.constraint, question.fromModule).getFrom();
380:                         domConstraint = question.newConstraint(AstFactory.newASetSetType(node.getLocation(), stype));
381:                 }
382:
383:                 node.getLeft().apply(THIS, domConstraint);
384:                 node.getRight().apply(THIS, question);
385:
386:                 if (!question.assistantFactory.createPTypeAssistant().isSet(node.getLeft().getType(), question.fromModule))
387:                 {
388:                         TypeCheckerErrors.report(3082, "Left of '<:' is not a set", node.getLocation(), node);
389:                         TypeCheckerErrors.detail("Actual", node.getLeft().getType());
390:                 } else if (!question.assistantFactory.createPTypeAssistant().isMap(node.getRight().getType(), question.fromModule))
391:                 {
392:                         TypeCheckerErrors.report(3083, "Right of '<:' is not a map", node.getLocation(), node);
393:                         TypeCheckerErrors.detail("Actual", node.getRight().getType());
394:                 } else
395:                 {
396:                         SSetType set = question.assistantFactory.createPTypeAssistant().getSet(node.getLeft().getType(), question.fromModule);
397:                         SMapType map = question.assistantFactory.createPTypeAssistant().getMap(node.getRight().getType(), question.fromModule);
398:
399:                         if (!question.assistantFactory.getTypeComparator().compatible(set.getSetof(), map.getFrom()))
400:                         {
401:                                 TypeCheckerErrors.report(3084,
402:                                                 "Restriction of map should be set of "
403:                                                                 + map.getFrom(), node.getLocation(), node);
404:                         }
405:                 }
406:
407:                 node.setType(node.getRight().getType());
408:                 return node.getType();
409:         }
410:
411:         @Override public PType caseAEqualsBinaryExp(AEqualsBinaryExp node,
412:                         TypeCheckInfo question) throws AnalysisException
413:         {
414:                 TypeCheckInfo noConstraint = question.newConstraint(null);
415:
416:                 node.getLeft().apply(THIS, noConstraint);
417:                 node.getRight().apply(THIS, noConstraint);
418:
419:                 if (question.assistantFactory.createPTypeAssistant().isUnion(node.getLeft().getType(), question.fromModule))
420:                 {
421:                         IQuestion<TypeCheckInfo> mEqC = question.assistantFactory.getMultipleEqualityChecker();
422:                         node.getLeft().getType().apply(mEqC,question);
423:                 }
424:
425:                 if (question.assistantFactory.createPTypeAssistant().isUnion(node.getRight().getType(), question.fromModule))
426:                 {
427:                         IQuestion<TypeCheckInfo> mEqC = question.assistantFactory.getMultipleEqualityChecker();
428:                         node.getRight().getType().apply(mEqC,question);
429:                 }
430:
431:                 if (!question.assistantFactory.getTypeComparator().compatible(node.getLeft().getType(), node.getRight().getType())
432:                                 || !question.assistantFactory.getTypeComparator().compatible(node.getRight().getType(), node.getLeft().getType()))
433:                 {
434:                         TypeCheckerErrors.report(3087, "Left and right of '=' are incompatible types", node.getLocation(), node);
435:                         TypeCheckerErrors.detail2("Left", node.getLeft().getType(), "Right", node.getRight().getType());
436:                 }
437:
438:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
439:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
440:         }
441:
442:         @Override public PType caseAInSetBinaryExp(AInSetBinaryExp node,
443:                         TypeCheckInfo question) throws AnalysisException
444:         {
445:                 TypeCheckInfo noConstraint = question.newConstraint(null);
446:
447:                 PType ltype = node.getLeft().apply(THIS, noConstraint);
448:                 PType rtype = node.getRight().apply(THIS, noConstraint);
449:
450:                 if (!question.assistantFactory.createPTypeAssistant().isSet(node.getRight().getType(), question.fromModule))
451:                 {
452:                         TypeCheckerErrors.report(3110, "Argument of 'in set' is not a set", node.getLocation(), node);
453:                         TypeCheckerErrors.detail("Actual", rtype);
454:                 } else
455:                 {
456:                         SSetType stype = question.assistantFactory.createPTypeAssistant().getSet(rtype, question.fromModule);
457:
458:                         if (!question.assistantFactory.getTypeComparator().compatible(stype.getSetof(), ltype))
459:                         {
460:                                 TypeCheckerErrors.report(3319, "'in set' expression is always false", node.getLocation(), node);
461:                                 TypeCheckerErrors.detail2("Element", ltype, "Set", stype);
462:                         }
463:                 }
464:
465:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
466:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
467:         }
468:
469:         @Override public PType caseAMapUnionBinaryExp(AMapUnionBinaryExp node,
470:                         TypeCheckInfo question) throws AnalysisException
471:         {
472:                 node.getLeft().apply(THIS, question);
473:                 node.getRight().apply(THIS, question);
474:
475:                 if (!question.assistantFactory.createPTypeAssistant().isMap(node.getLeft().getType(), question.fromModule))
476:                 {
477:                         TypeCheckerErrors.report(3123, "Left hand of 'munion' is not a map", node.getLocation(), node);
478:                         TypeCheckerErrors.detail("Type", node.getLeft().getType());
479:                         node.setType(AstFactory.newAMapMapType(node.getLocation())); // Unknown
480:                         // types
481:                         return node.getType();
482:                 } else if (!question.assistantFactory.createPTypeAssistant().isMap(node.getRight().getType(), question.fromModule))
483:                 {
484:                         TypeCheckerErrors.report(3124, "Right hand of 'munion' is not a map", node.getLocation(), node);
485:                         TypeCheckerErrors.detail("Type", node.getRight().getType());
486:                         node.setType(node.getLeft().getType());
487:                         return node.getType();
488:                 } else
489:                 {
490:                         SMapType ml = question.assistantFactory.createPTypeAssistant().getMap(node.getLeft().getType(), question.fromModule);
491:                         SMapType mr = question.assistantFactory.createPTypeAssistant().getMap(node.getRight().getType(), question.fromModule);
492:
493:                         PTypeSet from = new PTypeSet(question.assistantFactory);
494:                         from.add(ml.getFrom());
495:                         from.add(mr.getFrom());
496:                         PTypeSet to = new PTypeSet(question.assistantFactory);
497:                         to.add(ml.getTo());
498:                         to.add(mr.getTo());
499:
500:                         node.setType(AstFactory.newAMapMapType(node.getLocation(), from.getType(node.getLocation()), to.getType(node.getLocation())));
501:                         return node.getType();
502:                 }
503:         }
504:
505:         @Override public PType caseANotEqualBinaryExp(ANotEqualBinaryExp node,
506:                         TypeCheckInfo question) throws AnalysisException
507:         {
508:                 node.getLeft().apply(THIS, question.newConstraint(null));
509:                 node.getRight().apply(THIS, question.newConstraint(null));
510:
511:                 if (question.assistantFactory.createPTypeAssistant().isUnion(node.getLeft().getType(), question.fromModule))
512:                 {
513:                         IQuestion<TypeCheckInfo> mEqC = question.assistantFactory.getMultipleEqualityChecker();
514:                         node.getLeft().getType().apply(mEqC,question);
515:                 }
516:
517:                 if (question.assistantFactory.createPTypeAssistant().isUnion(node.getRight().getType(), question.fromModule))
518:                 {
519:                         IQuestion<TypeCheckInfo> mEqC = question.assistantFactory.getMultipleEqualityChecker();
520:                         node.getRight().apply(mEqC,question);
521:                 }
522:
523:                 if (!question.assistantFactory.getTypeComparator().compatible(node.getLeft().getType(), node.getRight().getType()))
524:                 {
525:                         TypeCheckerErrors.report(3136, "Left and right of '<>' different types", node.getLocation(), node);
526:                         TypeCheckerErrors.detail2("Left", node.getLeft().getType(), "Right", node.getRight().getType());
527:                 }
528:
529:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
530:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
531:         }
532:
533:
534:         @Override public PType caseANotInSetBinaryExp(ANotInSetBinaryExp node,
535:                         TypeCheckInfo question) throws AnalysisException
536:         {
537:                 TypeCheckInfo noConstraint = question.newConstraint(null);
538:
539:                 PType ltype = node.getLeft().apply(THIS, noConstraint);
540:                 PType rtype = node.getRight().apply(THIS, noConstraint);
541:
542:                 if (!question.assistantFactory.createPTypeAssistant().isSet(node.getRight().getType(), question.fromModule))
543:                 {
544:                         TypeCheckerErrors.report(3138, "Argument of 'not in set' is not a set", node.getLocation(), node);
545:                         TypeCheckerErrors.detail("Actual", node.getRight().getType());
546:                 } else
547:                 {
548:                         SSetType stype = question.assistantFactory.createPTypeAssistant().getSet(rtype, question.fromModule);
549:
550:                         if (!question.assistantFactory.getTypeComparator().compatible(stype.getSetof(), ltype))
551:                         {
552:                                 TypeCheckerErrors.report(3320, "'not in set' expression is always true", node.getLocation(), node);
553:                                 TypeCheckerErrors.detail2("Element", ltype, "Set", stype);
554:                         }
555:                 }
556:
557:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
558:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
559:         }
560:
561:         @Override public PType caseADivNumericBinaryExp(ADivNumericBinaryExp node,
562:                         TypeCheckInfo question) throws AnalysisException
563:         {
564:                 checkNumeric(node, THIS, question.newConstraint(null));
565:                 node.setType(AstFactory.newAIntNumericBasicType(node.getLocation()));
566:                 return node.getType();
567:         }
568:
569:         @Override public PType caseADivideNumericBinaryExp(
570:                         ADivideNumericBinaryExp node, TypeCheckInfo question)
571:                         throws AnalysisException
572:         {
573:                 checkNumeric(node, THIS, question.newConstraint(null));
574:                 node.setType(AstFactory.newARealNumericBasicType(node.getLocation()));
575:                 return node.getType();
576:         }
577:
578:         @Override public PType caseAGreaterEqualNumericBinaryExp(
579:                         AGreaterEqualNumericBinaryExp node, TypeCheckInfo question)
580:                         throws AnalysisException
581:         {
582:                 checkOrdered(node, THIS, question.newConstraint(null));
583:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
584:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
585:         }
586:
587:         @Override public PType caseAGreaterNumericBinaryExp(
588:                         AGreaterNumericBinaryExp node, TypeCheckInfo question)
589:                         throws AnalysisException
590:         {
591:                 checkOrdered(node, THIS, question.newConstraint(null));
592:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
593:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
594:         }
595:
596:         @Override public PType caseAModNumericBinaryExp(AModNumericBinaryExp node,
597:                         TypeCheckInfo question) throws AnalysisException
598:         {
599:                 checkNumeric(node, THIS, question.newConstraint(null));
600:                 node.setType(AstFactory.newAIntNumericBasicType(node.getLocation()));
601:                 return node.getType();
602:         }
603:
604:         @Override public PType caseAPlusNumericBinaryExp(APlusNumericBinaryExp node,
605:                         TypeCheckInfo question) throws AnalysisException
606:         {
607:                 checkNumeric(node, THIS, question.newConstraint(null));
608:
609:                 SNumericBasicType ln = question.assistantFactory.createPTypeAssistant().getNumeric(node.getLeft().getType(), question.fromModule);
610:                 SNumericBasicType rn = question.assistantFactory.createPTypeAssistant().getNumeric(node.getRight().getType(), question.fromModule);
611:
612:                 if (ln instanceof ARealNumericBasicType)
613:                 {
614:                         node.setType(ln);
615:                         return ln;
616:                 } else if (rn instanceof ARealNumericBasicType)
617:                 {
618:                         node.setType(rn);
619:                         return rn;
620:                 } else if (ln instanceof AIntNumericBasicType)
621:                 {
622:                         node.setType(ln);
623:                         return ln;
624:                 } else if (rn instanceof AIntNumericBasicType)
625:                 {
626:                         node.setType(rn);
627:                         return rn;
628:                 } else if (ln instanceof ANatNumericBasicType
629:                                 && rn instanceof ANatNumericBasicType)
630:                 {
631:                         node.setType(ln);
632:                         return ln;
633:                 } else
634:                 {
635:                         node.setType(AstFactory.newANatOneNumericBasicType(ln.getLocation()));
636:                         return node.getType();
637:                 }
638:         }
639:
640:         @Override public PType caseARemNumericBinaryExp(ARemNumericBinaryExp node,
641:                         TypeCheckInfo question) throws AnalysisException
642:         {
643:                 checkNumeric(node, THIS, question.newConstraint(null));
644:                 node.setType(AstFactory.newAIntNumericBasicType(node.getLocation()));
645:                 return node.getType();
646:         }
647:
648:         @Override public PType caseASubtractNumericBinaryExp(
649:                         ASubtractNumericBinaryExp node, TypeCheckInfo question)
650:                         throws AnalysisException
651:         {
652:                 checkNumeric(node, THIS, question.newConstraint(null));
653:                 
654:                 if (question.assistantFactory.createPTypeAssistant().isType(node.getLeft().getType(), ARealNumericBasicType.class) ||
655:                         question.assistantFactory.createPTypeAssistant().isType(node.getRight().getType(), ARealNumericBasicType.class))
656:                 {
657:                         node.setType(AstFactory.newARealNumericBasicType(node.getLocation()));
658:                         return node.getType();
659:                 }
660:                 else if (question.assistantFactory.createPTypeAssistant().isType(node.getLeft().getType(), ARationalNumericBasicType.class) ||
661:                                  question.assistantFactory.createPTypeAssistant().isType(node.getRight().getType(), ARationalNumericBasicType.class))
662:                 {
663:                         node.setType(AstFactory.newARationalNumericBasicType(node.getLocation()));
664:                         return node.getType();
665:                 }
666:                 else
667:                 {
668:                         node.setType(AstFactory.newAIntNumericBasicType(node.getLocation()));
669:                         return node.getType();
670:                 }
671:         }
672:
673:         @Override public PType caseATimesNumericBinaryExp(
674:                         ATimesNumericBinaryExp node, TypeCheckInfo question)
675:                         throws AnalysisException
676:         {
677:                 checkNumeric(node, THIS, question.newConstraint(null));
678:
679:                 SNumericBasicType ln = question.assistantFactory.createPTypeAssistant().getNumeric(node.getLeft().getType(), question.fromModule);
680:                 SNumericBasicType rn = question.assistantFactory.createPTypeAssistant().getNumeric(node.getRight().getType(), question.fromModule);
681:
682:                 if (ln instanceof ARealNumericBasicType)
683:                 {
684:                         node.setType(ln);
685:                         return ln;
686:                 } else if (rn instanceof ARealNumericBasicType)
687:                 {
688:                         node.setType(rn);
689:                         return rn;
690:                 } else if (ln instanceof AIntNumericBasicType)
691:                 {
692:                         node.setType(ln);
693:                         return ln;
694:                 } else if (rn instanceof AIntNumericBasicType)
695:                 {
696:                         node.setType(rn);
697:                         return rn;
698:                 } else if (ln instanceof ANatNumericBasicType)
699:                 {
700:                         node.setType(ln);
701:                         return ln;
702:                 } else if (rn instanceof ANatNumericBasicType)
703:                 {
704:                         node.setType(rn);
705:                         return rn;
706:                 } else
707:                 {
708:                         node.setType(AstFactory.newANatOneNumericBasicType(ln.getLocation()));
709:                         return node.getType();
710:                 }
711:         }
712:
713:         @Override public PType caseAPlusPlusBinaryExp(APlusPlusBinaryExp node,
714:                         TypeCheckInfo question) throws AnalysisException
715:         {
716:                 TypeCheckInfo leftcons = question.newConstraint(null);
717:                 TypeCheckInfo mapcons = question.newConstraint(null);
718:
719:                 if (question.constraint != null
720:                                 && question.assistantFactory.createPTypeAssistant().isSeq(question.constraint, question.fromModule))
721:                 {
722:                         SSeqType st = question.assistantFactory.createPTypeAssistant().getSeq(question.constraint, question.fromModule);
723:                         mapcons = question.newConstraint(AstFactory.newAMapMapType(node.getLocation(), AstFactory.newANatOneNumericBasicType(node.getLocation()), st.getSeqof()));
724:                         leftcons = question.newConstraint(AstFactory.newASeqSeqType(node.getLocation()));
725:                 } else if (question.constraint != null
726:                                 && question.assistantFactory.createPTypeAssistant().isMap(question.constraint, question.fromModule))
727:                 {
728:                         SMapType mt = question.assistantFactory.createPTypeAssistant().getMap(question.constraint, question.fromModule);
729:                         mapcons = question.newConstraint(mt);
730:                         leftcons = question.newConstraint(AstFactory.newAMapMapType(node.getLocation(), mt.getFrom(), AstFactory.newAUnknownType(node.getLocation())));
731:                 }
732:
733:                 node.getLeft().apply(THIS, leftcons);
734:                 node.getRight().apply(THIS, mapcons);
735:
736:                 PTypeSet result = new PTypeSet(question.assistantFactory);
737:
738:                 boolean unique =
739:                                 !question.assistantFactory.createPTypeAssistant().isUnion(node.getLeft().getType(), question.fromModule)
740:                                                 && !question.assistantFactory.createPTypeAssistant().isUnion(node.getRight().getType(), question.fromModule);
741:
742:                 if (question.assistantFactory.createPTypeAssistant().isMap(node.getLeft().getType(), question.fromModule))
743:                 {
744:                         if (!question.assistantFactory.createPTypeAssistant().isMap(node.getRight().getType(), question.fromModule))
745:                         {
746:                                 TypeCheckerErrors.concern(unique, 3141, "Right hand of '++' is not a map", node.getLocation(), node);
747:                                 TypeCheckerErrors.detail(unique, "Type", node.getRight().getType());
748:                                 node.setType(AstFactory.newAMapMapType(node.getLocation())); // Unknown
749:                                 // types
750:                                 return node.getType();
751:                         }
752:
753:                         SMapType lm = question.assistantFactory.createPTypeAssistant().getMap(node.getLeft().getType(), question.fromModule);
754:                         SMapType rm = question.assistantFactory.createPTypeAssistant().getMap(node.getRight().getType(), question.fromModule);
755:
756:                         PTypeSet domain = new PTypeSet(question.assistantFactory);
757:                         domain.add(lm.getFrom());
758:                         domain.add(rm.getFrom());
759:                         PTypeSet range = new PTypeSet(question.assistantFactory);
760:                         range.add(lm.getTo());
761:                         range.add(rm.getTo());
762:
763:                         result.add(AstFactory.newAMapMapType(node.getLocation(), domain.getType(node.getLocation()), range.getType(node.getLocation())));
764:                 }
765:
766:                 if (question.assistantFactory.createPTypeAssistant().isSeq(node.getLeft().getType(), question.fromModule))
767:                 {
768:                         SSeqType st = question.assistantFactory.createPTypeAssistant().getSeq(node.getLeft().getType(), question.fromModule);
769:
770:                         if (!question.assistantFactory.createPTypeAssistant().isMap(node.getRight().getType(), question.fromModule))
771:                         {
772:                                 TypeCheckerErrors.concern(unique, 3142, "Right hand of '++' is not a map", node.getLocation(), node);
773:                                 TypeCheckerErrors.detail(unique, "Type", node.getRight().getType());
774:                                 result.add(st);
775:                         } else
776:                         {
777:                                 SMapType mr = question.assistantFactory.createPTypeAssistant().getMap(node.getRight().getType(), question.fromModule);
778:
779:                                 if (!question.assistantFactory.createPTypeAssistant().isType(mr.getFrom(), SNumericBasicType.class))
780:                                 {
781:                                         TypeCheckerErrors.concern(unique, 3143, "Domain of right hand of '++' must be nat1", node.getLocation(), node);
782:                                         TypeCheckerErrors.detail(unique, "Type", mr.getFrom());
783:                                 }
784:
785:                                 PTypeSet type = new PTypeSet(question.assistantFactory);
786:                                 type.add(st.getSeqof());
787:                                 type.add(mr.getTo());
788:                                 result.add(AstFactory.newASeqSeqType(node.getLocation(), type.getType(node.getLocation())));
789:                         }
790:                 }
791:
792:                 if (result.isEmpty())
793:                 {
794:                         TypeCheckerErrors.report(3144, "Left of '++' is neither a map nor a sequence", node.getLocation(), node);
795:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
796:                         return node.getType();
797:                 }
798:
799:                 node.setType(result.getType(node.getLocation()));
800:                 return node.getType();
801:         }
802:
803:         @Override public PType caseAProperSubsetBinaryExp(
804:                         AProperSubsetBinaryExp node, TypeCheckInfo question)
805:                         throws AnalysisException
806:         {
807:                 TypeCheckInfo noConstraint = question.newConstraint(null);
808:
809:                 node.getLeft().apply(THIS, noConstraint);
810:                 node.getRight().apply(THIS, noConstraint);
811:
812:                 PType ltype = node.getLeft().getType();
813:                 PType rtype = node.getRight().getType();
814:
815:                 if (question.assistantFactory.createPTypeAssistant().isSet(ltype, question.fromModule)
816:                                 && question.assistantFactory.createPTypeAssistant().isSet(rtype, question.fromModule)
817:                                 && !question.assistantFactory.getTypeComparator().compatible(ltype, rtype))
818:                 {
819:                         TypeCheckerErrors.report(3335, "Subset will only be true if the LHS set is empty", node.getLocation(), node);
820:                         TypeCheckerErrors.detail("Left", ltype);
821:                         TypeCheckerErrors.detail("Right", rtype);
822:                 }
823:
824:                 if (!question.assistantFactory.createPTypeAssistant().isSet(ltype, question.fromModule))
825:                 {
826:                         TypeCheckerErrors.report(3146, "Left hand of " + node.getOp()
827:                                         + " is not a set", node.getLocation(), node);
828:                 }
829:
830:                 if (!question.assistantFactory.createPTypeAssistant().isSet(rtype, question.fromModule))
831:                 {
832:                         TypeCheckerErrors.report(3147, "Right hand of " + node.getOp()
833:                                         + " is not a set", node.getLocation(), node);
834:                 }
835:
836:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
837:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
838:         }
839:
840:         @Override public PType caseARangeResByBinaryExp(ARangeResByBinaryExp node,
841:                         TypeCheckInfo question) throws AnalysisException
842:         {
843:                 TypeCheckInfo rngConstraint = question;
844:
845:                 if (question.constraint != null
846:                                 && question.assistantFactory.createPTypeAssistant().isMap(question.constraint, question.fromModule))
847:                 {
848:                         PType stype = question.assistantFactory.createPTypeAssistant().getMap(question.constraint, question.fromModule).getTo();
849:                         rngConstraint = question.newConstraint(AstFactory.newASetSetType(node.getLocation(), stype));
850:                 }
851:
852:                 node.getLeft().apply(THIS, question);
853:                 node.getRight().apply(THIS, rngConstraint);
854:
855:                 PType ltype = node.getLeft().getType();
856:                 PType rtype = node.getRight().getType();
857:
858:                 if (!question.assistantFactory.createPTypeAssistant().isMap(ltype, question.fromModule))
859:                 {
860:                         TypeCheckerErrors.report(3148, "Left of ':->' is not a map", node.getLocation(), node);
861:                 } else if (!question.assistantFactory.createPTypeAssistant().isSet(rtype, question.fromModule))
862:                 {
863:                         TypeCheckerErrors.report(3149, "Right of ':->' is not a set", node.getLocation(), node);
864:                 } else
865:                 {
866:                         SMapType map = question.assistantFactory.createPTypeAssistant().getMap(ltype, question.fromModule);
867:                         SSetType set = question.assistantFactory.createPTypeAssistant().getSet(rtype, question.fromModule);
868:
869:                         if (!question.assistantFactory.getTypeComparator().compatible(set.getSetof(), map.getTo()))
870:                         {
871:                                 TypeCheckerErrors.report(3150,
872:                                                 "Restriction of map should be set of "
873:                                                                 + map.getTo(), node.getLocation(), node);
874:                         }
875:                 }
876:
877:                 node.setType(ltype);
878:                 return ltype;
879:         }
880:
881:         @Override public PType caseARangeResToBinaryExp(ARangeResToBinaryExp node,
882:                         TypeCheckInfo question) throws AnalysisException
883:         {
884:                 TypeCheckInfo rngConstraint = question;
885:
886:                 if (question.constraint != null
887:                                 && question.assistantFactory.createPTypeAssistant().isMap(question.constraint, question.fromModule))
888:                 {
889:                         PType stype = question.assistantFactory.createPTypeAssistant().getMap(question.constraint, question.fromModule).getTo();
890:                         rngConstraint = question.newConstraint(AstFactory.newASetSetType(node.getLocation(), stype));
891:                 }
892:
893:                 node.getLeft().apply(THIS, question);
894:                 node.getRight().apply(THIS, rngConstraint);
895:
896:                 PType ltype = node.getLeft().getType();
897:                 PType rtype = node.getRight().getType();
898:
899:                 if (!question.assistantFactory.createPTypeAssistant().isMap(ltype, question.fromModule))
900:                 {
901:                         TypeCheckerErrors.report(3151, "Left of ':>' is not a map", node.getLocation(), node);
902:                 } else if (!question.assistantFactory.createPTypeAssistant().isSet(rtype, question.fromModule))
903:                 {
904:                         TypeCheckerErrors.report(3152, "Right of ':>' is not a set", node.getLocation(), node);
905:                 } else
906:                 {
907:                         SMapType map = question.assistantFactory.createPTypeAssistant().getMap(ltype, question.fromModule);
908:                         SSetType set = question.assistantFactory.createPTypeAssistant().getSet(rtype, question.fromModule);
909:
910:                         if (!question.assistantFactory.getTypeComparator().compatible(set.getSetof(), map.getTo()))
911:                         {
912:                                 TypeCheckerErrors.report(3153,
913:                                                 "Restriction of map should be set of "
914:                                                                 + map.getTo(), node.getLocation(), node);
915:                         }
916:                 }
917:                 node.setType(ltype);
918:                 return ltype;
919:         }
920:
921:         @Override public PType caseASeqConcatBinaryExp(ASeqConcatBinaryExp node,
922:                         TypeCheckInfo question) throws AnalysisException
923:         {
924:                 TypeCheckInfo lrconstraint = question;
925:                 
926:                 if (question.constraint != null
927:                                 && question.assistantFactory.createPTypeAssistant().isSeq(question.constraint, question.fromModule))
928:                 {
929:                         SSeqType stype = question.assistantFactory.createPTypeAssistant().getSeq(question.constraint, question.fromModule);
930:                         
931:                         if (stype instanceof ASeq1SeqType)
932:                         {
933:                                 stype = AstFactory.newASeqSeqType(node.getLocation(), stype.getSeqof());
934:                                 lrconstraint = question.newConstraint(stype);
935:                         }
936:                 }
937:
938:                 node.getLeft().apply(THIS, lrconstraint);
939:                 node.getRight().apply(THIS, lrconstraint);
940:
941:                 PType ltype = node.getLeft().getType();
942:                 PType rtype = node.getRight().getType();
943:
944:                 if (!question.assistantFactory.createPTypeAssistant().isSeq(ltype, question.fromModule))
945:                 {
946:                         TypeCheckerErrors.report(3157, "Left hand of '^' is not a sequence", node.getLocation(), node);
947:                         ltype = AstFactory.newASeqSeqType(node.getLocation(), AstFactory.newAUnknownType(node.getLocation()));
948:                 }
949:
950:                 if (!question.assistantFactory.createPTypeAssistant().isSeq(rtype, question.fromModule))
951:                 {
952:                         TypeCheckerErrors.report(3158, "Right hand of '^' is not a sequence", node.getLocation(), node);
953:                         rtype = AstFactory.newASeqSeqType(node.getLocation(), AstFactory.newAUnknownType(node.getLocation()));
954:                 }
955:
956:                 PType lof = question.assistantFactory.createPTypeAssistant().getSeq(ltype, question.fromModule);
957:                 PType rof = question.assistantFactory.createPTypeAssistant().getSeq(rtype, question.fromModule);
958:                 boolean seq1 =
959:                                 lof instanceof ASeq1SeqType || rof instanceof ASeq1SeqType;
960:
961:                 lof = ((SSeqType) lof).getSeqof();
962:                 rof = ((SSeqType) rof).getSeqof();
963:                 PTypeSet ts = new PTypeSet(question.assistantFactory);
964:                 ts.add(lof);
965:                 ts.add(rof);
966:
967:                 node.setType(seq1 ?
968:                                 AstFactory.newASeq1SeqType(node.getLocation(), ts.getType(node.getLocation())) :
969:                                 AstFactory.newASeqSeqType(node.getLocation(), ts.getType(node.getLocation())));
970:                 return node.getType();
971:         }
972:
973:         @Override public PType caseASetDifferenceBinaryExp(
974:                         ASetDifferenceBinaryExp node, TypeCheckInfo question)
975:                         throws AnalysisException
976:         {
977:                 TypeCheckInfo noConstraint = question.newConstraint(null);
978:
979:                 node.getLeft().apply(THIS, noConstraint);
980:                 node.getRight().apply(THIS, noConstraint);
981:
982:                 PType ltype = node.getLeft().getType();
983:                 PType rtype = node.getRight().getType();
984:
985:                 if (!question.assistantFactory.createPTypeAssistant().isSet(ltype, question.fromModule))
986:                 {
987:                         TypeCheckerErrors.report(3160, "Left hand of '\\' is not a set", node.getLocation(), node);
988:                 }
989:
990:                 if (!question.assistantFactory.createPTypeAssistant().isSet(rtype, question.fromModule))
991:                 {
992:                         TypeCheckerErrors.report(3161, "Right hand of '\\' is not a set", node.getLocation(), node);
993:                 }
994:
995:                 if (!question.assistantFactory.getTypeComparator().compatible(ltype, rtype))
996:                 {
997:                         TypeCheckerErrors.report(3162, "Left and right of '\\' are different types", node.getLocation(), node);
998:                         TypeCheckerErrors.detail2("Left", ltype, "Right", rtype);
999:                 }
1000:
1001:                 if (ltype instanceof ASet1SetType)
1002:                 {
1003:                         ASet1SetType set1 = (ASet1SetType) ltype;
1004:                         ltype = AstFactory.newASetSetType(node.getLocation(), set1.getSetof());
1005:                 }
1006:
1007:                 node.setType(ltype);
1008:                 return ltype;
1009:         }
1010:
1011:         @Override public PType caseASetIntersectBinaryExp(
1012:                         ASetIntersectBinaryExp node, TypeCheckInfo question)
1013:                         throws AnalysisException
1014:         {
1015:                 TypeCheckInfo noConstraint = question.newConstraint(null);
1016:
1017:                 node.getLeft().apply(THIS, noConstraint);
1018:                 node.getRight().apply(THIS, noConstraint);
1019:
1020:                 PType ltype = node.getLeft().getType();
1021:                 PType rtype = node.getRight().getType();
1022:
1023:                 PType lset = null;
1024:                 PType rset = null;
1025:
1026:                 PTypeAssistantTC assistant = question.assistantFactory.createPTypeAssistant();
1027:
1028:                 if (!assistant.isSet(ltype, question.fromModule))
1029:                 {
1030:                         TypeCheckerErrors.report(3163, "Left hand of " + node.getLocation()
1031:                                         + " is not a set", node.getLocation(), node);
1032:                 } else
1033:                 {
1034:                         lset = assistant.getSet(ltype, question.fromModule).getSetof();
1035:                 }
1036:
1037:                 if (!assistant.isSet(rtype, question.fromModule))
1038:                 {
1039:                         TypeCheckerErrors.report(3164, "Right hand of " + node.getLocation()
1040:                                         + " is not a set", node.getLocation(), node);
1041:                 } else
1042:                 {
1043:                         rset = assistant.getSet(rtype, question.fromModule).getSetof();
1044:                 }
1045:
1046:                 PType result = ltype; // A guess
1047:
1048:                 if (lset != null && !assistant.isUnknown(lset) && rset != null
1049:                                 && !assistant.isUnknown(rset))
1050:                 {
1051:                         PType interTypes = question.assistantFactory.getTypeComparator().intersect(lset, rset);
1052:
1053:                         if (interTypes == null)
1054:                         {
1055:                                 TypeCheckerErrors.report(3165, "Left and right of intersect are different types", node.getLocation(), node);
1056:                                 TypeCheckerErrors.detail2("Left", ltype, "Right", rtype);
1057:                         } else
1058:                         {
1059:                                 result = AstFactory.newASetSetType(node.getLocation(), interTypes);
1060:                         }
1061:                 }
1062:
1063:                 node.setType(result);
1064:                 return result;
1065:         }
1066:
1067:         @Override public PType caseASetUnionBinaryExp(ASetUnionBinaryExp node,
1068:                         TypeCheckInfo question) throws AnalysisException
1069:         {
1070:                 node.getLeft().apply(THIS, question);
1071:                 node.getRight().apply(THIS, question);
1072:
1073:                 PType ltype = node.getLeft().getType();
1074:                 PType rtype = node.getRight().getType();
1075:
1076:                 if (!question.assistantFactory.createPTypeAssistant().isSet(ltype, question.fromModule))
1077:                 {
1078:                         TypeCheckerErrors.report(3168, "Left hand of " + node.getOp()
1079:                                         + " is not a set", node.getLocation(), node);
1080:                         ltype = AstFactory.newASetSetType(node.getLocation());
1081:                 }
1082:
1083:                 if (!question.assistantFactory.createPTypeAssistant().isSet(rtype, question.fromModule))
1084:                 {
1085:                         TypeCheckerErrors.report(3169, "Right hand of " + node.getOp()
1086:                                         + " is not a set", node.getLocation(), node);
1087:                         rtype = AstFactory.newASetSetType(node.getLocation());
1088:                 }
1089:
1090:                 PType lof = question.assistantFactory.createPTypeAssistant().getSet(ltype, question.fromModule).getSetof();
1091:                 PType rof = question.assistantFactory.createPTypeAssistant().getSet(rtype, question.fromModule).getSetof();
1092:                 boolean set1 =
1093:                                 lof instanceof ASet1SetType || rof instanceof ASet1SetType;
1094:
1095:                 PTypeSet result = new PTypeSet(question.assistantFactory);
1096:                 result.add(lof);
1097:                 result.add(rof);
1098:
1099:                 node.setType(set1 ?
1100:                                 AstFactory.newASet1SetType(node.getLocation(), result.getType(node.getLocation())) :
1101:                                 AstFactory.newASetSetType(node.getLocation(), result.getType(node.getLocation())));
1102:
1103:                 return node.getType();
1104:         }
1105:
1106:         @Override public PType caseAStarStarBinaryExp(AStarStarBinaryExp node,
1107:                         TypeCheckInfo question) throws AnalysisException
1108:         {
1109:                 TypeCheckInfo noConstraint = question.newConstraint(null);
1110:
1111:                 node.getLeft().apply(THIS, noConstraint);
1112:                 node.getRight().apply(THIS, noConstraint);
1113:
1114:                 PType ltype = node.getLeft().getType();
1115:                 PType rtype = node.getRight().getType();
1116:
1117:                 if (question.assistantFactory.createPTypeAssistant().isMap(ltype, question.fromModule))
1118:                 {
1119:                         question.assistantFactory.createPTypeAssistant();
1120:                         if (!question.assistantFactory.createPTypeAssistant().isNumeric(rtype, question.fromModule))
1121:                         {
1122:                                 // rtype.report(3170,
1123:                                 // "Map iterator expects nat as right hand arg");
1124:                                 TypeCheckerErrors.report(3170, "Map iterator expects nat as right hand arg", node.getRight().getLocation(), rtype);
1125:                         }
1126:                 } else if (question.assistantFactory.createPTypeAssistant().isFunction(ltype, question.fromModule))
1127:                 {
1128:                         question.assistantFactory.createPTypeAssistant();
1129:                         if (!question.assistantFactory.createPTypeAssistant().isNumeric(rtype, question.fromModule))
1130:                         {
1131:                                 TypeCheckerErrors.report(3171, "Function iterator expects nat as right hand arg", node.getRight().getLocation(), rtype);
1132:                         }
1133:                 } else
1134:                 {
1135:                         question.assistantFactory.createPTypeAssistant();
1136:                         if (question.assistantFactory.createPTypeAssistant().isNumeric(ltype, question.fromModule))
1137:                         {
1138:                                 question.assistantFactory.createPTypeAssistant();
1139:                                 if (!question.assistantFactory.createPTypeAssistant().isNumeric(rtype, question.fromModule))
1140:                                 {
1141:                                         TypeCheckerErrors.report(3172, "'**' expects number as right hand arg", node.getRight().getLocation(), rtype);
1142:                                 }
1143:                         } else
1144:                         {
1145:                                 TypeCheckerErrors.report(3173, "First arg of '**' must be a map, function or number", node.getLocation(), node);
1146:                                 node.setType(AstFactory.newAUnknownType(node.getLocation()));
1147:                                 return node.getType();
1148:                         }
1149:                 }
1150:
1151:                 node.setType(ltype);
1152:                 return ltype;
1153:         }
1154:
1155:         @Override public PType caseASubsetBinaryExp(ASubsetBinaryExp node,
1156:                         TypeCheckInfo question) throws AnalysisException
1157:         {
1158:                 TypeCheckInfo noConstraint = question.newConstraint(null);
1159:
1160:                 node.getLeft().apply(THIS, noConstraint);
1161:                 node.getRight().apply(THIS, noConstraint);
1162:
1163:                 PType ltype = node.getLeft().getType();
1164:                 PType rtype = node.getRight().getType();
1165:
1166:                 if (question.assistantFactory.createPTypeAssistant().isSet(ltype, question.fromModule)
1167:                                 && question.assistantFactory.createPTypeAssistant().isSet(rtype, question.fromModule)
1168:                                 && !question.assistantFactory.getTypeComparator().compatible(ltype, rtype))
1169:                 {
1170:                         TypeCheckerErrors.report(3335, "Subset will only be true if the LHS set is empty", node.getLocation(), node);
1171:                         TypeCheckerErrors.detail("Left", ltype);
1172:                         TypeCheckerErrors.detail("Right", rtype);
1173:                 }
1174:
1175:                 if (!question.assistantFactory.createPTypeAssistant().isSet(ltype, question.fromModule))
1176:                 {
1177:                         TypeCheckerErrors.report(3177, "Left hand of " + node.getOp()
1178:                                         + " is not a set", node.getLocation(), node);
1179:                         TypeCheckerErrors.detail("Type", ltype);
1180:                 }
1181:
1182:                 if (!question.assistantFactory.createPTypeAssistant().isSet(rtype, question.fromModule))
1183:                 {
1184:                         TypeCheckerErrors.report(3178, "Right hand of " + node.getOp()
1185:                                         + " is not a set", node.getLocation(), node);
1186:                         TypeCheckerErrors.detail("Type", rtype);
1187:                 }
1188:
1189:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
1190:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
1191:         }
1192:
1193:         @Override public PType caseABooleanConstExp(ABooleanConstExp node,
1194:                         TypeCheckInfo question)
1195:         {
1196:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
1197:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
1198:         }
1199:
1200:         @Override public PType caseACasesExp(ACasesExp node, TypeCheckInfo question)
1201:                         throws AnalysisException
1202:         {
1203:                 TypeCheckInfo noConstraint = question.newConstraint(null);
1204:                 question.qualifiers = null;
1205:
1206:                 PType expType = node.getExpression().apply(THIS, noConstraint);
1207:
1208:                 PTypeSet rtypes = new PTypeSet(question.assistantFactory);
1209:
1210:                 for (ACaseAlternative c : node.getCases())
1211:                 {
1212:                         rtypes.add(typeCheck(c, THIS, question, expType));
1213:                 }
1214:
1215:                 if (node.getOthers() != null)
1216:                 {
1217:                         rtypes.add(node.getOthers().apply(THIS, question));
1218:                 }
1219:
1220:                 node.setType(rtypes.getType(node.getLocation()));
1221:                 return node.getType();
1222:         }
1223:
1224:         @Override public PType caseACharLiteralExp(ACharLiteralExp node,
1225:                         TypeCheckInfo question)
1226:         {
1227:                 node.setType(AstFactory.newACharBasicType(node.getLocation()));
1228:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
1229:         }
1230:
1231:         @Override public PType caseAElseIfExp(AElseIfExp node,
1232:                         TypeCheckInfo question) throws AnalysisException
1233:         {
1234:                 node.setType(typeCheckAElseIf(node, node.getLocation(), node.getElseIf(), node.getThen(), question));
1235:                 return node.getType();
1236:         }
1237:
1238:         @Override public PType caseAExists1Exp(AExists1Exp node,
1239:                         TypeCheckInfo question) throws AnalysisException
1240:         {
1241:                 node.setDef(AstFactory.newAMultiBindListDefinition(node.getBind().getLocation(), question.assistantFactory.createPBindAssistant().getMultipleBindList(node.getBind())));
1242:                 node.getDef().apply(THIS, question.newConstraint(null));
1243:                 Environment local = new FlatCheckedEnvironment(question.assistantFactory, node.getDef(), question.env, question.scope);
1244:
1245:                 if (node.getBind() instanceof ATypeBind)
1246:                 {
1247:                         ATypeBind tb = (ATypeBind) node.getBind();
1248:                         question.assistantFactory.createATypeBindAssistant().typeResolve(tb, THIS, question);
1249:                 }
1250:
1251:                 question.qualifiers = null;
1252:                 if (!question.assistantFactory.createPTypeAssistant().isType(node.getPredicate().apply(THIS, new TypeCheckInfo(question.assistantFactory, local, question.scope, null, AstFactory.newABooleanBasicType(node.getLocation()), null, question.fromModule, question.mandatory)), ABooleanBasicType.class))
1253:                 {
1254:                         TypeCheckerErrors.report(3088, "Predicate is not boolean", node.getPredicate().getLocation(), node.getPredicate());
1255:                 }
1256:
1257:                 local.unusedCheck();
1258:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
1259:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
1260:         }
1261:
1262:         @Override public PType caseAExistsExp(AExistsExp node,
1263:                         TypeCheckInfo question) throws AnalysisException
1264:         {
1265:                 PDefinition def = AstFactory.newAMultiBindListDefinition(node.getLocation(), node.getBindList());
1266:                 def.apply(THIS, question.newConstraint(null));
1267:                 def.setNameScope(NameScope.LOCAL);
1268:                 Environment local = new FlatCheckedEnvironment(question.assistantFactory, def, question.env, question.scope);
1269:                 question = new TypeCheckInfo(question.assistantFactory, local, question.scope, null, AstFactory.newABooleanBasicType(node.getLocation()), null, question.fromModule, question.mandatory);
1270:                 if (!question.assistantFactory.createPTypeAssistant().isType(node.getPredicate().apply(THIS, question), ABooleanBasicType.class))
1271:                 {
1272:                         TypeCheckerErrors.report(3089, "Predicate is not boolean", node.getPredicate().getLocation(), node.getPredicate());
1273:                 }
1274:
1275:                 local.unusedCheck();
1276:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
1277:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
1278:         }
1279:
1280:         @Override public PType caseAFieldExp(AFieldExp node, TypeCheckInfo question)
1281:                         throws AnalysisException
1282:         {
1283:                 PType root = node.getObject().apply(THIS, new TypeCheckInfo(question.assistantFactory, question.env, question.scope).newModule(question.fromModule));
1284:
1285:                 if (question.assistantFactory.createPTypeAssistant().isUnknown(root))
1286:                 {
1287:                         node.setMemberName(new LexNameToken("?", node.getField()));
1288:                         node.setType(root);
1289:                         return root;
1290:                 }
1291:
1292:                 PTypeSet results = new PTypeSet(question.assistantFactory);
1293:                 boolean recOrClass = false;
1294:                 boolean unique = !question.assistantFactory.createPTypeAssistant().isUnion(root, question.fromModule);
1295:
1296:                 if (question.assistantFactory.createPTypeAssistant().isRecord(root, question.fromModule))
1297:                 {
1298:                         ARecordInvariantType rec = question.assistantFactory.createPTypeAssistant().getRecord(root, question.fromModule);
1299:                         AFieldField cf = question.assistantFactory.createARecordInvariantTypeAssistant().findField(rec, node.getField().getName());
1300:                         
1301:                 // Check for state access via state record
1302:                 AStateDefinition state = question.env.findStateDefinition();
1303:                 
1304:                 if (state != null && state.getRecordType().equals(rec))
1305:                 {
1306:                         LexNameToken sname = new LexNameToken(rec.getName().getModule(), node.getField().getName(), node.getLocation());
1307:                         question.assistantFactory.createPDefinitionAssistant().findName(state, sname, NameScope.STATE);                // Lookup marks as used
1308:                 }
1309:
1310:                         if (cf != null)
1311:                         {
1312:                                 results.add(cf.getType());
1313:                         } else
1314:                         {
1315:                                 TypeCheckerErrors.concern(unique, 3090,
1316:                                                 "Unknown field " + node.getField().getName()
1317:                                                                 + " in record "
1318:                                                                 + rec.getName(), node.getField().getLocation(), node.getField());
1319:                         }
1320:
1321:                         recOrClass = true;
1322:                 }
1323:
1324:                 if (question.env.isVDMPP()
1325:                                 && question.assistantFactory.createPTypeAssistant().isClass(root, question.env, question.fromModule))
1326:                 {
1327:                         AClassType cls = question.assistantFactory.createPTypeAssistant().getClassType(root, question.env, question.fromModule);
1328:                         ILexNameToken memberName = node.getMemberName();
1329:
1330:                         if (memberName == null)
1331:                         {
1332:                                 memberName = question.assistantFactory.createAClassTypeAssistant().getMemberName(cls, node.getField());
1333:                                 node.setMemberName(memberName);
1334:                         }
1335:
1336:                         memberName.setTypeQualifier(question.qualifiers);
1337:                         PDefinition encl = question.env.getEnclosingDefinition();
1338:                         NameScope findScope = question.scope;
1339:
1340:                         if (encl != null
1341:                                         && question.assistantFactory.createPDefinitionAssistant().isFunction(encl))
1342:                         {
1343:                                 findScope = NameScope.VARSANDNAMES; // Allow fields as well in functions
1344:                         }
1345:
1346:                         PDefinition fdef = question.assistantFactory.createAClassTypeAssistant().findName(cls, memberName, findScope);
1347:
1348:                         if (fdef == null)
1349:                         {
1350:                                 // The field may be a map or sequence, which would not
1351:                                 // have the type qualifier of its arguments in the name...
1352:
1353:                                 List<PType> oldq = memberName.getTypeQualifier();
1354:                                 memberName.setTypeQualifier(null);
1355:                                 fdef = // cls.apply(question.assistantFactory.getNameFinder(), new NameFinder.Newquestion(memberName,
1356:                                                 // question.scope));
1357:
1358:                                                 question.assistantFactory.createAClassTypeAssistant().findName(cls, memberName, question.scope);
1359:                                 memberName.setTypeQualifier(oldq); // Just for error text!
1360:                         }
1361:
1362:                         if (fdef == null && memberName.getTypeQualifier() == null)
1363:                         {
1364:                                 // We might be selecting a bare function or operation, without
1365:                                 // applying it (ie. no qualifiers). In this case, if there is
1366:                                 // precisely one possibility, we choose it.
1367:
1368:                                 for (PDefinition possible : question.env.findMatches(memberName))
1369:                                 {
1370:                                         if (question.assistantFactory.createPDefinitionAssistant().isFunctionOrOperation(possible))
1371:                                         {
1372:                                                 if (fdef != null)
1373:                                                 {
1374:                                                         fdef = null; // Alas, more than one
1375:                                                         break;
1376:                                                 } else
1377:                                                 {
1378:                                                         fdef = possible;
1379:                                                 }
1380:                                         }
1381:                                 }
1382:                         }
1383:
1384:                         if (fdef == null)
1385:                         {
1386:                                 TypeCheckerErrors.concern(unique, 3091,
1387:                                                 "Unknown member " + memberName + " of class "
1388:                                                                 + cls.getName().getName(), node.getField().getLocation(), node.getField());
1389:
1390:                                 if (unique)
1391:                                 {
1392:                                         question.env.listAlternatives(memberName);
1393:                                 }
1394:                         } else if (question.assistantFactory.createSClassDefinitionAssistant().isAccessible(question.env, fdef, false))
1395:                         {
1396:                                 // The following gives lots of warnings for self.value access
1397:                                 // to values as though they are fields of self in the CSK test
1398:                                 // suite, so commented out for now.
1399:
1400:                                 if (question.assistantFactory.createPDefinitionAssistant().isStatic(fdef))// && !env.isStatic())
1401:                                 {
1402:                                         // warning(5005, "Should access member " + field +
1403:                                         // " from a static context");
1404:                                 }
1405:
1406:                                 results.add(question.assistantFactory.createPDefinitionAssistant().getType(fdef));
1407:                                 // At runtime, type qualifiers must match exactly
1408:                                 memberName.setTypeQualifier(fdef.getName().getTypeQualifier());
1409:                         } else
1410:                         {
1411:                                 TypeCheckerErrors.concern(unique, 3092,
1412:                                                 "Inaccessible member " + memberName + " of class "
1413:                                                                 + cls.getName().getName(), node.getField().getLocation(), node.getField());
1414:                         }
1415:
1416:                         recOrClass = true;
1417:                 }
1418:
1419:                 if (results.isEmpty())
1420:                 {
1421:                         if (!recOrClass)
1422:                         {
1423:                                 if (root instanceof ARecordInvariantType && ((ARecordInvariantType)root).getOpaque())
1424:                                 {
1425:                                         TypeCheckerErrors.report(3093,
1426:                                                         "Field '" + node.getField().getName()
1427:                                                                         + "' applied to non-struct export", node.getObject().getLocation(), node.getObject());
1428:                                 }
1429:                                 else
1430:                                 {
1431:                                         TypeCheckerErrors.report(3093,
1432:                                                         "Field '" + node.getField().getName()
1433:                                                                         + "' applied to non-aggregate type", node.getObject().getLocation(), node.getObject());
1434:                                 }
1435:                         }
1436:
1437:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
1438:                         return node.getType();
1439:                 }
1440:
1441:                 PType resType = results.getType(node.getLocation());
1442:                 node.setType(resType);
1443:                 return question.assistantFactory.createPTypeAssistant().possibleConstraint(question.constraint, node.getType(), node.getLocation());
1444:         }
1445:
1446:         @Override public PType caseAFieldNumberExp(AFieldNumberExp node,
1447:                         TypeCheckInfo question) throws AnalysisException
1448:         {
1449:                 PExp tuple = node.getTuple();
1450:                 question.qualifiers = null;
1451:                 PType type = tuple.apply(THIS, question.newConstraint(null));
1452:                 node.setType(type);
1453:
1454:                 if (!question.assistantFactory.createPTypeAssistant().isProduct(type, question.fromModule))
1455:                 {
1456:                         TypeCheckerErrors.report(3094, "Field '#" + node.getField()
1457:                                         + "' applied to non-tuple type", tuple.getLocation(), tuple);
1458:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
1459:                         return node.getType();
1460:                 }
1461:
1462:                 AProductType product = question.assistantFactory.createPTypeAssistant().getProduct(type, question.fromModule);
1463:                 long fn = node.getField().getValue();
1464:
1465:                 if (fn > product.getTypes().size() || fn < 1)
1466:                 {
1467:                         TypeCheckerErrors.report(3095, "Field number does not match tuple size", node.getField().getLocation(), node.getField());
1468:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
1469:                         return node.getType();
1470:                 }
1471:
1472:                 node.setType(product.getTypes().get((int) fn - 1));
1473:                 return node.getType();
1474:         }
1475:
1476:         @Override public PType caseAForAllExp(AForAllExp node,
1477:                         TypeCheckInfo question) throws AnalysisException
1478:         {
1479:                 PDefinition def = AstFactory.newAMultiBindListDefinition(node.getLocation(), node.getBindList());
1480:                 def.apply(THIS, question.newConstraint(null));
1481:                 Environment local = new FlatCheckedEnvironment(question.assistantFactory, def, question.env, question.scope);
1482:                 if (!question.assistantFactory.createPTypeAssistant().isType(node.getPredicate().apply(THIS, new TypeCheckInfo(question.assistantFactory, local, question.scope, null, AstFactory.newABooleanBasicType(node.getLocation()), null, question.fromModule, question.mandatory)), ABooleanBasicType.class))
1483:                 {
1484:                         TypeCheckerErrors.report(3097, "Predicate is not boolean", node.getPredicate().getLocation(), node.getPredicate());
1485:                 }
1486:
1487:                 local.unusedCheck();
1488:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
1489:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
1490:         }
1491:
1492:         @Override public PType caseAFuncInstatiationExp(AFuncInstatiationExp node,
1493:                         TypeCheckInfo question) throws AnalysisException
1494:         {
1495:                 // If there are no type qualifiers passed because the poly function
1496:                 // value
1497:                 // is being accessed alone (not applied). In this case, the null
1498:                 // qualifier
1499:                 // will cause VariableExpression to search for anything that matches the
1500:                 // name alone. If there is precisely one, it is selected; if there are
1501:                 // several, this is an ambiguity error.
1502:                 //
1503:                 // Note that a poly function is hard to identify from the actual types
1504:                 // passed here because the number of parameters may not equal the number
1505:                 // of type parameters.
1506:
1507:                 PType ftype = node.getFunction().apply(THIS, question.newConstraint(null));
1508:
1509:                 if (question.assistantFactory.createPTypeAssistant().isUnknown(ftype))
1510:                 {
1511:                         node.setType(ftype);
1512:                         return ftype;
1513:                 }
1514:
1515:                 if (question.assistantFactory.createPTypeAssistant().isFunction(ftype, question.fromModule))
1516:                 {
1517:                         AFunctionType t = question.assistantFactory.createPTypeAssistant().getFunction(ftype);
1518:                         PTypeSet set = new PTypeSet(question.assistantFactory);
1519:
1520:                         if (t.getDefinitions().size() == 0)
1521:                         {
1522:                                 TypeCheckerErrors.report(3098, "Function value is not polymorphic", node.getLocation(), node);
1523:                                 set.add(AstFactory.newAUnknownType(node.getLocation()));
1524:                         } else
1525:                         {
1526:                                 boolean serious = t.getDefinitions().size() == 1;
1527:
1528:                                 for (PDefinition def : t.getDefinitions()) // Possibly a union
1529:                                 // of several
1530:                                 {
1531:                                         List<ILexNameToken> typeParams = null;
1532:                                         def = question.assistantFactory.createPDefinitionAssistant().deref(def);
1533:
1534:                                         if (def instanceof AExplicitFunctionDefinition)
1535:                                         {
1536:                                                 node.setExpdef((AExplicitFunctionDefinition) def);
1537:                                                 typeParams = node.getExpdef().getTypeParams();
1538:                                         } else if (def instanceof AImplicitFunctionDefinition)
1539:                                         {
1540:                                                 node.setImpdef((AImplicitFunctionDefinition) def);
1541:                                                 typeParams = node.getImpdef().getTypeParams();
1542:                                         } else
1543:                                         {
1544:                                                 TypeCheckerErrors.report(3099, "Polymorphic function is not in scope", node.getLocation(), node);
1545:                                                 continue;
1546:                                         }
1547:
1548:                                         if (typeParams.size() == 0)
1549:                                         {
1550:                                                 TypeCheckerErrors.concern(serious, 3100, "Function has no type parameters", node.getLocation(), node);
1551:                                                 continue;
1552:                                         }
1553:
1554:                                         if (node.getActualTypes().size() != typeParams.size())
1555:                                         {
1556:                                                 TypeCheckerErrors.concern(serious, 3101,
1557:                                                                 "Expecting " + typeParams.size()
1558:                                                                                 + " type parameters", node.getLocation(), node);
1559:                                                 continue;
1560:                                         }
1561:
1562:                                         List<PType> fixed = new Vector<PType>();
1563:
1564:                                         for (PType ptype : node.getActualTypes())
1565:                                         {
1566:                                                 if (ptype instanceof AParameterType) // Recursive
1567:                                                 // polymorphism
1568:                                                 {
1569:                                                         AParameterType pt = (AParameterType) ptype;
1570:                                                         PDefinition d = question.env.findName(pt.getName(), question.scope);
1571:
1572:                                                         if (d == null)
1573:                                                         {
1574:                                                                 TypeCheckerErrors.report(3102,
1575:                                                                                 "Parameter name " + pt
1576:                                                                                                 + " not defined", node.getLocation(), node);
1577:                                                                 ptype = AstFactory.newAUnknownType(node.getLocation());
1578:                                                         } else
1579:                                                         {
1580:                                                                 ptype = d.getType();
1581:                                                         }
1582:                                                 }
1583:
1584:                                                 ptype = question.assistantFactory.createPTypeAssistant().typeResolve(ptype, null, THIS, question);
1585:                                                 fixed.add(ptype);
1586:                                                 question.assistantFactory.getTypeComparator().checkComposeTypes(ptype, question.env, false);
1587:                                         }
1588:
1589:                                         node.setActualTypes(fixed);
1590:
1591:                                         node.setType(node.getExpdef() == null ?
1592:                                                         question.assistantFactory.createAImplicitFunctionDefinitionAssistant().getType(node.getImpdef(), node.getActualTypes()) :
1593:                                                         question.assistantFactory.createAExplicitFunctionDefinitionAssistant().getType(node.getExpdef(), node.getActualTypes()));
1594:
1595:                                         // type = expdef == null ?
1596:                                         // impdef.getType(actualTypes) :
1597:                                         // expdef.getType(actualTypes);
1598:
1599:                                         set.add(node.getType());
1600:                                 }
1601:                         }
1602:
1603:                         if (!set.isEmpty())
1604:                         {
1605:                                 node.setType(set.getType(node.getLocation()));
1606:                                 return node.getType();
1607:                         }
1608:                 } else
1609:                 {
1610:                         TypeCheckerErrors.report(3103, "Function instantiation does not yield a function", node.getLocation(), node);
1611:                 }
1612:
1613:                 node.setType(AstFactory.newAUnknownType(node.getLocation()));
1614:                 return node.getType();
1615:         }
1616:
1617:         @Override public PType caseAHistoryExp(AHistoryExp node,
1618:                         TypeCheckInfo question)
1619:         {
1620:                 SClassDefinition classdef = question.env.findClassDefinition();
1621:
1622:                 for (ILexNameToken opname : node.getOpnames())
1623:                 {
1624:                         int found = 0;
1625:
1626:                         List<PDefinition> allDefs = (List<PDefinition>) classdef.getDefinitions().clone();
1627:                         allDefs.addAll(classdef.getAllInheritedDefinitions());
1628:
1629:                         for (PDefinition def : allDefs)
1630:                         {
1631:                                 if (def.getName() != null && def.getName().matches(opname))
1632:                                 {
1633:                                         found++;
1634:
1635:                                         if (!question.assistantFactory.createPDefinitionAssistant().isCallableOperation(def))
1636:                                         {
1637:                                                 TypeCheckerErrors.report(3105, opname
1638:                                                                 + " is not an explicit operation", opname.getLocation(), opname);
1639:                                         }
1640:
1641:                                         if (def.getAccess().getPure())
1642:                                         {
1643:                                                 TypeCheckerErrors.report(3342, "Cannot use history counters for pure operations", opname.getLocation(), opname);
1644:                                         }
1645:
1646:                                         if (def.getAccess().getStatic() == null
1647:                                                         && question.env.isStatic())
1648:                                         {
1649:                                                 TypeCheckerErrors.report(3349, "Cannot see non-static operation from static context", opname.getLocation(), opname);
1650:                                         }
1651:                                 }
1652:                         }
1653:
1654:                         if (found == 0)
1655:                         {
1656:                                 TypeCheckerErrors.report(3106, opname
1657:                                                 + " is not in scope", opname.getLocation(), opname);
1658:                         } else if (found > 1)
1659:                         {
1660:                                 TypeCheckerErrors.warning(5004, "History expression of overloaded operation", opname.getLocation(), opname);
1661:                         }
1662:
1663:                         if (opname.getName().equals(classdef.getName().getName()))
1664:                         {
1665:                                 TypeCheckerErrors.report(3107, "Cannot use history of a constructor", opname.getLocation(), opname);
1666:                         }
1667:                 }
1668:
1669:                 node.setType(AstFactory.newANatNumericBasicType(node.getLocation()));
1670:
1671:                 return node.getType();
1672:         }
1673:
1674:         @Override public PType caseAIfExp(AIfExp node, TypeCheckInfo question)
1675:                         throws AnalysisException
1676:         {
1677:                 node.setType(typeCheckIf(node.getLocation(), node.getTest(), node.getThen(), node.getElseList(), node.getElse(), question));// rtypes.getType(node.getLocation()));
1678:                 return node.getType();
1679:         }
1680:
1681:         @Override public PType caseAIntLiteralExp(AIntLiteralExp node,
1682:                         TypeCheckInfo question)
1683:         {
1684:                 if (node.getValue().getValue() < 0)
1685:                 {
1686:                         node.setType(AstFactory.newAIntNumericBasicType(node.getLocation()));
1687:                 } else if (node.getValue().getValue() == 0)
1688:                 {
1689:                         node.setType(AstFactory.newANatNumericBasicType(node.getLocation()));
1690:                 } else
1691:                 {
1692:                         node.setType(AstFactory.newANatOneNumericBasicType(node.getLocation()));
1693:                 }
1694:
1695:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
1696:         }
1697:
1698:         @Override public PType caseAIotaExp(AIotaExp node, TypeCheckInfo question)
1699:                         throws AnalysisException
1700:         {
1701:                 PDefinition def = AstFactory.newAMultiBindListDefinition(node.getLocation(), question.assistantFactory.createPBindAssistant().getMultipleBindList(node.getBind()));
1702:
1703:                 def.apply(THIS, question.newConstraint(null));
1704:
1705:                 PType rt = null;
1706:                 PBind bind = node.getBind();
1707:
1708:                 if (bind instanceof ASetBind)
1709:                 {
1710:                         ASetBind sb = (ASetBind) bind;
1711:                         question.qualifiers = null;
1712:                         rt = sb.getSet().apply(THIS, question.newConstraint(null));
1713:
1714:                         if (question.assistantFactory.createPTypeAssistant().isSet(rt, question.fromModule))
1715:                         {
1716:                                 rt = question.assistantFactory.createPTypeAssistant().getSet(rt, question.fromModule).getSetof();
1717:                         } else
1718:                         {
1719:                                 TypeCheckerErrors.report(3112, "Iota set bind is not a set", node.getLocation(), node);
1720:                         }
1721:                 } else if (bind instanceof ASeqBind)
1722:                 {
1723:                         ASeqBind sb = (ASeqBind) bind;
1724:                         question.qualifiers = null;
1725:                         rt = sb.getSeq().apply(THIS, question.newConstraint(null));
1726:
1727:                         if (question.assistantFactory.createPTypeAssistant().isSeq(rt, question.fromModule))
1728:                         {
1729:                                 rt = question.assistantFactory.createPTypeAssistant().getSeq(rt, question.fromModule).getSeqof();
1730:                         } else
1731:                         {
1732:                                 TypeCheckerErrors.report(3112, "Iota seq bind is not a sequence", node.getLocation(), node);
1733:                         }
1734:                 } else
1735:                 {
1736:                         ATypeBind tb = (ATypeBind) bind;
1737:                         question.assistantFactory.createATypeBindAssistant().typeResolve(tb, THIS, question);
1738:                         rt = tb.getType();
1739:                 }
1740:
1741:                 Environment local = new FlatCheckedEnvironment(question.assistantFactory, def, question.env, question.scope);
1742:                 question.qualifiers = null;
1743:                 if (!question.assistantFactory.createPTypeAssistant().isType(node.getPredicate().apply(THIS, new TypeCheckInfo(question.assistantFactory, local, question.scope, null, AstFactory.newABooleanBasicType(node.getLocation()), null, question.fromModule, question.mandatory)), ABooleanBasicType.class))
1744:                 {
1745:                         TypeCheckerErrors.report(3088, "Predicate is not boolean", node.getPredicate().getLocation(), node.getPredicate());
1746:                 }
1747:
1748:                 local.unusedCheck();
1749:                 node.setType(rt);
1750:                 return rt;
1751:         }
1752:
1753:         @Override public PType caseAIsExp(AIsExp node, TypeCheckInfo question)
1754:                         throws AnalysisException
1755:         {
1756:                 question.qualifiers = null;
1757:                 node.getTest().apply(THIS, question.newConstraint(null));
1758:
1759:                 PType basictype = node.getBasicType();
1760:
1761:                 if (basictype != null)
1762:                 {
1763:                         basictype = question.assistantFactory.createPTypeAssistant().typeResolve(basictype, null, THIS, question);
1764:                         question.assistantFactory.getTypeComparator().checkComposeTypes(basictype, question.env, false);
1765:                 }
1766:
1767:                 ILexNameToken typename = node.getTypeName();
1768:
1769:                 if (typename != null)
1770:                 {
1771:                         PDefinition typeFound = question.env.findType(typename, node.getLocation().getModule());
1772:
1773:                         if (typeFound == null)
1774:                         {
1775:                                 TypeCheckerErrors.report(3113, "Unknown type name '" + typename
1776:                                                 + "'", node.getLocation(), node);
1777:                         } else
1778:                         {
1779:                                 node.setTypedef(typeFound.clone());
1780:                         }
1781:                 }
1782:
1783:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
1784:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
1785:         }
1786:
1787:         @Override public PType caseAIsOfBaseClassExp(AIsOfBaseClassExp node,
1788:                         TypeCheckInfo question) throws AnalysisException
1789:         {
1790:                 if (question.env.findType(node.getBaseClass(), null) == null)
1791:                 {
1792:                         TypeCheckerErrors.report(3114, "Undefined base class type: "
1793:                                         + node.getBaseClass().getName(), node.getLocation(), node);
1794:                 }
1795:
1796:                 question.qualifiers = null;
1797:                 PType rt = node.getExp().apply(THIS, question.newConstraint(null));
1798:
1799:                 if (!question.assistantFactory.createPTypeAssistant().isClass(rt, question.env, question.fromModule))
1800:                 {
1801:                         TypeCheckerErrors.report(3266, "Argument is not an object", node.getExp().getLocation(), node.getExp());
1802:                 }
1803:
1804:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
1805:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
1806:         }
1807:
1808:         @Override public PType caseAIsOfClassExp(AIsOfClassExp node,
1809:                         TypeCheckInfo question) throws AnalysisException
1810:         {
1811:                 ILexNameToken classname = node.getClassName();
1812:                 PDefinition cls = question.env.findType(classname, null);
1813:
1814:                 if (cls == null || !(cls instanceof SClassDefinition))
1815:                 {
1816:                         TypeCheckerErrors.report(3115, "Undefined class type: "
1817:                                         + classname.getName(), node.getLocation(), node);
1818:                 } else
1819:                 {
1820:                         node.setClassType((AClassType) cls.getType());
1821:                 }
1822:
1823:                 question.qualifiers = null;
1824:                 PType rt = node.getExp().apply(THIS, question.newConstraint(null));
1825:
1826:                 if (!question.assistantFactory.createPTypeAssistant().isClass(rt, question.env, question.fromModule))
1827:                 {
1828:                         TypeCheckerErrors.report(3266, "Argument is not an object", node.getExp().getLocation(), node.getExp());
1829:                 }
1830:
1831:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
1832:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
1833:         }
1834:
1835:         @Override public PType caseALambdaExp(ALambdaExp node,
1836:                         TypeCheckInfo question) throws AnalysisException
1837:         {
1838:                 question = question.newScope(NameScope.NAMES);        // Lambdas are always functions
1839:                 
1840:                 List<PMultipleBind> mbinds = new Vector<PMultipleBind>();
1841:                 List<PType> ptypes = new Vector<PType>();
1842:
1843:                 List<PPattern> paramPatterns = new Vector<PPattern>();
1844:                 List<PDefinition> paramDefinitions = new Vector<PDefinition>();
1845:
1846:                 // node.setParamPatterns(paramPatterns);
1847:                 for (ATypeBind tb : node.getBindList())
1848:                 {
1849:                         mbinds.addAll(tb.apply(question.assistantFactory.getMultipleBindLister()));
1850:                         paramDefinitions.addAll(question.assistantFactory.createPPatternAssistant(question.fromModule).getDefinitions(tb.getPattern(), tb.getType(), NameScope.LOCAL));
1851:                         paramPatterns.add(tb.getPattern());
1852:                         tb.setType(question.assistantFactory.createPTypeAssistant().typeResolve(tb.getType(), null, THIS, question));
1853:                         ptypes.add(tb.getType());
1854:                 }
1855:
1856:                 node.setParamPatterns(paramPatterns);
1857:
1858:                 question.assistantFactory.createPDefinitionListAssistant().implicitDefinitions(paramDefinitions, question.env);
1859:                 question.assistantFactory.createPDefinitionListAssistant().typeCheck(paramDefinitions, THIS, question);
1860:
1861:                 node.setParamDefinitions(paramDefinitions);
1862:
1863:                 PDefinition def = AstFactory.newAMultiBindListDefinition(node.getLocation(), mbinds);
1864:                 def.apply(THIS, question.newConstraint(null));
1865:                 Environment local = new FlatCheckedEnvironment(question.assistantFactory, def, question.env, question.scope);
1866:                 local.setFunctional(true);
1867:                 local.setEnclosingDefinition(def); // Prevent recursive checks
1868:                 TypeCheckInfo newInfo = new TypeCheckInfo(question.assistantFactory, local, question.scope);
1869:
1870:                 PType result = node.getExpression().apply(THIS, newInfo);
1871:                 local.unusedCheck();
1872:
1873:                 node.setType(AstFactory.newAFunctionType(node.getLocation(), true, ptypes, result));
1874:                 return node.getType();
1875:         }
1876:
1877:         @Override public PType caseALetBeStExp(ALetBeStExp node,
1878:                         TypeCheckInfo question) throws AnalysisException
1879:         {
1880:                 Entry<PType, AMultiBindListDefinition> res = typecheckLetBeSt(node, node.getLocation(), node.getBind(), node.getSuchThat(), node.getValue(), question);
1881:                 node.setDef(res.getValue());
1882:                 node.setType(res.getKey());
1883:                 return node.getType();
1884:         }
1885:
1886:         @Override public PType caseALetDefExp(ALetDefExp node,
1887:                         TypeCheckInfo question) throws AnalysisException
1888:         {
1889:                 node.setType(typeCheckLet(node, node.getLocalDefs(), node.getExpression(), question));
1890:                 return node.getType();
1891:         }
1892:
1893:         @Override public PType caseADefExp(ADefExp node, TypeCheckInfo question)
1894:                         throws AnalysisException
1895:         {
1896:                 // Each local definition is in scope for later local definitions...
1897:                 Environment local = question.env;
1898:
1899:                 for (PDefinition d : node.getLocalDefs())
1900:                 {
1901:                         if (d instanceof AExplicitFunctionDefinition)
1902:                         {
1903:                                 // Functions' names are in scope in their bodies, whereas
1904:                                 // simple variable declarations aren't
1905:
1906:                                 local = new FlatCheckedEnvironment(question.assistantFactory, d, local, question.scope); // cumulative
1907:                                 question.assistantFactory.createPDefinitionAssistant().implicitDefinitions(d, local);
1908:                                 TypeCheckInfo newQuestion = new TypeCheckInfo(question.assistantFactory, local, question.scope);
1909:
1910:                                 question.assistantFactory.createPDefinitionAssistant().typeResolve(d, THIS, question);
1911:
1912:                                 if (question.env.isVDMPP())
1913:                                 {
1914:                                         SClassDefinition cdef = question.env.findClassDefinition();
1915:                                         d.setClassDefinition(cdef);
1916:                                         d.setAccess(question.assistantFactory.createPAccessSpecifierAssistant().getStatic(d, true));
1917:                                 }
1918:
1919:                                 d.apply(THIS, newQuestion);
1920:                         } else
1921:                         {
1922:                                 question.assistantFactory.createPDefinitionAssistant().implicitDefinitions(d, local);
1923:                                 question.assistantFactory.createPDefinitionAssistant().typeResolve(d, THIS, new TypeCheckInfo(question.assistantFactory, local, question.scope, question.qualifiers));
1924:                                 d.apply(THIS, new TypeCheckInfo(question.assistantFactory, local, question.scope, question.qualifiers));
1925:                                 local = new FlatCheckedEnvironment(question.assistantFactory, d, local, question.scope); // cumulative
1926:                         }
1927:                 }
1928:
1929:                 PType r = node.getExpression().apply(THIS, new TypeCheckInfo(question.assistantFactory, local, question.scope, null, question.constraint, null, question.fromModule, question.mandatory));
1930:                 local.unusedCheck(question.env);
1931:                 node.setType(r);
1932:                 return r;
1933:         }
1934:
1935:         @Override public PType caseAMapCompMapExp(AMapCompMapExp node,
1936:                         TypeCheckInfo question) throws AnalysisException
1937:         {
1938:                 PDefinition def = AstFactory.newAMultiBindListDefinition(node.getLocation(), node.getBindings());
1939:                 def.apply(THIS, question.newConstraint(null));
1940:                 Environment local = new FlatCheckedEnvironment(question.assistantFactory, def, question.env, question.scope);
1941:
1942:                 PExp predicate = node.getPredicate();
1943:                 TypeCheckInfo pquestion = new TypeCheckInfo(question.assistantFactory, local, question.scope, null, AstFactory.newABooleanBasicType(node.getLocation()), null, question.fromModule, question.mandatory);
1944:
1945:                 if (predicate != null
1946:                                 && !question.assistantFactory.createPTypeAssistant().isType(predicate.apply(THIS, pquestion), ABooleanBasicType.class))
1947:                 {
1948:                         TypeCheckerErrors.report(3118, "Predicate is not boolean", predicate.getLocation(), predicate);
1949:                 }
1950:
1951:                 node.setType(node.getFirst().apply(THIS, question.newInfo(local)));
1952:                 local.unusedCheck();
1953:                 return node.getType();
1954:         }
1955:
1956:         @Override public PType caseAMapEnumMapExp(AMapEnumMapExp node,
1957:                         TypeCheckInfo question) throws AnalysisException
1958:         {
1959:                 node.setDomTypes(new Vector<PType>());
1960:                 node.setRngTypes(new Vector<PType>());
1961:
1962:                 if (node.getMembers().isEmpty())
1963:                 {
1964:                         node.setType(AstFactory.newAMapMapType(node.getLocation()));
1965:                         return node.getType();
1966:                 }
1967:
1968:                 PTypeSet dom = new PTypeSet(question.assistantFactory);
1969:                 PTypeSet rng = new PTypeSet(question.assistantFactory);
1970:
1971:                 for (AMapletExp ex : node.getMembers())
1972:                 {
1973:                         PType mt = ex.apply(THIS, question);
1974:
1975:                         if (!question.assistantFactory.createPTypeAssistant().isMap(mt, question.fromModule))
1976:                         {
1977:                                 TypeCheckerErrors.report(3121, "Element is not of maplet type", node.getLocation(), node);
1978:                         } else
1979:                         {
1980:                                 SMapType maplet = question.assistantFactory.createPTypeAssistant().getMap(mt, question.fromModule);
1981:                                 dom.add(maplet.getFrom());
1982:                                 node.getDomTypes().add(maplet.getFrom());
1983:                                 rng.add(maplet.getTo());
1984:                                 node.getRngTypes().add(maplet.getTo());
1985:                         }
1986:                 }
1987:                 node.setType(AstFactory.newAMapMapType(node.getLocation(), dom.getType(node.getLocation()), rng.getType(node.getLocation())));
1988:                 return question.assistantFactory.createPTypeAssistant().possibleConstraint(question.constraint, node.getType(), node.getLocation());
1989:         }
1990:
1991:         @Override public PType caseAMapletExp(AMapletExp node,
1992:                         TypeCheckInfo question) throws AnalysisException
1993:         {
1994:                 TypeCheckInfo domConstraint = question;
1995:                 TypeCheckInfo rngConstraint = question;
1996:
1997:                 if (question.constraint != null
1998:                                 && question.assistantFactory.createPTypeAssistant().isMap(question.constraint, question.fromModule))
1999:                 {
2000:                         PType dtype = question.assistantFactory.createPTypeAssistant().getMap(question.constraint, question.fromModule).getFrom();
2001:                         domConstraint = question.newConstraint(dtype);
2002:                         PType rtype = question.assistantFactory.createPTypeAssistant().getMap(question.constraint, question.fromModule).getTo();
2003:                         rngConstraint = question.newConstraint(rtype);
2004:                 }
2005:
2006:                 PType ltype = node.getLeft().apply(THIS, domConstraint);
2007:                 PType rtype = node.getRight().apply(THIS, rngConstraint);
2008:                 node.setType(AstFactory.newAMapMapType(node.getLocation(), ltype, rtype));
2009:                 return node.getType();
2010:         }
2011:
2012:         @Override public PType caseAMkBasicExp(AMkBasicExp node,
2013:                         TypeCheckInfo question) throws AnalysisException
2014:         {
2015:                 PType argtype = node.getArg().apply(THIS, question.newConstraint(null));
2016:
2017:                 if (!(node.getType() instanceof ATokenBasicType)
2018:                                 && !question.assistantFactory.createPTypeAssistant().equals(argtype, node.getType()))
2019:                 {
2020:                         TypeCheckerErrors.report(3125, "Argument of mk_" + node.getType()
2021:                                         + " is the wrong type", node.getLocation(), node);
2022:                 }
2023:
2024:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
2025:         }
2026:
2027:         @Override public PType caseAMkTypeExp(AMkTypeExp node,
2028:                         TypeCheckInfo question) throws AnalysisException
2029:         {
2030:                 PDefinition typeDef = question.env.findType(node.getTypeName(), node.getLocation().getModule());
2031:
2032:                 if (typeDef == null)
2033:                 {
2034:                         TypeCheckerErrors.report(3126, "Unknown type '" + node.getTypeName()
2035:                                         + "' in constructor", node.getLocation(), node);
2036:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
2037:                         return node.getType();
2038:                 }
2039:
2040:                 PType rec = null;
2041:                 if (typeDef instanceof ATypeDefinition)
2042:                 {
2043:                         rec = ((ATypeDefinition) typeDef).getType();
2044:                 } else if (typeDef instanceof AStateDefinition)
2045:                 {
2046:                         rec = ((AStateDefinition) typeDef).getRecordType();
2047:                 } else
2048:                 {
2049:                         rec = question.assistantFactory.createPDefinitionAssistant().getType(typeDef);
2050:                 }
2051:
2052:                 if (!(rec instanceof ARecordInvariantType))
2053:                 {
2054:                         TypeCheckerErrors.report(3127, "Type '" + node.getTypeName()
2055:                                         + "' is not a record type", node.getLocation(), node);
2056:                         node.setType(rec);
2057:                         return rec;
2058:                 }
2059:
2060:                 node.setRecordType((ARecordInvariantType) rec);
2061:
2062:                 if (TypeChecker.isOpaque(node.getRecordType(), question.fromModule))
2063:                 {
2064:                         TypeCheckerErrors.report(3127, "Type '" + node.getTypeName()
2065:                                         + "' has no struct export", node.getLocation(), node);
2066:                         node.setType(rec);
2067:                         return rec;
2068:                 }
2069:
2070:                 if (node.getTypeName().getExplicit())
2071:                 {
2072:                         // If the type name is explicit, the Type ought to have an explicit
2073:                         // name. This only really affects trace expansion.
2074:
2075:                         ARecordInvariantType recordType = node.getRecordType();
2076:                         AExplicitFunctionDefinition eq = recordType.getEqDef();
2077:                         AExplicitFunctionDefinition ord = recordType.getOrdDef();
2078:
2079:                         AExplicitFunctionDefinition inv = recordType.getInvDef();
2080:
2081:                         recordType = AstFactory.newARecordInvariantType(recordType.getName().getExplicit(true), recordType.getFields());
2082:                         recordType.setInvDef(inv);
2083:                         recordType.setEqDef(eq);
2084:                         recordType.setOrdDef(ord);
2085:                         node.setRecordType(recordType);
2086:                 }
2087:
2088:                 if (node.getRecordType().getFields().size() != node.getArgs().size())
2089:                 {
2090:                         TypeCheckerErrors.report(3128, "Record and constructor do not have same number of fields", node.getLocation(), node);
2091:                         node.setType(rec);
2092:                         return rec;
2093:                 }
2094:
2095:                 int i = 0;
2096:                 Iterator<AFieldField> fiter = node.getRecordType().getFields().iterator();
2097:                 node.setArgTypes(new LinkedList<PType>());
2098:                 List<PType> argTypes = node.getArgTypes();
2099:
2100:                 for (PExp arg : node.getArgs())
2101:                 {
2102:                         PType fieldType = fiter.next().getType();
2103:                         PType argType = arg.apply(THIS, question.newConstraint(fieldType));
2104:                         i++;
2105:
2106:                         if (!question.assistantFactory.getTypeComparator().compatible(fieldType, argType))
2107:                         {
2108:                                 TypeCheckerErrors.report(3129, "Constructor field " + i
2109:                                                 + " is of wrong type", node.getLocation(), node);
2110:                                 TypeCheckerErrors.detail2("Expected", fieldType, "Actual", argType);
2111:                         }
2112:
2113:                         argTypes.add(argType);
2114:                 }
2115:
2116:                 node.setType(node.getRecordType().clone());
2117:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getRecordType(), node.getLocation());
2118:         }
2119:
2120:         @Override public PType caseAMuExp(AMuExp node, TypeCheckInfo question)
2121:                         throws AnalysisException
2122:         {
2123:                 PType rtype = node.getRecord().apply(THIS, question.newConstraint(null));
2124:
2125:                 if (rtype instanceof AUnknownType)
2126:                 {
2127:                         node.setType(rtype);
2128:                         return rtype;
2129:                 }
2130:
2131:                 if (question.assistantFactory.createPTypeAssistant().isRecord(rtype, question.fromModule))
2132:                 {
2133:                         node.setRecordType(question.assistantFactory.createPTypeAssistant().getRecord(rtype, question.fromModule));
2134:                         node.setModTypes(new LinkedList<PType>());
2135:
2136:                         List<PType> modTypes = node.getModTypes();
2137:
2138:                         for (ARecordModifier rm : node.getModifiers())
2139:                         {
2140:                                 AFieldField f = question.assistantFactory.createARecordInvariantTypeAssistant().findField(node.getRecordType(), rm.getTag().getName());
2141:
2142:                                 if (f != null)
2143:                                 {
2144:                                         PType mtype = rm.getValue().apply(THIS, question.newConstraint(f.getType()));
2145:                                         modTypes.add(mtype);
2146:
2147:                                         if (!question.assistantFactory.getTypeComparator().compatible(f.getType(), mtype))
2148:                                         {
2149:                                                 TypeCheckerErrors.report(3130,
2150:                                                                 "Modifier for " + f.getTag() + " should be "
2151:                                                                                 + f.getType(), rm.getValue().getLocation(), node);
2152:                                                 TypeCheckerErrors.detail("Actual", mtype);
2153:                                         }
2154:                                 } else
2155:                                 {
2156:                                         TypeCheckerErrors.report(3131, "Modifier tag " + rm.getTag()
2157:                                                         + " not found in record", rm.getTag().getLocation(), node);
2158:                                 }
2159:                         }
2160:                 } else
2161:                 {
2162:                         TypeCheckerErrors.report(3132, "mu operation on non-record type", node.getLocation(), node);
2163:                 }
2164:
2165:                 node.setType(rtype);
2166:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, rtype, node.getLocation());
2167:         }
2168:
2169:         @Override public PType caseANarrowExp(ANarrowExp node,
2170:                         TypeCheckInfo question) throws AnalysisException
2171:         {
2172:                 node.getTest().setType(node.getTest().apply(THIS, question.newConstraint(null)));
2173:
2174:                 PType result = null;
2175:
2176:                 if (node.getBasicType() != null)
2177:                 {
2178:
2179:                         node.setBasicType(question.assistantFactory.createPTypeAssistant().typeResolve(node.getBasicType(), null, THIS, question));
2180:                         result = node.getBasicType();
2181:                         question.assistantFactory.getTypeComparator().checkComposeTypes(result, question.env, false);
2182:                 } else
2183:                 {
2184:                         node.setTypedef(question.env.findType(node.getTypeName(), node.getLocation().getModule()));
2185:
2186:                         if (node.getTypedef() == null)
2187:                         {
2188:                                 TypeCheckerErrors.report(3113,
2189:                                                 "Unknown type name '" + node.getTypeName()
2190:                                                                 + "'", node.getLocation(), node);
2191:                                 result = AstFactory.newAUnknownType(node.getLocation());
2192:                         } else
2193:                         {
2194:                                 result = question.assistantFactory.createPDefinitionAssistant().getType(node.getTypedef());
2195:                         }
2196:
2197:                 }
2198:
2199:                 if (!question.assistantFactory.getTypeComparator().compatible(result, node.getTest().getType()))
2200:                 {
2201:                         TypeCheckerErrors.report(3317, "Expression can never match narrow type", node.getLocation(), node);
2202:                 }
2203:
2204:                 node.setType(result);
2205:                 return question.assistantFactory.createPTypeAssistant().possibleConstraint(question.constraint, result, node.getLocation());
2206:         }
2207:
2208:         @Override public PType caseANewExp(ANewExp node, TypeCheckInfo question)
2209:                         throws AnalysisException
2210:         {
2211:                 PDefinition cdef = question.env.findType(node.getClassName().getClassName(), null);
2212:
2213:                 if (cdef == null || !(cdef instanceof SClassDefinition))
2214:                 {
2215:                         TypeCheckerErrors.report(3133, "Class name " + node.getClassName()
2216:                                         + " not in scope", node.getLocation(), node);
2217:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
2218:                         return node.getType();
2219:                 }
2220:
2221:                 if (Settings.release == Release.VDM_10 && question.env.isFunctional())
2222:                 {
2223:                         TypeCheckerErrors.report(3348, "Cannot use 'new' in a functional context", node.getLocation(), node);
2224:                 }
2225:
2226:                 node.setClassdef((SClassDefinition) cdef);
2227:
2228:                 SClassDefinition classdef = node.getClassdef();
2229:
2230:                 if (classdef instanceof ASystemClassDefinition)
2231:                 {
2232:                         TypeCheckerErrors.report(3279, "Cannot instantiate system class "
2233:                                         + classdef.getName(), node.getLocation(), node);
2234:                 }
2235:
2236:                 if (classdef.getIsAbstract())
2237:                 {
2238:                         TypeCheckerErrors.report(3330, "Cannot instantiate abstract class "
2239:                                         + classdef.getName(), node.getLocation(), node);
2240:
2241:                         PDefinitionAssistantTC assistant = question.assistantFactory.createPDefinitionAssistant();
2242:                         List<PDefinition> localDefs = new LinkedList<PDefinition>();
2243:                         localDefs.addAll(classdef.getDefinitions());
2244:                         localDefs.addAll(classdef.getLocalInheritedDefinitions());
2245:
2246:                         for (PDefinition d : localDefs)
2247:                         {
2248:                                 if (assistant.isSubclassResponsibility(d))
2249:                                 {
2250:                                         TypeCheckerErrors.detail("Unimplemented",
2251:                                                         d.getName().getName() + d.getType());
2252:                                 }
2253:                         }
2254:                 }
2255:
2256:                 List<PType> argtypes = new LinkedList<PType>();
2257:
2258:                 for (PExp a : node.getArgs())
2259:                 {
2260:                         argtypes.add(a.apply(THIS, question.newConstraint(null)));
2261:                 }
2262:
2263:                 PDefinition opdef = question.assistantFactory.createSClassDefinitionAssistant().findConstructor(classdef, argtypes);
2264:
2265:                 if (opdef == null)
2266:                 {
2267:                         if (!node.getArgs().isEmpty()) // Not having a default ctor is OK
2268:                         {
2269:                                 TypeCheckerErrors.report(3134, "Class has no constructor with these parameter types", node.getLocation(), node);
2270:                                 question.assistantFactory.createSClassDefinitionAssistant();
2271:                                 TypeCheckerErrors.detail("Called", SClassDefinitionAssistantTC.getCtorName(classdef, argtypes));
2272:                         } else if (classdef instanceof ACpuClassDefinition
2273:                                         || classdef instanceof ABusClassDefinition)
2274:                         {
2275:                                 TypeCheckerErrors.report(3297, "Cannot use default constructor for this class", node.getLocation(), node);
2276:                         }
2277:                 } else
2278:                 {
2279:                         if (!question.assistantFactory.createPDefinitionAssistant().isCallableOperation(opdef))
2280:                         {
2281:                                 TypeCheckerErrors.report(3135, "Class has no constructor with these parameter types", node.getLocation(), node);
2282:                                 question.assistantFactory.createSClassDefinitionAssistant();
2283:                                 TypeCheckerErrors.detail("Called", SClassDefinitionAssistantTC.getCtorName(classdef, argtypes));
2284:                         } else if (!question.assistantFactory.createSClassDefinitionAssistant().isAccessible(question.env, opdef, false))
2285:                         {
2286:                                 TypeCheckerErrors.report(3292, "Constructor is not accessible", node.getLocation(), node);
2287:                                 question.assistantFactory.createSClassDefinitionAssistant();
2288:                                 TypeCheckerErrors.detail("Called", SClassDefinitionAssistantTC.getCtorName(classdef, argtypes));
2289:                         } else
2290:                         {
2291:                                 node.setCtorDefinition(opdef);
2292:                         }
2293:                 }
2294:
2295:                 PType type = question.assistantFactory.createPDefinitionAssistant().getType(classdef);
2296:                 node.setType(type);
2297:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, type, node.getLocation());
2298:         }
2299:
2300:         @Override public PType caseANilExp(ANilExp node, TypeCheckInfo question)
2301:         {
2302:                 node.setType(AstFactory.newAOptionalType(node.getLocation(), AstFactory.newAUnknownType(node.getLocation())));
2303:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
2304:         }
2305:
2306:         @Override public PType caseANotYetSpecifiedExp(ANotYetSpecifiedExp node,
2307:                         TypeCheckInfo question)
2308:         {
2309:                 node.setType(typeCheckANotYetSpecifiedExp(node, node.getLocation()));
2310:                 return node.getType();
2311:         }
2312:
2313:         @Override public PType caseAPostOpExp(APostOpExp node,
2314:                         TypeCheckInfo question) throws AnalysisException
2315:         {
2316:                 node.setType(node.getPostexpression().apply(THIS, question.newConstraint(null)));
2317:                 return node.getType();
2318:         }
2319:
2320:         @Override public PType caseAPreExp(APreExp node, TypeCheckInfo question)
2321:                         throws AnalysisException
2322:         {
2323:                 node.getFunction().apply(THIS, question.newConstraint(null));
2324:
2325:                 for (PExp a : node.getArgs())
2326:                 {
2327:                         question.qualifiers = null;
2328:                         a.apply(THIS, question.newConstraint(null));
2329:                 }
2330:
2331:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
2332:                 return node.getType();
2333:         }
2334:
2335:         @Override public PType caseAPreOpExp(APreOpExp node, TypeCheckInfo question)
2336:                         throws AnalysisException
2337:         {
2338:                 node.setType(node.getExpression().apply(THIS, question.newConstraint(null)));
2339:                 return node.getType();
2340:         }
2341:
2342:         @Override public PType caseAQuoteLiteralExp(AQuoteLiteralExp node,
2343:                         TypeCheckInfo question)
2344:         {
2345:                 node.setType(AstFactory.newAQuoteType(node.getValue().clone()));
2346:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
2347:         }
2348:
2349:         @Override public PType caseARealLiteralExp(ARealLiteralExp node,
2350:                         TypeCheckInfo question)
2351:         {
2352:                 ILexRealToken value = node.getValue();
2353:
2354:•                if (Math.round(value.getValue()) == value.getValue())
2355:                 {
2356:•                        if (value.getValue() < 0)
2357:                         {
2358:                                 node.setType(AstFactory.newAIntNumericBasicType(node.getLocation()));
2359:•                        } else if (value.getValue() == 0)
2360:                         {
2361:                                 node.setType(AstFactory.newANatNumericBasicType(node.getLocation()));
2362:                         } else
2363:                         {
2364:                                 node.setType(AstFactory.newANatOneNumericBasicType(node.getLocation()));
2365:                         }
2366:                 } else
2367:                 {
2368:                         node.setType(AstFactory.newARationalNumericBasicType(node.getLocation()));
2369:                 }
2370:
2371:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
2372:         }
2373:
2374:         @Override public PType caseASameBaseClassExp(ASameBaseClassExp node,
2375:                         TypeCheckInfo question) throws AnalysisException
2376:         {
2377:                 PExp left = node.getLeft();
2378:                 PExp right = node.getRight();
2379:
2380:                 question.qualifiers = null;
2381:                 PType lt = left.apply(THIS, question.newConstraint(null));
2382:
2383:                 if (!question.assistantFactory.createPTypeAssistant().isClass(lt, question.env, question.fromModule))
2384:                 {
2385:                         TypeCheckerErrors.report(3266, "Argument is not an object", left.getLocation(), left);
2386:                 }
2387:
2388:                 question.qualifiers = null;
2389:                 PType rt = right.apply(THIS, question.newConstraint(null));
2390:
2391:                 if (!question.assistantFactory.createPTypeAssistant().isClass(rt, question.env, question.fromModule))
2392:                 {
2393:                         TypeCheckerErrors.report(3266, "Argument is not an object", right.getLocation(), right);
2394:                 }
2395:
2396:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
2397:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
2398:         }
2399:
2400:         @Override public PType caseASameClassExp(ASameClassExp node,
2401:                         TypeCheckInfo question) throws AnalysisException
2402:         {
2403:                 PExp left = node.getLeft();
2404:                 PExp right = node.getRight();
2405:
2406:                 question.qualifiers = null;
2407:                 PType lt = left.apply(THIS, question.newConstraint(null));
2408:
2409:                 if (!question.assistantFactory.createPTypeAssistant().isClass(lt, question.env, question.fromModule))
2410:                 {
2411:                         TypeCheckerErrors.report(3266, "Argument is not an object", left.getLocation(), left);
2412:                 }
2413:
2414:                 question.qualifiers = null;
2415:                 PType rt = right.apply(THIS, question.newConstraint(null));
2416:
2417:                 if (!question.assistantFactory.createPTypeAssistant().isClass(rt, question.env, question.fromModule))
2418:                 {
2419:                         TypeCheckerErrors.report(3266, "Argument is not an object", right.getLocation(), right);
2420:                 }
2421:
2422:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
2423:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
2424:         }
2425:
2426:         @Override public PType caseASelfExp(ASelfExp node, TypeCheckInfo question)
2427:         {
2428:                 PDefinition cdef = question.env.findName(node.getName(), question.scope);
2429:
2430:                 if (cdef == null)
2431:                 {
2432:                         TypeCheckerErrors.report(3154,
2433:                                         node.getName() + " not in scope", node.getLocation(), node);
2434:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
2435:                         return node.getType();
2436:                 }
2437:
2438:                 node.setType(cdef.getType());
2439:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
2440:         }
2441:
2442:         @Override public PType caseASeqCompSeqExp(ASeqCompSeqExp node,
2443:                         TypeCheckInfo question) throws AnalysisException
2444:         {
2445:                 PDefinition def = AstFactory.newAMultiBindListDefinition(node.getLocation(), question.assistantFactory.createPBindAssistant().getMultipleBindList(node.getBind()));
2446:                 def.parent(node.getBind());
2447:                 def.apply(THIS, question.newConstraint(null));
2448:
2449:                 if (node.getBind() instanceof ATypeBind)
2450:                 {
2451:                         ATypeBind tb = (ATypeBind) node.getBind();
2452:                         question.assistantFactory.createATypeBindAssistant().typeResolve(tb, THIS, question);
2453:                 }
2454:
2455:                 if ((node.getBind() instanceof ASetBind || node.getBind() instanceof ATypeBind) && (
2456:                                 question.assistantFactory.createPPatternAssistant(question.fromModule).getVariableNames(node.getBind().getPattern()).size()
2457:                                                 > 1
2458:                                                 || !question.assistantFactory.createPTypeAssistant().isOrdered(question.assistantFactory.createPDefinitionAssistant().getType(def), node.getLocation())))
2459:                 {
2460:                         TypeCheckerErrors.report(3155, "List comprehension must define one ordered bind variable", node.getLocation(), node);
2461:                 }
2462:
2463:                 Environment local = new FlatCheckedEnvironment(question.assistantFactory, def, question.env, question.scope);
2464:                 PType etype = node.getFirst().apply(THIS, new TypeCheckInfo(question.assistantFactory, local, question.scope, question.qualifiers));
2465:
2466:                 PExp predicate = node.getPredicate();
2467:
2468:                 if (predicate != null)
2469:                 {
2470:                         TypeCheckInfo pquestion = new TypeCheckInfo(question.assistantFactory, local, question.scope, null, AstFactory.newABooleanBasicType(node.getLocation()), null, question.fromModule, question.mandatory);
2471:
2472:                         question.qualifiers = null;
2473:                         if (!question.assistantFactory.createPTypeAssistant().isType(predicate.apply(THIS, pquestion), ABooleanBasicType.class))
2474:                         {
2475:                                 TypeCheckerErrors.report(3156, "Predicate is not boolean", predicate.getLocation(), predicate);
2476:                         }
2477:                 }
2478:
2479:                 local.unusedCheck();
2480:                 node.setType(AstFactory.newASeqSeqType(node.getLocation(), etype));
2481:                 return node.getType();
2482:         }
2483:
2484:         @Override public PType caseASeqEnumSeqExp(ASeqEnumSeqExp node,
2485:                         TypeCheckInfo question) throws AnalysisException
2486:         {
2487:                 PTypeSet ts = new PTypeSet(question.assistantFactory);
2488:                 node.setTypes(new LinkedList<PType>());
2489:                 List<PType> types = node.getTypes();
2490:                 TypeCheckInfo elemConstraint = question;
2491:
2492:                 if (question.constraint != null
2493:                                 && question.assistantFactory.createPTypeAssistant().isSeq(question.constraint, question.fromModule))
2494:                 {
2495:                         PType stype = question.assistantFactory.createPTypeAssistant().getSeq(question.constraint, question.fromModule).getSeqof();
2496:                         elemConstraint = question.newConstraint(stype);
2497:                 }
2498:
2499:                 for (PExp ex : node.getMembers())
2500:                 {
2501:                         question.qualifiers = null;
2502:                         PType mt = ex.apply(THIS, elemConstraint);
2503:                         ts.add(mt);
2504:                         types.add(mt);
2505:                 }
2506:
2507:                 node.setType(ts.isEmpty() ?
2508:                                 AstFactory.newASeqSeqType(node.getLocation()) :
2509:                                 AstFactory.newASeq1SeqType(node.getLocation(), ts.getType(node.getLocation())));
2510:
2511:                 return question.assistantFactory.createPTypeAssistant().possibleConstraint(question.constraint, node.getType(), node.getLocation());
2512:         }
2513:
2514:         @Override public PType caseASetCompSetExp(ASetCompSetExp node,
2515:                         TypeCheckInfo question) throws AnalysisException
2516:         {
2517:                 PDefinition def = AstFactory.newAMultiBindListDefinition(node.getFirst().getLocation(), node.getBindings());
2518:                 def.apply(THIS, question.newConstraint(null));
2519:
2520:                 Environment local = new FlatCheckedEnvironment(question.assistantFactory, def, question.env, question.scope);
2521:                 question = new TypeCheckInfo(question.assistantFactory, local, question.scope);
2522:
2523:                 PType etype = node.getFirst().apply(THIS, question.newConstraint(null));
2524:                 PExp predicate = node.getPredicate();
2525:
2526:                 if (predicate != null)
2527:                 {
2528:                         TypeCheckInfo pquestion = new TypeCheckInfo(question.assistantFactory, local, question.scope, null, AstFactory.newABooleanBasicType(node.getLocation()), null, question.fromModule, question.mandatory);
2529:
2530:                         if (!question.assistantFactory.createPTypeAssistant().isType(predicate.apply(THIS, pquestion), ABooleanBasicType.class))
2531:                         {
2532:                                 TypeCheckerErrors.report(3159, "Predicate is not boolean", predicate.getLocation(), predicate);
2533:                         }
2534:                 }
2535:
2536:                 local.unusedCheck();
2537:                 SSetType setType = AstFactory.newASetSetType(node.getLocation(), etype);
2538:                 node.setType(setType);
2539:                 node.setSetType(setType);
2540:                 return setType;
2541:         }
2542:
2543:         @Override public PType caseASetEnumSetExp(ASetEnumSetExp node,
2544:                         TypeCheckInfo question) throws AnalysisException
2545:         {
2546:                 PTypeSet ts = new PTypeSet(question.assistantFactory);
2547:                 node.setTypes(new LinkedList<PType>());
2548:                 List<PType> types = node.getTypes();
2549:                 TypeCheckInfo elemConstraint = question;
2550:
2551:                 if (question.constraint != null
2552:                                 && question.assistantFactory.createPTypeAssistant().isSet(question.constraint, question.fromModule))
2553:                 {
2554:                         PType setType = question.assistantFactory.createPTypeAssistant().getSet(question.constraint, question.fromModule).getSetof();
2555:                         elemConstraint = question.newConstraint(setType);
2556:                 }
2557:
2558:                 for (PExp ex : node.getMembers())
2559:                 {
2560:                         question.qualifiers = null;
2561:                         PType mt = ex.apply(THIS, elemConstraint);
2562:                         ts.add(mt);
2563:                         types.add(mt);
2564:                 }
2565:
2566:                 node.setType(ts.isEmpty() ?
2567:                                 AstFactory.newASetSetType(node.getLocation()) :
2568:                                 AstFactory.newASet1SetType(node.getLocation(), ts.getType(node.getLocation())));
2569:
2570:                 return question.assistantFactory.createPTypeAssistant().possibleConstraint(question.constraint, node.getType(), node.getLocation());
2571:         }
2572:
2573:         @Override public PType caseASetRangeSetExp(ASetRangeSetExp node,
2574:                         TypeCheckInfo question) throws AnalysisException
2575:         {
2576:                 PExp first = node.getFirst();
2577:                 PExp last = node.getLast();
2578:
2579:                 question.qualifiers = null;
2580:                 node.setFtype(first.apply(THIS, question.newConstraint(null)));
2581:                 question.qualifiers = null;
2582:                 node.setLtype(last.apply(THIS, question.newConstraint(null)));
2583:
2584:                 PType ftype = node.getFtype();
2585:                 PType ltype = node.getLtype();
2586:
2587:                 if (!question.assistantFactory.createPTypeAssistant().isNumeric(ftype, question.fromModule))
2588:                 {
2589:                         TypeCheckerErrors.report(3166, "Set range type must be a number", first.getLocation(), ftype);
2590:                         ftype = AstFactory.newAIntNumericBasicType(node.getLocation());
2591:                 }
2592:
2593:                 SNumericBasicType ntype = question.assistantFactory.createPTypeAssistant().getNumeric(ftype, question.fromModule);
2594:
2595:                 if (question.assistantFactory.createSNumericBasicTypeAssistant().getWeight(ntype)
2596:                                 > 1)
2597:                 {
2598:                         ftype = AstFactory.newAIntNumericBasicType(node.getLocation()); // Caused by ceiling/floor
2599:                 }
2600:
2601:                 if (!question.assistantFactory.createPTypeAssistant().isNumeric(ltype, question.fromModule))
2602:                 {
2603:                         TypeCheckerErrors.report(3167, "Set range type must be a number", last.getLocation(), ltype);
2604:                 }
2605:
2606:                 node.setType(AstFactory.newASetSetType(first.getLocation(), ftype));
2607:                 return question.assistantFactory.createPTypeAssistant().possibleConstraint(question.constraint, node.getType(), node.getLocation());
2608:         }
2609:
2610:         @Override public PType caseAStateInitExp(AStateInitExp node,
2611:                         TypeCheckInfo question) throws AnalysisException
2612:         {
2613:                 TypeCheckInfo noConstraint = question.newConstraint(null);
2614:                 PPattern pattern = node.getState().getInitPattern();
2615:                 PExp exp = node.getState().getInitExpression();
2616:                 boolean canBeExecuted = false;
2617:
2618:                 if (pattern instanceof AIdentifierPattern
2619:                                 && exp instanceof AEqualsBinaryExp)
2620:                 {
2621:                         AEqualsBinaryExp ee = (AEqualsBinaryExp) exp;
2622:                         ee.setType(AstFactory.newABooleanBasicType(ee.getLocation()));
2623:
2624:                         question.qualifiers = null;
2625:                         ee.getLeft().apply(THIS, noConstraint);
2626:
2627:                         if (ee.getLeft() instanceof AVariableExp)
2628:                         {
2629:                                 question.qualifiers = null;
2630:                                 PType rhs = ee.getRight().apply(THIS, noConstraint);
2631:
2632:                                 if (question.assistantFactory.createPTypeAssistant().isTag(rhs, question.fromModule))
2633:                                 {
2634:                                         ARecordInvariantType rt = question.assistantFactory.createPTypeAssistant().getRecord(rhs, question.fromModule);
2635:                                         canBeExecuted = rt.getName().getName().equals(node.getState().getName().getName());
2636:                                 }
2637:                         }
2638:                 } else
2639:                 {
2640:                         question.qualifiers = null;
2641:                         exp.apply(THIS, noConstraint);
2642:                 }
2643:
2644:                 if (!canBeExecuted)
2645:                 {
2646:                         TypeCheckerErrors.warning(5010, "State init expression cannot be executed", node.getLocation(), node);
2647:                         TypeCheckerErrors.detail("Expected",
2648:                                         "p == p = mk_" + node.getState().getName().getName()
2649:                                                         + "(...)");
2650:                 }
2651:
2652:                 node.getState().setCanBeExecuted(canBeExecuted);
2653:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
2654:                 return node.getType();
2655:         }
2656:
2657:         @Override public PType caseAStringLiteralExp(AStringLiteralExp node,
2658:                         TypeCheckInfo question)
2659:         {
2660:                 if (node.getValue().getValue().isEmpty())
2661:                 {
2662:                         ASeqSeqType tt = AstFactory.newASeqSeqType(node.getLocation(), AstFactory.newACharBasicType(node.getLocation()));
2663:                         node.setType(tt);
2664:                 } else
2665:                 {
2666:                         node.setType(AstFactory.newASeq1SeqType(node.getLocation(), AstFactory.newACharBasicType(node.getLocation())));
2667:                 }
2668:
2669:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
2670:         }
2671:
2672:         @Override public PType caseASubclassResponsibilityExp(
2673:                         ASubclassResponsibilityExp node, TypeCheckInfo question)
2674:         {
2675:                 node.setType(AstFactory.newAUnknownType(node.getLocation()));
2676:                 return node.getType(); // Because we terminate anyway
2677:         }
2678:
2679:         @Override public PType caseASubseqExp(ASubseqExp node,
2680:                         TypeCheckInfo question) throws AnalysisException
2681:         {
2682:                 TypeCheckInfo noConstraint = question.newConstraint(null);
2683:                 question.qualifiers = null;
2684:                 PType stype = node.getSeq().apply(THIS, noConstraint);
2685:                 question.qualifiers = null;
2686:                 node.setFtype(node.getFrom().apply(THIS, noConstraint));
2687:                 PType ftype = node.getFtype();
2688:                 question.qualifiers = null;
2689:                 node.setTtype(node.getTo().apply(THIS, noConstraint));
2690:                 PType ttype = node.getTtype();
2691:
2692:                 if (!question.assistantFactory.createPTypeAssistant().isSeq(stype, question.fromModule))
2693:                 {
2694:                         TypeCheckerErrors.report(3174, "Subsequence is not of a sequence type", node.getLocation(), node);
2695:                 }
2696:
2697:                 question.assistantFactory.createPTypeAssistant();
2698:                 if (!question.assistantFactory.createPTypeAssistant().isNumeric(ftype, question.fromModule))
2699:                 {
2700:                         TypeCheckerErrors.report(3175, "Subsequence range start is not a number", node.getLocation(), node);
2701:                 }
2702:
2703:                 question.assistantFactory.createPTypeAssistant();
2704:                 if (!question.assistantFactory.createPTypeAssistant().isNumeric(ttype, question.fromModule))
2705:                 {
2706:                         TypeCheckerErrors.report(3176, "Subsequence range end is not a number", node.getLocation(), node);
2707:                 }
2708:                 
2709:                 // "12345"(1,...,0) is seq not seq1, so convert here
2710:                 stype = question.assistantFactory.createPTypeAssistant().isSeq(stype, question.fromModule) ?
2711:                                 AstFactory.newASeqSeqType(node.getLocation(), question.assistantFactory.createPTypeAssistant().getSeq(stype, question.fromModule).getSeqof()) :
2712:                                 stype;
2713:
2714:                 node.setType(stype);
2715:                 return stype;
2716:         }
2717:
2718:         @Override public PType caseAThreadIdExp(AThreadIdExp node,
2719:                         TypeCheckInfo question)
2720:         {
2721:                 PDefinition encl = question.env.getEnclosingDefinition();
2722:
2723:                 if (encl != null && encl.getAccess().getPure())
2724:                 {
2725:                         TypeCheckerErrors.report(3346, "Cannot use 'threadid' in pure operations", node.getLocation(), node);
2726:                 }
2727:
2728:                 if (Settings.release == Release.VDM_10 && question.env.isFunctional())
2729:                 {
2730:                         TypeCheckerErrors.report(3348, "Cannot use 'threadid' in a functional context", node.getLocation(), node);
2731:                 }
2732:
2733:                 node.setType(AstFactory.newANatNumericBasicType(node.getLocation()));
2734:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
2735:         }
2736:
2737:         @Override public PType caseATimeExp(ATimeExp node, TypeCheckInfo question)
2738:         {
2739:                 PDefinition encl = question.env.getEnclosingDefinition();
2740:
2741:                 if (encl != null && encl.getAccess().getPure())
2742:                 {
2743:                         TypeCheckerErrors.report(3346, "Cannot use 'time' in pure operations", node.getLocation(), node);
2744:                 }
2745:
2746:                 if (Settings.release == Release.VDM_10 && question.env.isFunctional())
2747:                 {
2748:                         TypeCheckerErrors.report(3348, "Cannot use 'time' in a functional context", node.getLocation(), node);
2749:                 }
2750:
2751:                 node.setType(AstFactory.newANatNumericBasicType(node.getLocation()));
2752:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
2753:         }
2754:
2755:         @Override public PType caseATupleExp(ATupleExp node, TypeCheckInfo question)
2756:                         throws AnalysisException
2757:         {
2758:                 node.setTypes(new LinkedList<PType>());
2759:                 List<PType> types = node.getTypes();
2760:                 List<PType> elemConstraints = null;
2761:
2762:                 if (question.constraint != null
2763:                                 && question.assistantFactory.createPTypeAssistant().isProduct(question.constraint, question.fromModule))
2764:                 {
2765:                         elemConstraints = question.assistantFactory.createPTypeAssistant().getProduct(question.constraint, question.fromModule).getTypes();
2766:
2767:                         if (elemConstraints.size() != node.getArgs().size())
2768:                         {
2769:                                 elemConstraints = null;
2770:                         }
2771:                 }
2772:
2773:                 int i = 0;
2774:
2775:                 for (PExp arg : node.getArgs())
2776:                 {
2777:                         question.qualifiers = null;
2778:
2779:                         if (elemConstraints == null)
2780:                         {
2781:                                 types.add(arg.apply(THIS, question.newConstraint(null)));
2782:                         } else
2783:                         {
2784:                                 types.add(arg.apply(THIS, question.newConstraint(elemConstraints.get(i++))));
2785:                         }
2786:                 }
2787:
2788:                 node.setType(AstFactory.newAProductType(node.getLocation(), types));
2789:                 return question.assistantFactory.createPTypeAssistant().possibleConstraint(question.constraint, node.getType(), node.getLocation());
2790:         }
2791:
2792:         @Override public PType caseAUndefinedExp(AUndefinedExp node,
2793:                         TypeCheckInfo question)
2794:         {
2795:                 node.setType(AstFactory.newAUnknownType(node.getLocation()));
2796:                 return node.getType();
2797:         }
2798:
2799:         @Override public PType caseAVariableExp(AVariableExp node,
2800:                         TypeCheckInfo question)
2801:         {
2802:                 Environment env = question.env;
2803:                 ILexNameToken name = node.getName();
2804:
2805:                 if (env.isVDMPP())
2806:                 {
2807:
2808:                         name.setTypeQualifier(question.qualifiers);
2809:                         node.setVardef(env.findName(name, question.scope));
2810:                         PDefinition vardef = node.getVardef();
2811:
2812:                         if (vardef != null)
2813:                         {
2814:                                 if (vardef.getClassDefinition() != null)
2815:                                 {
2816:                                         SClassDefinition sd = vardef.getClassDefinition();
2817:                                         if (sd != null && node.getName().getModule().equals(""))
2818:                                         {
2819:                                                 node.setName(name.getModifiedName(sd.getName().getName()));
2820:                                         }
2821:
2822:                                         if (!question.assistantFactory.createSClassDefinitionAssistant().isAccessible(env, vardef, true))
2823:                                         {
2824:                                                 TypeCheckerErrors.report(3180,
2825:                                                                 "Inaccessible member " + name + " of class "
2826:                                                                                 + vardef.getClassDefinition().getName().getName(), node.getLocation(), node);
2827:                                                 node.setType(AstFactory.newAUnknownType(node.getLocation()));
2828:                                                 return node.getType();
2829:                                         } else if (
2830:                                                         !question.assistantFactory.createPAccessSpecifierAssistant().isStatic(vardef.getAccess())
2831:                                                                         && env.isStatic())
2832:                                         {
2833:                                                 TypeCheckerErrors.report(3181, "Cannot access " + name
2834:                                                                 + " from a static context", node.getLocation(), node);
2835:                                                 node.setType(AstFactory.newAUnknownType(node.getLocation()));
2836:                                                 return node.getType();
2837:                                         }
2838:                                         //AKM: a little test
2839:                                         // if(vardef.getClassDefinition().getName().getName().startsWith("$actionClass"))
2840:                                         // node.setName(name.getModifiedName(vardef.getClassDefinition().getName().getName()));
2841:                                 }
2842:                         } else if (question.qualifiers != null)
2843:                         {
2844:                                 // It may be an apply of a map or sequence, which would not
2845:                                 // have the type qualifier of its arguments in the name. Or
2846:                                 // it might be an apply of a function via a function variable
2847:                                 // which would not be qualified.
2848:
2849:                                 name.setTypeQualifier(null);
2850:                                 vardef = env.findName(name, question.scope);
2851:
2852:                                 if (vardef == null)
2853:                                 {
2854:                                         name.setTypeQualifier(question.qualifiers); // Just for
2855:                                         // error text!
2856:                                 } else
2857:                                 {
2858:                                         node.setVardef(vardef);
2859:                                 }
2860:
2861:                         } else
2862:                         {
2863:                                 // We may be looking for a bare function/op "x", when in fact
2864:                                 // there is one with a qualified name "x(args)". So we check
2865:                                 // the possible matches - if there is precisely one, we pick it,
2866:                                 // else we raise an ambiguity error.
2867:
2868:                                 for (PDefinition possible : env.findMatches(name))
2869:                                 {
2870:                                         if (question.assistantFactory.createPDefinitionAssistant().isFunctionOrOperation(possible))
2871:                                         {
2872:                                                 if (vardef != null)
2873:                                                 {
2874:                                                         TypeCheckerErrors.report(3269,
2875:                                                                         "Ambiguous function/operation name: "
2876:                                                                                         + name.getName(), node.getLocation(), node);
2877:                                                         env.listAlternatives(name);
2878:                                                         break;
2879:                                                 }
2880:
2881:                                                 vardef = possible;
2882:                                                 node.setVardef(vardef);
2883:                                                 // Set the qualifier so that it will find it at runtime.
2884:
2885:                                                 PType pt = possible.getType();
2886:
2887:                                                 if (pt instanceof AFunctionType)
2888:                                                 {
2889:                                                         AFunctionType ft = (AFunctionType) pt;
2890:                                                         name.setTypeQualifier(ft.getParameters());
2891:                                                 } else
2892:                                                 {
2893:                                                         AOperationType ot = (AOperationType) pt;
2894:                                                         name.setTypeQualifier(ot.getParameters());
2895:                                                 }
2896:                                         }
2897:                                 }
2898:                         }
2899:                 } else
2900:                 {
2901:                         PDefinition temp = env.findName(name, question.scope);
2902:                         node.setVardef(temp == null ? null : temp);
2903:                 }
2904:
2905:                 if (node.getVardef() == null)
2906:                 {
2907:                         TypeCheckerErrors.report(3182, "Name '" + name
2908:                                         + "' is not in scope", node.getLocation(), node);
2909:                         env.listAlternatives(name);
2910:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
2911:                         return node.getType();
2912:                 } else
2913:                 {
2914:                         PType result = question.assistantFactory.createPDefinitionAssistant().getType(node.getVardef());
2915:
2916:                         if (result instanceof AParameterType)
2917:                         {
2918:                                 AParameterType ptype = (AParameterType) result;
2919:
2920:                                 if (ptype.getName().equals(name)) // Referring to "T" of @T
2921:                                 {
2922:                                         TypeCheckerErrors.report(3351,
2923:                                                         "Type parameter '" + name.getName()
2924:                                                                         + "' cannot be used here", node.getLocation(), node);
2925:                                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
2926:                                         return node.getType();
2927:                                 }
2928:                         }
2929:
2930:                         // Note that we perform an extra typeResolve here. This is
2931:                         // how forward referenced types are resolved, and is the reason
2932:                         // we don't need to retry at the top level (assuming all names
2933:                         // are in the environment).
2934:                         node.setType(question.assistantFactory.createPTypeAssistant().typeResolve(question.assistantFactory.createPDefinitionAssistant().getType(node.getVardef()), null, THIS, question));
2935:
2936:                         // If a constraint is passed in, we can raise an error if it is
2937:                         // not possible for the type to match the constraint (rather than
2938:                         // certain, as checkConstraint would).
2939:
2940:                         return question.assistantFactory.createPTypeAssistant().possibleConstraint(question.constraint, node.getType(), node.getLocation());
2941:                 }
2942:         }
2943:
2944:         /**
2945:          * BINARY Expressions
2946:          *
2947:          * @throws AnalysisException
2948:          */
2949:         @Override public PType caseALessEqualNumericBinaryExp(
2950:                         ALessEqualNumericBinaryExp node, TypeCheckInfo question)
2951:                         throws AnalysisException
2952:         {
2953:                 checkOrdered(node, THIS, question);
2954:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
2955:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
2956:         }
2957:
2958:         @Override public PType caseALessNumericBinaryExp(ALessNumericBinaryExp node,
2959:                         TypeCheckInfo question) throws AnalysisException
2960:         {
2961:                 checkOrdered(node, THIS, question);
2962:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
2963:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
2964:         }
2965:
2966:         /**
2967:          * UNARY Expressions
2968:          *
2969:          * @throws AnalysisException
2970:          */
2971:         @Override public PType caseAAbsoluteUnaryExp(AAbsoluteUnaryExp node,
2972:                         TypeCheckInfo question) throws AnalysisException
2973:         {
2974:                 question.qualifiers = null;
2975:                 TypeCheckInfo absConstraint = question.newConstraint(null);
2976:
2977:                 if (question.constraint != null
2978:                                 && question.assistantFactory.createPTypeAssistant().isNumeric(question.constraint, question.fromModule))
2979:                 {
2980:                         if (question.constraint instanceof AIntNumericBasicType
2981:                                         || question.constraint instanceof ANatOneNumericBasicType)
2982:                         {
2983:                                 absConstraint = question.newConstraint(AstFactory.newAIntNumericBasicType(node.getLocation()));
2984:                         } else
2985:                         {
2986:                                 absConstraint = question;
2987:                         }
2988:                 }
2989:
2990:                 PType t = node.getExp().apply(THIS, absConstraint);
2991:
2992:                 if (!question.assistantFactory.createPTypeAssistant().isNumeric(t, question.fromModule))
2993:                 {
2994:                         TypeCheckerErrors.report(3053, "Argument of 'abs' is not numeric", node.getLocation(), node);
2995:                 } else if (t instanceof AIntNumericBasicType)
2996:                 {
2997:                         t = AstFactory.newANatNumericBasicType(t.getLocation());
2998:                 }
2999:
3000:                 node.setType(t);
3001:                 return t;
3002:         }
3003:         
3004:         @Override
3005:         public PType caseAAnnotatedUnaryExp(AAnnotatedUnaryExp node, TypeCheckInfo question)
3006:                         throws AnalysisException
3007:         {
3008:                 TypeCheckInfo unconstrained = question.newConstraint(null);
3009:                 node.getAnnotation().apply(THIS, unconstrained);                // check the annotation itself first?
3010:                 beforeAnnotation(node.getAnnotation(), node, unconstrained);
3011:                 PType result = node.getExp().apply(THIS, question);
3012:                 afterAnnotation(node.getAnnotation(), node, unconstrained);
3013:                 node.setType(result);
3014:                 return result;
3015:         }
3016:
3017:         @Override public PType caseACardinalityUnaryExp(ACardinalityUnaryExp node,
3018:                         TypeCheckInfo question) throws AnalysisException
3019:         {
3020:                 PExp exp = node.getExp();
3021:                 question.qualifiers = null;
3022:                 boolean set1 = false;
3023:                 PType etype = exp.apply(THIS, question.newConstraint(null));
3024:
3025:                 if (!question.assistantFactory.createPTypeAssistant().isSet(etype, question.fromModule))
3026:                 {
3027:                         TypeCheckerErrors.report(3067, "Argument of 'card' is not a set", exp.getLocation(), exp);
3028:                 }
3029:                 else
3030:                 {
3031:                         PType st = question.assistantFactory.createPTypeAssistant().getSet(etype, question.fromModule);
3032:                         set1 = st instanceof ASet1SetType;
3033:                 }
3034:
3035:                 node.setType(set1 ?
3036:                         AstFactory.newANatOneNumericBasicType(node.getLocation()) :
3037:                         AstFactory.newANatNumericBasicType(node.getLocation()));
3038:
3039:                 return question.assistantFactory.createPTypeAssistant().possibleConstraint(question.constraint, node.getType(), node.getLocation());
3040:         }
3041:
3042:         @Override public PType caseADistConcatUnaryExp(ADistConcatUnaryExp node,
3043:                         TypeCheckInfo question) throws AnalysisException
3044:         {
3045:                 PExp exp = node.getExp();
3046:                 question.qualifiers = null;
3047:                 TypeCheckInfo expConstraint = question;
3048:
3049:                 if (question.constraint != null)
3050:                 {
3051:                         PType stype = AstFactory.newASeqSeqType(node.getLocation(), question.constraint);
3052:                         expConstraint = question.newConstraint(stype);
3053:                 }
3054:
3055:                 PType result = exp.apply(THIS, expConstraint);
3056:
3057:                 if (question.assistantFactory.createPTypeAssistant().isSeq(result, question.fromModule))
3058:                 {
3059:                         PType inner = question.assistantFactory.createPTypeAssistant().getSeq(result, question.fromModule).getSeqof();
3060:
3061:                         if (question.assistantFactory.createPTypeAssistant().isSeq(inner, question.fromModule))
3062:                         {
3063:                                 node.setType(question.assistantFactory.createPTypeAssistant().getSeq(inner, question.fromModule));
3064:                                 return node.getType();
3065:                         }
3066:                 }
3067:
3068:                 TypeCheckerErrors.report(3075, "Argument of 'conc' is not a seq of seq", node.getLocation(), node);
3069:                 node.setType(AstFactory.newAUnknownType(node.getLocation()));
3070:                 return node.getType();
3071:         }
3072:
3073:         @Override public PType caseADistIntersectUnaryExp(
3074:                         ADistIntersectUnaryExp node, TypeCheckInfo question)
3075:                         throws AnalysisException
3076:         {
3077:                 PExp exp = node.getExp();
3078:                 question.qualifiers = null;
3079:                 PType arg = exp.apply(THIS, question.newConstraint(null));
3080:
3081:                 if (question.assistantFactory.createPTypeAssistant().isSet(arg, question.fromModule))
3082:                 {
3083:                         SSetType set = question.assistantFactory.createPTypeAssistant().getSet(arg, question.fromModule);
3084:
3085:                         if (set.getEmpty()
3086:                                         || question.assistantFactory.createPTypeAssistant().isSet(set.getSetof(), question.fromModule))
3087:                         {
3088:                                 node.setType(set.getSetof());
3089:                                 return set.getSetof();
3090:                         }
3091:                 }
3092:
3093:                 TypeCheckerErrors.report(3076, "Argument of 'dinter' is not a set of sets", node.getLocation(), node);
3094:                 node.setType(AstFactory.newAUnknownType(node.getLocation()));
3095:                 return node.getType();
3096:         }
3097:
3098:         @Override public PType caseADistMergeUnaryExp(ADistMergeUnaryExp node,
3099:                         TypeCheckInfo question) throws AnalysisException
3100:         {
3101:                 PExp exp = node.getExp();
3102:                 question.qualifiers = null;
3103:                 TypeCheckInfo expConstraint = question;
3104:
3105:                 if (question.constraint != null)
3106:                 {
3107:                         PType stype = AstFactory.newASetSetType(node.getLocation(), question.constraint);
3108:                         expConstraint = question.newConstraint(stype);
3109:                 }
3110:
3111:                 PType arg = exp.apply(THIS, expConstraint);
3112:
3113:                 if (question.assistantFactory.createPTypeAssistant().isSet(arg, question.fromModule))
3114:                 {
3115:                         SSetType set = question.assistantFactory.createPTypeAssistant().getSet(arg, question.fromModule);
3116:
3117:                         if (!set.getEmpty()
3118:                                         && question.assistantFactory.createPTypeAssistant().isMap(set.getSetof(), question.fromModule))
3119:                         {
3120:                                 node.setType(set.getSetof());
3121:                                 return set.getSetof();
3122:                         }
3123:                 }
3124:
3125:                 TypeCheckerErrors.report(3077, "Merge argument is not a set of maps", node.getLocation(), node);
3126:                 return AstFactory.newAMapMapType(node.getLocation()); // Unknown types
3127:         }
3128:
3129:         @Override public PType caseADistUnionUnaryExp(ADistUnionUnaryExp node,
3130:                         TypeCheckInfo question) throws AnalysisException
3131:         {
3132:                 PExp exp = node.getExp();
3133:                 question.qualifiers = null;
3134:                 TypeCheckInfo expConstraint = question;
3135:
3136:                 if (question.constraint != null)
3137:                 {
3138:                         PType stype = AstFactory.newASetSetType(node.getLocation(), question.constraint);
3139:                         expConstraint = question.newConstraint(stype);
3140:                 }
3141:
3142:                 PType type = exp.apply(THIS, expConstraint);
3143:
3144:                 if (question.assistantFactory.createPTypeAssistant().isSet(type, question.fromModule))
3145:                 {
3146:                         SSetType set = question.assistantFactory.createPTypeAssistant().getSet(type, question.fromModule);
3147:
3148:                         if (question.assistantFactory.createPTypeAssistant().isSet(set.getSetof(), question.fromModule))
3149:                         {
3150:                                 node.setType(set.getSetof());
3151:                                 return set.getSetof();
3152:                         }
3153:                 }
3154:
3155:                 TypeCheckerErrors.report(3078, "dunion argument is not a set of sets", node.getLocation(), node);
3156:                 node.setType(AstFactory.newASetSetType(node.getLocation(), AstFactory.newAUnknownType(node.getLocation())));
3157:                 return node.getType();
3158:         }
3159:
3160:         @Override public PType caseAFloorUnaryExp(AFloorUnaryExp node,
3161:                         TypeCheckInfo question) throws AnalysisException
3162:         {
3163:                 PExp exp = node.getExp();
3164:                 question.qualifiers = null;
3165:
3166:                 if (!question.assistantFactory.createPTypeAssistant().isNumeric(exp.apply(THIS, question.newConstraint(null)), question.fromModule))
3167:
3168:                 {
3169:                         TypeCheckerErrors.report(3096, "Argument to floor is not numeric", node.getLocation(), node);
3170:                 }
3171:
3172:                 node.setType(AstFactory.newAIntNumericBasicType(node.getLocation()));
3173:                 return node.getType();
3174:         }
3175:
3176:         @Override public PType caseAHeadUnaryExp(AHeadUnaryExp node,
3177:                         TypeCheckInfo question) throws AnalysisException
3178:         {
3179:                 PExp exp = node.getExp();
3180:                 question.qualifiers = null;
3181:
3182:                 PType etype = exp.apply(THIS, question.newConstraint(null));
3183:
3184:                 if (!question.assistantFactory.createPTypeAssistant().isSeq(etype, question.fromModule))
3185:                 {
3186:                         TypeCheckerErrors.report(3104, "Argument to 'hd' is not a sequence", node.getLocation(), node);
3187:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
3188:                         return node.getType();
3189:                 }
3190:
3191:                 node.setType(question.assistantFactory.createPTypeAssistant().getSeq(etype, question.fromModule).getSeqof());
3192:                 return node.getType();
3193:         }
3194:
3195:         @Override public PType caseAIndicesUnaryExp(AIndicesUnaryExp node,
3196:                         TypeCheckInfo question) throws AnalysisException
3197:         {
3198:                 PExp exp = node.getExp();
3199:                 question.qualifiers = null;
3200:
3201:                 PType etype = exp.apply(THIS, question.newConstraint(null));
3202:                 boolean empty = false;
3203:
3204:                 if (!question.assistantFactory.createPTypeAssistant().isSeq(etype, question.fromModule))
3205:                 {
3206:                         TypeCheckerErrors.report(3109, "Argument to 'inds' is not a sequence", node.getLocation(), node);
3207:                         TypeCheckerErrors.detail("Actual type", etype);
3208:                 }
3209:                 else
3210:                 {
3211:                         empty = question.assistantFactory.createPTypeAssistant().getSeq(etype, question.fromModule).getEmpty();
3212:                 }
3213:
3214:                 node.setType(AstFactory.newASetSetType(node.getLocation(), AstFactory.newANatOneNumericBasicType(node.getLocation())));
3215:                 ((ASetSetType)node.getType()).setEmpty(empty);
3216:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
3217:         }
3218:
3219:         @Override public PType caseALenUnaryExp(ALenUnaryExp node,
3220:                         TypeCheckInfo question) throws AnalysisException
3221:         {
3222:                 PExp exp = node.getExp();
3223:                 question.qualifiers = null;
3224:                 boolean seq1 = false;
3225:                 PType etype = exp.apply(THIS, question.newConstraint(null));
3226:
3227:                 if (!question.assistantFactory.createPTypeAssistant().isSeq(etype, question.fromModule))
3228:                 {
3229:                         TypeCheckerErrors.report(3116, "Argument to 'len' is not a sequence", node.getLocation(), node);
3230:                 }
3231:                 else
3232:                 {
3233:                         PType st = question.assistantFactory.createPTypeAssistant().getSeq(etype, question.fromModule);
3234:                         seq1 = st instanceof ASeq1SeqType;
3235:                 }
3236:
3237:                 node.setType(seq1 ?
3238:                         AstFactory.newANatOneNumericBasicType(node.getLocation()) :
3239:                         AstFactory.newANatNumericBasicType(node.getLocation()));
3240:
3241:                 return question.assistantFactory.createPTypeAssistant().possibleConstraint(question.constraint, node.getType(), node.getLocation());
3242:         }
3243:
3244:         @Override public PType caseAMapDomainUnaryExp(AMapDomainUnaryExp node,
3245:                         TypeCheckInfo question) throws AnalysisException
3246:         {
3247:                 PExp exp = node.getExp();
3248:                 question.qualifiers = null;
3249:
3250:                 PType etype = exp.apply(THIS, question.newConstraint(null));
3251:
3252:                 if (!question.assistantFactory.createPTypeAssistant().isMap(etype, question.fromModule))
3253:                 {
3254:                         TypeCheckerErrors.report(3120, "Argument to 'dom' is not a map", node.getLocation(), node);
3255:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
3256:                         return node.getType();
3257:                 }
3258:
3259:                 SMapType mt = question.assistantFactory.createPTypeAssistant().getMap(etype, question.fromModule);
3260:                 node.setType(AstFactory.newASetSetType(node.getLocation(), mt.getFrom()));
3261:                 return node.getType();
3262:         }
3263:
3264:         @Override public PType caseAMapInverseUnaryExp(AMapInverseUnaryExp node,
3265:                         TypeCheckInfo question) throws AnalysisException
3266:         {
3267:                 PExp exp = node.getExp();
3268:                 question.qualifiers = null;
3269:
3270:                 PType etype = exp.apply(THIS, question.newConstraint(null));
3271:
3272:                 if (!question.assistantFactory.createPTypeAssistant().isMap(etype, question.fromModule))
3273:                 {
3274:                         TypeCheckerErrors.report(3111, "Argument to 'inverse' is not a map", node.getLocation(), node);
3275:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
3276:                         return node.getType();
3277:                 }
3278:
3279:                 node.setMapType(question.assistantFactory.createPTypeAssistant().getMap(etype, question.fromModule));
3280:                 AMapMapType mm = AstFactory.newAMapMapType(node.getLocation(), node.getMapType().getTo(), node.getMapType().getFrom());
3281:                 node.setType(mm);
3282:
3283:                 return node.getType();
3284:         }
3285:
3286:         @Override public PType caseAMapRangeUnaryExp(AMapRangeUnaryExp node,
3287:                         TypeCheckInfo question) throws AnalysisException
3288:         {
3289:                 PExp exp = node.getExp();
3290:                 question.qualifiers = null;
3291:
3292:                 PType etype = exp.apply(THIS, question.newConstraint(null));
3293:
3294:                 if (!question.assistantFactory.createPTypeAssistant().isMap(etype, question.fromModule))
3295:                 {
3296:                         TypeCheckerErrors.report(3122, "Argument to 'rng' is not a map", node.getLocation(), node);
3297:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
3298:                         return node.getType();
3299:                 }
3300:
3301:                 SMapType mt = question.assistantFactory.createPTypeAssistant().getMap(etype, question.fromModule);
3302:                 node.setType(AstFactory.newASetSetType(node.getLocation(), mt.getTo()));
3303:                 return node.getType();
3304:         }
3305:
3306:         @Override public PType caseANotUnaryExp(ANotUnaryExp node,
3307:                         TypeCheckInfo question) throws AnalysisException
3308:         {
3309:                 PExp exp = node.getExp();
3310:                 question.qualifiers = null;
3311:
3312:                 PType t = exp.apply(THIS, question.newConstraint(null));
3313:
3314:                 if (!question.assistantFactory.createPTypeAssistant().isType(t, ABooleanBasicType.class))
3315:                 {
3316:                         TypeCheckerErrors.report(3137, "Not expression is not a boolean", node.getLocation(), node);
3317:                 }
3318:
3319:                 node.setType(AstFactory.newABooleanBasicType(node.getLocation()));
3320:                 return question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, node.getType(), node.getLocation());
3321:         }
3322:
3323:         @Override public PType caseAPowerSetUnaryExp(APowerSetUnaryExp node,
3324:                         TypeCheckInfo question) throws AnalysisException
3325:         {
3326:                 PExp exp = node.getExp();
3327:                 question.qualifiers = null;
3328:                 TypeCheckInfo argConstraint = question.newConstraint(null);
3329:
3330:                 if (question.constraint != null
3331:                                 && question.assistantFactory.createPTypeAssistant().isSet(question.constraint, question.fromModule))
3332:                 {
3333:                         PType stype = question.assistantFactory.createPTypeAssistant().getSet(question.constraint, question.fromModule).getSetof();
3334:                         argConstraint = question.newConstraint(stype);
3335:                 }
3336:
3337:                 PType etype = exp.apply(THIS, argConstraint);
3338:
3339:                 if (!question.assistantFactory.createPTypeAssistant().isSet(etype, question.fromModule))
3340:                 {
3341:                         TypeCheckerErrors.report(3145, "Argument to 'power' is not a set", node.getLocation(), node);
3342:                         node.setType(AstFactory.newAUnknownType(node.getLocation()));
3343:                         return node.getType();
3344:                 }
3345:
3346:                 SSetType eset = question.assistantFactory.createPTypeAssistant().getSet(etype, question.fromModule);
3347:
3348:                 node.setType(AstFactory.newASetSetType(node.getLocation(), AstFactory.newASetSetType(node.getLocation(), eset.getSetof())));
3349:                 return node.getType();
3350:         }
3351:
3352:         @Override public PType caseAReverseUnaryExp(AReverseUnaryExp node,
3353:                         TypeCheckInfo question) throws AnalysisException
3354:         {
3355:                 PExp exp = node.getExp();
3356:                 question.qualifiers = null;
3357:
3358:                 PType etype = exp.apply(THIS, question);
3359:
3360:                 if (!question.assistantFactory.createPTypeAssistant().isSeq(etype, question.fromModule))
3361:                 {
3362:                         TypeCheckerErrors.report(3295, "Argument to 'reverse' is not a sequence", node.getLocation(), node);
3363:                         ASeqSeqType tt = AstFactory.newASeqSeqType(node.getLocation(), AstFactory.newAUnknownType(node.getLocation()));
3364:                         node.setType(tt);
3365:                         return node.getType();
3366:                 }
3367:
3368:                 node.setType(etype);
3369:                 return etype;
3370:         }
3371:
3372:         @Override public PType caseATailUnaryExp(ATailUnaryExp node,
3373:                         TypeCheckInfo question) throws AnalysisException
3374:         {
3375:                 PExp exp = node.getExp();
3376:                 question.qualifiers = null;
3377:
3378:                 PType etype = exp.apply(THIS, question.newConstraint(null));
3379:
3380:                 if (!question.assistantFactory.createPTypeAssistant().isSeq(etype, question.fromModule))
3381:                 {
3382:                         TypeCheckerErrors.report(3179, "Argument to 'tl' is not a sequence", node.getLocation(), node);
3383:                         node.setType(AstFactory.newASeqSeqType(node.getLocation(), AstFactory.newAUnknownType(node.getLocation())));
3384:                         return node.getType();
3385:                 }
3386:                 else if (etype instanceof ASeq1SeqType)
3387:                 {
3388:                         ASeq1SeqType s = (ASeq1SeqType)etype;
3389:                         etype = AstFactory.newASeqSeqType(node.getLocation(), s.getSeqof());
3390:                 }
3391:
3392:                 node.setType(etype);
3393:                 return etype;
3394:         }
3395:
3396:         @Override public PType caseAUnaryMinusUnaryExp(AUnaryMinusUnaryExp node,
3397:                         TypeCheckInfo question) throws AnalysisException
3398:         {
3399:                 question.qualifiers = null;
3400:                 PType t = node.getExp().apply(THIS, question);
3401:
3402:                 if (t instanceof ANatNumericBasicType
3403:                                 || t instanceof ANatOneNumericBasicType)
3404:                 {
3405:                         t = AstFactory.newAIntNumericBasicType(node.getLocation());
3406:                         question.assistantFactory.createPTypeAssistant().checkConstraint(question.constraint, t, node.getLocation());
3407:                 }
3408:
3409:                 node.setType(t);
3410:                 return t;
3411:         }
3412:
3413:         @Override public PType caseAUnaryPlusUnaryExp(AUnaryPlusUnaryExp node,
3414:                         TypeCheckInfo question) throws AnalysisException
3415:         {
3416:                 question.qualifiers = null;
3417:                 node.setType(node.getExp().apply(THIS, question));
3418:                 return node.getType();
3419:         }
3420:
3421:         @Override public PType caseAElementsUnaryExp(AElementsUnaryExp node,
3422:                         TypeCheckInfo question) throws AnalysisException
3423:         {
3424:                 PExp etype = node.getExp();
3425:                 question.qualifiers = null;
3426:                 TypeCheckInfo argConstraint = question;
3427:
3428:                 if (question.constraint != null
3429:                                 && question.assistantFactory.createPTypeAssistant().isSet(question.constraint, question.fromModule))
3430:                 {
3431:                         PType stype = question.assistantFactory.createPTypeAssistant().getSet(question.constraint, question.fromModule).getSetof();
3432:                         stype = AstFactory.newASeqSeqType(node.getLocation(), stype);
3433:                         argConstraint = question.newConstraint(stype);
3434:                 }
3435:
3436:                 PType arg = etype.apply(THIS, argConstraint);
3437:
3438:                 if (!question.assistantFactory.createPTypeAssistant().isSeq(arg, question.fromModule))
3439:                 {
3440:                         TypeCheckerErrors.report(3085, "Argument of 'elems' is not a sequence", node.getLocation(), node);
3441:                         node.setType(AstFactory.newASetSetType(node.getLocation(), AstFactory.newAUnknownType(node.getLocation())));
3442:                         return node.getType();
3443:                 }
3444:
3445:                 SSeqType seq = question.assistantFactory.createPTypeAssistant().getSeq(arg, question.fromModule);
3446:                 node.setType(seq.getEmpty() ?
3447:                                 AstFactory.newASetSetType(node.getLocation()) :
3448:                                 AstFactory.newASetSetType(node.getLocation(), seq.getSeqof()));
3449:                 return node.getType();
3450:         }
3451:
3452:         private void checkNumeric(SNumericBinaryExp node,
3453:                         IQuestionAnswer<TypeCheckInfo, PType> rootVisitor,
3454:                         TypeCheckInfo question) throws AnalysisException
3455:         {
3456:                 node.getLeft().apply(rootVisitor, question.newConstraint(null));
3457:                 node.getRight().apply(rootVisitor, question.newConstraint(null));
3458:
3459:                 if (!question.assistantFactory.createPTypeAssistant().isNumeric(node.getLeft().getType(), question.fromModule))
3460:                 {
3461:                         TypeCheckerErrors.report(3139, "Left hand of " + node.getOp()
3462:                                         + " is not numeric", node.getLocation(), node);
3463:                         TypeCheckerErrors.detail("Actual", node.getLeft().getType());
3464:                         node.getLeft().setType(AstFactory.newARealNumericBasicType(node.getLocation()));
3465:                 }
3466:
3467:                 if (!question.assistantFactory.createPTypeAssistant().isNumeric(node.getRight().getType(), question.fromModule))
3468:                 {
3469:                         TypeCheckerErrors.report(3140, "Right hand of " + node.getOp()
3470:                                         + " is not numeric", node.getLocation(), node);
3471:                         TypeCheckerErrors.detail("Actual", node.getRight().getType());
3472:                         node.getRight().setType(AstFactory.newARealNumericBasicType(node.getLocation()));
3473:                 }
3474:
3475:         }
3476:
3477:         private void checkOrdered(SNumericBinaryExp node,
3478:                         IQuestionAnswer<TypeCheckInfo, PType> rootVisitor,
3479:                         TypeCheckInfo question) throws AnalysisException
3480:         {
3481:                 node.getLeft().apply(rootVisitor, question.newConstraint(null));
3482:                 node.getRight().apply(rootVisitor, question.newConstraint(null));
3483:
3484:                 if (!question.assistantFactory.createPTypeAssistant().isOrdered(node.getLeft().getType(), node.getLocation()))
3485:                 {
3486:                         TypeCheckerErrors.report(3139, "Left hand of " + node.getOp()
3487:                                         + " is not ordered", node.getLocation(), node);
3488:                         TypeCheckerErrors.detail("Actual", node.getLeft().getType());
3489:                         node.getLeft().setType(AstFactory.newARealNumericBasicType(node.getLocation()));
3490:                 }
3491:
3492:                 if (!question.assistantFactory.createPTypeAssistant().isOrdered(node.getRight().getType(), node.getLocation()))
3493:                 {
3494:                         TypeCheckerErrors.report(3140, "Right hand of " + node.getOp()
3495:                                         + " is not ordered", node.getLocation(), node);
3496:                         TypeCheckerErrors.detail("Actual", node.getRight().getType());
3497:                         node.getRight().setType(AstFactory.newARealNumericBasicType(node.getLocation()));
3498:                 }
3499:
3500:         }
3501:
3502:         public PType functionApply(AApplyExp node, boolean isSimple,
3503:                         AFunctionType ft, TypeCheckInfo question)
3504:         {
3505:                 List<PType> ptypes = ft.getParameters();
3506:
3507:                 if (node.getArgs().size() > ptypes.size())
3508:                 {
3509:                         TypeCheckerErrors.concern(isSimple, 3059, "Too many arguments", node.getLocation(), node);
3510:                         TypeCheckerErrors.detail2(isSimple, "Args", node.getArgs(), "Params", ptypes);
3511:                         return ft.getResult();
3512:                 } else if (node.getArgs().size() < ptypes.size())
3513:                 {
3514:                         TypeCheckerErrors.concern(isSimple, 3060, "Too few arguments", node.getLocation(), node);
3515:                         TypeCheckerErrors.detail2(isSimple, "Args", node.getArgs(), "Params", ptypes);
3516:                         return ft.getResult();
3517:                 }
3518:
3519:                 int i = 0;
3520:
3521:                 for (PType at : node.getArgtypes())
3522:                 {
3523:                         PType pt = ptypes.get(i++);
3524:
3525:                         if (!question.assistantFactory.getTypeComparator().compatible(pt, at))
3526:                         {
3527:                                 // TypeCheckerErrors.concern(isSimple, 3061, "Inappropriate type for argument " + i +
3528:                                 // ". (Expected: "+pt+" Actual: "+at+")",node.getLocation(),node);
3529:                                 TypeCheckerErrors.concern(isSimple, 3061,
3530:                                                 "Inappropriate type for argument "
3531:                                                                 + i, node.getArgs().get(
3532:                                                                 i - 1).getLocation(), node);
3533:                                 TypeCheckerErrors.detail2(isSimple, "Expect", pt, "Actual", at);
3534:                         } else if (at instanceof AFunctionType)
3535:                         {
3536:                                 AFunctionType fat = (AFunctionType) at;
3537:
3538:                                 if (fat.getInstantiated() != null && !fat.getInstantiated())
3539:                                 {
3540:                                         // Cannot pass uninstantiated polymorphic function arguments
3541:                                         TypeCheckerErrors.concern(isSimple, 3354, "Function argument must be instantiated", node.getArgs().get(
3542:                                                         i - 1).getLocation(), node);
3543:                                 }
3544:                         }
3545:                 }
3546:
3547:                 return ft.getResult();
3548:         }
3549:
3550:         public PType operationApply(AApplyExp node, boolean isSimple,
3551:                         AOperationType ot, TypeCheckInfo question)
3552:         {
3553:                 List<PType> ptypes = ot.getParameters();
3554:
3555:                 if (node.getArgs().size() > ptypes.size())
3556:                 {
3557:                         TypeCheckerErrors.concern(isSimple, 3062, "Too many arguments", node.getLocation(), node);
3558:                         TypeCheckerErrors.detail2(isSimple, "Args", node.getArgs(), "Params", ptypes);
3559:                         return ot.getResult();
3560:                 } else if (node.getArgs().size() < ptypes.size())
3561:                 {
3562:                         TypeCheckerErrors.concern(isSimple, 3063, "Too few arguments", node.getLocation(), node);
3563:                         TypeCheckerErrors.detail2(isSimple, "Args", node.getArgs(), "Params", ptypes);
3564:                         return ot.getResult();
3565:                 }
3566:
3567:                 int i = 0;
3568:
3569:                 for (PType at : node.getArgtypes())
3570:                 {
3571:                         PType pt = ptypes.get(i++);
3572:
3573:                         if (!question.assistantFactory.getTypeComparator().compatible(pt, at))
3574:                         {
3575:                                 // TypeCheckerErrors.concern(isSimple, 3064, "Inappropriate type for argument " + i
3576:                                 // +". (Expected: "+pt+" Actual: "+at+")",node.getLocation(),node);
3577:                                 TypeCheckerErrors.concern(isSimple, 3064,
3578:                                                 "Inappropriate type for argument "
3579:                                                                 + i, node.getLocation(), node);
3580:                                 TypeCheckerErrors.detail2(isSimple, "Expect", pt, "Actual", at);
3581:                         }
3582:                 }
3583:
3584:                 return ot.getResult();
3585:         }
3586:
3587:         public PType sequenceApply(AApplyExp node, boolean isSimple, SSeqType seq,
3588:                         TypeCheckInfo question)
3589:         {
3590:                 if (node.getArgs().size() != 1)
3591:                 {
3592:                         TypeCheckerErrors.concern(isSimple, 3055, "Sequence selector must have one argument", node.getLocation(), node);
3593:                 } else if (!question.assistantFactory.createPTypeAssistant().isNumeric(node.getArgtypes().get(0), question.fromModule))
3594:                 {
3595:                         TypeCheckerErrors.concern(isSimple, 3056, "Sequence application argument must be numeric", node.getLocation(), node);
3596:                 } else if (seq.getEmpty())
3597:                 {
3598:                         TypeCheckerErrors.concern(isSimple, 3268, "Empty sequence cannot be applied", node.getLocation(), node);
3599:                 }
3600:
3601:                 return seq.getSeqof();
3602:         }
3603:
3604:         public PType mapApply(AApplyExp node, boolean isSimple, SMapType map,
3605:                         TypeCheckInfo question)
3606:         {
3607:                 if (map.getEmpty())
3608:                 {
3609:                         TypeCheckerErrors.concern(isSimple, 3267, "Empty map cannot be applied", node.getLocation(), node);
3610:                 }
3611:
3612:                 if (node.getArgs().size() != 1)
3613:                 {
3614:                         TypeCheckerErrors.concern(isSimple, 3057, "Map application must have one argument", node.getLocation(), node);
3615:                 } else
3616:                 {
3617:                         PType argtype = node.getArgtypes().get(0);
3618:
3619:                         if (!question.assistantFactory.getTypeComparator().compatible(map.getFrom(), argtype))
3620:                         {
3621:                                 TypeCheckerErrors.concern(isSimple, 3058, "Map application argument is incompatible type", node.getLocation(), node);
3622:                                 TypeCheckerErrors.detail2(isSimple, "Map domain", map.getFrom(), "Argument", argtype);
3623:                         }
3624:                 }
3625:
3626:                 return map.getTo();
3627:         }
3628:
3629:         public PDefinition getRecursiveDefinition(AApplyExp node,
3630:                         TypeCheckInfo question)
3631:         {
3632:                 ILexNameToken fname = null;
3633:                 PExp root = node.getRoot();
3634:
3635:                 if (root instanceof AApplyExp)
3636:                 {
3637:                         AApplyExp aexp = (AApplyExp) root;
3638:                         return getRecursiveDefinition(aexp, question);
3639:                 } else if (root instanceof AVariableExp)
3640:                 {
3641:                         AVariableExp var = (AVariableExp) root;
3642:                         fname = var.getName();
3643:                 } else if (root instanceof AFuncInstatiationExp)
3644:                 {
3645:                         AFuncInstatiationExp fie = (AFuncInstatiationExp) root;
3646:
3647:                         if (fie.getExpdef() != null)
3648:                         {
3649:                                 fname = fie.getExpdef().getName();
3650:                         } else if (fie.getImpdef() != null)
3651:                         {
3652:                                 fname = fie.getImpdef().getName();
3653:                         }
3654:                 }
3655:
3656:                 if (fname != null)
3657:                 {
3658:                         return question.env.findName(fname, question.scope);
3659:                 } else
3660:                 {
3661:                         return null;
3662:                 }
3663:         }
3664:
3665:         /**
3666:          * Create a measure application string from this apply, turning the root function name into the measure name passed,
3667:          * and collapsing curried argument sets into one.
3668:          *
3669:          * @param node
3670:          * @param measure
3671:          * @param close
3672:          * @return
3673:          */
3674:         public String getMeasureApply(AApplyExp node, ILexNameToken measure,
3675:                         boolean close)
3676:         {
3677:                 String start = null;
3678:                 PExp root = node.getRoot();
3679:
3680:                 if (root instanceof AApplyExp)
3681:                 {
3682:                         AApplyExp aexp = (AApplyExp) root;
3683:                         start = getMeasureApply(aexp, measure, false);
3684:                 } else if (root instanceof AVariableExp)
3685:                 {
3686:                         start = measure.getFullName() + "(";
3687:                 } else if (root instanceof AFuncInstatiationExp)
3688:                 {
3689:                         AFuncInstatiationExp fie = (AFuncInstatiationExp) root;
3690:                         start = measure.getFullName() + "["
3691:                                         + Utils.listToString(fie.getActualTypes()) + "](";
3692:                 } else
3693:                 {
3694:                         start = root.toString() + "(";
3695:                 }
3696:
3697:                 return start + Utils.listToString(node.getArgs()) + (close ?
3698:                                 ")" :
3699:                                 ", ");
3700:         }
3701:
3702:         public PType typeCheck(ACaseAlternative c,
3703:                         IQuestionAnswer<TypeCheckInfo, PType> rootVisitor,
3704:                         TypeCheckInfo question, PType expType) throws AnalysisException
3705:         {
3706:
3707:                 if (c.getDefs().size() == 0)
3708:                 {
3709:                         // c.setDefs(new ArrayList<PDefinition>());
3710:                         question.assistantFactory.createPPatternAssistant(question.fromModule).typeResolve(c.getPattern(), rootVisitor, new TypeCheckInfo(question.assistantFactory, question.env));
3711:
3712:                         if (c.getPattern() instanceof AExpressionPattern)
3713:                         {
3714:                                 // Only expression patterns need type checking...
3715:                                 AExpressionPattern ep = (AExpressionPattern) c.getPattern();
3716:                                 PType ptype = ep.getExp().apply(rootVisitor, new TypeCheckInfo(question.assistantFactory, question.env, question.scope));
3717:
3718:                                 if (!question.assistantFactory.getTypeComparator().compatible(ptype, expType))
3719:                                 {
3720:                                         TypeCheckerErrors.report(3311, "Pattern cannot match", c.getPattern().getLocation(), c.getPattern());
3721:                                 }
3722:                         }
3723:
3724:                         try
3725:                         {
3726:                                 question.assistantFactory.createPPatternAssistant(question.fromModule).typeResolve(c.getPattern(), rootVisitor, new TypeCheckInfo(question.assistantFactory, question.env));
3727:                                 c.getDefs().addAll(question.assistantFactory.createPPatternAssistant(question.fromModule).getDefinitions(c.getPattern(), expType, NameScope.LOCAL));
3728:                         } catch (TypeCheckException e)
3729:                         {
3730:                                 c.getDefs().clear();
3731:                                 throw e;
3732:                         }
3733:                 }
3734:
3735:                 question.assistantFactory.createPPatternAssistant(question.fromModule).typeCheck(c.getPattern(), question, rootVisitor);
3736:                 question.assistantFactory.createPDefinitionListAssistant().typeCheck(c.getDefs(), rootVisitor, new TypeCheckInfo(question.assistantFactory, question.env, question.scope));
3737:
3738:                 if (!question.assistantFactory.createPPatternAssistant(question.fromModule).matches(c.getPattern(), expType))
3739:                 {
3740:                         TypeCheckerErrors.report(3311, "Pattern cannot match", c.getPattern().getLocation(), c.getPattern());
3741:                 }
3742:
3743:                 Environment local = new FlatCheckedEnvironment(question.assistantFactory, c.getDefs(), question.env, question.scope);
3744:                 question = question.newInfo(local);
3745:                 c.setType(c.getResult().apply(rootVisitor, question));
3746:                 local.unusedCheck();
3747:                 return c.getType();
3748:         }
3749:
3750:         public ABooleanBasicType binaryCheck(SBooleanBinaryExp node,
3751:                         ABooleanBasicType expected,
3752:                         IQuestionAnswer<TypeCheckInfo, PType> rootVisitor,
3753:                         TypeCheckInfo question) throws AnalysisException
3754:         {
3755:
3756:                 node.getLeft().apply(rootVisitor, question);
3757:                 node.getRight().apply(rootVisitor, question);
3758:
3759:                 if (!question.assistantFactory.createPTypeAssistant().isType(node.getLeft().getType(), expected.getClass()))
3760:                 {
3761:                         TypeCheckerErrors.report(3065,
3762:                                         "Left hand of " + node.getOp() + " is not "
3763:                                                         + expected, node.getLocation(), node);
3764:                 }
3765:
3766:                 if (!question.assistantFactory.createPTypeAssistant().isType(node.getRight().getType(), expected.getClass()))
3767:                 {
3768:                         TypeCheckerErrors.report(3066,
3769:                                         "Right hand of " + node.getOp() + " is not "
3770:                                                         + expected, node.getLocation(), node);
3771:                 }
3772:
3773:                 node.setType(expected);
3774:                 return (ABooleanBasicType) node.getType();
3775:
3776:         }
3777: }