diff options
author | Rustan Leino <leino@microsoft.com> | 2012-01-18 20:14:04 -0800 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2012-01-18 20:14:04 -0800 |
commit | a8abac3364f9af380d9854b490426c1a3b016d97 (patch) | |
tree | 9385a1c964bdc9b072fc38d68be8a7f8ab69e4ca /Dafny/Compiler.cs | |
parent | 7ffe46ca4bd9ff7c4ca0c0a550a841c6dc120875 (diff) |
Dafny: fixed bug in compilation of generic datatypes
Diffstat (limited to 'Dafny/Compiler.cs')
-rw-r--r-- | Dafny/Compiler.cs | 8 |
1 files changed, 5 insertions, 3 deletions
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);
}
}
}
|