Package: TypeCheckerExpVisitor

TypeCheckerExpVisitor

nameinstructionbranchcomplexitylinemethod
TypeCheckerExpVisitor(IQuestionAnswer)
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
binaryCheck(SBooleanBinaryExp, ABooleanBasicType, IQuestionAnswer, TypeCheckInfo)
M: 0 C: 75
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
caseAAbsoluteUnaryExp(AAbsoluteUnaryExp, TypeCheckInfo)
M: 0 C: 71
100%
M: 1 C: 11
92%
M: 1 C: 6
86%
M: 0 C: 14
100%
M: 0 C: 1
100%
caseAAndBooleanBinaryExp(AAndBooleanBinaryExp, TypeCheckInfo)
M: 0 C: 42
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
caseAAnnotatedUnaryExp(AAnnotatedUnaryExp, TypeCheckInfo)
M: 36 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 7 C: 0
0%
M: 1 C: 0
0%
caseAApplyExp(AApplyExp, TypeCheckInfo)
M: 60 C: 419
87%
M: 9 C: 65
88%
M: 7 C: 31
82%
M: 11 C: 65
86%
M: 0 C: 1
100%
caseABooleanConstExp(ABooleanConstExp, TypeCheckInfo)
M: 0 C: 16
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseACardinalityUnaryExp(ACardinalityUnaryExp, TypeCheckInfo)
M: 0 C: 65
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
caseACasesExp(ACasesExp, TypeCheckInfo)
M: 0 C: 65
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 11
100%
M: 0 C: 1
100%
caseACharLiteralExp(ACharLiteralExp, TypeCheckInfo)
M: 0 C: 16
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseACompBinaryExp(ACompBinaryExp, TypeCheckInfo)
M: 19 C: 253
93%
M: 1 C: 17
94%
M: 1 C: 9
90%
M: 4 C: 38
90%
M: 0 C: 1
100%
caseADefExp(ADefExp, TypeCheckInfo)
M: 59 C: 98
62%
M: 3 C: 3
50%
M: 2 C: 2
50%
M: 10 C: 12
55%
M: 0 C: 1
100%
caseADistConcatUnaryExp(ADistConcatUnaryExp, TypeCheckInfo)
M: 0 C: 79
100%
M: 0 C: 6
100%
M: 0 C: 4
100%
M: 0 C: 15
100%
M: 0 C: 1
100%
caseADistIntersectUnaryExp(ADistIntersectUnaryExp, TypeCheckInfo)
M: 0 C: 65
100%
M: 1 C: 5
83%
M: 1 C: 3
75%
M: 0 C: 12
100%
M: 0 C: 1
100%
caseADistMergeUnaryExp(ADistMergeUnaryExp, TypeCheckInfo)
M: 0 C: 74
100%
M: 0 C: 8
100%
M: 0 C: 5
100%
M: 0 C: 15
100%
M: 0 C: 1
100%
caseADistUnionUnaryExp(ADistUnionUnaryExp, TypeCheckInfo)
M: 0 C: 77
100%
M: 1 C: 5
83%
M: 1 C: 3
75%
M: 0 C: 15
100%
M: 0 C: 1
100%
caseADivNumericBinaryExp(ADivNumericBinaryExp, TypeCheckInfo)
M: 0 C: 16
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseADivideNumericBinaryExp(ADivideNumericBinaryExp, TypeCheckInfo)
M: 0 C: 16
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseADomainResByBinaryExp(ADomainResByBinaryExp, TypeCheckInfo)
M: 0 C: 130
100%
M: 0 C: 10
100%
M: 0 C: 6
100%
M: 0 C: 18
100%
M: 0 C: 1
100%
caseADomainResToBinaryExp(ADomainResToBinaryExp, TypeCheckInfo)
M: 0 C: 140
100%
M: 0 C: 10
100%
M: 0 C: 6
100%
M: 0 C: 20
100%
M: 0 C: 1
100%
caseAElementsUnaryExp(AElementsUnaryExp, TypeCheckInfo)
M: 0 C: 97
100%
M: 0 C: 8
100%
M: 0 C: 5
100%
M: 0 C: 18
100%
M: 0 C: 1
100%
caseAElseIfExp(AElseIfExp, TypeCheckInfo)
M: 0 C: 15
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseAEqualsBinaryExp(AEqualsBinaryExp, TypeCheckInfo)
M: 0 C: 137
100%
M: 1 C: 11
92%
M: 1 C: 6
86%
M: 0 C: 18
100%
M: 0 C: 1
100%
caseAExists1Exp(AExists1Exp, TypeCheckInfo)
M: 0 C: 107
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
caseAExistsExp(AExistsExp, TypeCheckInfo)
M: 0 C: 85
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 10
100%
M: 0 C: 1
100%
caseAFieldExp(AFieldExp, TypeCheckInfo)
M: 43 C: 388
90%
M: 8 C: 42
84%
M: 5 C: 21
81%
M: 9 C: 66
88%
M: 0 C: 1
100%
caseAFieldNumberExp(AFieldNumberExp, TypeCheckInfo)
M: 0 C: 102
100%
M: 1 C: 5
83%
M: 1 C: 3
75%
M: 0 C: 17
100%
M: 0 C: 1
100%
caseAFloorUnaryExp(AFloorUnaryExp, TypeCheckInfo)
M: 0 C: 35
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
caseAForAllExp(AForAllExp, TypeCheckInfo)
M: 0 C: 80
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
caseAFuncInstatiationExp(AFuncInstatiationExp, TypeCheckInfo)
M: 40 C: 248
86%
M: 3 C: 25
89%
M: 3 C: 12
80%
M: 7 C: 50
88%
M: 0 C: 1
100%
caseAGreaterEqualNumericBinaryExp(AGreaterEqualNumericBinaryExp, TypeCheckInfo)
M: 0 C: 24
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseAGreaterNumericBinaryExp(AGreaterNumericBinaryExp, TypeCheckInfo)
M: 0 C: 24
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseAHeadUnaryExp(AHeadUnaryExp, TypeCheckInfo)
M: 0 C: 50
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
caseAHistoryExp(AHistoryExp, TypeCheckInfo)
M: 39 C: 99
72%
M: 4 C: 18
82%
M: 4 C: 8
67%
M: 6 C: 21
78%
M: 0 C: 1
100%
caseAIfExp(AIfExp, TypeCheckInfo)
M: 0 C: 18
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseAInSetBinaryExp(AInSetBinaryExp, TypeCheckInfo)
M: 0 C: 83
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
caseAIndicesUnaryExp(AIndicesUnaryExp, TypeCheckInfo)
M: 0 C: 70
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 11
100%
M: 0 C: 1
100%
caseAIntLiteralExp(AIntLiteralExp, TypeCheckInfo)
M: 6 C: 34
85%
M: 1 C: 3
75%
M: 1 C: 2
67%
M: 1 C: 5
83%
M: 0 C: 1
100%
caseAIotaExp(AIotaExp, TypeCheckInfo)
M: 47 C: 136
74%
M: 4 C: 6
60%
M: 3 C: 3
50%
M: 8 C: 21
72%
M: 0 C: 1
100%
caseAIsExp(AIsExp, TypeCheckInfo)
M: 16 C: 71
82%
M: 1 C: 5
83%
M: 1 C: 3
75%
M: 2 C: 13
87%
M: 0 C: 1
100%
caseAIsOfBaseClassExp(AIsOfBaseClassExp, TypeCheckInfo)
M: 0 C: 69
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
caseAIsOfClassExp(AIsOfClassExp, TypeCheckInfo)
M: 0 C: 81
100%
M: 1 C: 5
83%
M: 1 C: 3
75%
M: 0 C: 12
100%
M: 0 C: 1
100%
caseALambdaExp(ALambdaExp, TypeCheckInfo)
M: 0 C: 161
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 26
100%
M: 0 C: 1
100%
caseALenUnaryExp(ALenUnaryExp, TypeCheckInfo)
M: 0 C: 65
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
caseALessEqualNumericBinaryExp(ALessEqualNumericBinaryExp, TypeCheckInfo)
M: 0 C: 22
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseALessNumericBinaryExp(ALessNumericBinaryExp, TypeCheckInfo)
M: 0 C: 22
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseALetBeStExp(ALetBeStExp, TypeCheckInfo)
M: 0 C: 27
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
caseALetDefExp(ALetDefExp, TypeCheckInfo)
M: 0 C: 14
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseAMapCompMapExp(AMapCompMapExp, TypeCheckInfo)
M: 6 C: 76
93%
M: 1 C: 3
75%
M: 1 C: 2
67%
M: 1 C: 10
91%
M: 0 C: 1
100%
caseAMapDomainUnaryExp(AMapDomainUnaryExp, TypeCheckInfo)
M: 0 C: 55
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 10
100%
M: 0 C: 1
100%
caseAMapEnumMapExp(AMapEnumMapExp, TypeCheckInfo)
M: 7 C: 115
94%
M: 1 C: 5
83%
M: 1 C: 3
75%
M: 1 C: 18
95%
M: 0 C: 1
100%
caseAMapInverseUnaryExp(AMapInverseUnaryExp, TypeCheckInfo)
M: 0 C: 62
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 11
100%
M: 0 C: 1
100%
caseAMapRangeUnaryExp(AMapRangeUnaryExp, TypeCheckInfo)
M: 0 C: 55
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 10
100%
M: 0 C: 1
100%
caseAMapUnionBinaryExp(AMapUnionBinaryExp, TypeCheckInfo)
M: 0 C: 140
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 22
100%
M: 0 C: 1
100%
caseAMapletExp(AMapletExp, TypeCheckInfo)
M: 0 C: 70
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
caseAMkBasicExp(AMkBasicExp, TypeCheckInfo)
M: 24 C: 25
51%
M: 3 C: 1
25%
M: 2 C: 1
33%
M: 3 C: 3
50%
M: 0 C: 1
100%
caseAMkTypeExp(AMkTypeExp, TypeCheckInfo)
M: 21 C: 237
92%
M: 1 C: 17
94%
M: 1 C: 9
90%
M: 4 C: 49
92%
M: 0 C: 1
100%
caseAModNumericBinaryExp(AModNumericBinaryExp, TypeCheckInfo)
M: 0 C: 16
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseAMuExp(AMuExp, TypeCheckInfo)
M: 0 C: 151
100%
M: 0 C: 10
100%
M: 0 C: 6
100%
M: 0 C: 26
100%
M: 0 C: 1
100%
caseANarrowExp(ANarrowExp, TypeCheckInfo)
M: 27 C: 84
76%
M: 2 C: 4
67%
M: 2 C: 2
50%
M: 5 C: 12
71%
M: 0 C: 1
100%
caseANewExp(ANewExp, TypeCheckInfo)
M: 22 C: 264
92%
M: 4 C: 28
88%
M: 4 C: 13
76%
M: 4 C: 47
92%
M: 0 C: 1
100%
caseANilExp(ANilExp, TypeCheckInfo)
M: 0 C: 19
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseANotEqualBinaryExp(ANotEqualBinaryExp, TypeCheckInfo)
M: 0 C: 99
100%
M: 0 C: 6
100%
M: 0 C: 4
100%
M: 0 C: 13
100%
M: 0 C: 1
100%
caseANotInSetBinaryExp(ANotInSetBinaryExp, TypeCheckInfo)
M: 0 C: 85
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
caseANotUnaryExp(ANotUnaryExp, TypeCheckInfo)
M: 0 C: 44
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 7
100%
M: 0 C: 1
100%
caseANotYetSpecifiedExp(ANotYetSpecifiedExp, TypeCheckInfo)
M: 0 C: 10
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseAPlusNumericBinaryExp(APlusNumericBinaryExp, TypeCheckInfo)
M: 0 C: 79
100%
M: 0 C: 12
100%
M: 0 C: 7
100%
M: 0 C: 20
100%
M: 0 C: 1
100%
caseAPlusPlusBinaryExp(APlusPlusBinaryExp, TypeCheckInfo)
M: 0 C: 364
100%
M: 0 C: 24
100%
M: 0 C: 13
100%
M: 0 C: 53
100%
M: 0 C: 1
100%
caseAPostOpExp(APostOpExp, TypeCheckInfo)
M: 0 C: 14
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseAPowerSetUnaryExp(APowerSetUnaryExp, TypeCheckInfo)
M: 0 C: 86
100%
M: 0 C: 6
100%
M: 0 C: 4
100%
M: 0 C: 15
100%
M: 0 C: 1
100%
caseAPreExp(APreExp, TypeCheckInfo)
M: 0 C: 40
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 7
100%
M: 0 C: 1
100%
caseAPreOpExp(APreOpExp, TypeCheckInfo)
M: 0 C: 14
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseAProperSubsetBinaryExp(AProperSubsetBinaryExp, TypeCheckInfo)
M: 0 C: 125
100%
M: 0 C: 10
100%
M: 0 C: 6
100%
M: 0 C: 19
100%
M: 0 C: 1
100%
caseAQuoteLiteralExp(AQuoteLiteralExp, TypeCheckInfo)
M: 0 C: 17
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseARangeResByBinaryExp(ARangeResByBinaryExp, TypeCheckInfo)
M: 0 C: 127
100%
M: 0 C: 10
100%
M: 0 C: 6
100%
M: 0 C: 20
100%
M: 0 C: 1
100%
caseARangeResToBinaryExp(ARangeResToBinaryExp, TypeCheckInfo)
M: 0 C: 127
100%
M: 0 C: 10
100%
M: 0 C: 6
100%
M: 0 C: 20
100%
M: 0 C: 1
100%
caseARealLiteralExp(ARealLiteralExp, TypeCheckInfo)
M: 6 C: 49
89%
M: 1 C: 5
83%
M: 1 C: 3
75%
M: 1 C: 8
89%
M: 0 C: 1
100%
caseARemNumericBinaryExp(ARemNumericBinaryExp, TypeCheckInfo)
M: 0 C: 16
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseAReverseUnaryExp(AReverseUnaryExp, TypeCheckInfo)
M: 19 C: 26
58%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 4 C: 6
60%
M: 0 C: 1
100%
caseASameBaseClassExp(ASameBaseClassExp, TypeCheckInfo)
M: 0 C: 78
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
caseASameClassExp(ASameClassExp, TypeCheckInfo)
M: 0 C: 78
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
caseASelfExp(ASelfExp, TypeCheckInfo)
M: 0 C: 47
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
caseASeqCompSeqExp(ASeqCompSeqExp, TypeCheckInfo)
M: 18 C: 141
89%
M: 4 C: 10
71%
M: 4 C: 4
50%
M: 3 C: 18
86%
M: 0 C: 1
100%
caseASeqConcatBinaryExp(ASeqConcatBinaryExp, TypeCheckInfo)
M: 0 C: 170
100%
M: 0 C: 16
100%
M: 0 C: 9
100%
M: 0 C: 29
100%
M: 0 C: 1
100%
caseASeqEnumSeqExp(ASeqEnumSeqExp, TypeCheckInfo)
M: 0 C: 99
100%
M: 0 C: 8
100%
M: 0 C: 5
100%
M: 0 C: 18
100%
M: 0 C: 1
100%
caseASetCompSetExp(ASetCompSetExp, TypeCheckInfo)
M: 8 C: 128
94%
M: 1 C: 9
90%
M: 1 C: 5
83%
M: 1 C: 20
95%
M: 0 C: 1
100%
caseASetDifferenceBinaryExp(ASetDifferenceBinaryExp, TypeCheckInfo)
M: 0 C: 89
100%
M: 0 C: 8
100%
M: 0 C: 5
100%
M: 0 C: 17
100%
M: 0 C: 1
100%
caseASetEnumSetExp(ASetEnumSetExp, TypeCheckInfo)
M: 6 C: 112
95%
M: 1 C: 11
92%
M: 1 C: 6
86%
M: 1 C: 19
95%
M: 0 C: 1
100%
caseASetIntersectBinaryExp(ASetIntersectBinaryExp, TypeCheckInfo)
M: 0 C: 139
100%
M: 0 C: 14
100%
M: 0 C: 8
100%
M: 0 C: 26
100%
M: 0 C: 1
100%
caseASetRangeSetExp(ASetRangeSetExp, TypeCheckInfo)
M: 0 C: 106
100%
M: 0 C: 6
100%
M: 0 C: 4
100%
M: 0 C: 18
100%
M: 0 C: 1
100%
caseASetUnionBinaryExp(ASetUnionBinaryExp, TypeCheckInfo)
M: 10 C: 132
93%
M: 3 C: 7
70%
M: 3 C: 3
50%
M: 0 C: 22
100%
M: 0 C: 1
100%
caseAStarStarBinaryExp(AStarStarBinaryExp, TypeCheckInfo)
M: 16 C: 117
88%
M: 2 C: 10
83%
M: 2 C: 5
71%
M: 2 C: 21
91%
M: 0 C: 1
100%
caseAStateInitExp(AStateInitExp, TypeCheckInfo)
M: 0 C: 124
100%
M: 0 C: 10
100%
M: 0 C: 6
100%
M: 0 C: 25
100%
M: 0 C: 1
100%
caseAStringLiteralExp(AStringLiteralExp, TypeCheckInfo)
M: 0 C: 35
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
caseASubclassResponsibilityExp(ASubclassResponsibilityExp, TypeCheckInfo)
M: 0 C: 8
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseASubseqExp(ASubseqExp, TypeCheckInfo)
M: 6 C: 116
95%
M: 1 C: 7
88%
M: 1 C: 4
80%
M: 1 C: 20
95%
M: 0 C: 1
100%
caseASubsetBinaryExp(ASubsetBinaryExp, TypeCheckInfo)
M: 0 C: 131
100%
M: 0 C: 10
100%
M: 0 C: 6
100%
M: 0 C: 21
100%
M: 0 C: 1
100%
caseASubtractNumericBinaryExp(ASubtractNumericBinaryExp, TypeCheckInfo)
M: 0 C: 68
100%
M: 0 C: 8
100%
M: 0 C: 5
100%
M: 0 C: 11
100%
M: 0 C: 1
100%
caseATailUnaryExp(ATailUnaryExp, TypeCheckInfo)
M: 0 C: 57
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
caseAThreadIdExp(AThreadIdExp, TypeCheckInfo)
M: 23 C: 34
60%
M: 4 C: 6
60%
M: 3 C: 3
50%
M: 4 C: 5
56%
M: 0 C: 1
100%
caseATimeExp(ATimeExp, TypeCheckInfo)
M: 23 C: 34
60%
M: 5 C: 5
50%
M: 4 C: 2
33%
M: 4 C: 5
56%
M: 0 C: 1
100%
caseATimesNumericBinaryExp(ATimesNumericBinaryExp, TypeCheckInfo)
M: 0 C: 84
100%
M: 0 C: 12
100%
M: 0 C: 7
100%
M: 0 C: 23
100%
M: 0 C: 1
100%
caseATupleExp(ATupleExp, TypeCheckInfo)
M: 0 C: 101
100%
M: 0 C: 10
100%
M: 0 C: 6
100%
M: 0 C: 17
100%
M: 0 C: 1
100%
caseAUnaryMinusUnaryExp(AUnaryMinusUnaryExp, TypeCheckInfo)
M: 0 C: 50
100%
M: 0 C: 6
100%
M: 0 C: 4
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
caseAUnaryPlusUnaryExp(AUnaryPlusUnaryExp, TypeCheckInfo)
M: 0 C: 29
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
caseAUndefinedExp(AUndefinedExp, TypeCheckInfo)
M: 0 C: 8
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseAVariableExp(AVariableExp, TypeCheckInfo)
M: 57 C: 259
82%
M: 6 C: 30
83%
M: 6 C: 13
68%
M: 13 C: 54
81%
M: 0 C: 1
100%
checkNumeric(SNumericBinaryExp, IQuestionAnswer, TypeCheckInfo)
M: 0 C: 91
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 13
100%
M: 0 C: 1
100%
checkOrdered(SNumericBinaryExp, IQuestionAnswer, TypeCheckInfo)
M: 0 C: 91
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 13
100%
M: 0 C: 1
100%
defaultSBooleanBinaryExp(SBooleanBinaryExp, TypeCheckInfo)
M: 0 C: 22
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
functionApply(AApplyExp, boolean, AFunctionType, TypeCheckInfo)
M: 17 C: 115
87%
M: 3 C: 11
79%
M: 2 C: 6
75%
M: 2 C: 22
92%
M: 0 C: 1
100%
getMeasureApply(AApplyExp, ILexNameToken, boolean)
M: 82 C: 0
0%
M: 8 C: 0
0%
M: 5 C: 0
0%
M: 14 C: 0
0%
M: 1 C: 0
0%
getRecursiveDefinition(AApplyExp, TypeCheckInfo)
M: 0 C: 58
100%
M: 1 C: 11
92%
M: 1 C: 6
86%
M: 0 C: 17
100%
M: 0 C: 1
100%
mapApply(AApplyExp, boolean, SMapType, TypeCheckInfo)
M: 0 C: 55
100%
M: 0 C: 6
100%
M: 0 C: 4
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
operationApply(AApplyExp, boolean, AOperationType, TypeCheckInfo)
M: 54 C: 45
45%
M: 3 C: 5
63%
M: 3 C: 2
40%
M: 9 C: 9
50%
M: 0 C: 1
100%
sequenceApply(AApplyExp, boolean, SSeqType, TypeCheckInfo)
M: 0 C: 77
100%
M: 0 C: 12
100%
M: 0 C: 7
100%
M: 0 C: 11
100%
M: 0 C: 1
100%
typeCheck(ACaseAlternative, IQuestionAnswer, TypeCheckInfo, PType)
M: 6 C: 162
96%
M: 1 C: 7
88%
M: 1 C: 4
80%
M: 3 C: 19
86%
M: 0 C: 1
100%

Coverage

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