Package: TypeCheckerDefinitionVisitor

TypeCheckerDefinitionVisitor

nameinstructionbranchcomplexitylinemethod
TypeCheckerDefinitionVisitor(IQuestionAnswer)
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseAApplyExpressionTraceCoreDefinition(AApplyExpressionTraceCoreDefinition, TypeCheckInfo)
M: 0 C: 8
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
caseAAssignmentDefinition(AAssignmentDefinition, TypeCheckInfo)
M: 8 C: 70
90%
M: 1 C: 3
75%
M: 1 C: 2
67%
M: 1 C: 11
92%
M: 0 C: 1
100%
caseABracketedExpressionTraceCoreDefinition(ABracketedExpressionTraceCoreDefinition, TypeCheckInfo)
M: 0 C: 32
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
caseAClassInvariantDefinition(AClassInvariantDefinition, TypeCheckInfo)
M: 0 C: 51
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 10
100%
M: 0 C: 1
100%
caseAConcurrentExpressionTraceCoreDefinition(AConcurrentExpressionTraceCoreDefinition, TypeCheckInfo)
M: 0 C: 20
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
caseAEqRelation(AEqRelation, TypeCheckInfo)
M: 0 C: 8
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
caseAEqualsDefinition(AEqualsDefinition, TypeCheckInfo)
M: 111 C: 171
61%
M: 8 C: 8
50%
M: 6 C: 3
33%
M: 15 C: 26
63%
M: 0 C: 1
100%
caseAExplicitFunctionDefinition(AExplicitFunctionDefinition, TypeCheckInfo)
M: 41 C: 474
92%
M: 7 C: 39
85%
M: 7 C: 17
71%
M: 7 C: 76
92%
M: 0 C: 1
100%
caseAExplicitOperationDefinition(AExplicitOperationDefinition, TypeCheckInfo)
M: 119 C: 683
85%
M: 13 C: 75
85%
M: 12 C: 33
73%
M: 18 C: 97
84%
M: 0 C: 1
100%
caseAExternalDefinition(AExternalDefinition, TypeCheckInfo)
M: 0 C: 2
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
caseAImplicitFunctionDefinition(AImplicitFunctionDefinition, TypeCheckInfo)
M: 122 C: 422
78%
M: 16 C: 36
69%
M: 13 C: 14
52%
M: 20 C: 66
77%
M: 0 C: 1
100%
caseAImplicitOperationDefinition(AImplicitOperationDefinition, TypeCheckInfo)
M: 162 C: 875
84%
M: 25 C: 95
79%
M: 20 C: 41
67%
M: 19 C: 137
88%
M: 0 C: 1
100%
caseAImportedDefinition(AImportedDefinition, TypeCheckInfo)
M: 12 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
caseAInheritedDefinition(AInheritedDefinition, TypeCheckInfo)
M: 12 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
caseAInstanceVariableDefinition(AInstanceVariableDefinition, TypeCheckInfo)
M: 22 C: 131
86%
M: 2 C: 8
80%
M: 2 C: 4
67%
M: 3 C: 19
86%
M: 0 C: 1
100%
caseALetBeStBindingTraceDefinition(ALetBeStBindingTraceDefinition, TypeCheckInfo)
M: 0 C: 23
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseALetDefBindingTraceDefinition(ALetDefBindingTraceDefinition, TypeCheckInfo)
M: 0 C: 10
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
caseALocalDefinition(ALocalDefinition, TypeCheckInfo)
M: 0 C: 18
100%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseAMultiBindListDefinition(AMultiBindListDefinition, TypeCheckInfo)
M: 10 C: 49
83%
M: 1 C: 3
75%
M: 1 C: 2
67%
M: 1 C: 9
90%
M: 0 C: 1
100%
caseAMutexSyncDefinition(AMutexSyncDefinition, TypeCheckInfo)
M: 51 C: 148
74%
M: 8 C: 24
75%
M: 8 C: 9
53%
M: 7 C: 28
80%
M: 0 C: 1
100%
caseANamedTraceDefinition(ANamedTraceDefinition, TypeCheckInfo)
M: 0 C: 75
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 10
100%
M: 0 C: 1
100%
caseAOrdRelation(AOrdRelation, TypeCheckInfo)
M: 0 C: 26
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
caseAPerSyncDefinition(APerSyncDefinition, TypeCheckInfo)
M: 72 C: 165
70%
M: 9 C: 21
70%
M: 9 C: 7
44%
M: 10 C: 37
79%
M: 0 C: 1
100%
caseARenamedDefinition(ARenamedDefinition, TypeCheckInfo)
M: 12 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
caseARepeatTraceDefinition(ARepeatTraceDefinition, TypeCheckInfo)
M: 6 C: 16
73%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 1 C: 2
67%
M: 0 C: 1
100%
caseAStateDefinition(AStateDefinition, TypeCheckInfo)
M: 8 C: 110
93%
M: 1 C: 11
92%
M: 1 C: 6
86%
M: 2 C: 20
91%
M: 0 C: 1
100%
caseAThreadDefinition(AThreadDefinition, TypeCheckInfo)
M: 0 C: 56
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
caseATypeDefinition(ATypeDefinition, TypeCheckInfo)
M: 17 C: 252
94%
M: 5 C: 29
85%
M: 4 C: 14
78%
M: 1 C: 46
98%
M: 0 C: 1
100%
caseAUntypedDefinition(AUntypedDefinition, TypeCheckInfo)
M: 9 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
caseAValueDefinition(AValueDefinition, TypeCheckInfo)
M: 27 C: 156
85%
M: 2 C: 18
90%
M: 2 C: 9
82%
M: 4 C: 32
89%
M: 0 C: 1
100%
checkAnnotations(PDefinition, TypeCheckInfo)
M: 11 C: 8
42%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 2 C: 2
50%
M: 0 C: 1
100%
checkMeasure(TypeCheckInfo, SFunctionDefinitionBase, ILexNameToken, PType)
M: 54 C: 11
17%
M: 7 C: 1
13%
M: 4 C: 1
20%
M: 11 C: 3
21%
M: 0 C: 1
100%
getDefinitions(APatternListTypePair, NameScope, ITypeCheckerAssistantFactory)
M: 0 C: 29
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
setMeasureDef(TypeCheckInfo, SFunctionDefinitionBase, ILexNameToken, Environment, NameScope)
M: 166 C: 109
40%
M: 24 C: 18
43%
M: 20 C: 2
9%
M: 18 C: 26
59%
M: 0 C: 1
100%
setMeasureExp(TypeCheckInfo, SFunctionDefinitionBase, Environment, Environment, NameScope)
M: 180 C: 0
0%
M: 12 C: 0
0%
M: 7 C: 0
0%
M: 33 C: 0
0%
M: 1 C: 0
0%
static {...}
M: 2 C: 6
75%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 1
100%
M: 0 C: 1
100%
typeCheck(List, IQuestionAnswer, TypeCheckInfo)
M: 0 C: 17
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
typeResolve(AExternalClause, IQuestionAnswer, TypeCheckInfo)
M: 0 C: 12
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%

Coverage

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