Method: typeCheck(List, IQuestionAnswer, 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.Collection;
25: import java.util.Collections;
26: import java.util.List;
27: import java.util.Vector;
28: import java.util.Map.Entry;
29:
30: import org.overture.ast.analysis.AnalysisException;
31: import org.overture.ast.analysis.intf.IQuestionAnswer;
32: import org.overture.ast.annotations.PAnnotation;
33: import org.overture.ast.definitions.AAssignmentDefinition;
34: import org.overture.ast.definitions.AClassInvariantDefinition;
35: import org.overture.ast.definitions.AEqualsDefinition;
36: import org.overture.ast.definitions.AExplicitFunctionDefinition;
37: import org.overture.ast.definitions.AExplicitOperationDefinition;
38: import org.overture.ast.definitions.AExternalDefinition;
39: import org.overture.ast.definitions.AImplicitFunctionDefinition;
40: import org.overture.ast.definitions.AImplicitOperationDefinition;
41: import org.overture.ast.definitions.AImportedDefinition;
42: import org.overture.ast.definitions.AInheritedDefinition;
43: import org.overture.ast.definitions.AInstanceVariableDefinition;
44: import org.overture.ast.definitions.ALocalDefinition;
45: import org.overture.ast.definitions.AMultiBindListDefinition;
46: import org.overture.ast.definitions.AMutexSyncDefinition;
47: import org.overture.ast.definitions.ANamedTraceDefinition;
48: import org.overture.ast.definitions.APerSyncDefinition;
49: import org.overture.ast.definitions.ARenamedDefinition;
50: import org.overture.ast.definitions.AStateDefinition;
51: import org.overture.ast.definitions.AThreadDefinition;
52: import org.overture.ast.definitions.ATypeDefinition;
53: import org.overture.ast.definitions.AUntypedDefinition;
54: import org.overture.ast.definitions.AValueDefinition;
55: import org.overture.ast.definitions.PDefinition;
56: import org.overture.ast.definitions.SClassDefinition;
57: import org.overture.ast.definitions.SFunctionDefinitionBase;
58: import org.overture.ast.definitions.relations.AEqRelation;
59: import org.overture.ast.definitions.relations.AOrdRelation;
60: import org.overture.ast.definitions.traces.AApplyExpressionTraceCoreDefinition;
61: import org.overture.ast.definitions.traces.ABracketedExpressionTraceCoreDefinition;
62: import org.overture.ast.definitions.traces.AConcurrentExpressionTraceCoreDefinition;
63: import org.overture.ast.definitions.traces.ALetBeStBindingTraceDefinition;
64: import org.overture.ast.definitions.traces.ALetDefBindingTraceDefinition;
65: import org.overture.ast.definitions.traces.ARepeatTraceDefinition;
66: import org.overture.ast.definitions.traces.ATraceDefinitionTerm;
67: import org.overture.ast.definitions.traces.PTraceDefinition;
68: import org.overture.ast.expressions.ANotYetSpecifiedExp;
69: import org.overture.ast.expressions.ASubclassResponsibilityExp;
70: import org.overture.ast.expressions.AUndefinedExp;
71: import org.overture.ast.expressions.AVariableExp;
72: import org.overture.ast.factory.AstFactory;
73: import org.overture.ast.intf.lex.ILexNameToken;
74: import org.overture.ast.lex.LexNameToken;
75: import org.overture.ast.lex.VDMToken;
76: import org.overture.ast.node.NodeList;
77: import org.overture.ast.patterns.APatternListTypePair;
78: import org.overture.ast.patterns.ATypeBind;
79: import org.overture.ast.patterns.PMultipleBind;
80: import org.overture.ast.patterns.PPattern;
81: import org.overture.ast.statements.AErrorCase;
82: import org.overture.ast.statements.AExternalClause;
83: import org.overture.ast.statements.ANotYetSpecifiedStm;
84: import org.overture.ast.statements.ASubclassResponsibilityStm;
85: import org.overture.ast.typechecker.NameScope;
86: import org.overture.ast.typechecker.Pass;
87: import org.overture.ast.types.ABooleanBasicType;
88: import org.overture.ast.types.AClassType;
89: import org.overture.ast.types.AFieldField;
90: import org.overture.ast.types.AFunctionType;
91: import org.overture.ast.types.ANamedInvariantType;
92: import org.overture.ast.types.AOperationType;
93: import org.overture.ast.types.AProductType;
94: import org.overture.ast.types.ARecordInvariantType;
95: import org.overture.ast.types.AUnknownType;
96: import org.overture.ast.types.AVoidType;
97: import org.overture.ast.types.PType;
98: import org.overture.ast.util.PTypeSet;
99: import org.overture.typechecker.Environment;
100: import org.overture.typechecker.ExcludedDefinitions;
101: import org.overture.typechecker.FlatCheckedEnvironment;
102: import org.overture.typechecker.FlatEnvironment;
103: import org.overture.typechecker.PrivateClassEnvironment;
104: import org.overture.typechecker.TypeCheckInfo;
105: import org.overture.typechecker.TypeChecker;
106: import org.overture.typechecker.TypeCheckerErrors;
107: import org.overture.typechecker.assistant.ITypeCheckerAssistantFactory;
108: import org.overture.typechecker.assistant.definition.PAccessSpecifierAssistantTC;
109: import org.overture.typechecker.assistant.type.PTypeAssistantTC;
110: import org.overture.typechecker.utilities.DefinitionTypeResolver;
111: import org.overture.typechecker.utilities.type.QualifiedDefinition;
112:
113: public class TypeCheckerDefinitionVisitor extends AbstractTypeCheckVisitor
114: {
115:
116:         public TypeCheckerDefinitionVisitor(
117:                         IQuestionAnswer<TypeCheckInfo, PType> typeCheckVisitor)
118:         {
119:                 super(typeCheckVisitor);
120:         }
121:
122:         @Override
123:         public PType caseAAssignmentDefinition(AAssignmentDefinition node,
124:                         TypeCheckInfo question) throws AnalysisException
125:         {
126:                 question.qualifiers = null;
127:
128:                 node.setType(question.assistantFactory.createPTypeAssistant().typeResolve(question.assistantFactory.createPDefinitionAssistant().getType(node), null, THIS, question));
129:
130:                 ExcludedDefinitions.setExcluded(node);
131:                 node.setExpType(node.getExpression().apply(THIS, question));
132:                 ExcludedDefinitions.clearExcluded();
133:
134:                 question.assistantFactory.getTypeComparator().checkComposeTypes(node.getType(), question.env, false);
135:
136:                 if (node.getExpType() instanceof AVoidType)
137:                 {
138:                         TypeCheckerErrors.report(3048, "Expression does not return a value", node.getExpression().getLocation(), node.getExpression());
139:                 }
140:
141:                 if (!question.assistantFactory.getTypeComparator().compatible(node.getType(), node.getExpType()))
142:                 {
143:                         TypeCheckerErrors.report(3000, "Expression does not match declared type", node.getExpression().getLocation(), node);
144:                         TypeCheckerErrors.detail2("Declared", node.getType(), "Expression", node.getExpType());
145:                 }
146:
147:                 return node.getType();
148:         }
149:
150:         @Override
151:         public PType caseAInstanceVariableDefinition(
152:                         AInstanceVariableDefinition node, TypeCheckInfo question)
153:                         throws AnalysisException
154:         {
155:                 checkAnnotations(node, question);
156:                 beforeAnnotations(node.getAnnotations(), node, question);
157:
158:                 if (node.getExpression() instanceof AUndefinedExp)
159:                 {
160:                         if (question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()))
161:                         {
162:                                 TypeCheckerErrors.report(3037, "Static instance variable is not initialized: "
163:                                                 + node.getName(), node.getLocation(), node);
164:                         }
165:                 }
166:
167:                 // Initializers can reference class members, so create a new env.
168:                 // We set the type qualifier to unknown so that type-based name
169:                 // resolution will succeed.
170:
171:                 Environment cenv = new PrivateClassEnvironment(question.assistantFactory, node.getClassDefinition(), question.env);
172:
173:                 if (question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()))
174:                 {
175:                         FlatCheckedEnvironment checked = new FlatCheckedEnvironment(question.assistantFactory, new Vector<PDefinition>(), question.env, NameScope.NAMES);
176:                         checked.setStatic(true);
177:                         cenv = checked;
178:                 }
179:                 
180:                 // TODO: This should be a call to the assignment definition typecheck
181:                 // but instance is not an subclass of
182:                 // assignment in our tree
183:                 ExcludedDefinitions.setExcluded(node);
184:                 node.setExpType(node.getExpression().apply(THIS, new TypeCheckInfo(question.assistantFactory, cenv, NameScope.NAMESANDSTATE, question.qualifiers)));
185:                 ExcludedDefinitions.clearExcluded();
186:                 node.setType(question.assistantFactory.createPTypeAssistant().typeResolve(question.assistantFactory.createPDefinitionAssistant().getType(node), null, THIS, question));
187:
188:                 if (node.getExpType() instanceof AVoidType)
189:                 {
190:                         TypeCheckerErrors.report(3048, "Expression does not return a value", node.getExpression().getLocation(), node.getExpression());
191:                 }
192:
193:                 if (!question.assistantFactory.getTypeComparator().compatible(question.assistantFactory.createPDefinitionAssistant().getType(node), node.getExpType()))
194:                 {
195:                         TypeCheckerErrors.report(3000, "Expression does not match declared type", node.getLocation(), node);
196:                         TypeCheckerErrors.detail2("Declared", question.assistantFactory.createPDefinitionAssistant().getType(node), "Expression", node.getExpType());
197:                 }
198:
199:                 afterAnnotations(node.getAnnotations(), node, question);
200:                 return node.getType();
201:
202:         }
203:
204:         @Override
205:         public PType caseAClassInvariantDefinition(AClassInvariantDefinition node,
206:                         TypeCheckInfo question) throws AnalysisException
207:         {
208:                 Environment newEnv = new FlatEnvironment(question.assistantFactory, question.env, true);
209:                 newEnv.setEnclosingDefinition(node);
210:                 TypeCheckInfo functional = question.newInfo(newEnv);
211:                 functional.qualifiers = null;
212:                 functional.scope = NameScope.NAMESANDSTATE;
213:                 
214:                 PType type = node.getExpression().apply(THIS, functional);
215:
216:                 if (!question.assistantFactory.createPTypeAssistant().isType(type, ABooleanBasicType.class))
217:                 {
218:                         TypeCheckerErrors.report(3013, "Class invariant is not a boolean expression", node.getLocation(), node);
219:                 }
220:
221:                 node.setType(type);
222:                 return node.getType();
223:         }
224:
225:         @Override
226:         public PType caseAEqualsDefinition(AEqualsDefinition node,
227:                         TypeCheckInfo question) throws AnalysisException
228:         {
229:
230:                 question.qualifiers = null;
231:
232:                 node.setExpType(node.getTest().apply(THIS, question));
233:                 PPattern pattern = node.getPattern();
234:
235:                 if (pattern != null)
236:                 {
237:                         question.assistantFactory.createPPatternAssistant(question.fromModule).typeResolve(pattern, THIS, question);
238:                         node.setDefs(question.assistantFactory.createPPatternAssistant(question.fromModule).getDefinitions(pattern, node.getExpType(), question.scope));
239:                         node.setDefType(node.getExpType());
240:                 }
241:                 else if (node.getTypebind() != null)
242:                 {
243:                         question.assistantFactory.createATypeBindAssistant().typeResolve(node.getTypebind(), THIS, question);
244:                         ATypeBind typebind = node.getTypebind();
245:
246:                         if (!question.assistantFactory.getTypeComparator().compatible(typebind.getType(), node.getExpType()))
247:                         {
248:                                 TypeCheckerErrors.report(3014, "Expression is not compatible with type bind", typebind.getLocation(), typebind);
249:                         }
250:
251:                         node.setDefType(typebind.getType()); // Effectively a cast
252:                         node.setDefs(question.assistantFactory.createPPatternAssistant(question.fromModule).getDefinitions(typebind.getPattern(), node.getDefType(), question.scope));
253:                 }
254:                 else if (node.getSetbind() != null)
255:                 {
256:                         question.qualifiers = null;
257:                         PType st = node.getSetbind().getSet().apply(THIS, question);
258:
259:                         if (!question.assistantFactory.createPTypeAssistant().isSet(st, question.fromModule))
260:                         {
261:                                 TypeCheckerErrors.report(3015, "Set bind is not a set type?", node.getLocation(), node);
262:                                 node.setDefType(node.getExpType());
263:                         }
264:                         else
265:                         {
266:                                 PType setof = question.assistantFactory.createPTypeAssistant().getSet(st, question.fromModule).getSetof();
267:
268:                                 if (!question.assistantFactory.getTypeComparator().compatible(node.getExpType(), setof))
269:                                 {
270:                                         TypeCheckerErrors.report(3016, "Expression is not compatible with set bind", node.getSetbind().getLocation(), node.getSetbind());
271:                                 }
272:
273:                                 node.setDefType(setof); // Effectively a cast
274:                         }
275:
276:                         question.assistantFactory.createPPatternAssistant(question.fromModule).typeResolve(node.getSetbind().getPattern(), THIS, question);
277:                         node.setDefs(question.assistantFactory.createPPatternAssistant(question.fromModule).getDefinitions(node.getSetbind().getPattern(), node.getDefType(), question.scope));
278:                 }
279:                 else // Seq bind
280:                 {
281:                         question.qualifiers = null;
282:                         PType st = node.getSeqbind().getSeq().apply(THIS, question);
283:
284:                         if (!question.assistantFactory.createPTypeAssistant().isSeq(st, question.fromModule))
285:                         {
286:                                 TypeCheckerErrors.report(3015, "Seq bind is not a seq type?", node.getLocation(), node);
287:                                 node.setDefType(node.getExpType());
288:                         }
289:                         else
290:                         {
291:                                 PType seqof = question.assistantFactory.createPTypeAssistant().getSeq(st, question.fromModule).getSeqof();
292:
293:                                 if (!question.assistantFactory.getTypeComparator().compatible(node.getExpType(), seqof))
294:                                 {
295:                                         TypeCheckerErrors.report(3016, "Expression is not compatible with seq bind", node.getSeqbind().getLocation(), node.getSeqbind());
296:                                 }
297:
298:                                 node.setDefType(seqof); // Effectively a cast
299:                         }
300:
301:                         question.assistantFactory.createPPatternAssistant(question.fromModule).typeResolve(node.getSeqbind().getPattern(), THIS, question);
302:                         node.setDefs(question.assistantFactory.createPPatternAssistant(question.fromModule).getDefinitions(node.getSeqbind().getPattern(), node.getDefType(), question.scope));
303:                 }
304:
305:                 question.assistantFactory.createPDefinitionListAssistant().typeCheck(node.getDefs(), THIS, question);
306:                 return node.getType();
307:         }
308:
309:         @Override
310:         public PType caseAExplicitFunctionDefinition(
311:                         AExplicitFunctionDefinition node, TypeCheckInfo question)
312:                         throws AnalysisException
313:         {
314:                 checkAnnotations(node, question);
315:                 beforeAnnotations(node.getAnnotations(), node, question);
316:
317:                 NodeList<PDefinition> defs = new NodeList<PDefinition>(node);
318:                 question.assistantFactory.getTypeComparator().checkComposeTypes(node.getType(), question.env, false);
319:
320:                 if (node.getTypeParams() != null)
321:                 {
322:                         defs.addAll(question.assistantFactory.createAExplicitFunctionDefinitionAssistant().getTypeParamDefinitions(node));
323:                 }
324:
325:                 PType expectedResult = question.assistantFactory.createAExplicitFunctionDefinitionAssistant().checkParams(node, node.getParamPatternList().listIterator(), (AFunctionType) node.getType());
326:                 node.setExpectedResult(expectedResult);
327:                 List<List<PDefinition>> paramDefinitionList = question.assistantFactory.createSFunctionDefinitionAssistant().getParamDefinitions(node, (AFunctionType) node.getType(), node.getParamPatternList(), node.getLocation());
328:
329:                 Collections.reverse(paramDefinitionList);
330:
331:                 for (List<PDefinition> pdef : paramDefinitionList)
332:                 {
333:                         defs.addAll(pdef); // All definitions of all parameter lists
334:                 }
335:
336:                 FlatCheckedEnvironment local = new FlatCheckedEnvironment(question.assistantFactory, defs, question.env, question.scope);
337:
338:                 local.setStatic(question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()));
339:                 local.setEnclosingDefinition(node);
340:                 local.setFunctional(true);
341:
342:
343:                 // building the new scope for subtypechecks
344:
345:                 question.assistantFactory.createPDefinitionListAssistant().typeCheck(defs, this, new TypeCheckInfo(question.assistantFactory, local, question.scope, question.qualifiers)); // can
346:                                                                                                                                                                                                                                                                                                                                                                         // be
347:                                                                                                                                                                                                                                                                                                                                                                         // this
348:                                                                                                                                                                                                                                                                                                                                                                         // because
349:                                                                                                                                                                                                                                                                                                                                                                         // its
350:                                                                                                                                                                                                                                                                                                                                                                         // a
351:                                                                                                                                                                                                                                                                                                                                                                         // definition
352:                                                                                                                                                                                                                                                                                                                                                                         // list
353:
354:                 if (question.env.isVDMPP()
355:                                 && !question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()))
356:                 {
357:                         local.add(question.assistantFactory.createPDefinitionAssistant().getSelfDefinition(node));
358:                 }
359:
360:                 List<QualifiedDefinition> qualified = new Vector<QualifiedDefinition>();
361:
362:                 if (node.getPredef() != null)
363:                 {
364:                         // building the new scope for subtypechecks
365:                         FlatEnvironment pre = new FlatEnvironment(question.assistantFactory, new Vector<PDefinition>(), local);
366:                         pre.setFunctional(true);
367:                         pre.setEnclosingDefinition(node.getPredef());
368:
369:                         PType b = node.getPredef().getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, pre, NameScope.NAMES));
370:                         ABooleanBasicType expected = AstFactory.newABooleanBasicType(node.getLocation());
371:
372:                         if (!question.assistantFactory.createPTypeAssistant().isType(b, ABooleanBasicType.class))
373:                         {
374:                                 TypeChecker.report(3018, "Precondition returns unexpected type", node.getLocation());
375:                                 TypeChecker.detail2("Actual", b, "Expected", expected);
376:                         }
377:
378:                         qualified = node.getPredef().getBody().apply(question.assistantFactory.getQualificationVisitor(), new TypeCheckInfo(question.assistantFactory, local, NameScope.NAMES));
379:
380:                         for (QualifiedDefinition qdef : qualified)
381:                         {
382:                                 qdef.qualifyType();
383:                         }
384:                 }
385:
386:                 if (node.getPostdef() != null)
387:                 {
388:                         LexNameToken result = new LexNameToken(node.getName().getModule(), "RESULT", node.getLocation());
389:                         PPattern rp = AstFactory.newAIdentifierPattern(result);
390:                         List<PDefinition> rdefs = question.assistantFactory.createPPatternAssistant(question.fromModule).getDefinitions(rp, expectedResult, NameScope.NAMES);
391:                         FlatCheckedEnvironment post = new FlatCheckedEnvironment(question.assistantFactory, rdefs, local, NameScope.NAMES);
392:                         post.setFunctional(true);
393:                         post.setEnclosingDefinition(node.getPostdef());
394:
395:                         // building the new scope for subtypechecks
396:                         PType b = node.getPostdef().getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, post, NameScope.NAMES));
397:                         ABooleanBasicType expected = AstFactory.newABooleanBasicType(node.getLocation());
398:
399:                         if (!question.assistantFactory.createPTypeAssistant().isType(b, ABooleanBasicType.class))
400:                         {
401:                                 TypeChecker.report(3018, "Postcondition returns unexpected type", node.getLocation());
402:                                 TypeChecker.detail2("Actual", b, "Expected", expected);
403:                         }
404:                 }
405:
406:                 // This check returns the type of the function body in the case where
407:                 // all of the curried parameter sets are provided.
408:
409:                 PType actualResult = node.getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, local, question.scope, null, expectedResult, null, question.fromModule, question.mandatory));
410:
411:                 node.setActualResult(actualResult);
412:
413:                 for (QualifiedDefinition qdef : qualified)
414:                 {
415:                         qdef.resetType();
416:                 }
417:
418:                 if (!question.assistantFactory.getTypeComparator().compatible(expectedResult, node.getActualResult()))
419:                 {
420:                         TypeChecker.report(3018, "Function returns unexpected type", node.getLocation());
421:                         TypeChecker.detail2("Actual", node.getActualResult(), "Expected", expectedResult);
422:                 }
423:
424:                 if (question.assistantFactory.createPTypeAssistant().narrowerThan(node.getType(), node.getAccess()))
425:                 {
426:                         TypeCheckerErrors.report(3019, "Function parameter visibility less than function definition", node.getLocation(), node);
427:                 }
428:
429:                 if (question.env.isVDMPP())
430:                 {
431:                         PAccessSpecifierAssistantTC assist = question.assistantFactory.createPAccessSpecifierAssistant();
432:
433:                         if (assist.isPrivate(node.getAccess())
434:                                         && node.getBody() instanceof ASubclassResponsibilityExp)
435:                         {
436:                                 TypeCheckerErrors.report(3329, "Abstract function/operation must be public or protected", node.getLocation(), node);
437:                         }
438:                 }
439:
440:                 if (node.getMeasure() instanceof AVariableExp)
441:                 {
442:                         AVariableExp exp = (AVariableExp)node.getMeasure();
443:                         List<PType> params = question.assistantFactory.createAExplicitFunctionDefinitionAssistant().getMeasureParams(node);
444:                         if (question.env.isVDMPP()) exp.getName().setTypeQualifier(params);
445:                         PDefinition def = question.env.findName(exp.getName(), question.scope);
446:                         
447:                         if (def instanceof AExplicitFunctionDefinition)
448:                         {
449:                                 setMeasureDef(question, node, exp.getName(), question.env, question.scope);
450:                         }
451:                         else
452:                         {
453:                                 setMeasureExp(question, node, question.env, local, question.scope);
454:                         }
455:                 }
456:                 else if (node.getMeasure() instanceof ANotYetSpecifiedExp)
457:                 {
458:                         // Undefined measure, so ignore (without warning).
459:                         node.setMeasureDef(null);
460:                         node.setMeasureName(null);
461:                 }
462:                 else if (node.getMeasure() != null)
463:                 {
464:                         setMeasureExp(question, node, question.env, local, question.scope);
465:                 }
466:
467:                 if (!(node.getBody() instanceof ANotYetSpecifiedExp)
468:                                 && !(node.getBody() instanceof ASubclassResponsibilityExp)
469:                                 && !(node.getName().toString().startsWith("measure_")))
470:                 {
471:                         local.unusedCheck();
472:                 }
473:
474:                 node.setType(node.getType());
475:                 afterAnnotations(node.getAnnotations(), node, question);
476:                 return node.getType();
477:         }
478:
479:         @Override
480:         public PType caseAExternalDefinition(AExternalDefinition node,
481:                         TypeCheckInfo question)
482:         {
483:                 // Nothing to do - state is type checked separately
484:                 return null;
485:         }
486:
487:         @Override
488:         public PType caseAImplicitFunctionDefinition(
489:                         AImplicitFunctionDefinition node, TypeCheckInfo question)
490:                         throws AnalysisException
491:         {
492:                 checkAnnotations(node, question);
493:                 beforeAnnotations(node.getAnnotations(), node, question);
494:
495:                 question.assistantFactory.getTypeComparator().checkComposeTypes(node.getType(), question.env, false);
496:                 List<PDefinition> defs = new Vector<PDefinition>();
497:
498:                 if (node.getTypeParams() != null)
499:                 {
500:                         defs.addAll(question.assistantFactory.createAImplicitFunctionDefinitionAssistant().getTypeParamDefinitions(node));
501:                 }
502:
503:                 List<PDefinition> argdefs = new Vector<PDefinition>();
504:
505:                 for (APatternListTypePair pltp : node.getParamPatterns())
506:                 {
507:                         argdefs.addAll(getDefinitions(pltp, NameScope.LOCAL, question.assistantFactory));
508:                 }
509:
510:                 defs.addAll(question.assistantFactory.createPDefinitionAssistant().checkDuplicatePatterns(node, argdefs));
511:                 FlatCheckedEnvironment local = new FlatCheckedEnvironment(question.assistantFactory, defs, question.env, question.scope);
512:                 local.setStatic(question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()));
513:                 local.setEnclosingDefinition(node);
514:                 local.setFunctional(true);
515:
516:                 question.assistantFactory.createPDefinitionListAssistant().typeCheck(defs, THIS, new TypeCheckInfo(question.assistantFactory, local, question.scope, question.qualifiers));
517:
518:                 List<QualifiedDefinition> qualified = new Vector<QualifiedDefinition>();
519:
520:                 if (node.getPredef() != null)
521:                 {
522:                         FlatEnvironment pre = new FlatEnvironment(question.assistantFactory, new Vector<PDefinition>(), local);
523:                         pre.setFunctional(true);
524:                         pre.setEnclosingDefinition(node.getPredef());
525:
526:                         PType b = node.getPredef().getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, pre, question.scope));
527:                         ABooleanBasicType expected = AstFactory.newABooleanBasicType(node.getLocation());
528:
529:                         if (!question.assistantFactory.createPTypeAssistant().isType(b, ABooleanBasicType.class))
530:                         {
531:                                 TypeCheckerErrors.report(3018, "Precondition returns unexpected type", node.getLocation(), node);
532:                                 TypeCheckerErrors.detail2("Actual", b, "Expected", expected);
533:                         }
534:
535:                         qualified = node.getPredef().getBody().apply(question.assistantFactory.getQualificationVisitor(), new TypeCheckInfo(question.assistantFactory, local, question.scope));
536:
537:                         for (QualifiedDefinition qdef : qualified)
538:                         {
539:                                 qdef.qualifyType();
540:                         }
541:                 }
542:
543:                 if (node.getBody() != null)
544:                 {
545:                         if (node.getClassDefinition() != null
546:                                         && !question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()))
547:                         {
548:                                 local.add(question.assistantFactory.createPDefinitionAssistant().getSelfDefinition(node));
549:                         }
550:
551:                         node.setActualResult(node.getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, local, question.scope, question.qualifiers, node.getResult().getType(), null, question.fromModule, question.mandatory)));
552:
553:                         if (!question.assistantFactory.getTypeComparator().compatible(node.getResult().getType(), node.getActualResult()))
554:                         {
555:                                 TypeCheckerErrors.report(3029, "Function returns unexpected type", node.getLocation(), node);
556:                                 TypeCheckerErrors.detail2("Actual", node.getActualResult(), "Expected", node.getResult().getType());
557:                         }
558:                 }
559:
560:                 for (QualifiedDefinition qdef : qualified)
561:                 {
562:                         qdef.resetType();
563:                 }
564:
565:                 if (question.assistantFactory.createPTypeAssistant().narrowerThan(question.assistantFactory.createPDefinitionAssistant().getType(node), node.getAccess()))
566:                 {
567:                         TypeCheckerErrors.report(3030, "Function parameter visibility less than function definition", node.getLocation(), node);
568:                 }
569:
570:                 if (question.env.isVDMPP())
571:                 {
572:                         PAccessSpecifierAssistantTC assist = question.assistantFactory.createPAccessSpecifierAssistant();
573:
574:                         if (assist.isPrivate(node.getAccess())
575:                                         && node.getBody() instanceof ASubclassResponsibilityExp)
576:                         {
577:                                 TypeCheckerErrors.report(3329, "Abstract function/operation must be public or protected", node.getLocation(), node);
578:                         }
579:                 }
580:
581:                 // The result variables are in scope for the post condition
582:
583:                 if (node.getPostdef() != null)
584:                 {
585:                         PType b = null;
586:
587:                         if (node.getResult() != null)
588:                         {
589:                                 List<PDefinition> postdefs = question.assistantFactory.createAPatternTypePairAssistant(question.fromModule).getDefinitions(node.getResult());
590:                                 FlatCheckedEnvironment post = new FlatCheckedEnvironment(question.assistantFactory, postdefs, local, NameScope.NAMES);
591:                                 post.setStatic(question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()));
592:                                 post.setEnclosingDefinition(node.getPostdef());
593:                                 post.setFunctional(true);
594:                                 b = node.getPostdef().getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, post, NameScope.NAMES));
595:                                 post.unusedCheck();
596:                         } else
597:                         {
598:                                 b = node.getPostdef().getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, local, NameScope.NAMES));
599:                         }
600:
601:                         ABooleanBasicType expected = AstFactory.newABooleanBasicType(node.getLocation());
602:
603:                         if (!question.assistantFactory.createPTypeAssistant().isType(b, ABooleanBasicType.class))
604:                         {
605:                                 TypeCheckerErrors.report(3018, "Postcondition returns unexpected type", node.getLocation(), node);
606:                                 TypeCheckerErrors.detail2("Actual", b, "Expected", expected);
607:                         }
608:                 }
609:
610:                 if (node.getMeasure() != null && node.getBody() == null)
611:                 {
612:                         TypeCheckerErrors.report(3273, "Measure not allowed for an implicit function", node.getMeasure().getLocation(), node);
613:                 }
614:                 else if (node.getMeasure() instanceof AVariableExp)
615:                 {
616:                         AVariableExp exp = (AVariableExp)node.getMeasure();
617:                         List<PType> params = node.getType().getParameters();
618:                         if (question.env.isVDMPP()) exp.getName().setTypeQualifier(params);
619:                         PDefinition def = question.env.findName(exp.getName(), question.scope);
620:                         
621:                         if (def instanceof AExplicitFunctionDefinition)
622:                         {
623:                                 setMeasureDef(question, node, exp.getName(), question.env, question.scope);
624:                         }
625:                         else
626:                         {
627:                                 setMeasureExp(question, node, question.env, local, question.scope);
628:                         }
629:                 }
630:                 else if (node.getMeasure() instanceof ANotYetSpecifiedExp)
631:                 {
632:                         // Undefined measure, so ignore (without warning).
633:                         node.setMeasureDef(null);
634:                         node.setMeasureName(null);
635:                 }
636:                 else if (node.getMeasure() != null)
637:                 {
638:                         setMeasureExp(question, node, question.env, local, question.scope);
639:                 }
640:
641:                 if (!(node.getBody() instanceof ANotYetSpecifiedExp)
642:                                 && !(node.getBody() instanceof ASubclassResponsibilityExp))
643:                 {
644:                         local.unusedCheck();
645:                 }
646:
647:                 node.setType(node.getType());
648:                 afterAnnotations(node.getAnnotations(), node, question);
649:                 return node.getType();
650:         }
651:
652:         @Override
653:         public PType caseAExplicitOperationDefinition(
654:                         AExplicitOperationDefinition node, TypeCheckInfo question)
655:                         throws AnalysisException
656:         {
657:                 checkAnnotations(node, question);
658:                 beforeAnnotations(node.getAnnotations(), node, question);
659:
660:                 question.assistantFactory.getTypeComparator().checkComposeTypes(node.getType(), question.env, false);
661:                 List<PType> ptypes = ((AOperationType) node.getType()).getParameters();
662:
663:                 if (node.getParameterPatterns().size() > ptypes.size())
664:                 {
665:                         TypeCheckerErrors.report(3023, "Too many parameter patterns", node.getLocation(), node);
666:                         TypeCheckerErrors.detail2("Type params", ptypes.size(), "Patterns", node.getParameterPatterns().size());
667:                         return null;
668:                 } else if (node.getParameterPatterns().size() < ptypes.size())
669:                 {
670:                         TypeCheckerErrors.report(3024, "Too few parameter patterns", node.getLocation(), node);
671:                         TypeCheckerErrors.detail2("Type params", ptypes.size(), "Patterns", node.getParameterPatterns().size());
672:                         return null;
673:                 }
674:
675:                 node.setParamDefinitions(question.assistantFactory.createAExplicitOperationDefinitionAssistant(question.fromModule).getParamDefinitions(node));
676:                 question.assistantFactory.createPDefinitionListAssistant().typeCheck(node.getParamDefinitions(), THIS, new TypeCheckInfo(question.assistantFactory, question.env, NameScope.NAMESANDSTATE, question.qualifiers));
677:
678:                 FlatCheckedEnvironment local = new FlatCheckedEnvironment(question.assistantFactory, node.getParamDefinitions(), question.env, NameScope.NAMESANDSTATE);
679:                 local.setStatic(question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()));
680:                 local.setEnclosingDefinition(node);
681:                 local.setFunctional(false);
682:
683:                 if (question.env.isVDMPP())
684:                 {
685:                         if (!question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()))
686:                         {
687:                                 local.add(question.assistantFactory.createPDefinitionAssistant().getSelfDefinition(node));
688:                         }
689:
690:                         if (node.getIsConstructor())
691:                         {
692:                                 if (question.assistantFactory.createPAccessSpecifierAssistant().isAsync(node.getAccess()) ||
693:                                         question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()) ||
694:                                         node.getAccess().getPure())
695:                                 {
696:                                         TypeCheckerErrors.report(3286, "Constructor cannot be 'async', 'static' or 'pure'", node.getLocation(), node);
697:                                 }
698:
699:                                 if (question.assistantFactory.createPTypeAssistant().isClass(((AOperationType) node.getType()).getResult(), question.env, question.fromModule))
700:                                 {
701:                                         AClassType ctype = question.assistantFactory.createPTypeAssistant().getClassType(((AOperationType) node.getType()).getResult(), question.env, question.fromModule);
702:
703:                                         if (ctype.getClassdef() != node.getClassDefinition())
704:                                         {
705:                                                 // FIXME: This is a TEST, it should be tried to see if
706:                                                 // it is valid
707:                                                 TypeCheckerErrors.report(3025, "Constructor operation must have return type "
708:                                                                 + node.getClassDefinition().getName().getName(), node.getLocation(), node);
709:                                         }
710:                                         // TODO: THIS COULD BE A HACK to code (ctype.getClassdef()
711:                                         // != node.getClassDefinition())
712:                                         if (!question.assistantFactory.getLexNameTokenAssistant().isEqual(ctype.getClassdef().getName(), node.getClassDefinition().getName()))
713:                                         {
714:                                                 TypeCheckerErrors.report(3025, "Constructor operation must have return type "
715:                                                                 + node.getClassDefinition().getName().getName(), node.getLocation(), node);
716:                                         }
717:                                 } else
718:                                 {
719:                                         TypeCheckerErrors.report(3026, "Constructor operation must have return type "
720:                                                         + node.getClassDefinition().getName().getName(), node.getLocation(), node);
721:                                 }
722:                         }
723:                 }
724:
725:                 List<QualifiedDefinition> qualified = new Vector<QualifiedDefinition>();
726:
727:                 if (node.getPredef() != null)
728:                 {
729:                         FlatEnvironment pre = new FlatEnvironment(question.assistantFactory, new Vector<PDefinition>(), local);
730:                         pre.setEnclosingDefinition(node.getPredef());
731:                         pre.setFunctional(true);
732:
733:                         PType b = node.getPredef().getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, pre, NameScope.NAMESANDSTATE));
734:
735:                         ABooleanBasicType expected = AstFactory.newABooleanBasicType(node.getLocation());
736:
737:                         if (!question.assistantFactory.createPTypeAssistant().isType(b, ABooleanBasicType.class))
738:                         {
739:                                 TypeCheckerErrors.report(3018, "Precondition returns unexpected type", node.getLocation(), node);
740:                                 TypeCheckerErrors.detail2("Actual", b, "Expected", expected);
741:                         }
742:
743:                         qualified = node.getPredef().getBody().apply(question.assistantFactory.getQualificationVisitor(), new TypeCheckInfo(question.assistantFactory, pre, NameScope.NAMESANDSTATE));
744:
745:                         for (QualifiedDefinition qdef : qualified)
746:                         {
747:                                 qdef.qualifyType();
748:                         }
749:                 }
750:
751:                 if (node.getPostdef() != null)
752:                 {
753:                         LexNameToken result = new LexNameToken(node.getName().getModule(), "RESULT", node.getLocation());
754:                         PPattern rp = AstFactory.newAIdentifierPattern(result);
755:                         List<PDefinition> rdefs = question.assistantFactory.createPPatternAssistant(question.fromModule).getDefinitions(rp, ((AOperationType) node.getType()).getResult(), NameScope.NAMESANDANYSTATE);
756:                         FlatEnvironment post = new FlatEnvironment(question.assistantFactory, rdefs, local);
757:                         post.setEnclosingDefinition(node.getPostdef());
758:                         post.setFunctional(true);
759:                         PType b = node.getPostdef().getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, post, NameScope.NAMESANDANYSTATE));
760:                         ABooleanBasicType expected = AstFactory.newABooleanBasicType(node.getLocation());
761:
762:                         if (!question.assistantFactory.createPTypeAssistant().isType(b, ABooleanBasicType.class))
763:                         {
764:                                 TypeCheckerErrors.report(3018, "Postcondition returns unexpected type", node.getLocation(), node);
765:                                 TypeCheckerErrors.detail2("Actual", b, "Expected", expected);
766:                         }
767:                 }
768:
769:                 PType expectedResult = ((AOperationType) node.getType()).getResult();
770:                 PType actualResult = node.getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, local, NameScope.NAMESANDSTATE, null, null, expectedResult, question.fromModule, !node.getIsConstructor()));
771:                 node.setActualResult(actualResult);
772:                 boolean compatible = question.assistantFactory.getTypeComparator().compatible(expectedResult, node.getActualResult());
773:
774:                 for (QualifiedDefinition qdef : qualified)
775:                 {
776:                         qdef.resetType();
777:                 }
778:
779:                 if (node.getIsConstructor()
780:                                 && !question.assistantFactory.createPTypeAssistant().isType(node.getActualResult(), AVoidType.class)
781:                                 && !compatible || !node.getIsConstructor() && !compatible)
782:                 {
783:                         TypeCheckerErrors.report(3027, "Operation returns unexpected type", node.getLocation(), node);
784:                         TypeCheckerErrors.detail2("Actual", node.getActualResult(), "Expected", ((AOperationType) node.getType()).getResult());
785:                 } else if (!node.getIsConstructor()
786:                                 && !question.assistantFactory.createPTypeAssistant().isUnknown(actualResult))
787:                 {
788:                         if (question.assistantFactory.createPTypeAssistant().isVoid(((AOperationType) node.getType()).getResult())
789:                                         && !question.assistantFactory.createPTypeAssistant().isVoid(actualResult))
790:                         {
791:                                 TypeCheckerErrors.report(3312, "Void operation returns non-void value", node.getLocation(), node);
792:                                 TypeCheckerErrors.detail2("Actual", actualResult, "Expected", ((AOperationType) node.getType()).getResult());
793:                         } else if (!question.assistantFactory.createPTypeAssistant().isVoid(((AOperationType) node.getType()).getResult())
794:                                         && question.assistantFactory.createPTypeAssistant().hasVoid(actualResult))
795:                         {
796:                                 TypeCheckerErrors.report(3313, "Operation returns void value", node.getLocation(), node);
797:                                 TypeCheckerErrors.detail2("Actual", actualResult, "Expected", ((AOperationType) node.getType()).getResult());
798:                         }
799:                 }
800:
801:                 if (question.assistantFactory.createPAccessSpecifierAssistant().isAsync(node.getAccess())
802:                                 && !question.assistantFactory.createPTypeAssistant().isType(((AOperationType) node.getType()).getResult(), AVoidType.class))
803:                 {
804:                         TypeCheckerErrors.report(3293, "Asynchronous operation '"
805:                                         + node.getName() + "' cannot return a value", node.getLocation(), node);
806:                 }
807:
808:                 if (node.getAccess().getPure() &&
809:                         question.assistantFactory.createPTypeAssistant().isType(((AOperationType) node.getType()).getResult(), AVoidType.class) &&
810:                         !question.assistantFactory.createPTypeAssistant().isUnknown(((AOperationType) node.getType()).getResult()))
811:                 {
812:                         TypeCheckerErrors.report(3344, "Pure operation '" + node.getName() + "' must return a value", node.getLocation(), node);
813:                 }
814:
815:                 if (node.getAccess().getPure() && question.assistantFactory.createPAccessSpecifierAssistant().isAsync(node.getAccess()))
816:                 {
817:                         TypeCheckerErrors.report(3345, "Pure operation '" + node.getName() + "' cannot also be async", node.getLocation(), node);
818:                 }
819:
820:                 if (question.assistantFactory.createPTypeAssistant().narrowerThan(node.getType(), node.getAccess()))
821:                 {
822:                         TypeCheckerErrors.report(3028, "Operation parameter visibility less than operation definition", node.getLocation(), node);
823:                 }
824:
825:                 if (question.env.isVDMPP())
826:                 {
827:                         PAccessSpecifierAssistantTC assist = question.assistantFactory.createPAccessSpecifierAssistant();
828:
829:                         if (assist.isPrivate(node.getAccess())
830:                                         && node.getBody() instanceof ASubclassResponsibilityStm)
831:                         {
832:                                 TypeCheckerErrors.report(3329, "Abstract function/operation must be public or protected", node.getLocation(), node);
833:                         }
834:                 }
835:
836:                 if (!(node.getBody() instanceof ANotYetSpecifiedStm)
837:                                 && !(node.getBody() instanceof ASubclassResponsibilityStm))
838:                 {
839:                         local.unusedCheck();
840:                 }
841:
842:                 if (node.getPossibleExceptions() == null)
843:                 {
844:                         node.setPossibleExceptions(new PTypeSet(question.assistantFactory));
845:                         IQuestionAnswer<Environment, PTypeSet> collector = question.assistantFactory.getExitTypeCollector();
846:                         node.setPossibleExceptions(node.getBody().apply(collector, question.env));
847:                 }
848:
849:                 node.setType(node.getType());
850:                 afterAnnotations(node.getAnnotations(), node, question);
851:                 return node.getType();
852:         }
853:
854:         @Override
855:         public PType caseAImplicitOperationDefinition(
856:                         AImplicitOperationDefinition node, TypeCheckInfo question)
857:                         throws AnalysisException
858:         {
859:                 checkAnnotations(node, question);
860:                 beforeAnnotations(node.getAnnotations(), node, question);
861:
862:                 question.assistantFactory.getTypeComparator().checkComposeTypes(node.getType(), question.env, false);
863:                 question = new TypeCheckInfo(question.assistantFactory, question.env, NameScope.NAMESANDSTATE, question.qualifiers);
864:                 List<PDefinition> defs = new Vector<PDefinition>();
865:                 List<PDefinition> argdefs = new Vector<PDefinition>();
866:
867:                 if (question.env.isVDMPP())
868:                 {
869:                         node.setStateDefinition(question.env.findClassDefinition());
870:                 } else
871:                 {
872:                         node.setStateDefinition(question.env.findStateDefinition());
873:                 }
874:
875:                 for (APatternListTypePair ptp : node.getParameterPatterns())
876:                 {
877:                         argdefs.addAll(getDefinitions(ptp, NameScope.LOCAL, question.assistantFactory));
878:                 }
879:
880:                 defs.addAll(question.assistantFactory.createPDefinitionAssistant().checkDuplicatePatterns(node, argdefs));
881:
882:                 if (node.getResult() != null)
883:                 {
884:                         defs.addAll(question.assistantFactory.createPPatternAssistant(question.fromModule).getDefinitions(node.getResult().getPattern(), ((AOperationType) node.getType()).getResult(), NameScope.STATE));
885:                 }
886:
887:                 // Now we build local definitions for each of the externals, so
888:                 // that they can be added to the local environment, while the
889:                 // global state is made inaccessible - but only if we have
890:                 // an "ext" clause
891:
892:                 boolean limitStateScope = false;
893:
894:                 if (node.getExternals().size() != 0)
895:                 {
896:                         for (AExternalClause clause : node.getExternals())
897:                         {
898:                                 question.assistantFactory.getTypeComparator().checkComposeTypes(clause.getType(), question.env, false);
899:
900:                                 for (ILexNameToken exname : clause.getIdentifiers())
901:                                 {
902:                                         PDefinition sdef = question.env.findName(exname, NameScope.STATE);
903:                                         typeResolve(clause, THIS, question);
904:
905:                                         if (sdef == null)
906:                                         {
907:                                                 TypeCheckerErrors.report(3031, "Unknown state variable "
908:                                                                 + exname, exname.getLocation(), exname);
909:                                         } else
910:                                         {
911:                                                 if (!(clause.getType() instanceof AUnknownType)
912:                                                                 && !question.assistantFactory.createPTypeAssistant().equals(sdef.getType(), clause.getType()))
913:                                                 {
914:                                                         TypeCheckerErrors.report(3032, "State variable "
915:                                                                         + exname + " is not this type", node.getLocation(), node);
916:                                                         TypeCheckerErrors.detail2("Declared", sdef.getType(), "ext type", clause.getType());
917:                                                 } else
918:                                                 {
919:                                                         defs.add(AstFactory.newAExternalDefinition(sdef, clause.getMode()));
920:                                                         argdefs.add(AstFactory.newAExternalDefinition(sdef, clause.getMode()));
921:
922:                                                         // VDM++ "ext wr" clauses in a constructor
923:                                                         // effectively
924:                                                         // initialize the instance variable concerned.
925:
926:                                                         if (clause.getMode().getType() == VDMToken.WRITE
927:                                                                         && sdef instanceof AInstanceVariableDefinition
928:                                                                         && node.getName().getName().equals(node.getClassDefinition().getName().getName()))
929:                                                         {
930:                                                                 AInstanceVariableDefinition iv = (AInstanceVariableDefinition) sdef;
931:                                                                 iv.setInitialized(true);
932:                                                         }
933:                                                 }
934:                                         }
935:                                 }
936:                         }
937:
938:                         // All relevant globals are now in defs (local), so we
939:                         // limit the state searching scope
940:
941:                         limitStateScope = true;
942:                 }
943:
944:                 question.assistantFactory.createPDefinitionListAssistant().typeCheck(defs, THIS, question);
945:
946:                 FlatCheckedEnvironment local = new FlatCheckedEnvironment(question.assistantFactory, defs, question.env, question.scope);
947:                 local.setLimitStateScope(limitStateScope);
948:                 local.setStatic(question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()));
949:                 local.setEnclosingDefinition(node);
950:                 local.setFunctional(false);
951:
952:                 if (question.env.isVDMPP())
953:                 {
954:                         if (node.getIsConstructor())
955:                         {
956:                                 if (question.assistantFactory.createPAccessSpecifierAssistant().isAsync(node.getAccess()) ||
957:                                         question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()) ||
958:                                         node.getAccess().getPure())
959:                                 {
960:                                         TypeCheckerErrors.report(3286, "Constructor cannot be 'async', 'static' or 'pure'", node.getLocation(), node);
961:                                 }
962:
963:                                 if (question.assistantFactory.createPTypeAssistant().isClass(((AOperationType) node.getType()).getResult(), question.env, question.fromModule))
964:                                 {
965:                                         AClassType ctype = question.assistantFactory.createPTypeAssistant().getClassType(((AOperationType) node.getType()).getResult(), question.env, question.fromModule);
966:
967:                                         if (ctype.getClassdef() != node.getClassDefinition())
968:                                         {
969:                                                 TypeCheckerErrors.report(3025, "Constructor operation must have return type "
970:                                                                 + node.getClassDefinition().getName().getName(), node.getLocation(), node);
971:                                         }
972:                                 } else
973:                                 {
974:                                         TypeCheckerErrors.report(3026, "Constructor operation must have return type "
975:                                                         + node.getClassDefinition().getName().getName(), node.getLocation(), node);
976:
977:                                 }
978:                         }
979:                 }
980:
981:                 List<QualifiedDefinition> qualified = new Vector<QualifiedDefinition>();
982:
983:                 if (node.getPredef() != null)
984:                 {
985:                         FlatEnvironment pre = new FlatEnvironment(question.assistantFactory, argdefs, question.env);
986:                         pre.setLimitStateScope(limitStateScope);
987:                         pre.setEnclosingDefinition(node.getPredef());
988:                         pre.setFunctional(true);
989:                         PType b = node.getPredef().getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, pre, NameScope.NAMESANDSTATE));
990:                         ABooleanBasicType expected = AstFactory.newABooleanBasicType(node.getLocation());
991:
992:                         if (!question.assistantFactory.createPTypeAssistant().isType(b, ABooleanBasicType.class))
993:                         {
994:                                 TypeCheckerErrors.report(3018, "Precondition returns unexpected type", node.getLocation(), node);
995:                                 TypeCheckerErrors.detail2("Actual", b, "Expected", expected);
996:                         }
997:
998:                         qualified = node.getPredef().getBody().apply(question.assistantFactory.getQualificationVisitor(), new TypeCheckInfo(question.assistantFactory, pre, NameScope.NAMESANDSTATE));
999:
1000:                         for (QualifiedDefinition qdef : qualified)
1001:                         {
1002:                                 qdef.qualifyType();
1003:                         }
1004:                 }
1005:
1006:                 if (node.getBody() != null)
1007:                 {
1008:                         if (node.getClassDefinition() != null
1009:                                         && !question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()))
1010:                         {
1011:                                 local.add(question.assistantFactory.createPDefinitionAssistant().getSelfDefinition(node));
1012:                         }
1013:
1014:                         PType expectedResult = ((AOperationType) node.getType()).getResult();
1015:                         node.setActualResult(node.getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, local, NameScope.NAMESANDSTATE, null, null, expectedResult, question.fromModule, !node.getIsConstructor())));
1016:
1017:                         boolean compatible = question.assistantFactory.getTypeComparator().compatible(expectedResult, node.getActualResult());
1018:
1019:                         if (node.getIsConstructor()
1020:                                         && !question.assistantFactory.createPTypeAssistant().isType(node.getActualResult(), AVoidType.class)
1021:                                         && !compatible || !node.getIsConstructor() && !compatible)
1022:                         {
1023:                                 TypeCheckerErrors.report(3035, "Operation returns unexpected type", node.getLocation(), node);
1024:                                 TypeCheckerErrors.detail2("Actual", node.getActualResult(), "Expected", ((AOperationType) node.getType()).getResult());
1025:                         } else if (!node.getIsConstructor()
1026:                                         && !question.assistantFactory.createPTypeAssistant().isUnknown(node.getActualResult()))
1027:                         {
1028:                                 if (question.assistantFactory.createPTypeAssistant().isVoid(((AOperationType) node.getType()).getResult())
1029:                                                 && !question.assistantFactory.createPTypeAssistant().isVoid(node.getActualResult()))
1030:                                 {
1031:                                         TypeCheckerErrors.report(3312, "Void operation returns non-void value", node.getLocation(), node);
1032:                                         TypeCheckerErrors.detail2("Actual", node.getActualResult(), "Expected", ((AOperationType) node.getType()).getResult());
1033:                                 } else if (!question.assistantFactory.createPTypeAssistant().isVoid(((AOperationType) node.getType()).getResult())
1034:                                                 && question.assistantFactory.createPTypeAssistant().hasVoid(node.getActualResult()))
1035:                                 {
1036:                                         TypeCheckerErrors.report(3313, "Operation returns void value", node.getLocation(), node);
1037:                                         TypeCheckerErrors.detail2("Actual", node.getActualResult(), "Expected", ((AOperationType) node.getType()).getResult());
1038:                                 }
1039:                         }
1040:                 }
1041:
1042:                 for (QualifiedDefinition qdef : qualified)
1043:                 {
1044:                         qdef.resetType();
1045:                 }
1046:
1047:                 if (question.assistantFactory.createPAccessSpecifierAssistant().isAsync(node.getAccess())
1048:                                 && !question.assistantFactory.createPTypeAssistant().isType(((AOperationType) node.getType()).getResult(), AVoidType.class))
1049:                 {
1050:                         TypeCheckerErrors.report(3293, "Asynchronous operation "
1051:                                         + node.getName() + " cannot return a value", node.getLocation(), node);
1052:                 }
1053:
1054:                 if (node.getAccess().getPure() &&
1055:                         question.assistantFactory.createPTypeAssistant().isType(((AOperationType) node.getType()).getResult(), AVoidType.class) &&
1056:                         !question.assistantFactory.createPTypeAssistant().isUnknown(((AOperationType) node.getType()).getResult()))
1057:                 {
1058:                         TypeCheckerErrors.report(3344, "Pure operation '" + node.getName() + "' must return a value", node.getLocation(), node);
1059:                 }
1060:
1061:                 if (node.getAccess().getPure() &&
1062:                         question.assistantFactory.createPAccessSpecifierAssistant().isAsync(node.getAccess()))
1063:                 {
1064:                         TypeCheckerErrors.report(3345, "Pure operation '" + node.getName() + "' cannot also be async", node.getLocation(), node);
1065:                 }
1066:
1067:                 if (question.assistantFactory.createPTypeAssistant().narrowerThan(node.getType(), node.getAccess()))
1068:                 {
1069:                         TypeCheckerErrors.report(3036, "Operation parameter visibility less than operation definition", node.getLocation(), node);
1070:                 }
1071:
1072:                 if (question.env.isVDMPP())
1073:                 {
1074:                         PAccessSpecifierAssistantTC assist = question.assistantFactory.createPAccessSpecifierAssistant();
1075:
1076:                         if (assist.isPrivate(node.getAccess())
1077:                                         && node.getBody() instanceof ASubclassResponsibilityStm)
1078:                         {
1079:                                 TypeCheckerErrors.report(3329, "Abstract function/operation must be public or protected", node.getLocation(), node);
1080:                         }
1081:                 }
1082:
1083:                 // The result variables are in scope for the post condition
1084:
1085:                 if (node.getPostdef() != null)
1086:                 {
1087:                         PType b = null;
1088:
1089:                         if (node.getResult() != null)
1090:                         {
1091:                                 List<PDefinition> postdefs = question.assistantFactory.createAPatternTypePairAssistant(question.fromModule).getDefinitions(node.getResult());
1092:                                 FlatCheckedEnvironment post = new FlatCheckedEnvironment(question.assistantFactory, postdefs, local, NameScope.NAMESANDANYSTATE);
1093:                                 post.setStatic(question.assistantFactory.createPAccessSpecifierAssistant().isStatic(node.getAccess()));
1094:                                 post.setEnclosingDefinition(node.getPostdef());
1095:                                 post.setFunctional(true);
1096:                                 b = node.getPostdef().getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, post, NameScope.NAMESANDANYSTATE));
1097:                                 post.unusedCheck();
1098:                         } else
1099:                         {
1100:                                 FlatEnvironment post = new FlatEnvironment(question.assistantFactory, new Vector<PDefinition>(), local);
1101:                                 post.setEnclosingDefinition(node.getPostdef());
1102:                                 post.setFunctional(true);
1103:                                 b = node.getPostdef().getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, post, NameScope.NAMESANDANYSTATE));
1104:                         }
1105:
1106:                         ABooleanBasicType expected = AstFactory.newABooleanBasicType(node.getLocation());
1107:
1108:                         if (!question.assistantFactory.createPTypeAssistant().isType(b, ABooleanBasicType.class))
1109:                         {
1110:                                 TypeCheckerErrors.report(3018, "Postcondition returns unexpected type", node.getLocation(), node);
1111:                                 TypeCheckerErrors.detail2("Actual", b, "Expected", expected);
1112:                         }
1113:                 }
1114:
1115:                 if (node.getErrors() != null)
1116:                 {
1117:                         for (AErrorCase error : node.getErrors())
1118:                         {
1119:                                 TypeCheckInfo newQuestion = new TypeCheckInfo(question.assistantFactory, local, NameScope.NAMESANDSTATE);
1120:                                 PType a = error.getLeft().apply(THIS, newQuestion);
1121:
1122:                                 if (!question.assistantFactory.createPTypeAssistant().isType(a, ABooleanBasicType.class))
1123:                                 {
1124:                                         TypeCheckerErrors.report(3307, "Errs clause is not bool -> bool", error.getLeft().getLocation(), error.getLeft());
1125:                                 }
1126:
1127:                                 newQuestion.scope = NameScope.NAMESANDANYSTATE;
1128:                                 PType b = error.getRight().apply(THIS, newQuestion);
1129:
1130:                                 if (!question.assistantFactory.createPTypeAssistant().isType(b, ABooleanBasicType.class))
1131:                                 {
1132:                                         TypeCheckerErrors.report(3307, "Errs clause is not bool -> bool", error.getRight().getLocation(), error.getRight());
1133:                                 }
1134:                         }
1135:                 }
1136:
1137:                 if (!(node.getBody() instanceof ANotYetSpecifiedStm)
1138:                                 && !(node.getBody() instanceof ASubclassResponsibilityStm))
1139:                 {
1140:                         local.unusedCheck();
1141:                 }
1142:
1143:                 if (node.getPossibleExceptions() == null && node.getBody() != null)
1144:                 {
1145:                         node.setPossibleExceptions(new PTypeSet(question.assistantFactory));
1146:                         IQuestionAnswer<Environment, PTypeSet> collector = question.assistantFactory.getExitTypeCollector();
1147:                         node.setPossibleExceptions(node.getBody().apply(collector, question.env));
1148:                 }
1149:
1150:                 // node.setType(node.getActualResult());
1151:                 afterAnnotations(node.getAnnotations(), node, question);
1152:                 return node.getType();
1153:         }
1154:
1155:         @Override
1156:         public PType caseAImportedDefinition(AImportedDefinition node,
1157:                         TypeCheckInfo question) throws AnalysisException
1158:         {
1159:                 node.setType(node.getDef().apply(THIS, question));
1160:
1161:                 return node.getType();
1162:         }
1163:
1164:         @Override
1165:         public PType caseAInheritedDefinition(AInheritedDefinition node,
1166:                         TypeCheckInfo question) throws AnalysisException
1167:         {
1168:                 node.setType(node.getSuperdef().apply(THIS, question));
1169:                 return node.getType();
1170:         }
1171:
1172:         @Override
1173:         public PType caseALocalDefinition(ALocalDefinition node,
1174:                         TypeCheckInfo question)
1175:         {
1176:                 if (node.getType() != null)
1177:                 {
1178:                         node.setType(question.assistantFactory.createPTypeAssistant().typeResolve(node.getType(), null, THIS, question));
1179:                 }
1180:
1181:                 return node.getType();
1182:         }
1183:
1184:         @Override
1185:         public PType caseAMultiBindListDefinition(AMultiBindListDefinition node,
1186:                         TypeCheckInfo question) throws AnalysisException
1187:         {
1188:                 if (node.getType() != null)
1189:                 {
1190:                         question.assistantFactory.getTypeComparator().checkComposeTypes(node.getType(), question.env, false);
1191:                 }
1192:
1193:                 List<PDefinition> defs = new Vector<PDefinition>();
1194:
1195:                 for (PMultipleBind mb : node.getBindings())
1196:                 {
1197:                         PType type = mb.apply(THIS, question);
1198:                         defs.addAll(question.assistantFactory.createPMultipleBindAssistant().getDefinitions(mb, type, question));
1199:                 }
1200:
1201:                 question.assistantFactory.createPDefinitionListAssistant().typeCheck(defs, THIS, question);
1202:                 node.setDefs(defs);
1203:                 return null;
1204:         }
1205:
1206:         @Override
1207:         public PType caseAMutexSyncDefinition(AMutexSyncDefinition node,
1208:                         TypeCheckInfo question) throws AnalysisException
1209:         {
1210:                 checkAnnotations(node, question);
1211:                 beforeAnnotations(node.getAnnotations(), node, question);
1212:                 SClassDefinition classdef = question.env.findClassDefinition();
1213:
1214:                 if (node.getOperations().isEmpty())
1215:                 {
1216:                         // Add all locally visibly callable operations for mutex(all)
1217:
1218:                         for (PDefinition def : node.getClassDefinition().apply(question.assistantFactory.getDefinitionCollector()))
1219:                         // SClassDefinitionAssistantTC.getLocalDefinitions(node.getClassDefinition()))
1220:                         {
1221:                                 if (question.assistantFactory.createPDefinitionAssistant().isCallableOperation(def)
1222:                                                 && !def.getName().getName().equals(classdef.getName().getName()))
1223:                                 {
1224:                                         node.getOperations().add(def.getName());
1225:                                 }
1226:                         }
1227:                 }
1228:
1229:                 for (ILexNameToken opname : node.getOperations())
1230:                 {
1231:                         int found = 0;
1232:
1233:                         List<PDefinition> definitions = question.assistantFactory.createPDefinitionAssistant().getDefinitions(classdef);
1234:
1235:                         for (PDefinition def : definitions)
1236:                         {
1237:                                 if (def.getName() != null && def.getName().matches(opname))
1238:                                 {
1239:                                         found++;
1240:
1241:                                         if (!question.assistantFactory.createPDefinitionAssistant().isCallableOperation(def))
1242:                                         {
1243:                                                 TypeCheckerErrors.report(3038, opname
1244:                                                                 + " is not an explicit operation", opname.getLocation(), opname);
1245:                                         }
1246:                                         
1247:                                         if (def.getAccess().getPure())
1248:                                         {
1249:                                                 TypeCheckerErrors.report(3343, "Cannot have a mutex with pure operations", opname.getLocation(), opname);
1250:                                         }
1251:                                 }
1252:                         }
1253:
1254:                         if (found == 0)
1255:                         {
1256:                                 TypeCheckerErrors.report(3039, opname + " is not in scope", opname.getLocation(), opname);
1257:                         } else if (found > 1)
1258:                         {
1259:                                 TypeCheckerErrors.warning(5002, "Mutex of overloaded operation", opname.getLocation(), opname);
1260:                         }
1261:
1262:                         if (opname.getName().equals(classdef.getName().getName()))
1263:                         {
1264:                                 TypeCheckerErrors.report(3040, "Cannot put mutex on a constructor", opname.getLocation(), opname);
1265:                         }
1266:
1267:                         for (ILexNameToken other : node.getOperations())
1268:                         {
1269:                                 if (opname != other
1270:                                                 && question.assistantFactory.getLexNameTokenAssistant().isEqual(opname, other))
1271:                                 {
1272:                                         TypeCheckerErrors.report(3041, "Duplicate mutex name", opname.getLocation(), opname);
1273:                                 }
1274:                         }
1275:
1276:                 }
1277:
1278:                 afterAnnotations(node.getAnnotations(), node, question);
1279:                 return null;
1280:         }
1281:
1282:         @Override
1283:         public PType caseANamedTraceDefinition(ANamedTraceDefinition node,
1284:                         TypeCheckInfo question) throws AnalysisException
1285:         {
1286:                 checkAnnotations(node, question);
1287:                 beforeAnnotations(node.getAnnotations(), node, question);
1288:
1289:                 if (question.env.isVDMPP())
1290:                 {
1291:                         question = new TypeCheckInfo(question.assistantFactory, new FlatEnvironment(question.assistantFactory, question.assistantFactory.createPDefinitionAssistant().getSelfDefinition(node), question.env), question.scope, question.qualifiers);
1292:                 }
1293:
1294:                 for (ATraceDefinitionTerm term : node.getTerms())
1295:                 {
1296:                         typeCheck(term.getList(), THIS, new TypeCheckInfo(question.assistantFactory, question.env, NameScope.NAMESANDSTATE));
1297:                 }
1298:
1299:                 // Mark node as used, as traces are not used anyway
1300:                 question.assistantFactory.createPDefinitionAssistant().markUsed(node);
1301:                 
1302:                 afterAnnotations(node.getAnnotations(), node, question);
1303:                 return null;
1304:         }
1305:
1306:         @Override
1307:         public PType caseAPerSyncDefinition(APerSyncDefinition node,
1308:                         TypeCheckInfo question) throws AnalysisException
1309:         {
1310:                 checkAnnotations(node, question);
1311:                 beforeAnnotations(node.getAnnotations(), node, question);
1312:                 Environment base = question.env;
1313:
1314:                 SClassDefinition classdef = base.findClassDefinition();
1315:                 int opfound = 0;
1316:                 int perfound = 0;
1317:                 Boolean isStatic = null;
1318:
1319:                 List<PDefinition> definitions = question.assistantFactory.createPDefinitionAssistant().getDefinitions(classdef);
1320:
1321:                 for (PDefinition def : definitions)
1322:                 {
1323:                         if (def.getName() != null
1324:                                         && def.getName().matches(node.getOpname()))
1325:                         {
1326:                                 opfound++;
1327:
1328:                                 if (!question.assistantFactory.createPDefinitionAssistant().isCallableOperation(def))
1329:                                 {
1330:                                         TypeCheckerErrors.report(3042, node.getOpname()
1331:                                                         + " is not an explicit operation", node.getOpname().getLocation(), node.getOpname());
1332:                                 }
1333:
1334:                                 if (isStatic != null
1335:                                                 && isStatic != question.assistantFactory.createPDefinitionAssistant().isStatic(def))
1336:                                 {
1337:                                         TypeCheckerErrors.report(3323, "Overloaded operation cannot mix static and non-static", node.getLocation(), node.getOpname());
1338:                                 }
1339:
1340:                                 if (def.getAccess().getPure())
1341:                                 {
1342:                                         TypeCheckerErrors.report(3340, "Pure operation cannot have permission predicate",
1343:                                                 node.getOpname().getLocation(), node.getOpname());
1344:                                 }
1345:
1346:                                 isStatic = question.assistantFactory.createPDefinitionAssistant().isStatic(def);
1347:                         }
1348:
1349:                         if (def instanceof APerSyncDefinition)
1350:                         {
1351:                                 APerSyncDefinition psd = (APerSyncDefinition) def;
1352:
1353:                                 if (psd.getOpname().equals(node.getOpname()))
1354:                                 {
1355:                                         perfound++;
1356:                                 }
1357:                         }
1358:                 }
1359:
1360:                 ILexNameToken opname = node.getOpname();
1361:
1362:                 if (opfound == 0)
1363:                 {
1364:                         TypeCheckerErrors.report(3043, opname + " is not in scope", opname.getLocation(), opname);
1365:                 } else if (opfound > 1)
1366:                 {
1367:                         TypeCheckerErrors.warning(5003, "Permission guard of overloaded operation", opname.getLocation(), opname);
1368:                 }
1369:
1370:                 if (perfound != 1)
1371:                 {
1372:                         TypeCheckerErrors.report(3044, "Duplicate permission guard found for "
1373:                                         + opname, opname.getLocation(), opname);
1374:                 }
1375:
1376:                 if (opname.getName().equals(classdef.getName().getName()))
1377:                 {
1378:                         TypeCheckerErrors.report(3045, "Cannot put guard on a constructor", opname.getLocation(), opname);
1379:                 }
1380:
1381:                 FlatCheckedEnvironment local = new FlatCheckedEnvironment(question.assistantFactory, node, base, NameScope.NAMESANDSTATE);
1382:                 local.setEnclosingDefinition(node); // Prevent op calls
1383:
1384:                 if (isStatic != null)
1385:                 {
1386:                         local.setStatic(isStatic);
1387:                 }
1388:
1389:                 PType rt = node.getGuard().apply(THIS, new TypeCheckInfo(question.assistantFactory, local, NameScope.NAMESANDSTATE));
1390:
1391:                 if (!question.assistantFactory.createPTypeAssistant().isType(rt, ABooleanBasicType.class))
1392:                 {
1393:                         TypeCheckerErrors.report(3046, "Guard is not a boolean expression", node.getGuard().getLocation(), node.getGuard());
1394:                 }
1395:
1396:                 node.setType(rt);
1397:                 afterAnnotations(node.getAnnotations(), node, question);
1398:                 return node.getType();
1399:         }
1400:
1401:         @Override
1402:         public PType caseARenamedDefinition(ARenamedDefinition node,
1403:                         TypeCheckInfo question) throws AnalysisException
1404:         {
1405:
1406:                 node.setType(node.getDef().apply(THIS, question));
1407:                 return node.getType();
1408:         }
1409:
1410:         @Override
1411:         public PType caseAStateDefinition(AStateDefinition node,
1412:                         TypeCheckInfo question) throws AnalysisException
1413:         {
1414:                 checkAnnotations(node, question);
1415:                 beforeAnnotations(node.getAnnotations(), node, question);
1416:
1417:                 if (node.getPass() == Pass.TYPES)
1418:                 {
1419:                         Environment base = question.env;
1420:
1421:                         if (base.findStateDefinition() != node)
1422:                         {
1423:                                 TypeCheckerErrors.report(3047, "Only one state definition allowed per module", node.getLocation(), node);
1424:                                 return null;
1425:                         }
1426:
1427:                         for (PDefinition def : node.getStateDefs())
1428:                         {
1429:                                 if (!def.getName().getOld()) // Don't check old names
1430:                                 {
1431:                                         question.assistantFactory.getTypeComparator().checkComposeTypes(def.getType(), question.env, false);
1432:                                 }
1433:                         }
1434:
1435:                         question.assistantFactory.createPDefinitionListAssistant().typeCheck(node.getStateDefs(), THIS, question);
1436:                         node.setPass(Pass.DEFS);
1437:                 }
1438:                 else
1439:                 {
1440:                         if (node.getInvdef() != null)
1441:                         {
1442:                                 node.getInvdef().apply(THIS, question);
1443:                                 question.assistantFactory.createPPatternAssistant(question.fromModule).typeResolve(node.getInvPattern(), THIS, question);
1444:                         }
1445:
1446:                         if (node.getInitdef() != null)
1447:                         {
1448:                                 node.getInitdef().apply(THIS, question);
1449:                                 question.assistantFactory.createPPatternAssistant(question.fromModule).typeResolve(node.getInitPattern(), THIS, question);
1450:                         }
1451:                 }
1452:
1453:                 afterAnnotations(node.getAnnotations(), node, question);
1454:                 return null;
1455:         }
1456:
1457:         @Override
1458:         public PType caseAThreadDefinition(AThreadDefinition node,
1459:                         TypeCheckInfo question) throws AnalysisException
1460:         {
1461:
1462:                 question.scope = NameScope.NAMESANDSTATE;
1463:                 FlatEnvironment local = new FlatEnvironment(question.assistantFactory, question.assistantFactory.createPDefinitionAssistant().getSelfDefinition(node), question.env);
1464:
1465:                 PType rt = node.getStatement().apply(THIS, new TypeCheckInfo(question.assistantFactory, local, question.scope).newMandatory(false));
1466:
1467:                 if (!(rt instanceof AVoidType) && !(rt instanceof AUnknownType))
1468:                 {
1469:                         TypeCheckerErrors.report(3049, "Thread statement/operation must not return a value", node.getLocation(), node);
1470:                 }
1471:
1472:                 node.setType(rt);
1473:                 node.getOperationDef().setBody(node.getStatement().clone());// This
1474:                                                                                                                                         // operation
1475:                                                                                                                                         // is a
1476:                                                                                                                                         // wrapper
1477:                                                                                                                                         // for the
1478:                                                                                                                                         // thread
1479:                 return rt;
1480:         }
1481:
1482:         @Override
1483:         public PType caseATypeDefinition(ATypeDefinition node,
1484:                         TypeCheckInfo question) throws AnalysisException
1485:         {
1486:                 checkAnnotations(node, question);
1487:                 beforeAnnotations(node.getAnnotations(), node, question);
1488:
1489:                 if (node.getPass() == Pass.DEFS)
1490:                 {
1491:                         if (node.getInvdef() != null)
1492:                         {
1493:                                 question.scope = NameScope.NAMES;
1494:                                 node.getInvdef().apply(THIS, question);
1495:                         }
1496:         
1497:                         if (node.getEqRelation() != null)
1498:                         {
1499:                                 question.scope = NameScope.NAMES;
1500:                                 node.getEqRelation().apply(THIS,question);
1501:                         }
1502:         
1503:                         if (node.getOrdRelation() != null)
1504:                         {
1505:                                 question.scope = NameScope.NAMES;
1506:                                 node.getOrdRelation().apply(THIS,question);
1507:                         }
1508:                 }
1509:                 else
1510:                 {
1511:                         node.setPass(Pass.DEFS);                // Come back later to do inv definitions above.
1512:                         
1513:                         PType type = question.assistantFactory.createPDefinitionAssistant().getType(node);
1514:                         node.setType(type);
1515:         
1516:                         // We have to do the "top level" here, rather than delegating to the types
1517:                         // because the definition pointer from these top level types just refers
1518:                         // to the definition we are checking, which is never "narrower" than itself.
1519:                         // See the narrowerThan method in NamedType and RecordType.
1520:         
1521:                         if (type instanceof ANamedInvariantType)
1522:                         {
1523:                                 ANamedInvariantType ntype = (ANamedInvariantType) type;
1524:         
1525:                                 // Rebuild the compose definitions, after we check whether they already exist
1526:                                 node.getComposeDefinitions().clear();
1527:         
1528:                                 for (PType compose : question.assistantFactory.getTypeComparator().checkComposeTypes(ntype.getType(), question.env, true))
1529:                                 {
1530:                                         ARecordInvariantType rtype = (ARecordInvariantType) compose;
1531:                                         PDefinition cdef = AstFactory.newATypeDefinition(rtype.getName(), rtype, null, null);
1532:                                         cdef.setAccess(node.getAccess().clone());
1533:                                         node.getComposeDefinitions().add(cdef);
1534:                                         rtype.getDefinitions().get(0).setAccess(node.getAccess().clone());
1535:                                 }
1536:         
1537:                                 if (question.assistantFactory.createPTypeAssistant().narrowerThan(ntype.getType(), node.getAccess()))
1538:                                 {
1539:                                         TypeCheckerErrors.report(3321, "Type component visibility less than type's definition", node.getLocation(), node);
1540:                                 }
1541:                         } else if (type instanceof ARecordInvariantType)
1542:                         {
1543:                                 ARecordInvariantType rtype = (ARecordInvariantType) type;
1544:         
1545:                                 for (AFieldField field : rtype.getFields())
1546:                                 {
1547:                                         question.assistantFactory.getTypeComparator().checkComposeTypes(field.getType(), question.env, false);
1548:         
1549:                                         if (question.assistantFactory.createPTypeAssistant().narrowerThan(field.getType(), node.getAccess()))
1550:                                         {
1551:                                                 TypeCheckerErrors.report(3321, "Field type visibility less than type's definition", field.getTagname().getLocation(), field.getTagname());
1552:                                         }
1553:                                 }
1554:                         }
1555:                 }
1556:
1557:                 afterAnnotations(node.getAnnotations(), node, question);
1558:                 return node.getType();
1559:
1560:         }
1561:
1562:         @Override
1563:         public PType caseAUntypedDefinition(AUntypedDefinition node,
1564:                         TypeCheckInfo question)
1565:         {
1566:
1567:                 assert false : "Can't type check untyped definition?";
1568:                 return null;
1569:         }
1570:
1571:         @Override
1572:         public PType caseAValueDefinition(AValueDefinition node,
1573:                         TypeCheckInfo question) throws AnalysisException
1574:         {
1575:                 checkAnnotations(node, question);
1576:                 beforeAnnotations(node.getAnnotations(), node, question);
1577:
1578:                 if (node.getType() != null)
1579:                 {
1580:                         question.assistantFactory.getTypeComparator().checkComposeTypes(node.getType(), question.env, false);
1581:                 }
1582:
1583:                 // Enable constraint checking
1584:                 question = question.newConstraint(node.getType());
1585:
1586:                 question.qualifiers = null;
1587:                 ExcludedDefinitions.setExcluded(node.getDefs());
1588:                 PType expType = node.getExpression().apply(THIS, question);
1589:                 ExcludedDefinitions.clearExcluded();
1590:                 node.setExpType(expType);
1591:                 PType type = node.getType(); // PDefinitionAssistant.getType(node);
1592:                 
1593:                 if (expType instanceof AUnknownType)
1594:                 {
1595:                         node.setPass(Pass.FINAL);        // Do it again later
1596:                 }
1597:                 
1598:                 if (expType instanceof AVoidType)
1599:                 {
1600:                         TypeCheckerErrors.report(3048, "Expression does not return a value", node.getExpression().getLocation(), node.getExpression());
1601:                 } else if (type != null && !(type instanceof AUnknownType))
1602:                 {
1603:                         if (!question.assistantFactory.getTypeComparator().compatible(type, expType))
1604:                         {
1605:                                 TypeCheckerErrors.report(3051, "Expression does not match declared type", node.getLocation(), node);
1606:                                 TypeCheckerErrors.detail2("Declared", type, "Expression", expType);
1607:                         }
1608:                 } else
1609:                 {
1610:                         type = expType;
1611:                         node.setType(expType);
1612:                 }
1613:
1614:                 Environment base = question.env;
1615:
1616:                 if (base.isVDMPP() && type instanceof ANamedInvariantType)
1617:                 {
1618:                         ANamedInvariantType named = (ANamedInvariantType) type;
1619:                         PDefinition typedef = base.findType(named.getName(), node.getLocation().getModule());
1620:
1621:                         if (typedef == null)
1622:                         {
1623:                                 TypeCheckerErrors.report(2048, "Cannot find symbol "
1624:                                                 + named.getName().toString(), named.getLocation(), named);
1625:                                 return node.getType();
1626:                         }
1627:
1628:                         if (question.assistantFactory.createPAccessSpecifierAssistant().narrowerThan(typedef.getAccess(), node.getAccess()))
1629:                         {
1630:                                 TypeCheckerErrors.report(3052, "Value type visibility less than value definition", node.getLocation(), node);
1631:                         }
1632:                 }
1633:
1634:                 node.apply(question.assistantFactory.getDefinitionTypeResolver(), new DefinitionTypeResolver.NewQuestion(THIS, question));
1635:                 // PPatternAssistantTC.typeResolve(pattern, THIS, question);
1636:                 // question.assistantFactory.getTypeResolver().updateDefs(node, question);
1637:                 question.qualifiers = null;
1638:                 question.assistantFactory.createPDefinitionListAssistant().typeCheck(node.getDefs(), THIS, question);
1639:
1640:                 afterAnnotations(node.getAnnotations(), node, question);
1641:                 return node.getType();
1642:         }
1643:
1644:         @Override
1645:         public PType caseALetDefBindingTraceDefinition(
1646:                         ALetDefBindingTraceDefinition node, TypeCheckInfo question)
1647:                         throws AnalysisException
1648:         {
1649:                 return typeCheckLet(node, node.getLocalDefs(), node.getBody(), question);
1650:         }
1651:
1652:         @Override
1653:         public PType caseALetBeStBindingTraceDefinition(
1654:                         ALetBeStBindingTraceDefinition node, TypeCheckInfo question)
1655:                         throws AnalysisException
1656:         {
1657:                 Entry<PType, AMultiBindListDefinition> res = typecheckLetBeSt(node, node.getLocation(), node.getBind(), node.getStexp(), node.getBody(), question);
1658:                 node.setDef(res.getValue());
1659:                 return res.getKey();
1660:         }
1661:
1662:         @Override
1663:         public PType caseARepeatTraceDefinition(ARepeatTraceDefinition node,
1664:                         TypeCheckInfo question) throws AnalysisException
1665:         {
1666:                 if (node.getFrom() > node.getTo())
1667:                 {
1668:                         TypeCheckerErrors.report(3277, "Trace repeat illegal values", node.getLocation(), node);
1669:                 }
1670:
1671:                 // Environment local = question.env;
1672:                 return node.getCore().apply(THIS, question);
1673:
1674:         }
1675:
1676:         @Override
1677:         public PType caseAConcurrentExpressionTraceCoreDefinition(
1678:                         AConcurrentExpressionTraceCoreDefinition node,
1679:                         TypeCheckInfo question) throws AnalysisException
1680:         {
1681:                 for (PTraceDefinition d : node.getDefs())
1682:                 {
1683:                         d.apply(THIS, question);
1684:                 }
1685:
1686:                 return null;
1687:         }
1688:
1689:         @Override
1690:         public PType caseABracketedExpressionTraceCoreDefinition(
1691:                         ABracketedExpressionTraceCoreDefinition node, TypeCheckInfo question)
1692:                         throws AnalysisException
1693:         {
1694:                 for (ATraceDefinitionTerm term : node.getTerms())
1695:                 {
1696:                         for (PTraceDefinition def : term.getList())
1697:                         {
1698:                                 def.apply(THIS, question);
1699:                         }
1700:                 }
1701:
1702:                 return null;
1703:         }
1704:
1705:         @Override
1706:         public PType caseAApplyExpressionTraceCoreDefinition(
1707:                         AApplyExpressionTraceCoreDefinition node, TypeCheckInfo question)
1708:                         throws AnalysisException
1709:         {
1710:                 return node.getCallStatement().apply(THIS, question);
1711:
1712:         }
1713:
1714:         @Override
1715:         public PType caseAEqRelation(AEqRelation node, TypeCheckInfo question) throws AnalysisException {
1716:                 return node.getRelDef().apply(THIS,question);
1717:         }
1718:
1719:         @Override
1720:         public PType caseAOrdRelation(AOrdRelation node, TypeCheckInfo question) throws AnalysisException {
1721:                 // Do not report TC errors for Min or Max. Just confusing.
1722:                 TypeChecker.suppressErrors(true);
1723:                 node.getMinDef().apply(THIS,question);
1724:                 node.getMaxDef().apply(THIS,question);
1725:                 TypeChecker.suppressErrors(false);
1726:                 return node.getRelDef().apply(THIS, question);
1727:         }
1728:
1729:         public void typeCheck(List<PTraceDefinition> term,
1730:                                                  IQuestionAnswer<TypeCheckInfo, PType> rootVisitor,
1731:                                                  TypeCheckInfo question) throws AnalysisException
1732:         {
1733:
1734:•                for (PTraceDefinition def : term)
1735:                 {
1736:                         def.apply(rootVisitor, question);
1737:                 }
1738:
1739:         }
1740:         
1741:         public Collection<? extends PDefinition> getDefinitions(
1742:                         APatternListTypePair pltp, NameScope scope, ITypeCheckerAssistantFactory assistantFactory)
1743:         {
1744:                 List<PDefinition> list = new Vector<PDefinition>();
1745:
1746:                 for (PPattern p : pltp.getPatterns())
1747:                 {
1748:                         list.addAll(assistantFactory.createPPatternAssistant(null).getDefinitions(p, pltp.getType(), scope));
1749:                 }
1750:
1751:                 return list;
1752:         }
1753:         
1754:         public void typeResolve(AExternalClause clause,
1755:                         IQuestionAnswer<TypeCheckInfo, PType> rootVisitor,
1756:                         TypeCheckInfo question)
1757:         {
1758:                 clause.setType(question.assistantFactory.createPTypeAssistant().typeResolve(clause.getType(), null, rootVisitor, question));
1759:
1760:         }
1761:
1762:         /**
1763:          * Set measureDef to a newly created function, based on the measure expression.
1764:          * @throws AnalysisException
1765:          */
1766:         private void setMeasureExp(TypeCheckInfo question, SFunctionDefinitionBase node, Environment base, Environment local, NameScope scope) throws AnalysisException
1767:         {
1768:                 PType actual = node.getMeasure().apply(THIS, question.newInfo(local));
1769:                 node.setMeasureName(node.getName().getMeasureName(node.getName().getLocation()));
1770:                 checkMeasure(question, node, node.getMeasureName(), actual);
1771:                 
1772:                 List<List<PPattern>> cpll = new Vector<List<PPattern>>();
1773:                 boolean isCurried;
1774:                 
1775:                 if (node instanceof AExplicitFunctionDefinition)
1776:                 {
1777:                         // Concatenate the parameter patterns into one list for curried measures
1778:                         List<PPattern> all = new Vector<PPattern>();
1779:                         AExplicitFunctionDefinition ex = (AExplicitFunctionDefinition) node;
1780:                         
1781:                         for (List<PPattern> pl: ex.getParamPatternList())
1782:                         {
1783:                                 for (PPattern p: pl)
1784:                                 {
1785:                                         all.add(p.clone());
1786:                                 }
1787:                         }
1788:                         
1789:                         cpll.add(all);
1790:                         isCurried = ex.getIsCurried();
1791:                 }
1792:                 else
1793:                 {
1794:                         List<PPattern> all = new Vector<PPattern>();
1795:                         AImplicitFunctionDefinition imp = (AImplicitFunctionDefinition) node;
1796:                         
1797:                         for (APatternListTypePair ptp: imp.getParamPatterns())
1798:                         {
1799:                                 for (PPattern p: ptp.getPatterns())
1800:                                 {
1801:                                         all.add(p.clone());
1802:                                 }
1803:                         }
1804:
1805:                         cpll.add(all);
1806:                         isCurried = false;
1807:                 }
1808:                 
1809:                 AFunctionType mtype = question.assistantFactory.createAFunctionTypeAssistant().getMeasureType((AFunctionType) node.getType(), isCurried, actual, question.fromModule);
1810:                 
1811:                 AExplicitFunctionDefinition def = AstFactory.newAExplicitFunctionDefinition(node.getMeasureName(), scope,
1812:                                 (List<ILexNameToken>) node.getTypeParams().clone(), mtype, cpll, node.getMeasure(), null, null, false, null);
1813:
1814:                 def.setClassDefinition(node.getClassDefinition() == null ? null : node.getClassDefinition().clone());
1815:                 def.setAccess(node.getAccess().clone());
1816:                 question.assistantFactory.createPDefinitionAssistant().typeResolve(def, THIS, question);
1817:
1818:                 node.setMeasureDef(def);
1819:                 def.apply(THIS, question);
1820:         }
1821:
1822:         /**
1823:          * Check that measure is an existing named explicit function definition.
1824:          */
1825:         private void setMeasureDef(TypeCheckInfo question, SFunctionDefinitionBase node, ILexNameToken mname, Environment base, NameScope scope)
1826:         {
1827:                 if (question.env.isVDMPP())
1828:                 {
1829:                         if (node instanceof AExplicitFunctionDefinition)
1830:                         {
1831:                                 AExplicitFunctionDefinition ex = (AExplicitFunctionDefinition)node;
1832:                                 mname.setTypeQualifier(question.assistantFactory.createAExplicitFunctionDefinitionAssistant().getMeasureParams(ex));
1833:                         }
1834:                         else
1835:                         {
1836:                                 AImplicitFunctionDefinition imp = (AImplicitFunctionDefinition) node;
1837:                                 mname.setTypeQualifier(imp.getType().getParameters());
1838:                         }
1839:                 }
1840:                 
1841:                 PDefinition mdef = question.env.findName(mname, question.scope);
1842:
1843:                 if (mdef == null)
1844:                 {
1845:                         TypeCheckerErrors.report(3270, "Measure " + node.getMeasure()
1846:                                         + " is not in scope", node.getMeasure().getLocation(), node.getMeasure());
1847:                 }
1848:                 else if (!(mdef instanceof AExplicitFunctionDefinition))
1849:                 {
1850:                         TypeCheckerErrors.report(3271, "Measure " + node.getMeasure()
1851:                                         + " is not an explicit function", node.getMeasure().getLocation(), node.getMeasure());
1852:                 }
1853:                 else if (mdef == node)
1854:                 {
1855:                         TypeCheckerErrors.report(3304, "Recursive function cannot be its own measure", node.getMeasure().getLocation(), node.getMeasure());
1856:                 }
1857:                 else
1858:                 {
1859:                         AExplicitFunctionDefinition efd = (AExplicitFunctionDefinition) mdef;
1860:                         node.setMeasureDef(efd);
1861:                         node.setMeasureName(efd.getName());
1862:
1863:                         if (node.getTypeParams() == null && efd.getTypeParams() != null)
1864:                         {
1865:                                 TypeCheckerErrors.report(3309, "Measure must not be polymorphic", node.getMeasure().getLocation(), node.getMeasure());
1866:                         }
1867:                         else if (node.getTypeParams() != null && efd.getTypeParams() == null)
1868:                         {
1869:                                 TypeCheckerErrors.report(3310, "Measure must also be polymorphic", node.getMeasure().getLocation(), node.getMeasure());
1870:                         }
1871:                         else if (node.getTypeParams() != null && efd.getTypeParams() != null
1872:                                         && !node.getTypeParams().equals(efd.getTypeParams()))
1873:                         {
1874:                                 TypeCheckerErrors.report(3318, "Measure's type parameters must match function's", node.getMeasure().getLocation(), node.getMeasure());
1875:                                 TypeChecker.detail2("Actual", efd.getTypeParams(), "Expected", node.getTypeParams());
1876:                         }
1877:
1878:                         AFunctionType mtype = (AFunctionType) efd.getType();
1879:                         List<PType> exParams = null;
1880:                         
1881:                         if (node instanceof AExplicitFunctionDefinition)
1882:                         {
1883:                                 AExplicitFunctionDefinition ex = (AExplicitFunctionDefinition) node;
1884:                                 exParams = question.assistantFactory.createAExplicitFunctionDefinitionAssistant().getMeasureParams(ex);
1885:                         }
1886:
1887:                         if (node.getTypeParams() != null && !node.getTypeParams().isEmpty() && exParams != null)
1888:                         {
1889:                                 if (!mtype.getParameters().toString().equals(exParams.toString()))
1890:                                 {
1891:                                         TypeCheckerErrors.report(3303, "Measure parameters different to function", node.getMeasure().getLocation(), node.getMeasure());
1892:                                         TypeChecker.detail2(node.getMeasureName().toString(), mtype.getParameters(), "Expected", exParams);
1893:                                 }
1894:                         }
1895:                         else if (exParams != null && !question.assistantFactory.getTypeComparator().compatible(mtype.getParameters(), exParams))
1896:                         {
1897:                                 TypeCheckerErrors.report(3303, "Measure parameters different to function", node.getMeasure().getLocation(), node.getMeasure());
1898:                                 TypeCheckerErrors.detail2(mname.toString(), mtype.getParameters(), node.getName().getName(), exParams);
1899:                         }
1900:                         else if (exParams == null && !question.assistantFactory.getTypeComparator().compatible(mtype.getParameters(), ((AFunctionType) node.getType()).getParameters()))
1901:                         {
1902:                                 TypeCheckerErrors.report(3303, "Measure parameters different to function", node.getMeasure().getLocation(), node.getMeasure());
1903:                                 TypeCheckerErrors.detail2(mname.toString(), mtype.getParameters(), node.getName().getName(), ((AFunctionType) node.getType()).getParameters());
1904:                         }
1905:
1906:                         checkMeasure(question, node, efd.getName(), mtype.getResult());
1907:                 }
1908:         }
1909:
1910:         /**
1911:          * A measure must return a nat or nat-tuple.
1912:          */
1913:         private void checkMeasure(TypeCheckInfo question, SFunctionDefinitionBase node, ILexNameToken iLexNameToken, PType result)
1914:         {
1915:                 PTypeAssistantTC assistant = question.assistantFactory.createPTypeAssistant();
1916:                 
1917:                 if (!assistant.isNumeric(result, question.fromModule))
1918:                 {
1919:                         if (assistant.isProduct(result, question.fromModule))
1920:                         {
1921:                                 AProductType pt = assistant.getProduct(result, question.fromModule);
1922:
1923:                                 for (PType t : pt.getTypes())
1924:                                 {
1925:                                         if (!assistant.isNumeric(t, question.fromModule))
1926:                                         {
1927:                                                 TypeCheckerErrors.report(3272, "Measure range is not a nat, or a nat tuple", node.getMeasure().getLocation(), node.getMeasure());
1928:                                                 TypeCheckerErrors.detail("Actual", result);
1929:                                                 break;
1930:                                         }
1931:                                 }
1932:                         }
1933:                         else
1934:                         {
1935:                                 TypeCheckerErrors.report(3272, "Measure range is not a nat, or a nat tuple", node.getMeasure().getLocation(), node.getMeasure());
1936:                                 TypeCheckerErrors.detail("Actual", result);
1937:                         }
1938:                 }
1939:         }
1940:         
1941:         /**
1942:          * Typecheck annotations.
1943:          */
1944:         private void checkAnnotations(PDefinition node, TypeCheckInfo question) throws AnalysisException
1945:         {
1946:                 for (PAnnotation annotation: node.getAnnotations())
1947:                 {
1948:                         annotation.apply(THIS, question);        // Check the annotation itself
1949:                 }
1950:         }
1951: }