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)

16 files changed, 168 insertions, 165 deletions

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index ebaeab84..9f7e272e 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -88,7 +88,7 @@ class Map<Key,Value> {
     }

   }

 

-  method Remove(key: Key)

+  method Remove(key: Key)// returns (ghost h: int)

     requires Valid();

     modifies Repr;

     ensures Valid() && fresh(Repr - old(Repr));

@@ -111,6 +111,9 @@ class Map<Key,Value> {
     if (p != null) {

       Keys := Keys[..n] + Keys[n+1..];

       Values := Values[..n] + Values[n+1..];

+      assert Keys[n..] == old(Keys)[n+1..];

+      assert Values[n..] == old(Values)[n+1..];

+

       nodes := nodes[..n] + nodes[n+1..];

       if (prev == null) {

         head := head.next;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index e0874a66..d9d3a572 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -53,7 +53,7 @@ datatype List<T> {
 

 datatype WildData {

   Something;

-  JustAboutAnything<G, H>(G, myName: set<H>, int, WildData);

+  JustAboutAnything(bool, myName: set<int>, int, WildData);

   More(List<int>);

 }

 

@@ -620,7 +620,7 @@ Execution trace:
     (0,0): anon5

     Termination.dfy(119,3): anon12_Else

     (0,0): anon7

-Termination.dfy(248,36): Error: cannot prove termination; try supplying a decreases clause

+Termination.dfy(248,35): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon6_Else

     (0,0): anon7_Else

@@ -694,7 +694,7 @@ DTypes.dfy(134,6): Related location: Related location
 DTypes.dfy(93,3): Related location: Related location

 Execution trace:

     (0,0): anon0

-DTypes.dfy(160,13): Error: assertion violation

+DTypes.dfy(160,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy
index 35d939d3..2c9b3a35 100644
--- a/Test/dafny0/ControlStructures.dfy
+++ b/Test/dafny0/ControlStructures.dfy
@@ -9,7 +9,7 @@ method M0(d: D)
 }

 

 method M1(d: D)

-  requires d != #D.Blue;

+  requires d != D.Blue;

 {

   match (d) {  // error: missing case: Purple

     case Green =>

@@ -18,7 +18,7 @@ method M1(d: D)
 }

 

 method M2(d: D)

-  requires d != #D.Blue && d != #D.Purple;

+  requires d != D.Blue && d != D.Purple;

 {

   match (d) {

     case Green =>

@@ -27,9 +27,9 @@ method M2(d: D)
 }

 

 method M3(d: D)

-  requires d == #D.Green;

+  requires d == D.Green;

 {

-  if (d != #D.Green) {

+  if (d != D.Green) {

     match (d) {

       // nothing here

     }

@@ -37,9 +37,9 @@ method M3(d: D)
 }

 

 method M4(d: D)

-  requires d == #D.Green || d == #D.Red;

+  requires d == D.Green || d == D.Red;

 {

-  if (d != #D.Green) {

+  if (d != D.Green) {

     match (d) {  // error: missing case Red

       // nothing here

     }

@@ -56,7 +56,7 @@ function F0(d: D): int
 

 function F1(d: D, x: int): int

   requires x < 100;

-  requires d == #D.Red ==> x == 200;  // (an impossibility, given the first precondition, so d != Red)

+  requires d == D.Red ==> x == 200;  // (an impossibility, given the first precondition, so d != Red)

 {

   match (d)

   case Purple => 80

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index 2f59db73..b402c335 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -80,7 +80,7 @@ datatype Data {
 }

 

 function G(d: Data): int

-  requires d != #Data.Lemon;

+  requires d != Data.Lemon;

 {

   match d

   case Lemon => G(d)

@@ -144,19 +144,19 @@ class DatatypeInduction<T> {
   method IntegerInduction_Succeeds(a: array<int>)

     requires a != null;

     requires a.Length == 0 || a[0] == 0;

-    requires (forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1);

+    requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;

   {

     // The following assertion can be proved by induction:

-    assert (forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n);

+    assert forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n;

   }

 

   method IntegerInduction_Fails(a: array<int>)

     requires a != null;

     requires a.Length == 0 || a[0] == 0;

-    requires (forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1);

+    requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;

   {

     // ...but the induction heuristics don't recognize the situation as one where

     // applying induction would be profitable:

-    assert (forall n :: 0 <= n && n < a.Length ==> a[n] == n*n);  // error reported

+    assert forall n :: 0 <= n && n < a.Length ==> a[n] == n*n;  // error reported

   }

 }

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;

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 6b7ce9b9..161ac22f 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -47,7 +47,7 @@ function method FenEric<T>(t0: T, t1: T): T;
 datatype Pair<T> { Pr(T, T); }

 

 method K(n: nat, i: int) {

-  match (#Pair.Pr(n, i)) {

+  match (Pair.Pr(n, i)) {

     case Pr(k, l) =>

       assert k == n;  // fine: although the type of k is int, we know it's equal to n

       assert 0 <= k;

diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy
index d8c8d91d..930c4253 100644
--- a/Test/dafny0/Simple.dfy
+++ b/Test/dafny0/Simple.dfy
@@ -46,7 +46,7 @@ datatype List<T> {
 

 datatype WildData {

   Something();

-  JustAboutAnything<G,H>(G, myName: set<H>, int, WildData);

+  JustAboutAnything(bool, myName: set<int>, int, WildData);

   More(List<int>);

 }

 

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

   }

 }

 

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 226eadbe..5d411eb3 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -79,7 +79,7 @@ class Termination {
 

   method Q<T>(list: List<T>) {

     var l := list;

-    while (l != #List.Nil)

+    while (l != List.Nil)

       decreases l;

     {

       call x, l := Traverse(l);

@@ -87,8 +87,8 @@ class Termination {
   }

 

   method Traverse<T>(a: List<T>) returns (val: T, b: List<T>);

-    requires a != #List.Nil;

-    ensures a == #List.Cons(val, b);

+    requires a != List.Nil;

+    ensures a == List.Cons(val, b);

 }

 

 datatype List<T> {

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

   match a

   case Nil => b

-  case Cons(x, c) => #List.Cons(x, Zipper0(b, c))  // error: cannot prove termination

+  case Cons(x, c) => List.Cons(x, Zipper0(b, c))  // error: cannot prove termination

 }

 

 function Zipper1<T>(a: List<T>, b: List<T>, k: bool): List<T>

@@ -253,7 +253,7 @@ function Zipper1<T>(a: List<T>, b: List<T>, k: bool): List<T>
 {

   match a

   case Nil => b

-  case Cons(x, c) => #List.Cons(x, Zipper1(b, c, !k))

+  case Cons(x, c) => List.Cons(x, Zipper1(b, c, !k))

 }

 

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

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

   match a

   case Nil => b

-  case Cons(x, c) => #List.Cons(x, Zipper2(b, c))

+  case Cons(x, c) => List.Cons(x, Zipper2(b, c))

 }

 

 // -------------------------- test translation of while (*) -----------------

diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index 6fe86493..a932eccf 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -7,14 +7,14 @@ datatype Unit { It; }
 datatype Color { Yellow; Blue; }

 

 function F(a: Wrapper<Unit>): bool

-  ensures a == #Wrapper.Wrap(#Unit.It);

+  ensures a == Wrapper.Wrap(Unit.It);

 {

   match a

   case Wrap(u) => G(u)

 }

 

 function G(u: Unit): bool

-  ensures u == #Unit.It;

+  ensures u == Unit.It;

 {

   match u

   case It => true

@@ -23,19 +23,19 @@ function G(u: Unit): bool
 method BadLemma(c0: Color, c1: Color)

   ensures c0 == c1;

 {

-  var w0 := #Wrapper.Wrap(c0);

-  var w1 := #Wrapper.Wrap(c1);

+  var w0 := Wrapper.Wrap(c0);

+  var w1 := Wrapper.Wrap(c1);

 

   // Manually, add the following assertions in Boogie.  (These would

   // be ill-typed in Dafny.)

-  //     assert _default.F($Heap, this, w0#6);

-  //     assert _default.F($Heap, this, w1#7);

+  //     assert _default.F($Heap, this, w#06);

+  //     assert _default.F($Heap, this, w#17);

 

   assert w0 == w1;  // this would be bad news (it should be reported as an error)

 }

 

 method Main() {

-  call BadLemma(#Color.Yellow, #Color.Blue);

+  call BadLemma(Color.Yellow, Color.Blue);

   assert false;  // this shows how things can really go wrong if BadLemma verified successfully

 }

 

@@ -82,9 +82,9 @@ method M(list: List, S: set<MyClass>) returns (ret: int)
   // note, the definedness problem in the next line sits inside an unreachable branch

   assert (forall t: MyClass :: t != null ==> (if t.H() == 5 then true else 10 / 0 == 3));

 

-  assert TakesADatatype(#List.Nil) == 12;

-  assert TakesADatatype(#List.Cons(null, #List.Nil)) == 12;

-  assert AlsoTakesADatatype(#GenData.Pair(false, true)) == 17;

+  assert TakesADatatype(List.Nil) == 12;

+  assert TakesADatatype(List.Cons(null, List.Nil)) == 12;

+  assert AlsoTakesADatatype(GenData.Pair(false, true)) == 17;

 }

 

 method N() returns (k: MyClass)

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 792c8fac..7deeb0a1 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -1,9 +1,9 @@
 class C {

   function F(c: C, d: D): bool { true }

   method M(x: int) returns (y: int, c: C)

-    requires F(#D.A, this);  // 2 errors

+    requires F(D.A, this);  // 2 errors

     requires F(4, 5);  // 2 errors

-    requires F(this, #D.A);  // good

+    requires F(this, D.A);  // good

   { }

 

   method Caller()

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index d785eead..0e4c58e0 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -169,7 +169,7 @@ function FooD(n: nat, d: D): int
 {

   match d

   case Nothing =>

-    if n == 0 then 10 else FooD(n-1, #D.Something(d))

+    if n == 0 then 10 else FooD(n-1, D.Something(d))

   case Something(next) =>

     if n < 100 then n + 12 else FooD(n-13, next)

 }

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index d5b3862b..3a455077 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -17,13 +17,13 @@ datatype Tree { Leaf; Node(Tree, Nat, Tree); }
 function not(b: Bool): Bool

 {

   match b

-  case False => #Bool.True

-  case True => #Bool.False

+  case False => True

+  case True => False

 }

 

 function and(a: Bool, b: Bool): Bool

 {

-  if a == #Bool.True && b == #Bool.True then #Bool.True else #Bool.False

+  if a == True && b == True then True else False

 }

 

 // Natural number functions

@@ -32,13 +32,13 @@ function add(x: Nat, y: Nat): Nat
 {

   match x

   case Zero => y

-  case Suc(w) => #Nat.Suc(add(w, y))

+  case Suc(w) => Suc(add(w, y))

 }

 

 function minus(x: Nat, y: Nat): Nat

 {

   match x

-  case Zero => #Nat.Zero

+  case Zero => Zero

   case Suc(a) => match y

     case Zero => x

     case Suc(b) => minus(a, b)

@@ -48,38 +48,38 @@ function eq(x: Nat, y: Nat): Bool
 {

   match x

   case Zero => (match y

-    case Zero => #Bool.True

-    case Suc(b) => #Bool.False)

+    case Zero => True

+    case Suc(b) => False)

   case Suc(a) => (match y

-    case Zero => #Bool.False

+    case Zero => False

     case Suc(b) => eq(a, b))

 }

 

 function leq(x: Nat, y: Nat): Bool

 {

   match x

-  case Zero => #Bool.True

+  case Zero => True

   case Suc(a) => match y

-    case Zero => #Bool.False

+    case Zero => False

     case Suc(b) => leq(a, b)

 }

 

 function less(x: Nat, y: Nat): Bool

 {

   match y

-  case Zero => #Bool.False

+  case Zero => False

   case Suc(b) => match x

-    case Zero => #Bool.True

+    case Zero => True

     case Suc(a) => less(a, b)

 }

 

 function min(x: Nat, y: Nat): Nat

 {

   match x

-  case Zero => #Nat.Zero

+  case Zero => Zero

   case Suc(a) => match y

-    case Zero => #Nat.Zero

-    case Suc(b) => #Nat.Suc(min(a, b))

+    case Zero => Zero

+    case Suc(b) => Suc(min(a, b))

 }

 

 function max(x: Nat, y: Nat): Nat

@@ -88,7 +88,7 @@ function max(x: Nat, y: Nat): Nat
   case Zero => y

   case Suc(a) => match y

     case Zero => x

-    case Suc(b) => #Nat.Suc(max(a, b))

+    case Suc(b) => Suc(max(a, b))

 }

 

 // List functions

@@ -97,22 +97,22 @@ function concat(xs: List, ys: List): List
 {

   match xs

   case Nil => ys

-  case Cons(x,tail) => #List.Cons(x, concat(tail, ys))

+  case Cons(x,tail) => Cons(x, concat(tail, ys))

 }

 

 function mem(x: Nat, xs: List): Bool

 {

   match xs

-  case Nil => #Bool.False

-  case Cons(y, ys) => if x == y then #Bool.True else mem(x, ys)

+  case Nil => False

+  case Cons(y, ys) => if x == y then True else mem(x, ys)

 }

 

 function delete(n: Nat, xs: List): List

 {

   match xs

-  case Nil => #List.Nil

+  case Nil => Nil

   case Cons(y, ys) =>

-    if y == n then delete(n, ys) else #List.Cons(y, delete(n, ys))

+    if y == n then delete(n, ys) else Cons(y, delete(n, ys))

 }

 

 function drop(n: Nat, xs: List): List

@@ -120,38 +120,38 @@ function drop(n: Nat, xs: List): List
   match n

   case Zero => xs

   case Suc(m) => match xs

-    case Nil => #List.Nil

+    case Nil => Nil

     case Cons(x, tail) => drop(m, tail)

 }

 

 function take(n: Nat, xs: List): List

 {

   match n

-  case Zero => #List.Nil

+  case Zero => Nil

   case Suc(m) => match xs

-    case Nil => #List.Nil

-    case Cons(x, tail) => #List.Cons(x, take(m, tail))

+    case Nil => Nil

+    case Cons(x, tail) => Cons(x, take(m, tail))

 }

 

 function len(xs: List): Nat

 {

   match xs

-  case Nil => #Nat.Zero

-  case Cons(y, ys) => #Nat.Suc(len(ys))

+  case Nil => Zero

+  case Cons(y, ys) => Suc(len(ys))

 }

 

 function count(x: Nat, xs: List): Nat

 {

   match xs

-  case Nil => #Nat.Zero

+  case Nil => Zero

   case Cons(y, ys) =>

-    if x == y then #Nat.Suc(count(x, ys)) else count(x, ys)

+    if x == y then Suc(count(x, ys)) else count(x, ys)

 }

 

 function last(xs: List): Nat

 {

   match xs

-  case Nil => #Nat.Zero

+  case Nil => Zero

   case Cons(y, ys) => match ys

     case Nil => y

     case Cons(z, zs) => last(ys)

@@ -160,39 +160,39 @@ function last(xs: List): Nat
 function mapF(xs: List): List

 {

   match xs

-  case Nil => #List.Nil

-  case Cons(y, ys) => #List.Cons(HardcodedUninterpretedFunction(y), mapF(ys))

+  case Nil => Nil

+  case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys))

 }

 function HardcodedUninterpretedFunction(n: Nat): Nat;

 

 function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List

 {

   match xs

-  case Nil => #List.Nil

+  case Nil => Nil

   case Cons(y, ys) =>

-    if whilePredicate(hardcodedResultOfP, y) == #Bool.True

-    then #List.Cons(y, takeWhileAlways(hardcodedResultOfP, ys))

-    else #List.Nil

+    if whilePredicate(hardcodedResultOfP, y) == True

+    then Cons(y, takeWhileAlways(hardcodedResultOfP, ys))

+    else Nil

 }

 function whilePredicate(result: Bool, arg: Nat): Bool { result }

 

 function dropWhileAlways(hardcodedResultOfP: Bool, xs: List): List

 {

   match xs

-  case Nil => #List.Nil

+  case Nil => Nil

   case Cons(y, ys) =>

-    if whilePredicate(hardcodedResultOfP, y) == #Bool.True

+    if whilePredicate(hardcodedResultOfP, y) == True

     then dropWhileAlways(hardcodedResultOfP, ys)

-    else #List.Cons(y, ys)

+    else Cons(y, ys)

 }

 

 function filterP(xs: List): List

 {

   match xs

-  case Nil => #List.Nil

+  case Nil => Nil

   case Cons(y, ys) =>

-    if HardcodedUninterpretedPredicate(y) == #Bool.True

-    then #List.Cons(y, filterP(ys))

+    if HardcodedUninterpretedPredicate(y) == True

+    then Cons(y, filterP(ys))

     else filterP(ys)

 }

 function HardcodedUninterpretedPredicate(n: Nat): Bool;

@@ -200,37 +200,37 @@ function HardcodedUninterpretedPredicate(n: Nat): Bool;
 function insort(n: Nat, xs: List): List

 {

   match xs

-  case Nil => #List.Cons(n, #List.Nil)

+  case Nil => Cons(n, Nil)

   case Cons(y, ys) =>

-    if leq(n, y) == #Bool.True

-    then #List.Cons(n, #List.Cons(y, ys))

-    else #List.Cons(y, ins(n, ys))

+    if leq(n, y) == True

+    then Cons(n, Cons(y, ys))

+    else Cons(y, ins(n, ys))

 }

 

 function ins(n: Nat, xs: List): List

 {

   match xs

-  case Nil => #List.Cons(n, #List.Nil)

+  case Nil => Cons(n, Nil)

   case Cons(y, ys) =>

-    if less(n, y) == #Bool.True

-    then #List.Cons(n, #List.Cons(y, ys))

-    else #List.Cons(y, ins(n, ys))

+    if less(n, y) == True

+    then Cons(n, Cons(y, ys))

+    else Cons(y, ins(n, ys))

 }

 

 function ins1(n: Nat, xs: List): List

 {

   match xs

-  case Nil => #List.Cons(n, #List.Nil)

+  case Nil => Cons(n, Nil)

   case Cons(y, ys) =>

     if n == y

-    then #List.Cons(y, ys)

-    else #List.Cons(y, ins1(n, ys))

+    then Cons(y, ys)

+    else Cons(y, ins1(n, ys))

 }

 

 function sort(xs: List): List

 {

   match xs

-  case Nil => #List.Nil

+  case Nil => Nil

   case Cons(y, ys) => insort(y, sort(ys))

 }

 

@@ -239,17 +239,17 @@ function sort(xs: List): List
 function zip(a: List, b: List): PList

 {

   match a

-  case Nil => #PList.PNil

+  case Nil => PNil

   case Cons(x, xs) => match b

-    case Nil => #PList.PNil

-    case Cons(y, ys) => #PList.PCons(#Pair.Pair(x, y), zip(xs, ys))

+    case Nil => PNil

+    case Cons(y, ys) => PCons(Pair.Pair(x, y), zip(xs, ys))

 }

 

 function zipConcat(x: Nat, xs: List, more: List): PList

 {

   match more

-  case Nil => #PList.PNil

-  case Cons(y, ys) => #PList.PCons(#Pair.Pair(x, y), zip(xs, ys))

+  case Nil => PNil

+  case Cons(y, ys) => PCons(Pair.Pair(x, y), zip(xs, ys))

 }

 

 // Binary tree functions

@@ -257,15 +257,15 @@ function zipConcat(x: Nat, xs: List, more: List): PList
 function height(t: Tree): Nat

 {

   match t

-  case Leaf => #Nat.Zero

-  case Node(l, x, r) => #Nat.Suc(max(height(l), height(r)))

+  case Leaf => Zero

+  case Node(l, x, r) => Suc(max(height(l), height(r)))

 }

 

 function mirror(t: Tree): Tree

 {

   match t

-  case Leaf => #Tree.Leaf

-  case Node(l, x, r) => #Tree.Node(mirror(r), x, mirror(l))

+  case Leaf => Leaf

+  case Node(l, x, r) => Node(mirror(r), x, mirror(l))

 }

 

 // The theorems to be proved

@@ -281,24 +281,24 @@ ghost method P2()
 }

 

 ghost method P3()

-  ensures (forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == #Bool.True);

+  ensures (forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == True);

 {

 }

 

 ghost method P4()

-  ensures (forall n, xs :: add(#Nat.Suc(#Nat.Zero), count(n, xs)) == count(n, #List.Cons(n, xs)));

+  ensures (forall n, xs :: add(Suc(Zero), count(n, xs)) == count(n, Cons(n, xs)));

 {

 }

 

 ghost method P5()

   ensures (forall n, xs, x ::

-    add(#Nat.Suc(#Nat.Zero), count(n, xs)) == count(n, #List.Cons(x, xs))

+    add(Suc(Zero), count(n, xs)) == count(n, Cons(x, xs))

     ==> n == x);

 {

 }

 

 ghost method P6()

-  ensures (forall m, n :: minus(n, add(n, m)) == #Nat.Zero);

+  ensures (forall m, n :: minus(n, add(n, m)) == Zero);

 {

 }

 

@@ -318,12 +318,12 @@ ghost method P9()
 }

 

 ghost method P10()

-  ensures (forall m :: minus(m, m) == #Nat.Zero);

+  ensures (forall m :: minus(m, m) == Zero);

 {

 }

 

 ghost method P11()

-  ensures (forall xs :: drop(#Nat.Zero, xs) == xs);

+  ensures (forall xs :: drop(Zero, xs) == xs);

 {

 }

 

@@ -333,7 +333,7 @@ ghost method P12()
 }

 

 ghost method P13()

-  ensures (forall n, x, xs :: drop(#Nat.Suc(n), #List.Cons(x, xs)) == drop(n, xs));

+  ensures (forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs));

 {

 }

 

@@ -343,22 +343,22 @@ ghost method P14()
 }

 

 ghost method P15()

-  ensures (forall x, xs :: len(ins(x, xs)) == #Nat.Suc(len(xs)));

+  ensures (forall x, xs :: len(ins(x, xs)) == Suc(len(xs)));

 {

 }

 

 ghost method P16()

-  ensures (forall x, xs :: xs == #List.Nil ==> last(#List.Cons(x, xs)) == x);

+  ensures (forall x, xs :: xs == Nil ==> last(Cons(x, xs)) == x);

 {

 }

 

 ghost method P17()

-  ensures (forall n :: leq(n, #Nat.Zero) == #Bool.True <==> n == #Nat.Zero);

+  ensures (forall n :: leq(n, Zero) == True <==> n == Zero);

 {

 }

 

 ghost method P18()

-  ensures (forall i, m :: less(i, #Nat.Suc(add(i, m))) == #Bool.True);

+  ensures (forall i, m :: less(i, Suc(add(i, m))) == True);

 {

 }

 

@@ -371,15 +371,15 @@ ghost method P20()
   ensures (forall xs :: len(sort(xs)) == len(xs));

 {

   // proving this theorem requires an additional lemma:

-  assert (forall k, ks :: len(ins(k, ks)) == len(#List.Cons(k, ks)));

+  assert (forall k, ks :: len(ins(k, ks)) == len(Cons(k, ks)));

   // ...and one manually introduced case study:

   assert (forall ys ::

-           sort(ys) == #List.Nil ||

-           (exists z, zs :: sort(ys) == #List.Cons(z, zs)));

+           sort(ys) == Nil ||

+           (exists z, zs :: sort(ys) == Cons(z, zs)));

 }

 

 ghost method P21()

-  ensures (forall n, m :: leq(n, add(n, m)) == #Bool.True);

+  ensures (forall n, m :: leq(n, add(n, m)) == True);

 {

 }

 

@@ -394,37 +394,37 @@ ghost method P23()
 }

 

 ghost method P24()

-  ensures (forall a, b :: max(a, b) == a <==> leq(b, a) == #Bool.True);

+  ensures (forall a, b :: max(a, b) == a <==> leq(b, a) == True);

 {

 }

 

 ghost method P25()

-  ensures (forall a, b :: max(a, b) == b <==> leq(a, b) == #Bool.True);

+  ensures (forall a, b :: max(a, b) == b <==> leq(a, b) == True);

 {

 }

 

 ghost method P26()

-  ensures (forall x, xs, ys :: mem(x, xs) == #Bool.True ==> mem(x, concat(xs, ys)) == #Bool.True);

+  ensures (forall x, xs, ys :: mem(x, xs) == True ==> mem(x, concat(xs, ys)) == True);

 {

 }

 

 ghost method P27()

-  ensures (forall x, xs, ys :: mem(x, ys) == #Bool.True ==> mem(x, concat(xs, ys)) == #Bool.True);

+  ensures (forall x, xs, ys :: mem(x, ys) == True ==> mem(x, concat(xs, ys)) == True);

 {

 }

 

 ghost method P28()

-  ensures (forall x, xs :: mem(x, concat(xs, #List.Cons(x, #List.Nil))) == #Bool.True);

+  ensures (forall x, xs :: mem(x, concat(xs, Cons(x, Nil))) == True);

 {

 }

 

 ghost method P29()

-  ensures (forall x, xs :: mem(x, ins1(x, xs)) == #Bool.True);

+  ensures (forall x, xs :: mem(x, ins1(x, xs)) == True);

 {

 }

 

 ghost method P30()

-  ensures (forall x, xs :: mem(x, ins(x, xs)) == #Bool.True);

+  ensures (forall x, xs :: mem(x, ins(x, xs)) == True);

 {

 }

 

@@ -439,43 +439,43 @@ ghost method P32()
 }

 

 ghost method P33()

-  ensures (forall a, b :: min(a, b) == a <==> leq(a, b) == #Bool.True);

+  ensures (forall a, b :: min(a, b) == a <==> leq(a, b) == True);

 {

 }

 

 ghost method P34()

-  ensures (forall a, b :: min(a, b) == b <==> leq(b, a) == #Bool.True);

+  ensures (forall a, b :: min(a, b) == b <==> leq(b, a) == True);

 {

 }

 

 ghost method P35()

-  ensures (forall xs :: dropWhileAlways(#Bool.False, xs) == xs);

+  ensures (forall xs :: dropWhileAlways(False, xs) == xs);

 {

 }

 

 ghost method P36()

-  ensures (forall xs :: takeWhileAlways(#Bool.True, xs) == xs);

+  ensures (forall xs :: takeWhileAlways(True, xs) == xs);

 {

 }

 

 ghost method P37()

-  ensures (forall x, xs :: not(mem(x, delete(x, xs))) == #Bool.True);

+  ensures (forall x, xs :: not(mem(x, delete(x, xs))) == True);

 {

 }

 

 ghost method P38()

-  ensures (forall n, xs :: count(n, concat(xs, #List.Cons(n, #List.Nil))) == #Nat.Suc(count(n, xs)));

+  ensures (forall n, xs :: count(n, concat(xs, Cons(n, Nil))) == Suc(count(n, xs)));

 {

 }

 

 ghost method P39()

   ensures (forall n, x, xs ::

-            add(count(n, #List.Cons(x, #List.Nil)), count(n, xs)) == count(n, #List.Cons(x, xs)));

+            add(count(n, Cons(x, Nil)), count(n, xs)) == count(n, Cons(x, xs)));

 {

 }

 

 ghost method P40()

-  ensures (forall xs :: take(#Nat.Zero, xs) == #List.Nil);

+  ensures (forall xs :: take(Zero, xs) == Nil);

 {

 }

 

@@ -485,7 +485,7 @@ ghost method P41()
 }

 

 ghost method P42()

-  ensures (forall n, x, xs :: take(#Nat.Suc(n), #List.Cons(x, xs)) == #List.Cons(x, take(n, xs)));

+  ensures (forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs)));

 {

 }

 

@@ -496,19 +496,19 @@ ghost method P43(p: Bool)
 }

 

 ghost method P44()

-  ensures (forall x, xs, ys :: zip(#List.Cons(x, xs), ys) == zipConcat(x, xs, ys));

+  ensures (forall x, xs, ys :: zip(Cons(x, xs), ys) == zipConcat(x, xs, ys));

 {

 }

 

 ghost method P45()

   ensures (forall x, xs, y, ys ::

-            zip(#List.Cons(x, xs), #List.Cons(y, ys)) ==

-            #PList.PCons(#Pair.Pair(x, y), zip(xs, ys)));

+            zip(Cons(x, xs), Cons(y, ys)) ==

+            PCons(Pair.Pair(x, y), zip(xs, ys)));

 {

 }

 

 ghost method P46()

-  ensures (forall ys :: zip(#List.Nil, ys) == #PList.PNil);

+  ensures (forall ys :: zip(Nil, ys) == PNil);

 {

 }

 

@@ -530,27 +530,27 @@ ghost method P54()
 }

 

 ghost method P65()

-  ensures (forall i, m :: less(i, #Nat.Suc(add(m, i))) == #Bool.True);

+  ensures (forall i, m :: less(i, Suc(add(m, i))) == True);

 {

   if (*) {

     // the proof of this theorem follows from two lemmas:

-    assert (forall i, m :: less(i, #Nat.Suc(add(i, m))) == #Bool.True);

+    assert (forall i, m :: less(i, Suc(add(i, m))) == True);

     assert (forall m, n :: add(m, n) == add(n, m));

   } else {

     // a different way to prove it uses the following lemma:

-    assert (forall x,y :: add(x, #Nat.Suc(y)) == #Nat.Suc(add(x,y)));

+    assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));

   }

 }

 

 ghost method P67()

-  ensures (forall m, n :: leq(n, add(m, n)) == #Bool.True);

+  ensures (forall m, n :: leq(n, add(m, n)) == True);

 {

   if (*) {

     // the proof of this theorem follows from two lemmas:

-    assert (forall m, n :: leq(n, add(n, m)) == #Bool.True);

+    assert (forall m, n :: leq(n, add(n, m)) == True);

     assert (forall m, n :: add(m, n) == add(n, m));

   } else {

     // a different way to prove it uses the following lemma:

-    assert (forall x,y :: add(x, #Nat.Suc(y)) == #Nat.Suc(add(x,y)));

+    assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));

   }

 }

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 0d69b1b8..33442219 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -182,7 +182,7 @@ class Main {
   {

     var t := root;

     var p: Node := null;  // parent of t in original graph

-    ghost var path := #Path.Empty;

+    ghost var path := Path.Empty;

     t.marked := true;

     t.pathFromRoot := path;

     ghost var stackNodes := [];

@@ -256,7 +256,7 @@ class Main {
         t.children := t.children[..t.childrenVisited] + [p] + t.children[t.childrenVisited + 1..];

         p := t;

         stackNodes := stackNodes + [t];

-        path := #Path.Extend(path, t);

+        path := Path.Extend(path, t);

         t := newT;

         t.marked := true;

         t.pathFromRoot := path;

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 8d51bdd1..5cee5f6a 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -13,15 +13,15 @@ static function Subst(e: Expr, v: int, val: int): Expr
 {

   match e

   case Const(c) => e

-  case Var(x) => if x == v then #Expr.Const(val) else e

-  case Nary(op, args) => #Expr.Nary(op, SubstList(args, v, val))

+  case Var(x) => if x == v then Expr.Const(val) else e

+  case Nary(op, args) => Expr.Nary(op, SubstList(args, v, val))

 }

 

 static function SubstList(l: List, v: int, val: int): List

 {

   match l

   case Nil => l

-  case Cons(e, tail) => #List.Cons(Subst(e, v, val), SubstList(tail, v, val))

+  case Cons(e, tail) => Cons(Subst(e, v, val), SubstList(tail, v, val))

 }

 

 static ghost method Theorem(e: Expr, v: int, val: int)

@@ -59,8 +59,8 @@ static function Substitute(e: Expression, v: int, val: int): Expression
 {

   match e

   case Const(c) => e

-  case Var(x) => if x == v then #Expression.Const(val) else e

-  case Nary(op, args) => #Expression.Nary(op, SubstSeq(e, args, v, val))

+  case Var(x) => if x == v then Expression.Const(val) else e

+  case Nary(op, args) => Expression.Nary(op, SubstSeq(e, args, v, val))

 }

 

 static function SubstSeq(/*ghost*/ parent: Expression,

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>