diff options
| -rw-r--r-- | Source/Dafny/Compiler.cs | 8 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 19 |
2 files changed, 21 insertions, 6 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index e98062ce..f5e8ff30 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -88,6 +88,10 @@ namespace Microsoft.Dafny { public void Compile(Program program) {
Contract.Requires(program != null);
wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);
+ wr.WriteLine("// To recompile, use 'csc' with: /r:System.Numerics.dll");
+ wr.WriteLine("// and choosing /target:exe or /target:library");
+ wr.WriteLine("// You might also want to include compiler switches like:");
+ wr.WriteLine("// /debug /nowarn:0164 /nowarn:0219");
wr.WriteLine();
ReadRuntimeSystem();
CompileBuiltIns(program.BuiltIns);
@@ -675,7 +679,7 @@ namespace Microsoft.Dafny { foreach (var member in c.Members) {
var m = member as Method;
if (m != null) {
- if (!m.IsGhost && m.Name == "Main" && m.Ins.Count == 0 && m.Outs.Count == 0 && m.Req.Count == 0) {
+ if (!m.IsGhost && m.Name == "Main" && m.TypeArgs.Count == 0 && m.Ins.Count == 0 && m.Outs.Count == 0 && m.Req.Count == 0) {
return true;
}
}
@@ -763,7 +767,7 @@ namespace Microsoft.Dafny { Indent(indent); wr.WriteLine("}");
// allow the Main method to be an instance method
- if (!m.IsStatic && m.Name == "Main" && m.Ins.Count == 0 && m.Outs.Count == 0 && m.Req.Count == 0) {
+ if (!m.IsStatic && m.Name == "Main" && m.TypeArgs.Count == 0 && m.Ins.Count == 0 && m.Outs.Count == 0 && m.Req.Count == 0) {
Indent(indent);
wr.WriteLine("public static void Main(string[] args) {");
Contract.Assert(m.EnclosingClass == c);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 82844d56..44351754 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6145,10 +6145,21 @@ namespace Microsoft.Dafny case BinaryExpr.Opcode.Eq:
case BinaryExpr.Opcode.Neq:
- if (!ComparableTypes(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);
- }
+ // We will both check for comparability and attempt to unify the types, and we do them in this order so that
+ // the compatibility check is not influenced by the unification.
+ var areComparable = ComparableTypes(e.E0.Type, e.E1.Type);
+ var unificationSuccess = UnifyTypes(e.E0.Type, e.E1.Type);
+ if (areComparable) {
+ // The expression is legal. For example, we may have received two equal types, or we have have gotten types like
+ // array<T> and array<U> where T is a type parameter and U is some type.
+ // Still, we're still happy that we did the type unification to assign type proxies as needed.
+ } else if (unificationSuccess) {
+ // The expression is legal. This can happen if one of the types contains a type proxy. For example, if the
+ // first type is array<T> and the second type is a proxy, then the compatibility check will return false but
+ // unification will succeed.
+ } else {
+ // The types are not comparable and do not unify. It's time for an error message.
+ Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
}
expr.Type = Type.Bool;
break;
|