Dafny: permanently changed the syntax of "datatype" declarations to what previously was an alternative syntax

17 files changed, 116 insertions, 191 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index bf3ba197..5cfee29d 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -46,16 +46,9 @@ class MyClass<T, U> {
   }

 }

 

-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

+datatype List<T> = Nil | Cons(T, List<T>);

 

-datatype WildData {

-  Something;

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

-  More(List<int>);

-}

+datatype WildData = Something | JustAboutAnything(bool, myName: set<int>, int, WildData) | More(List<int>);

 

 class C {

   var w: WildData;

@@ -65,7 +58,7 @@ class C {
 Dafny program verifier finished with 0 verified, 0 errors

 

 -------------------- TypeTests.dfy --------------------

-TypeTests.dfy(95,9): Error: sorry, cannot instantiate collection type with a subrange type

+TypeTests.dfy(84,9): Error: sorry, cannot instantiate collection type with a subrange type

 TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)

 TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)

 TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)

@@ -73,21 +66,20 @@ TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, g
 TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)

 TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)

 TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)

-TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed

-TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-TypeTests.dfy(55,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-TypeTests.dfy(64,6): Error: Duplicate local-variable name: z

-TypeTests.dfy(66,6): Error: Duplicate local-variable name: x

-TypeTests.dfy(69,8): Error: Duplicate local-variable name: x

-TypeTests.dfy(72,6): Error: Duplicate local-variable name: y

-TypeTests.dfy(79,17): Error: member F in class C does not refer to a method

-TypeTests.dfy(80,17): Error: a method called as an initialization method must not have any result arguments

-TypeTests.dfy(89,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

-TypeTests.dfy(90,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

-TypeTests.dfy(96,9): Error: sorry, cannot instantiate type parameter with a subrange type

-TypeTests.dfy(97,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-TypeTests.dfy(98,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-22 resolution/type errors detected in TypeTests.dfy

+TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

+TypeTests.dfy(44,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+TypeTests.dfy(53,6): Error: Duplicate local-variable name: z

+TypeTests.dfy(55,6): Error: Duplicate local-variable name: x

+TypeTests.dfy(58,8): Error: Duplicate local-variable name: x

+TypeTests.dfy(61,6): Error: Duplicate local-variable name: y

+TypeTests.dfy(68,17): Error: member F in class C does not refer to a method

+TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments

+TypeTests.dfy(78,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

+TypeTests.dfy(79,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

+TypeTests.dfy(85,9): Error: sorry, cannot instantiate type parameter with a subrange type

+TypeTests.dfy(86,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+TypeTests.dfy(87,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+21 resolution/type errors detected in TypeTests.dfy

 

 -------------------- NatTypes.dfy --------------------

 NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative

@@ -114,16 +106,16 @@ NatTypes.dfy(54,16): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-NatTypes.dfy(71,16): Error: assertion violation

+NatTypes.dfy(68,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

-NatTypes.dfy(89,16): Error: value assigned to a nat must be non-negative

+NatTypes.dfy(86,16): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-NatTypes.dfy(104,45): Error: value assigned to a nat must be non-negative

+NatTypes.dfy(101,45): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon6_Else

     (0,0): anon7_Else

@@ -192,14 +184,14 @@ Execution trace:
     (0,0): anon6

     (0,0): anon14_Then

     (0,0): anon11

-SmallTests.dfy(272,24): Error BP5002: A precondition for this call might not hold.

-SmallTests.dfy(250,30): Related location: This is the precondition that might not hold.

+SmallTests.dfy(271,24): Error BP5002: A precondition for this call might not hold.

+SmallTests.dfy(249,30): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(267,19): anon3_Else

+    SmallTests.dfy(266,19): anon3_Else

     (0,0): anon2

-SmallTests.dfy(307,3): Error BP5003: A postcondition might not hold on this return path.

-SmallTests.dfy(301,11): Related location: This is the postcondition that might not hold.

+SmallTests.dfy(306,3): Error BP5003: A postcondition might not hold on this return path.

+SmallTests.dfy(300,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

     (0,0): anon18_Else

@@ -379,7 +371,7 @@ Execution trace:
 Dafny program verifier finished with 23 verified, 34 errors

 

 -------------------- FunctionSpecifications.dfy --------------------

-FunctionSpecifications.dfy(31,13): Error: possible violation of function postcondition

+FunctionSpecifications.dfy(28,13): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon10_Else

     (0,0): anon11_Else

@@ -387,13 +379,13 @@ Execution trace:
     (0,0): anon13_Else

     (0,0): anon7

     (0,0): anon9

-FunctionSpecifications.dfy(40,24): Error: possible violation of function postcondition

+FunctionSpecifications.dfy(37,24): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon12_Else

     (0,0): anon15_Else

     (0,0): anon16_Then

     (0,0): anon11

-FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause

+FunctionSpecifications.dfy(50,11): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon9_Then

@@ -557,10 +549,10 @@ Modules0.dfy(187,12): Error: match source expression 'l' has already been used a
 13 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------

-Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0

+Modules1.dfy(52,3): Error: decreases expression must be bounded below by 0

 Execution trace:

     (0,0): anon0

-Modules1.dfy(61,3): Error: failure to decrease termination measure

+Modules1.dfy(58,3): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

 

@@ -755,57 +747,57 @@ Execution trace:
 Dafny program verifier finished with 18 verified, 10 errors

 

 -------------------- Termination.dfy --------------------

-Termination.dfy(103,3): Error: cannot prove termination; try supplying a decreases clause for the loop

+Termination.dfy(100,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

     (0,0): anon0

-    Termination.dfy(103,3): anon7_LoopHead

+    Termination.dfy(100,3): anon7_LoopHead

     (0,0): anon7_LoopBody

-    Termination.dfy(103,3): anon8_Else

+    Termination.dfy(100,3): anon8_Else

     (0,0): anon3

-    Termination.dfy(103,3): anon9_Else

+    Termination.dfy(100,3): anon9_Else

     (0,0): anon5

-Termination.dfy(111,3): Error: cannot prove termination; try supplying a decreases clause for the loop

+Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

     (0,0): anon0

-    Termination.dfy(111,3): anon9_LoopHead

+    Termination.dfy(108,3): anon9_LoopHead

     (0,0): anon9_LoopBody

-    Termination.dfy(111,3): anon10_Else

+    Termination.dfy(108,3): anon10_Else

     (0,0): anon11_Then

     (0,0): anon5

-    Termination.dfy(111,3): anon12_Else

+    Termination.dfy(108,3): anon12_Else

     (0,0): anon7

-Termination.dfy(120,3): Error: decreases expression might not decrease

+Termination.dfy(117,3): Error: decreases expression might not decrease

 Execution trace:

     (0,0): anon0

-    Termination.dfy(120,3): anon9_LoopHead

+    Termination.dfy(117,3): anon9_LoopHead

     (0,0): anon9_LoopBody

-    Termination.dfy(120,3): anon10_Else

+    Termination.dfy(117,3): anon10_Else

     (0,0): anon11_Then

     (0,0): anon5

-    Termination.dfy(120,3): anon12_Else

+    Termination.dfy(117,3): anon12_Else

     (0,0): anon7

-Termination.dfy(121,17): Error: decreases expression must be bounded below by 0 at end of loop iteration

+Termination.dfy(118,17): Error: decreases expression must be bounded below by 0 at end of loop iteration

 Execution trace:

     (0,0): anon0

-    Termination.dfy(120,3): anon9_LoopHead

+    Termination.dfy(117,3): anon9_LoopHead

     (0,0): anon9_LoopBody

-    Termination.dfy(120,3): anon10_Else

+    Termination.dfy(117,3): anon10_Else

     (0,0): anon11_Then

     (0,0): anon5

-    Termination.dfy(120,3): anon12_Else

+    Termination.dfy(117,3): anon12_Else

     (0,0): anon7

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

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

 Execution trace:

     (0,0): anon6_Else

     (0,0): anon7_Else

     (0,0): anon8_Then

-Termination.dfy(289,3): Error: decreases expression might not decrease

+Termination.dfy(286,3): Error: decreases expression might not decrease

 Execution trace:

     (0,0): anon0

-    Termination.dfy(289,3): anon10_LoopHead

+    Termination.dfy(286,3): anon10_LoopHead

     (0,0): anon10_LoopBody

-    Termination.dfy(289,3): anon11_Else

-    Termination.dfy(289,3): anon12_Else

+    Termination.dfy(286,3): anon11_Else

+    Termination.dfy(286,3): anon12_Else

     (0,0): anon13_Else

     (0,0): anon8

 

@@ -818,20 +810,20 @@ Execution trace:
 DTypes.dfy(53,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

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

-DTypes.dfy(94,3): Related location: Related location

+DTypes.dfy(117,13): Error: assertion violation

+DTypes.dfy(89,30): Related location: Related location

 Execution trace:

     (0,0): anon0

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

-DTypes.dfy(93,3): Related location: Related location

+DTypes.dfy(123,13): Error: assertion violation

+DTypes.dfy(89,20): Related location: Related location

 Execution trace:

     (0,0): anon0

-DTypes.dfy(139,12): Error: assertion violation

-DTypes.dfy(134,6): Related location: Related location

-DTypes.dfy(93,3): Related location: Related location

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

+DTypes.dfy(128,6): Related location: Related location

+DTypes.dfy(89,20): Related location: Related location

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

@@ -883,7 +875,7 @@ Execution trace:
 Dafny program verifier finished with 33 verified, 5 errors

 

 -------------------- Datatypes.dfy --------------------

-Datatypes.dfy(82,20): Error: assertion violation

+Datatypes.dfy(79,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon20_Else

@@ -897,11 +889,11 @@ Execution trace:
 Dafny program verifier finished with 17 verified, 1 error

 

 -------------------- TypeAntecedents.dfy --------------------

-TypeAntecedents.dfy(34,13): Error: assertion violation

+TypeAntecedents.dfy(32,13): Error: assertion violation

 Execution trace:

     (0,0): anon0

-TypeAntecedents.dfy(60,1): Error BP5003: A postcondition might not hold on this return path.

-TypeAntecedents.dfy(59,15): Related location: This is the postcondition that might not hold.

+TypeAntecedents.dfy(55,1): Error BP5003: A postcondition might not hold on this return path.

+TypeAntecedents.dfy(54,15): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

     (0,0): anon15_Then

@@ -913,7 +905,7 @@ Execution trace:
     (0,0): anon20_Then

     (0,0): anon21_Then

     (0,0): anon14

-TypeAntecedents.dfy(68,16): Error: assertion violation

+TypeAntecedents.dfy(63,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon15_Else

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index b402c335..55d107c5 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -74,10 +74,7 @@ class Node { }
 class CP<T,U> {

 }

 

-datatype Data {

-  Lemon;

-  Kiwi(int);

-}

+datatype Data = Lemon | Kiwi(int);

 

 function G(d: Data): int

   requires d != Data.Lemon;

@@ -89,10 +86,7 @@ function G(d: Data): int
 

 // -------- some things about induction ---------------------------------

 

-datatype Tree<T> {

-  Leaf(T);

-  Branch(Tree<T>, Tree<T>);

-}

+datatype Tree<T> = Leaf(T) | Branch(Tree<T>, Tree<T>);

 

 class DatatypeInduction<T> {

   function LeafCount<G>(tree: Tree<G>): int

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index 9a16a91a..99e5e920 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -1,7 +1,4 @@
-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

+datatype List<T> = Nil | Cons(T, List<T>);

 

 class Node {

   var data: int;

diff --git a/Test/dafny0/FunctionSpecifications.dfy b/Test/dafny0/FunctionSpecifications.dfy
index 21ce5468..13171c47 100644
--- a/Test/dafny0/FunctionSpecifications.dfy
+++ b/Test/dafny0/FunctionSpecifications.dfy
@@ -6,10 +6,7 @@ function Fib(n: int): int
   Fib(n-2) + Fib(n-1)

 }

 

-datatype List {

-  Nil;

-  Cons(int, List);

-}

+datatype List = Nil | Cons(int, List);

 

 function Sum(a: List): int

   ensures 0 <= Sum(a);

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index 01e14585..c14aece6 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -138,7 +138,7 @@ method SpecialFunctions()
 

 // ---------------------- illegal match expressions ---------------

 

-datatype Tree { Nil; Cons(int, Tree, Tree); }

+datatype Tree = Nil | Cons(int, Tree, Tree);

 

 function NestedMatch0(tree: Tree): int

 {

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index ff84b84b..ad17c7d8 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -5,10 +5,7 @@ module A imports B {
       decreases 5, 4, 3;

     { z.G() }  // fine; this goes to a different module

   }

-  datatype Y {

-    Cons(int, Y);

-    Empty;

-  }

+  datatype Y = Cons(int, Y) | Empty;

 }

 

 class C {

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index e4d0cbe7..53d3bf03 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -44,7 +44,7 @@ method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
 

 function method FenEric<T>(t0: T, t1: T): T;

 

-datatype Pair<T> { Pr(T, T); }

+datatype Pair<T> = Pr(T, T);

 

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

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

@@ -55,10 +55,7 @@ method K(n: nat, i: int) {
   }

 }

 

-datatype List<T> {

-  Nil;

-  Cons(nat, T, List<T>);

-}

+datatype List<T> = Nil | Cons(nat, T, List<T>);

 

 method MatchIt(list: List<object>) returns (k: nat)

 {

diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy
index e1416094..ac3a4792 100644
--- a/Test/dafny0/Simple.dfy
+++ b/Test/dafny0/Simple.dfy
@@ -39,16 +39,12 @@ class MyClass<T,U> {
 

 // some datatype stuff:

 

-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

+datatype List<T> = Nil | Cons(T, List<T>);

 

-datatype WildData {

-  Something();

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

+datatype WildData =

+  Something() |

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

   More(List<int>);

-}

 

 class C {

   var w: WildData;

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index fcc764aa..b4dc6599 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -227,11 +227,10 @@ class AllocatedTests {
   }

 }

 

-datatype Lindgren {

-  Pippi(Node);

-  Longstocking(seq<object>, Lindgren);

+datatype Lindgren =

+  Pippi(Node) |

+  Longstocking(seq<object>, Lindgren) |

   HerrNilsson;

-}

 

 // --------------------------------------------------

 

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 155fbaef..d4d1dfcf 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -92,10 +92,7 @@ class Termination {
     ensures a == List.Cons(val, b);

 }

 

-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

+datatype List<T> = Nil | Cons(T, List<T>);

 

 method FailureToProveTermination0(N: int)

 {

diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index 38050b88..2bedd37d 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -1,10 +1,8 @@
 // -------- This is an example of what was once logically (although not trigger-ly) unsound ---

 

-datatype Wrapper<T> {

-  Wrap(T);

-}

-datatype Unit { It; }

-datatype Color { Yellow; Blue; }

+datatype Wrapper<T> = Wrap(T);

+datatype Unit = It;

+datatype Color = Yellow | Blue;

 

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

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

@@ -49,10 +47,7 @@ class MyClass {
   function H(): int { 5 }

 }

 

-datatype List {

-  Nil;

-  Cons(MyClass, List);

-}

+datatype List =  Nil | Cons(MyClass, List);

 

 method M(list: List, S: set<MyClass>) returns (ret: int)

   modifies S;

@@ -97,8 +92,6 @@ function NF(): MyClass;
 

 function TakesADatatype(a: List): int { 12 }

 

-datatype GenData<T> {

-  Pair(T, T);

-}

+datatype GenData<T> = Pair(T, T);

 

 function AlsoTakesADatatype<U>(p: GenData<U>): int { 17 }

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 21f0dda8..9df11a67 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -13,37 +13,26 @@ class C {
   }

 }

 

-datatype D {

-  A;

-}

-

-datatype Nothing {  // error: no grounding constructor

-}

+datatype D = A;

 

-datatype NeverendingList {  // error: no grounding constructor

-  Cons(int, NeverendingList);

-}

+datatype NeverendingList = Cons(int, NeverendingList);  // error: no grounding constructor

 

-datatype MutuallyRecursiveDataType<T> {

-  FromANumber(int);  // this is the base case

+datatype MutuallyRecursiveDataType<T> =

+  FromANumber(int) |  // this is the base case

   Else(TheCounterpart<T>, C);

-}

 

-datatype TheCounterpart<T> {

-  TreeLike(TheCounterpart<T>, TheCounterpart<T>);

+datatype TheCounterpart<T> =

+  TreeLike(TheCounterpart<T>, TheCounterpart<T>) |

   More(MutuallyRecursiveDataType<T>);

-}

 

 // these 'ReverseOrder_' order tests may be called white-box unit tests

-datatype ReverseOrder_MutuallyRecursiveDataType<T> {

-  FromANumber(int);  // this is the base case

+datatype ReverseOrder_MutuallyRecursiveDataType<T> =

+  FromANumber(int) |  // this is the base case

   Else(ReverseOrder_TheCounterpart<T>, C);

-}

 

-datatype ReverseOrder_TheCounterpart<T> {

-  TreeLike(ReverseOrder_TheCounterpart<T>, ReverseOrder_TheCounterpart<T>);

+datatype ReverseOrder_TheCounterpart<T> =

+  TreeLike(ReverseOrder_TheCounterpart<T>, ReverseOrder_TheCounterpart<T>) |

   More(ReverseOrder_MutuallyRecursiveDataType<T>);

-}

 

 // ---------------------

 

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 2c90769b..de5a3358 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -136,10 +136,7 @@ class IntegerInduction {
   }

 }

 

-datatype Tree<T> {

-  Leaf(T);

-  Branch(Tree<T>, Tree<T>);

-}

+datatype Tree<T> = Leaf(T) | Branch(Tree<T>, Tree<T>);

 

 class DatatypeInduction<T> {

   function LeafCount<T>(tree: Tree<T>): int

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 3a455077..fdce6dc7 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -1,16 +1,16 @@
 // Datatypes

 

-datatype Bool { False; True; }

+datatype Bool = False | True;

 

-datatype Nat { Zero; Suc(Nat); }

+datatype Nat = Zero | Suc(Nat);

 

-datatype List { Nil; Cons(Nat, List); }

+datatype List = Nil | Cons(Nat, List);

 

-datatype Pair { Pair(Nat, Nat); }

+datatype Pair = Pair(Nat, Nat);

 

-datatype PList { PNil; PCons(Pair, PList); }

+datatype PList = PNil | PCons(Pair, PList);

 

-datatype Tree { Leaf; Node(Tree, Nat, Tree); }

+datatype Tree = Leaf | Node(Tree, Nat, Tree);

 

 // Boolean functions

 

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 95cdab89..8da32b05 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -10,6 +10,8 @@ class Node {
   ghost var pathFromRoot: Path;

 }

 

+datatype Path = Empty | Extend(Path, Node);

+

 class Main {

   method RecursiveMark(root: Node, ghost S: set<Node>)

     requires root in S;

@@ -265,8 +267,3 @@ class Main {
     }

   }

 }

-

-datatype Path {

-  Empty;

-  Extend(Path, Node);

-}

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 11c8c878..ad39e3f2 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -1,13 +1,9 @@
-datatype List {

-  Nil;

-  Cons(Expr, List);

-}

+datatype List = Nil | Cons(Expr, List);

 

-datatype Expr {

-  Const(int);

-  Var(int);

+datatype Expr =

+  Const(int) |

+  Var(int) |

   Nary(int, List);

-}

 

 static function Subst(e: Expr, v: int, val: int): Expr

 {

@@ -48,11 +44,10 @@ static ghost method Lemma(l: List, v: int, val: int)
 

 // -------------------------------

 

-datatype Expression {

-  Const(int);

-  Var(int);

+datatype Expression =

+  Const(int) |

+  Var(int) |

   Nary(int, seq<Expression>);

-}

 

 static function Substitute(e: Expression, v: int, val: int): Expression

   decreases e;

diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy
index f363a023..a94283e6 100644
--- a/Test/dafny1/TreeDatatype.dfy
+++ b/Test/dafny1/TreeDatatype.dfy
@@ -1,13 +1,8 @@
 // ------------------ generic list, non-generic tree

 

-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

+datatype List<T> = Nil | Cons(T, List<T>);

 

-datatype Tree {

-  Node(int, List<Tree>);

-}

+datatype Tree = Node(int, List<Tree>);

 

 static function Inc(t: Tree): Tree

 {

@@ -24,9 +19,7 @@ static function ForestInc(forest: List<Tree>): List<Tree>
 

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

 

-datatype GTree<T> {

-  Node(T, List<GTree<T>>);

-}

+datatype GTree<T> = Node(T, List<GTree<T>>);

 

 static function GInc(t: GTree<int>): GTree<int>

 {

@@ -43,14 +36,9 @@ static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
 

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

 

-datatype TreeList {

-  Nil;

-  Cons(OneTree, TreeList);

-}

+datatype TreeList = Nil | Cons(OneTree, TreeList);

 

-datatype OneTree {

-  Node(int, TreeList);

-}

+datatype OneTree = Node(int, TreeList);

 

 static function XInc(t: OneTree): OneTree

 {