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, 17 insertions, 6 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index f00db25a..661666ef 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -434,6 +434,9 @@ namespace Dafny
     public static Sequence<T> FromElements(params T[] values) {

       return new Sequence<T>(values);

     }

+    public static Sequence<char> FromString(string s) {

+      return new Sequence<char>(s.ToCharArray());

+    }

     public BigInteger Length {

       get { return new BigInteger(elmts.Length); }

     }

@@ -467,13 +470,21 @@ namespace Dafny
       return elmts.GetHashCode();

     }

     public override string ToString() {

-      var s = "[";

-      var sep = "";

-      foreach (var t in elmts) {

-        s += sep + t.ToString();

-        sep = ", ";

+      if (elmts is char[]) {

+        var s = "";

+        foreach (var t in elmts) {

+          s += t.ToString();

+        }

+        return s;

+      } else {

+        var s = "[";

+        var sep = "";

+        foreach (var t in elmts) {

+          s += sep + t.ToString();

+          sep = ", ";

+        }

+        return s + "]";

       }

-      return s + "]";

     }

     bool EqualUntil(Sequence<T> other, int n) {

       for (int i = 0; i < n; i++) {