From 2d672bd83995d33c2adca085ea4cdbef351ab29f Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 16 Feb 2012 13:19:29 -0800 Subject: Dafny: fixed a couple of compiler bugs --- Dafny/Compiler.cs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'Dafny/Compiler.cs') diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index caf3df24..a1f9e4fc 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -1216,7 +1216,7 @@ namespace Microsoft.Dafny { } else { if (rhs is ExprRhs) { SpillLetVariableDecls(((ExprRhs)rhs).Expr, indent); - } else if (tRhs != null) { + } else if (tRhs != null && tRhs.ArrayDimensions != null) { foreach (Expression dim in tRhs.ArrayDimensions) { SpillLetVariableDecls(dim, indent); } @@ -1582,7 +1582,11 @@ namespace Microsoft.Dafny { } else if (expr is DatatypeValue) { DatatypeValue dtv = (DatatypeValue)expr; Contract.Assert(dtv.Ctor != null); // since dtv has been successfully resolved - wr.Write("new {0}(new {1}", dtv.DatatypeName, DtCtorName(dtv.Ctor)); + wr.Write("new {0}", dtv.DatatypeName); + if (dtv.InferredTypeArgs.Count != 0) { + wr.Write("<{0}>", TypeNames(dtv.InferredTypeArgs)); + } + wr.Write("(new {0}", DtCtorName(dtv.Ctor)); if (dtv.InferredTypeArgs.Count != 0) { wr.Write("<{0}>", TypeNames(dtv.InferredTypeArgs)); } -- cgit v1.2.3