From 4d5757e19265d5e065a1b3848beab1c583a40a4c Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Thu, 14 Jun 2012 13:35:11 -0700
Subject: Dafny: fixed a couple of compiler bugs

---
 Binaries/DafnyRuntime.cs         |  3 ++-
 Source/Dafny/Compiler.cs         | 10 ++++++++++
 Test/dafny2/StoreAndRetrieve.dfy |  2 +-
 3 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index f7eecfc5..61df448f 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -1,8 +1,9 @@
 using System.Numerics;
-using System.Collections.Generic;
 
 namespace Dafny
 {
+  using System.Collections.Generic;
+
   public class Set<T>
   {
     Dictionary<T, bool> dict;
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 911e5aac..3938ec8d 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1829,6 +1829,11 @@ namespace Microsoft.Dafny {
             Type t = cce.NonNull(e.E0.Type);
             if (t.IsDatatype || t.IsTypeParameter) {
               callString = "Equals";
+            } else if (t.IsRefType) {
+              // Dafny's type rules are slightly different C#, so we may need a cast here.
+              // For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some
+              // type parameter.
+              opString = "== (object)";
             } else {
               opString = "==";
             }
@@ -1839,6 +1844,11 @@ namespace Microsoft.Dafny {
             if (t.IsDatatype || t.IsTypeParameter) {
               preOpString = "!";
               callString = "Equals";
+            } else if (t.IsRefType) {
+              // Dafny's type rules are slightly different C#, so we may need a cast here.
+              // For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some
+              // type parameter.
+              opString = "!= (object)";
             } else {
               opString = "!=";
             }
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index ea26a234..15c82d65 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -1,4 +1,4 @@
-module A imports Library {
+ghost module A imports Library {
   class {:autocontracts} StoreAndRetrieve<Thing> {
     ghost var Contents: set<Thing>;
     predicate Valid
-- 
cgit v1.2.3