Dafny:

* started rewriting parsing of qualified identifiers in expressions
* annoyingly, had to introduce AST nodes for concrete syntax
* previous syntax for invoking datatype constructors: #List.Cons(h, t)
  new syntax:  List.Cons(h, t)
  or, if only one datatype has a constructor named Cons:  Cons(h, t)
* Removed type parameters for datatype constructors from the grammar
* Helped Test/VSI-Benchmarks/b4.dfy along with a couple of assertions (previously, its proving performance was highly varied)

1 files changed, 5 insertions, 5 deletions

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index 998b20bc..9a16a91a 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -19,14 +19,14 @@ class Node {
 

   method Init()

     modifies this;

-    ensures Repr(#List.Nil);

+    ensures Repr(Nil);

   {

     next := null;

   }

 

   method Add(d: int, L: List<int>) returns (r: Node)

     requires Repr(L);

-    ensures r != null && r.Repr(#List.Cons(d, L));

+    ensures r != null && r.Repr(Cons(d, L));

   {

     r := new Node;

     r.data := d;

@@ -49,14 +49,14 @@ class AnotherNode {
   }

 

   method Create() returns (n: AnotherNode)

-    ensures Repr(n, #List.Nil);

+    ensures Repr(n, Nil);

   {

     n := null;

   }

 

   method Add(n: AnotherNode, d: int, L: List<int>) returns (r: AnotherNode)

     requires Repr(n, L);

-    ensures Repr(r, #List.Cons(d, L));

+    ensures Repr(r, Cons(d, L));

   {

     r := new AnotherNode;

     r.data := d;

@@ -117,7 +117,7 @@ class NestedMatchExpr {
   method TestNesting0()

   {

     var x := 5;

-    var list := #List.Cons(3, #List.Cons(6, #List.Nil));

+    var list := Cons(3, Cons(6, Nil));

     assert Cadr(list, x) == 6;

     match (list) {

       case Nil => assert false;