From a8abac3364f9af380d9854b490426c1a3b016d97 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 18 Jan 2012 20:14:04 -0800
Subject: Dafny: fixed bug in compilation of generic datatypes

---
 Dafny/Compiler.cs | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'Dafny/Compiler.cs')

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 6ede64fb..4a2b41a1 100644
--- a/Dafny/Compiler.cs
+++ b/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);
           }
         }
       }
-- 
cgit v1.2.3