From 9dbf2a6ce1e130f634c27da7bc300001e28aedaf Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Sat, 21 May 2011 18:15:17 -0700
Subject: 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)

---
 Test/dafny1/Induction.dfy    |   2 +-
 Test/dafny1/Rippling.dfy     | 208 +++++++++++++++++++++----------------------
 Test/dafny1/SchorrWaite.dfy  |   4 +-
 Test/dafny1/Substitution.dfy |  10 +--
 Test/dafny1/TreeDatatype.dfy |  16 ++--
 5 files changed, 120 insertions(+), 120 deletions(-)

(limited to 'Test/dafny1')

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>
-- 
cgit v1.2.3