diff options
| -rw-r--r-- | Dafny/Compiler.cs | 14 |
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) {
|