diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-13 17:46:24 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-13 17:46:24 -0700 |
| commit | e07ce1423cf6b75adc8884d2d01e09b4d0f9519b (patch) | |
| tree | 59ca08a9f8edbdd041829adceba71c0a03aebdf8 /Dafny | |
| parent | 3d56fc351f6a71d90e72ef115477d1be663cfba5 (diff) | |
| parent | 7cabbe6e10f11b90df4e4b5f5a3bb1c2253b87c5 (diff) | |
Merge
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/Resolver.cs | 35 |
1 files changed, 33 insertions, 2 deletions
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 3ff0c12b..3780e0d9 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -2889,8 +2889,10 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Eq:
case BinaryExpr.Opcode.Neq:
- if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
- Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
+ if (!CouldPossiblyBeSameType(e.E0.Type, e.E1.Type)) {
+ if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
+ Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
+ }
}
expr.Type = Type.Bool;
break;
@@ -3282,6 +3284,35 @@ namespace Microsoft.Dafny { }
}
+ private bool CouldPossiblyBeSameType(Type A, Type B) {
+ if (A.IsTypeParameter || B.IsTypeParameter) {
+ return true;
+ }
+ if (A.IsArrayType && B.IsArrayType) {
+ Type a = UserDefinedType.ArrayElementType(A);
+ Type b = UserDefinedType.ArrayElementType(B);
+ return CouldPossiblyBeSameType(a, b);
+ }
+ if (A is UserDefinedType && B is UserDefinedType) {
+ UserDefinedType a = (UserDefinedType)A;
+ UserDefinedType b = (UserDefinedType)B;
+ if (a.ResolvedClass != null && b.ResolvedClass != null && a.ResolvedClass == b.ResolvedClass) {
+ if (a.TypeArgs.Count != b.TypeArgs.Count) {
+ return false; // this probably doesn't happen if the classes are the same.
+ }
+ for (int i = 0; i < a.TypeArgs.Count; i++) {
+ if (!CouldPossiblyBeSameType(a.TypeArgs[i], b.TypeArgs[i]))
+ return false;
+ }
+ // all parameters could be the same
+ return true;
+ }
+ // either we don't know what class it is yet, or the classes mismatch
+ return false;
+ }
+ return false;
+ }
+
/// <summary>
/// Generate an error for every non-ghost feature used in "expr".
/// Requires "expr" to have been successfully resolved.
|