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