Dafny: fixed datatype GetHashCode() to make it consistent with Equals()

1 files changed, 13 insertions, 1 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 70b16578..57623068 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -217,6 +217,7 @@ namespace Microsoft.Dafny {
         wr.WriteLine("}");

       }

 

+      int constructorIndex = 0; // used to give each constructor a different

       foreach (DatatypeCtor ctor in dt.Ctors) {

         // class Dt_Ctor<T,U> : Base_Dt<T> {

         //   Fields;

@@ -286,7 +287,17 @@ namespace Microsoft.Dafny {
 

         // GetHashCode method

         Indent(ind); wr.WriteLine("public override int GetHashCode() {");

-        Indent(ind + IndentAmount); wr.WriteLine("return base.GetHashCode();  // surely this can be improved");

+        Indent(ind + IndentAmount); wr.Write("return " + constructorIndex);

+

+        i = 0;

+        foreach (Formal arg in ctor.Formals) {

+          if (!arg.IsGhost) {

+            string nm = FormalName(arg, i);

+            wr.Write(" ^ this.@{0}.GetHashCode()", nm);

+            i++;

+          }

+        }

+        wr.WriteLine(";");

         Indent(ind); wr.WriteLine("}");

 

         if (dt is IndDatatypeDecl) {

@@ -313,6 +324,7 @@ namespace Microsoft.Dafny {
 

         Indent(indent);  wr.WriteLine("}");

       }

+      constructorIndex ++;

     }

 

     void CompileDatatypeStruct(DatatypeDecl dt, int indent) {