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.

2 files changed, 36 insertions, 6 deletions

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;

@@ -70,6 +73,17 @@ 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++) {