Added types "char" and "string" (the latter being a synonym for "seq<char>").

Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings.
Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions.
Fixed lack of operator resolution in custom attributes.

1 files changed, 6 insertions, 8 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 6ec05a50..5eba44ee 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -403,19 +403,14 @@ namespace Microsoft.Dafny {
       }

     }

 

-    public void PrintAttributeArgs(List<Attributes.Argument> args, bool isFollowedBySemicolon) {

+    public void PrintAttributeArgs(List<Expression> args, bool isFollowedBySemicolon) {

       Contract.Requires(args != null);

       string prefix = " ";

-      foreach (Attributes.Argument arg in args) {

+      foreach (var arg in args) {

         Contract.Assert(arg != null);

         wr.Write(prefix);

         prefix = ", ";

-        if (arg.S != null) {

-          wr.Write("\"{0}\"", arg.S);

-        } else {

-          Contract.Assert( arg.E != null);

-          PrintExpression(arg.E, isFollowedBySemicolon);

-        }

+        PrintExpression(arg, isFollowedBySemicolon);

       }

     }

 

@@ -1219,6 +1214,9 @@ namespace Microsoft.Dafny {
           wr.Write("null");

         } else if (e.Value is bool) {

           wr.Write((bool)e.Value ? "true" : "false");

+        } else if (e.Value is string) {

+          var str = (StringLiteralExpr)e;

+          wr.Write("{0}\"{1}\"", str.IsVerbatim ? "@" : "", (string)e.Value);

         } else if (e.Value is Basetypes.BigDec) {

           Basetypes.BigDec dec = (Basetypes.BigDec)e.Value;

           wr.Write((dec.Mantissa >= 0) ? "" : "-");