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

diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy
index f576850e..f363a023 100644
--- a/Test/dafny1/TreeDatatype.dfy
+++ b/Test/dafny1/TreeDatatype.dfy
@@ -12,14 +12,14 @@ datatype Tree {
 static function Inc(t: Tree): Tree

 {

   match t

-  case Node(n, children) => #Tree.Node(n+1, ForestInc(children))

+  case Node(n, children) => Tree.Node(n+1, ForestInc(children))

 }

 

 static function ForestInc(forest: List<Tree>): List<Tree>

 {

   match forest

   case Nil => forest

-  case Cons(tree, tail) => #List.Cons(Inc(tree), ForestInc(tail))

+  case Cons(tree, tail) => List.Cons(Inc(tree), ForestInc(tail))

 }

 

 // ------------------ generic list, generic tree (but GInc defined only for GTree<int>

@@ -31,14 +31,14 @@ datatype GTree<T> {
 static function GInc(t: GTree<int>): GTree<int>

 {

   match t

-  case Node(n, children) => #GTree.Node(n+1, GForestInc(children))

+  case Node(n, children) => GTree.Node(n+1, GForestInc(children))

 }

 

 static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>

 {

   match forest

   case Nil => forest

-  case Cons(tree, tail) => #List.Cons(GInc(tree), GForestInc(tail))

+  case Cons(tree, tail) => List.Cons(GInc(tree), GForestInc(tail))

 }

 

 // ------------------ non-generic structures

@@ -55,14 +55,14 @@ datatype OneTree {
 static function XInc(t: OneTree): OneTree

 {

   match t

-  case Node(n, children) => #OneTree.Node(n+1, XForestInc(children))

+  case Node(n, children) => OneTree.Node(n+1, XForestInc(children))

 }

 

 static function XForestInc(forest: TreeList): TreeList

 {

   match forest

   case Nil => forest

-  case Cons(tree, tail) => #TreeList.Cons(XInc(tree), XForestInc(tail))

+  case Cons(tree, tail) => TreeList.Cons(XInc(tree), XForestInc(tail))

 }

 

 // ------------------ fun with recursive functions

@@ -77,7 +77,7 @@ function len<T>(l: List<T>): int
 function SingletonList<T>(h: T): List<T>

   ensures len(SingletonList(h)) == 1;

 {

-  #List.Cons(h, #List.Nil)

+  List.Cons(h, List.Nil)

 }

 

 function Append<T>(a: List<T>, b: List<T>): List<T>

@@ -85,7 +85,7 @@ function Append<T>(a: List<T>, b: List<T>): List<T>
 {

   match a

   case Nil => b

-  case Cons(h,t) => #List.Cons(h, Append(t, b))

+  case Cons(h,t) => List.Cons(h, Append(t, b))

 }

 

 function Rotate<T>(n: int, l: List<T>): List<T>