From 82edb1b179916ee61655ab7e425a17ab5145fac8 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Mon, 20 Oct 2014 17:08:46 -0700
Subject: 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.

---
 Binaries/DafnyRuntime.cs | 23 +++++++++++++++++------
 1 file changed, 17 insertions(+), 6 deletions(-)

(limited to 'Binaries/DafnyRuntime.cs')

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++) {
-- 
cgit v1.2.3