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.

5 files changed, 68 insertions, 4 deletions

diff --git a/Test/cloudmake/CloudMake-CachedBuilds.dfy b/Test/cloudmake/CloudMake-CachedBuilds.dfy
index 11df8efe..9e1b511e 100644
--- a/Test/cloudmake/CloudMake-CachedBuilds.dfy
+++ b/Test/cloudmake/CloudMake-CachedBuilds.dfy
@@ -247,7 +247,6 @@ abstract module M0 {
   type Path(==)

   function Loc(cmd: string, deps: set<Path>, exp: string): Path

 

-  type string(==)

   type Artifact

   type Identifier

 

diff --git a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy
index 9463d8bc..815352f6 100644
--- a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy
+++ b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy
@@ -334,7 +334,6 @@ datatype Primitive = primCreatePath | primExec
 datatype Reason = rCompatibility | rValidity | rInconsistentCache

 

 datatype Path = OpaquePath(int) | TransparentPath(int)

-type string(==)

 type Artifact

 type Identifier

 

diff --git a/Test/cloudmake/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy
index a4f327ff..07cae317 100644
--- a/Test/cloudmake/CloudMake-ParallelBuilds.dfy
+++ b/Test/cloudmake/CloudMake-ParallelBuilds.dfy
@@ -153,7 +153,6 @@ abstract module M0 {
   type Path(==)

   function Loc(cmd: string, deps: set<Path>, exp: string): Path

 

-  type string(==)

   type Artifact

   type Identifier

 

@@ -778,7 +777,6 @@ module M3 refines M2 {
     a

   }

 

-  datatype string = stringCons(int)

   datatype Artifact = ArtifactCons(int)

   datatype Identifier = IdentifierCons(int)

 

diff --git a/Test/dafny0/Strings.dfy b/Test/dafny0/Strings.dfy
new file mode 100644
index 00000000..54764662
--- /dev/null
+++ b/Test/dafny0/Strings.dfy
@@ -0,0 +1,57 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%2.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+method Char(a: char, s: string, i: int) returns (b: char)

+{

+  var ch: char;

+  if a == ch {

+    b := ch;

+  } else if 0 <= i < |s| {

+    b := s[i];

+  }

+}

+

+// An attribute parameter that is a string literal is passed down

+// to Boogie as a string literal.

+method {:MyAttribute "hello", "hi" + "there", 57} AttrTest()

+{

+}

+

+method M(a: char, b: char) returns (s: string, t: seq<char>)

+  ensures |s| == 3 ==> t == [a, b, b];

+{

+  s := s + [a, b, b] + s;

+  t := s;

+  s := t[0..|s|];

+}

+

+method Main()

+{

+  var ch: char;

+  var s, t := M(ch, ch);

+  print "ch = ", ch, "\n";

+  print "The string is: " + s + "\n";

+  var x, y, z := Escapes();

+  print "Escape X: ", x, "\n";

+  print "Escape Y: ", y, "\n";

+  print "Escape Z: ", z, "\n";

+}

+

+method GimmieAChar(s: string) returns (ch: char)

+{

+  if s == "" {

+    ch := "tn"[1];

+    assert ch == "nt"[0];

+  } else {

+    var i :| 0 <= i < |s|;  // if guard guarantees such an i exists

+    ch := s[i];

+  }

+}

+

+method Escapes() returns (x: string, y: string, z: string)

+{

+  x := "I say \"hello\" \\ you say \'good bye'";

+  y := @"I say ""hello"" \ you say 'good bye'";

+  assert x == y;

+  z := "There needs to be \u0052\u0026\u0044\n\tYes, sir";

+}

diff --git a/Test/dafny0/Strings.dfy.expect b/Test/dafny0/Strings.dfy.expect
new file mode 100644
index 00000000..56bffd98
--- /dev/null
+++ b/Test/dafny0/Strings.dfy.expect
@@ -0,0 +1,11 @@
+

+Dafny program verifier finished with 12 verified, 0 errors

+Program compiled successfully

+Running...

+

+ch = D
+The string is: DDD
+Escape X: I say "hello" \ you say 'good bye'
+Escape Y: I say "hello" \ you say 'good bye'
+Escape Z: There needs to be R&D
+	Yes, sir