![[Jenkins]](/jenkins/static/4ffc0891/images/jenkins-header-logo-v2.svg){kind=logo}
Method: caseAExplicitOperationDefinition(AExplicitOperationDefinition, 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: }