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, 4 insertions, 4 deletions

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index a5f02dc6..3359cff1 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -211,19 +211,19 @@ class AllocatedTests {
     assert allocated(6);

     assert allocated(6);

     assert allocated(null);

-    assert allocated(#Lindgren.HerrNilsson);

+    assert allocated(Lindgren.HerrNilsson);

 

     match (d) {

       case Pippi(n) => assert allocated(n);

       case Longstocking(q, dd) => assert allocated(q); assert allocated(dd);

       case HerrNilsson => assert old(allocated(d));

     }

-    var ls := #Lindgren.Longstocking([], d);

+    var ls := Lindgren.Longstocking([], d);

     assert allocated(ls);

     assert old(allocated(ls));

 

-    assert old(allocated(#Lindgren.Longstocking([r], d)));

-    assert old(allocated(#Lindgren.Longstocking([n], d)));  // error, because n was not allocated initially

+    assert old(allocated(Lindgren.Longstocking([r], d)));

+    assert old(allocated(Lindgren.Longstocking([n], d)));  // error, because n was not allocated initially

   }

 }