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, 4 insertions, 2 deletions

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 17867100..43333f22 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -444,6 +444,8 @@ namespace Microsoft.Dafny
 

       if (prev is BoolType) {

         return next is BoolType;

+      } else if (prev is CharType) {

+        return next is CharType;

       } else if (prev is IntType) {

         if (next is IntType) {

           return (prev is NatType) == (next is NatType);

@@ -1071,7 +1073,7 @@ namespace Microsoft.Dafny
                 var e = refinementCloner.CloneExpr(oldAssume.Expr);

                 var attrs = refinementCloner.MergeAttributes(oldAssume.Attributes, skel.Attributes);

                 body.Add(new AssertStmt(new Translator.ForceCheckToken(skel.Tok), new Translator.ForceCheckToken(skel.EndTok),

-                  e, new Attributes("prependAssertToken", new List<Attributes.Argument>(), attrs)));

+                  e, new Attributes("prependAssertToken", new List<Expression>(), attrs)));

                 ReportAdditionalInformation(c.ConditionEllipsis, "assume->assert: " + Printer.ExprToString(e), 3);

                 i++; j++;

               }

@@ -1589,7 +1591,7 @@ namespace Microsoft.Dafny
       if (moreAttrs == null) {

         return CloneAttributes(prevAttrs);

       } else {

-        return new Attributes(moreAttrs.Name, moreAttrs.Args.ConvertAll(CloneAttrArg), MergeAttributes(prevAttrs, moreAttrs.Prev));

+        return new Attributes(moreAttrs.Name, moreAttrs.Args.ConvertAll(CloneExpr), MergeAttributes(prevAttrs, moreAttrs.Prev));

       }

     }

   }