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, 5 insertions, 9 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index c195e14b..75c6ddfe 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -228,14 +228,7 @@ namespace Microsoft.Dafny
       if (attrs == null) {

         return null;

       } else {

-        return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneAttrArg), CloneAttributes(attrs.Prev));

-      }

-    }

-    public Attributes.Argument CloneAttrArg(Attributes.Argument aa) {

-      if (aa.E != null) {

-        return new Attributes.Argument(Tok(aa.Tok), CloneExpr(aa.E));

-      } else {

-        return new Attributes.Argument(Tok(aa.Tok), aa.S);

+        return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev));

       }

     }

 

@@ -256,6 +249,9 @@ namespace Microsoft.Dafny
           return new LiteralExpr(Tok(e.tok));

         } else if (e.Value is bool) {

           return new LiteralExpr(Tok(e.tok), (bool)e.Value);

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

+          var str = (StringLiteralExpr)e;

+          return new StringLiteralExpr(Tok(e.tok), (string)e.Value, str.IsVerbatim);

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

           return new LiteralExpr(Tok(e.tok), (Basetypes.BigDec)e.Value);

         } else {

@@ -479,7 +475,7 @@ namespace Microsoft.Dafny
 

       } else if (stmt is PrintStmt) {

         var s = (PrintStmt)stmt;

-        r = new PrintStmt(Tok(s.Tok), Tok(s.EndTok), s.Args.ConvertAll(CloneAttrArg));

+        r = new PrintStmt(Tok(s.Tok), Tok(s.EndTok), s.Args.ConvertAll(CloneExpr));

 

       } else if (stmt is BreakStmt) {

         var s = (BreakStmt)stmt;