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

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)));

   }

 }