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/DafnyPrelude.bpl | 19 +++++++++++++++++++
 Binaries/DafnyRuntime.cs  | 23 +++++++++++++++++------
 2 files changed, 36 insertions(+), 6 deletions(-)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 993ada51..4cdb21e9 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -15,6 +15,7 @@ axiom $$Language$Dafny;        // coming from a Dafny program.
 type Ty;
 
 const unique TBool : Ty;
+const unique TChar : Ty;
 const unique TInt  : Ty;
 const unique TNat  : Ty;
 const unique TReal : Ty;
@@ -41,6 +42,7 @@ type TyTag;
 function Tag(Ty) : TyTag;
 
 const unique TagBool     : TyTag;
+const unique TagChar     : TyTag;
 const unique TagInt      : TyTag;
 const unique TagNat      : TyTag;
 const unique TagReal     : TyTag;
@@ -51,6 +53,7 @@ const unique TagMap      : TyTag;
 const unique TagClass    : TyTag;
 
 axiom Tag(TBool) == TagBool;
+axiom Tag(TChar) == TagChar;
 axiom Tag(TInt) == TagInt;
 axiom Tag(TNat) == TagNat;
 axiom Tag(TReal) == TagReal;
@@ -69,6 +72,17 @@ axiom (forall x: real :: { $Box(LitReal(x)) } $Box(LitReal(x)) == Lit($Box(x)) )
 function {:identity} Lit<T>(x: T): T { x }
 axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
 
+// ---------------------------------------------------------------
+// -- Characters -------------------------------------------------
+// ---------------------------------------------------------------
+
+type char;
+function char#FromInt(int): char;
+function char#ToInt(char): int;  // inverse of char#FromInt
+axiom (forall n: int ::
+  { char#FromInt(n) }
+  0 <= n && n < 65536 ==> char#ToInt(char#FromInt(n)) == n);
+
 // ---------------------------------------------------------------
 // -- References -------------------------------------------------
 // ---------------------------------------------------------------
@@ -115,6 +129,9 @@ axiom (forall bx : Box ::
 axiom (forall bx : Box ::
     { $IsBox(bx, TBool) }
     ( $IsBox(bx, TBool) ==> $Box($Unbox(bx) : bool) == bx && $Is($Unbox(bx) : bool, TBool)));
+axiom (forall bx : Box ::
+    { $IsBox(bx, TChar) }
+    ( $IsBox(bx, TChar) ==> $Box($Unbox(bx) : char) == bx && $Is($Unbox(bx) : char, TChar)));
 axiom (forall bx : Box, t : Ty ::
     { $IsBox(bx, TSet(t)) }
     ( $IsBox(bx, TSet(t)) ==> $Box($Unbox(bx) : Set Box) == bx && $Is($Unbox(bx) : Set Box, TSet(t))));
@@ -169,11 +186,13 @@ axiom(forall v : int  :: { $Is(v,TInt) }  $Is(v,TInt));
 axiom(forall v : int  :: { $Is(v,TNat) }  $Is(v,TNat) <==> v >= 0);
 axiom(forall v : real :: { $Is(v,TReal) } $Is(v,TReal));
 axiom(forall v : bool :: { $Is(v,TBool) } $Is(v,TBool));
+axiom(forall v : char :: { $Is(v,TChar) } $Is(v,TChar));
 
 axiom(forall h : Heap, v : int  :: { $IsAlloc(v,TInt,h) }  $IsAlloc(v,TInt,h));
 axiom(forall h : Heap, v : int  :: { $IsAlloc(v,TNat,h) }  $IsAlloc(v,TNat,h));
 axiom(forall h : Heap, v : real :: { $IsAlloc(v,TReal,h) } $IsAlloc(v,TReal,h));
 axiom(forall h : Heap, v : bool :: { $IsAlloc(v,TBool,h) } $IsAlloc(v,TBool,h));
+axiom(forall h : Heap, v : char :: { $IsAlloc(v,TChar,h) } $IsAlloc(v,TChar,h));
 
 axiom (forall v: Set Box, t0: Ty :: { $Is(v, TSet(t0)) }
   $Is(v, TSet(t0)) <==>
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