From 2cde0265070d65f738b9ee236f7246e765536f08 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Tue, 17 Nov 2015 13:13:40 -0800 Subject: Fix issue 107. Instead of writing out StaticReceiverExpr as null valued LiteralExpr, write out its type instead. --- Source/Dafny/Compiler.cs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 82795480..8f199da4 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -2310,7 +2310,9 @@ namespace Microsoft.Dafny { Contract.Requires(expr != null); if (expr is LiteralExpr) { LiteralExpr e = (LiteralExpr)expr; - if (e.Value == null) { + if (e is StaticReceiverExpr) { + wr.Write(TypeName(e.Type, wr)); + } else if (e.Value == null) { wr.Write("({0})null", TypeName(e.Type, wr)); } else if (e.Value is bool) { wr.Write((bool)e.Value ? "true" : "false"); @@ -2394,7 +2396,7 @@ namespace Microsoft.Dafny { wr.Write(".@{0}", sf.CompiledName); wr.Write(sf.PostString); } else { - TrParenExpr(e.Obj, wr, inLetExprBody); + TrExpr(e.Obj, wr, inLetExprBody); wr.Write(".@{0}", e.Member.CompileName); } -- cgit v1.2.3