Dafny: fixed bug in compilation of generic datatypes

1 files changed, 5 insertions, 3 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 6ede64fb..4a2b41a1 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -290,8 +290,10 @@ namespace Microsoft.Dafny {
       //   ...

       // }

       string DtT = dt.Name;

+      string DtT_TypeArgs = "";

       if (dt.TypeArgs.Count != 0) {

-        DtT += "<" + TypeParameters(dt.TypeArgs) + ">";

+        DtT_TypeArgs = "<" + TypeParameters(dt.TypeArgs) + ">";

+        DtT += DtT_TypeArgs;

       }

 

       Indent(indent);

@@ -342,7 +344,7 @@ namespace Microsoft.Dafny {
       foreach (var ctor in dt.Ctors) {

         //   public bool _Ctor0 { get { return _D is Dt_Ctor0; } }

         Indent(ind);

-        wr.WriteLine("public bool _{0} {{ get {{ return _D is {1}_{0}; }} }}", ctor.Name, DtT);

+        wr.WriteLine("public bool _{0} {{ get {{ return _D is {1}_{0}{2}; }} }}", ctor.Name, dt.Name, DtT_TypeArgs);

       }

 

       // destructors

@@ -351,7 +353,7 @@ namespace Microsoft.Dafny {
           if (arg.HasName) {

             //   public T0 @Dtor0 { get { return ((DT_Ctor)_D).@Dtor0; } }

             Indent(ind);

-            wr.WriteLine("public {0} dtor_{1} {{ get {{ return (({2}_{3})_D).@{1}; }} }}", TypeName(arg.Type), arg.Name, DtT, ctor.Name);

+            wr.WriteLine("public {0} dtor_{1} {{ get {{ return (({2}_{3}{4})_D).@{1}; }} }}", TypeName(arg.Type), arg.Name, dt.Name, ctor.Name, DtT_TypeArgs);

           }

         }

       }