Stop pretty-print from emitting deprecated semi-colons.

61 files changed, 235 insertions, 237 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 1280e3fd..d1391277 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -550,9 +550,8 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
     [ SYNC ";"

         // This semi-colon used to be required, but it seems silly to have it.

         // To stage the transition toward not having it at all, let's make it optional for now.  Then,

-        // in a next big version of Dafny, including the following warning message:

-        //     (. errors.Warning(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)

-        // And in a version after that, don't allow the semi-colon at all.

+        // in the next big version of Dafny, don't allow the semi-colon at all.

+        (. errors.Warning(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)

     ]

     (. if (submodule == null) {

          idPath = new List<IToken>();

@@ -678,9 +677,8 @@ DatatypeDecl<ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt>
   [ SYNC ";"

       // This semi-colon used to be required, but it seems silly to have it.

       // To stage the transition toward not having it at all, let's make it optional for now.  Then,

-      // in a next big version of Dafny, including the following warning message:

-      //     (. errors.Warning(t, "the semi-colon that used to terminate a (co)datatype declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)

-      // And in a version after that, don't allow the semi-colon at all.

+      // in the next big version of Dafny, don't allow the semi-colon at all.

+      (. errors.Warning(t, "the semi-colon that used to terminate a (co)datatype declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)

   ]

   (. if (co) {

        dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);

@@ -761,9 +759,8 @@ OtherTypeDecl<ModuleDefinition module, out TopLevelDecl td>
   [ SYNC ";"

       // This semi-colon used to be required, but it seems silly to have it.

       // To stage the transition toward not having it at all, let's make it optional for now.  Then,

-      // in a next big version of Dafny, including the following warning message:

-      //     (. errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)

-      // And in a version after that, don't allow the semi-colon at all.

+      // in the next big version of Dafny, don't allow the semi-colon at all.

+      (. errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)

   ]

   .

 GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 295160c2..d67def8c 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -673,6 +673,7 @@ bool IsType(ref IToken pt) {
 			if (la.kind == 26) {

 				while (!(la.kind == 0 || la.kind == 26)) {SynErr(135); Get();}

 				Get();

+				errors.Warning(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); 

 			}

 			if (submodule == null) {

 			 idPath = new List<IToken>();

@@ -759,6 +760,7 @@ bool IsType(ref IToken pt) {
 		if (la.kind == 26) {

 			while (!(la.kind == 0 || la.kind == 26)) {SynErr(140); Get();}

 			Get();

+			errors.Warning(t, "the semi-colon that used to terminate a (co)datatype declaration has been deprecated; in the new syntax, just leave off the semi-colon"); 

 		}

 		if (co) {

 		 dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);

@@ -837,6 +839,7 @@ bool IsType(ref IToken pt) {
 		if (la.kind == 26) {

 			while (!(la.kind == 0 || la.kind == 26)) {SynErr(143); Get();}

 			Get();

+			errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); 

 		}

 	}

 

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index bf483528..5ae5643b 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -457,7 +457,6 @@ namespace Microsoft.Dafny {
       PrintAttributes(field.Attributes);

       wr.Write(" {0}: ", field.Name);

       PrintType(field.Type);

-      wr.Write(";");

       if (field.IsUserMutable) {

         // nothing more to say

       } else if (field.IsMutable) {

@@ -619,7 +618,7 @@ namespace Microsoft.Dafny {
         Indent(indent);

         wr.Write("{0} ", kind);

         PrintExpression(e, true);

-        wr.WriteLine(";");

+        wr.WriteLine();

       }

     }

 

@@ -636,9 +635,9 @@ namespace Microsoft.Dafny {
         wr.Write(" ");

         PrintExpressionList(decs.Expressions, true);

         if (newLine) {

-          wr.WriteLine(";");

+          wr.WriteLine();

         } else {

-          wr.Write(";");

+          wr.Write(" ");

         }

       }

     }

@@ -655,9 +654,9 @@ namespace Microsoft.Dafny {
         wr.Write(" ");

         PrintFrameExpressionList(ee);

         if (newLine) {

-          wr.WriteLine(";");

+          wr.WriteLine();

         } else {

-          wr.Write(";");

+          wr.Write(" ");

         }

       }

     }

@@ -679,11 +678,10 @@ namespace Microsoft.Dafny {
 

         wr.Write(" ");

         PrintExpression(e.E, true);

-

         if (newLine) {

-          wr.WriteLine(";");

+          wr.WriteLine();

         } else {

-          wr.Write(";");

+          wr.Write(" ");

         }

       }

     }

diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy
index 99e8298e..acfe6b8d 100644
--- a/Test/dafny0/AutoReq.dfy
+++ b/Test/dafny0/AutoReq.dfy
@@ -225,7 +225,7 @@ module {:autoReq} M1 {
 }

 

 module Datatypes {

-  datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);

+  datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType)

 

   function f1(t:TheType):bool

     requires t.TheType_builder? && t.x > 3;

@@ -255,7 +255,7 @@ module Datatypes {
 }

 

 module Matches {

-  datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);

+  datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType)

 

   function f1(x:int):bool

     requires x > 3;

diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy
index 532ac746..0becb24d 100644
--- a/Test/dafny0/CoPrefix.dfy
+++ b/Test/dafny0/CoPrefix.dfy
@@ -3,7 +3,7 @@
 

 // ----- Stream

 

-codatatype Stream = Nil | Cons(head: int, tail: Stream);

+codatatype Stream = Nil | Cons(head: int, tail: Stream)

 

 function append(M: Stream, N: Stream): Stream

 {

@@ -49,7 +49,7 @@ ghost method Theorem0_Manual()
   }

 }

 

-datatype Natural = Zero | Succ(Natural);

+datatype Natural = Zero | Succ(Natural)

 

 colemma {:induction false} Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)

   ensures atmost(zeros(), ones());

@@ -89,7 +89,7 @@ colemma {:induction false} Theorem1()
   Theorem1();

 }

 

-codatatype IList = ICons(head: int, tail: IList);

+codatatype IList = ICons(head: int, tail: IList)

 

 function UpIList(n: int): IList

 {

@@ -114,7 +114,7 @@ colemma {:induction false} Theorem2_NotAProof(n: int)
 {  // error: this is not a proof (without automatic induction)

 }

 

-codatatype TList<T> = TCons(head: T, tail: TList);

+codatatype TList<T> = TCons(head: T, tail: TList)

 

 function Next<T>(t: T): T

 

diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
index dfa99dd6..ff4c3dbf 100644
--- a/Test/dafny0/CoResolution.dfy
+++ b/Test/dafny0/CoResolution.dfy
@@ -34,7 +34,7 @@ module TestModule {
 }

 

 module GhostCheck0 {

-  codatatype Stream<G> = Cons(head: G, tail: Stream);

+  codatatype Stream<G> = Cons(head: G, tail: Stream)

   method UseStream0(s: Stream)

   {

     var x := 3;

@@ -44,7 +44,7 @@ module GhostCheck0 {
   }

 }

 module GhostCheck1 {

-  codatatype Stream<G> = Cons(head: G, tail: Stream);

+  codatatype Stream<G> = Cons(head: G, tail: Stream)

   method UseStream1(s: Stream)

   {

     var x := 3;

@@ -54,7 +54,7 @@ module GhostCheck1 {
   }

 }

 module GhostCheck2 {

-  codatatype Stream<G> = Cons(head: G, tail: Stream);

+  codatatype Stream<G> = Cons(head: G, tail: Stream)

   ghost method UseStreamGhost(s: Stream)

   {

     var x := 3;

diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
index 30ee287b..99b263a5 100644
--- a/Test/dafny0/Coinductive.dfy
+++ b/Test/dafny0/Coinductive.dfy
@@ -7,61 +7,61 @@ module TestInductiveDatatypes
 {

   // The following types test for cycles that go via instantiated type arguments

 

-  datatype Record<T> = Ctor(T);

+  datatype Record<T> = Ctor(T)

 

-  datatype RecInt = Ctor(Record<int>);  // this is fine

-  datatype Rec_Forever = Ctor(Record<Rec_Forever>);  // error

-  datatype Rec_Stops = Cons(Record<Rec_Stops>, Rec_Stops) | Nil;  // this is okay

+  datatype RecInt = Ctor(Record<int>)  // this is fine

+  datatype Rec_Forever = Ctor(Record<Rec_Forever>)  // error

+  datatype Rec_Stops = Cons(Record<Rec_Stops>, Rec_Stops) | Nil  // this is okay

 

-  datatype D<T> = Ctor(E<D<T>>);  // error: illegal cycle

-  datatype E<T> = Ctor(T);

+  datatype D<T> = Ctor(E<D<T>>)  // error: illegal cycle

+  datatype E<T> = Ctor(T)

 

   // the following is okay

-  datatype MD<T> = Ctor(ME<T>);

-  datatype ME<T> = Ctor(T);

+  datatype MD<T> = Ctor(ME<T>)

+  datatype ME<T> = Ctor(T)

   method M()

   {

     var d: MD<MD<int>>;

   }

 

-  datatype A = Ctor(B);  // superficially looks like a cycle, but can still be constructed

-  datatype B = Ctor(List<A>);

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

+  datatype A = Ctor(B)  // superficially looks like a cycle, but can still be constructed

+  datatype B = Ctor(List<A>)

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

 }

 

 module MoreInductive {

-  datatype Tree<G> = Node(G, List<Tree<G>>);

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

+  datatype Tree<G> = Node(G, List<Tree<G>>)

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

 

-  datatype M = All(List<M>);

-  datatype H<'a> = HH('a, Tree<'a>);

-  datatype K<'a> = KK('a, Tree<K<'a>>);  // error

-  datatype L<'a> = LL('a, Tree<List<L<'a>>>);

+  datatype M = All(List<M>)

+  datatype H<'a> = HH('a, Tree<'a>)

+  datatype K<'a> = KK('a, Tree<K<'a>>)  // error

+  datatype L<'a> = LL('a, Tree<List<L<'a>>>)

 }

 

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

 

 module TestCoinductiveDatatypes

 {

-  codatatype InfList<T> = Done | Continue(T, InfList);

+  codatatype InfList<T> = Done | Continue(T, InfList)

 

-  codatatype Stream<T> = More(T, Stream<T>);

+  codatatype Stream<T> = More(T, Stream<T>)

 

-  codatatype BinaryTreeForever<T> = BNode(val: T, left: BinaryTreeForever<T>, right: BinaryTreeForever<T>);

+  codatatype BinaryTreeForever<T> = BNode(val: T, left: BinaryTreeForever<T>, right: BinaryTreeForever<T>)

 

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

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

 

-  codatatype BestBushEver<T> = Node(value: T, branches: List<BestBushEver<T>>);

+  codatatype BestBushEver<T> = Node(value: T, branches: List<BestBushEver<T>>)

 

-  codatatype LazyRecord<T> = Lazy(contents: T);

+  codatatype LazyRecord<T> = Lazy(contents: T)

   class MyClass<T> { }

-  datatype GenericDt<T> = Blue | Green(T);

-  datatype GenericRecord<T> = Rec(T);

+  datatype GenericDt<T> = Blue | Green(T)

+  datatype GenericRecord<T> = Rec(T)

 

-  datatype FiniteEnough_Class = Ctor(MyClass<FiniteEnough_Class>);

-  datatype FiniteEnough_Co = Ctor(LazyRecord<FiniteEnough_Co>);

-  datatype FiniteEnough_Dt = Ctor(GenericDt<FiniteEnough_Dt>);  // fine

-  datatype NotFiniteEnough_Dt = Ctor(GenericRecord<NotFiniteEnough_Dt>);  // error

+  datatype FiniteEnough_Class = Ctor(MyClass<FiniteEnough_Class>)

+  datatype FiniteEnough_Co = Ctor(LazyRecord<FiniteEnough_Co>)

+  datatype FiniteEnough_Dt = Ctor(GenericDt<FiniteEnough_Dt>)  // fine

+  datatype NotFiniteEnough_Dt = Ctor(GenericRecord<NotFiniteEnough_Dt>)  // error

 

 }

 

@@ -69,7 +69,7 @@ module TestCoinductiveDatatypes
 

 module CoPredicateResolutionErrors {

 

-  codatatype Stream<T> = StreamCons(head: T, tail: Stream);

+  codatatype Stream<T> = StreamCons(head: T, tail: Stream)

 

   function Upward(n: int): Stream<int>

   {

@@ -158,7 +158,7 @@ module CoPredicateResolutionErrors {
 // --------------------------------------------------

 

 module UnfruitfulCoLemmaConclusions {

-  codatatype Stream<T> = Cons(head: T, tail: Stream);

+  codatatype Stream<T> = Cons(head: T, tail: Stream)

 

   copredicate Positive(s: Stream<int>)

   {

diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index 8ce16419..d990ae51 100644
--- a/Test/dafny0/CoinductiveProofs.dfy
+++ b/Test/dafny0/CoinductiveProofs.dfy
@@ -1,7 +1,7 @@
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

-codatatype Stream<T> = Cons(head: T, tail: Stream);

+codatatype Stream<T> = Cons(head: T, tail: Stream)

 

 function Upward(n: int): Stream<int>

 {

@@ -159,7 +159,7 @@ colemma {:induction false} BadEquality1(n: int)
 

 // test that match statements/expressions get the correct assumption (which wasn't always the case)

 

-codatatype IList<T> = INil | ICons(head: T, tail: IList<T>);

+codatatype IList<T> = INil | ICons(head: T, tail: IList<T>)

 

 ghost method M(s: IList)

 {

diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index d515e559..a2b96996 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -5,7 +5,7 @@
 // program snippets that are tricky to compile or whose compilation once was buggy.

 

 module OnceBuggy {

-  datatype MyDt<T> = Nil | Cons(T, MyDt<T>);

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

 

   method M<U>(x: MyDt<int>)

   {

@@ -20,14 +20,14 @@ module OnceBuggy {
 // --------------------------------------------------

 

 module CoRecursion {

-  codatatype Stream<T> = More(head: T, rest: Stream);

+  codatatype Stream<T> = More(head: T, rest: Stream)

 

   function method AscendingChain(n: int): Stream<int>

   {

     More(n, AscendingChain(n+1))

   }

 

-  datatype List<T> = Nil | Cons(car: T, cdr: List);

+  datatype List<T> = Nil | Cons(car: T, cdr: List)

 

   function method Prefix(n: nat, s: Stream): List

   {

@@ -76,9 +76,9 @@ module T refines S {
   }

 }

 module A {

-   import X as S default T;

-   import Y as S default T;

-   import Z = T;

+   import X as S default T

+   import Y as S default T

+   import Z = T

    method run() {

      var x := new X.C;

      x.m();

@@ -95,7 +95,7 @@ method NotMain() {
 

 

 abstract module S1 {

-  import B as S default T;

+  import B as S default T

   method do()

 }

 

@@ -105,7 +105,7 @@ module T1 refines S1 {
   }

 }

 module A1 {

-   import X as S1 default T1;

+   import X as S1 default T1

    method run() {

      X.do();

      var x := new X.B.C;

diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy
index 70a7820e..d0436815 100644
--- a/Test/dafny0/Comprehensions.dfy
+++ b/Test/dafny0/Comprehensions.dfy
@@ -14,7 +14,7 @@ method M()
 

 function method Id(x: int): int { x }  // for triggering

 

-datatype D = A | B;

+datatype D = A | B

 // The following mainly test that set comprehensions can be compiled, but one would

 // have to run the resulting program to check that the compiler is doing the right thing.

 method Main()

diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy
index 83b2a571..a3ea666f 100644
--- a/Test/dafny0/Computations.dfy
+++ b/Test/dafny0/Computations.dfy
@@ -19,7 +19,7 @@ ghost method compute_fact6_plus()
 {

 }

 

-datatype intlist = IntNil | IntCons(head: int, tail: intlist);

+datatype intlist = IntNil | IntCons(head: int, tail: intlist)

 function intsize(l: intlist): nat

 {

   if (l.IntNil?) then 0 else 1+intsize(l.tail)

@@ -56,7 +56,7 @@ ghost method compute_cintsize4()
   ensures cintsize(IntCons(1, IntCons(2, IntCons(3, IntCons(4, IntNil))))) == 4;

 {

 }

-datatype list<A> = Nil | Cons(head: A, tail: list);

+datatype list<A> = Nil | Cons(head: A, tail: list)

 function size(l: list): nat

 {

   if (l.Nil?) then 0 else 1+size(l.tail)

@@ -78,7 +78,7 @@ ghost method compute_appsize()
 {

 }

 

-datatype exp = Plus(e1: exp, e2: exp) | Num(n: int) | Var(x: int);

+datatype exp = Plus(e1: exp, e2: exp) | Num(n: int) | Var(x: int)

 function interp(env: map<int,int>, e: exp): int

   decreases e;

 {

diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy
index 8300c160..8d027acb 100644
--- a/Test/dafny0/ControlStructures.dfy
+++ b/Test/dafny0/ControlStructures.dfy
@@ -1,7 +1,7 @@
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

-datatype D = Green | Blue | Red | Purple;

+datatype D = Green | Blue | Red | Purple

 

 method M0(d: D)

 {

diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy
index cfdc2897..28714611 100644
--- a/Test/dafny0/Corecursion.dfy
+++ b/Test/dafny0/Corecursion.dfy
@@ -4,7 +4,7 @@
 // --------------------------------------------------

 

 module CoRecursion {

-  codatatype Stream<T> = More(head: T, rest: Stream);

+  codatatype Stream<T> = More(head: T, rest: Stream)

 

   function AscendingChain(n: int): Stream<int>

   {

@@ -23,7 +23,7 @@ module CoRecursion {
     More(n, AscendingChainAndPostcondition(n+1))  // error: cannot prove termination

   }

 

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

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

 

   function Prefix(n: nat, s: Stream): List

   {

@@ -35,7 +35,7 @@ module CoRecursion {
 // --------------------------------------------------

 

 module CoRecursionNotUsed {

-  codatatype Stream<T> = More(T, Stream);

+  codatatype Stream<T> = More(T, Stream)

 

   function F(s: Stream, n: nat): Stream

     decreases n, true;

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index 70f9bbd0..c8c893a0 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -78,7 +78,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;

@@ -90,7 +90,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/DatatypeUpdate.dfy b/Test/dafny0/DatatypeUpdate.dfy
index f39aa4ce..76cce5ce 100644
--- a/Test/dafny0/DatatypeUpdate.dfy
+++ b/Test/dafny0/DatatypeUpdate.dfy
@@ -3,7 +3,7 @@
 

 datatype MyDataType = MyConstructor(myint:int, mybool:bool) 

                     | MyOtherConstructor(otherbool:bool) 

-                    | MyNumericConstructor(42:int);

+                    | MyNumericConstructor(42:int)

 

 method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:MyDataType, jkl:MyDataType)

     requires foo.MyConstructor?;

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index 488f6056..25adaa91 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -1,7 +1,7 @@
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

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

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

 

 class Node {

   var data: int;

@@ -140,7 +140,7 @@ class NestedMatchExpr {
 

 // ------------------- datatype destructors ---------------------------------------

 

-datatype XList = XNil | XCons(Car: int, Cdr: XList);

+datatype XList = XNil | XCons(Car: int, Cdr: XList)

 

 method Destructors0(d: XList) {

   Lemma_AllCases(d);

@@ -208,8 +208,8 @@ method MatchingDestructor(d: XList) returns (r: XList)
   r := XCons(5, XNil);

 }

 

-datatype Triple = T(a: int, b: int, c: int);  // just one constructor

-datatype TripleAndMore = T'(a: int, b: int, c: int) | NotATriple;

+datatype Triple = T(a: int, b: int, c: int)  // just one constructor

+datatype TripleAndMore = T'(a: int, b: int, c: int) | NotATriple

 

 method Rotate0(t: Triple) returns (u: Triple)

 {

@@ -249,7 +249,7 @@ function FwdBugFunction(f: Fwd): bool
   // There was once a bug in Dafny, where this had caused an ill-defined Boogie program.

 }

 

-datatype Fwd = FwdNil | FwdCons(k: int, w: Fwd);

+datatype Fwd = FwdNil | FwdCons(k: int, w: Fwd)

 

 method TestAllCases(f: Fwd)

 {

diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy
index c04ee2c1..b2812759 100644
--- a/Test/dafny0/EqualityTypes.dfy
+++ b/Test/dafny0/EqualityTypes.dfy
@@ -2,8 +2,8 @@
 // RUN: %diff "%s.expect" "%t"

 

 module A {

-  datatype Explicit<T(==)> = Nil | Cons(set<T>, Explicit<T>);

-  datatype Inferred<T> = Nil | Cons(set<T>, Inferred<T>);

+  datatype Explicit<T(==)> = Nil | Cons(set<T>, Explicit<T>)

+  datatype Inferred<T> = Nil | Cons(set<T>, Inferred<T>)

 

   class C {

     method M<T>(x: Explicit<T>)

@@ -21,42 +21,42 @@ module B refines A {
 // ----------------------------

 

 module C {

-  type X(==);

-  type Y(==);

+  type X(==)

+  type Y(==)

 }

 

 module D refines C {

   class X { }

-  datatype Y = Red | Green | Blue;

+  datatype Y = Red | Green | Blue

 }

 

 module E refines C {

-  codatatype X = Next(int, X);  // error: X requires equality and codatatypes don't got it

-  datatype Y = Nil | Something(Z) | More(Y, Y);  // error: Y does not support equality

-  codatatype Z = Red | Green(X) | Blue;

+  codatatype X = Next(int, X)  // error: X requires equality and codatatypes don't got it

+  datatype Y = Nil | Something(Z) | More(Y, Y)  // error: Y does not support equality

+  codatatype Z = Red | Green(X) | Blue

 }

 

 module F refines C {

-  datatype X<T> = Nil | Cons(T, X<T>);  // error: not allowed to add a type parameter to type X

+  datatype X<T> = Nil | Cons(T, X<T>)  // error: not allowed to add a type parameter to type X

   class Y<T> { }  // error: not allowed to add a type parameter to type Y

 }

 

 module G refines C {

-  datatype X = Nil | Next(Z, X);  // error: X does not support equality

-  datatype Y = Nil | Something(Z) | More(Y, Y);  // error: Y does not support equality

-  codatatype Z = Red | Green | Blue;

+  datatype X = Nil | Next(Z, X)  // error: X does not support equality

+  datatype Y = Nil | Something(Z) | More(Y, Y)  // error: Y does not support equality

+  codatatype Z = Red | Green | Blue

 }

 

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

 

 module H {

-  datatype Dt<T> = Nil | Cons(T, Dt);

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

 

-  datatype BulkyList<T> = Nothing | Wrapper(T, BulkyListAux);

-  datatype BulkyListAux<T> = Kons(set<T>, BulkyListAuxAux);

-  datatype BulkyListAuxAux<T> = GoBack(BulkyList);

+  datatype BulkyList<T> = Nothing | Wrapper(T, BulkyListAux)

+  datatype BulkyListAux<T> = Kons(set<T>, BulkyListAuxAux)

+  datatype BulkyListAuxAux<T> = GoBack(BulkyList)

 

-  codatatype Stream<T> = Next(head: T, tail: Stream<T>);

+  codatatype Stream<T> = Next(head: T, tail: Stream<T>)

 

   method M<T(==)>(x: T)

   { }

diff --git a/Test/dafny0/FunctionSpecifications.dfy b/Test/dafny0/FunctionSpecifications.dfy
index 1b7c8bfc..d5040b11 100644
--- a/Test/dafny0/FunctionSpecifications.dfy
+++ b/Test/dafny0/FunctionSpecifications.dfy
@@ -9,7 +9,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/MatchBraces.dfy.expect b/Test/dafny0/MatchBraces.dfy.expect
index dfe1215f..385cad7a 100644
--- a/Test/dafny0/MatchBraces.dfy.expect
+++ b/Test/dafny0/MatchBraces.dfy.expect
@@ -85,7 +85,7 @@ method P(c: Color, d: Color)
 }

 

 lemma HeatIsEven(c: Color)

-  ensures Heat(c) % 2 == 0;

+  ensures Heat(c) % 2 == 0

 {

   match c

   case Red =>

@@ -96,7 +96,7 @@ lemma HeatIsEven(c: Color)
 }

 

 method DegenerateExamples(c: Color)

-  requires Heat(c) == 10;

+  requires Heat(c) == 10

 {

   match c

   case Red =>

@@ -108,7 +108,7 @@ method DegenerateExamples(c: Color)
 }

 

 method MoreDegenerateExamples(c: Color)

-  requires Heat(c) == 10;

+  requires Heat(c) == 10

 {

   if c == Green {

     var x: int := match c;

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index b6ad5d6b..34aba3de 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -6,13 +6,13 @@
 module Wazzup {

   class WazzupA { }

   class WazzupA { }  // error: duplicate type

-  datatype WazzupA = W_A_X;  // error: duplicate type

-  type WazzupA;  // error: duplicate type

+  datatype WazzupA = W_A_X  // error: duplicate type

+  type WazzupA  // error: duplicate type

 

-  type WazzupB;

-  type WazzupB;  // error: duplicate type

+  type WazzupB

+  type WazzupB  // error: duplicate type

   class WazzupB { }  // error: duplicate type

-  datatype WazzupB = W_B_X;  // error: duplicate type

+  datatype WazzupB = W_B_X  // error: duplicate type

 }

 

 // ---------------------- duplicate types across modules

@@ -27,15 +27,15 @@ module N {
 }

 

 module U {

-  import NN = N;

+  import NN = N

 }

 

 

 module A {  // Note, this has the effect of importing two different T's,

             // but that's okay as long as the module doesn't try to access

             // one of them

-  import MM = M;

-  import NN = N;

+  import MM = M

+  import NN = N

   class X {

     var t: MM.T;  // error: use of the ambiguous name T

     function F(x: MM.T):  // error: use of the ambiguous name T

@@ -60,7 +60,7 @@ module X0 {
 }

 

 module X1 {

-  import X0' = X0;

+  import X0' = X0

   class MyClass1 {

     method Down(x0: X0'.MyClass0) {

       x0.Down();

@@ -151,7 +151,7 @@ class AClassWithSomeField {
 

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

 

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

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

 

 function NestedMatch0(tree: Tree): int

 {

@@ -218,7 +218,7 @@ module ATr {
 }

 

 module BTr {

-  import A = ATr;

+  import A = ATr

   class Y {

     method N() returns (x: A.X)

       ensures x != null;

@@ -229,14 +229,14 @@ module BTr {
 }

 

 module CTr {

-  import B = BTr;

+  import B = BTr

   class Z {

     var b: B.Y;  // fine

     var a: B.X;  // error: imports don't reach name X explicitly

   }

 }

 module CTs {

-  import B = BTr;

+  import B = BTr

   method P() {

     var y := new B.Y;

     var x := y.N();  // this is allowed and will correctly infer the type of x to

@@ -275,8 +275,8 @@ module NonLocalB {
 }

 

 module Local {

-  import AA = NonLocalA;

-  import BB = NonLocalB;

+  import AA = NonLocalA

+  import BB = NonLocalB

   class MyClass {

     method MyMethod()

     {

@@ -302,7 +302,7 @@ module Local {
 

 module Q_Imp {

   class Node { }

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

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

   class Klassy {

     method Init()

   }

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index c134bb9a..699a730c 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -2,14 +2,14 @@
 // RUN: %diff "%s.expect" "%t"

 

 module A {

-  import B = Babble;

+  import B = Babble

   class X {

     function Fx(z: B.Z): int

       requires z != null;

       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 {

@@ -84,7 +84,7 @@ module A_Visibility {
 }

 

 module B_Visibility {

-  import A = A_Visibility;

+  import A = A_Visibility

   method Main() {

     var y;

     if (A.C.P(y)) {

@@ -106,7 +106,7 @@ module Q_Imp {
 }

 

 module Q_M {

-  import Q = Q_Imp;

+  import Q = Q_Imp

   method MyMethod(root: Q.Node, S: set<Q.Node>)

     requires root in S;

   {

diff --git a/Test/dafny0/Modules2.dfy b/Test/dafny0/Modules2.dfy
index 6a68c38e..a8dde8ce 100644
--- a/Test/dafny0/Modules2.dfy
+++ b/Test/dafny0/Modules2.dfy
@@ -5,18 +5,18 @@ module A {
   class C {

     var f: int;

   }

-  datatype D = E(int) | F(int);

+  datatype D = E(int) | F(int)

   function f(n:nat): nat

 }

 module B {

   class C {

     var f: int;

   }

-  datatype D = E(int) | F(int);

+  datatype D = E(int) | F(int)

   function f(n:nat): nat

 }

 module Test {

-  import opened A; // nice shorthand for import opened A = A; (see below)

+  import opened A // nice shorthand for import opened A = A; (see below)

   method m() {

     var c := new C;   // fine, as A was opened

     var c' := new A.C;// also fine, as A is bound

@@ -31,7 +31,7 @@ module Test {
 }

 

 module Test2 {

-  import opened B as A;

+  import opened B as A

   method m() {

     var c := new C;   // fine, as A was opened

     var c' := new B.C;// also fine, as A is bound

@@ -40,8 +40,8 @@ module Test2 {
 }

 

 module Test3 {

-  import opened A;

-  import opened B; // everything in B clashes with A

+  import opened A

+  import opened B // everything in B clashes with A

   method m() {

     var c := new C;    // bad, ambiguous between A.C and B.C

     var c' := new A.C; // good: qualified.

@@ -54,6 +54,6 @@ module Test3 {
 }

 

 module Test4 {

-  import A = A; // good: looks strange, but A is not bound on the RHS of the equality

-  import B; // the same as the above, but for module B

+  import A = A // good: looks strange, but A is not bound on the RHS of the equality

+  import B // the same as the above, but for module B

 }

diff --git a/Test/dafny0/ModulesCycle.dfy b/Test/dafny0/ModulesCycle.dfy
index 885677d3..11a14cbf 100644
--- a/Test/dafny0/ModulesCycle.dfy
+++ b/Test/dafny0/ModulesCycle.dfy
@@ -2,13 +2,13 @@
 // RUN: %diff "%s.expect" "%t"

 

 module V {

-  import t = T;  // error: T is not visible (and isn't even a module)

+  import t = T  // error: T is not visible (and isn't even a module)

 }

 

 module A {

-  import B = C;

+  import B = C

 }

 

 module C {

-  import D = A;

+  import D = A

 }

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 86f8c127..2415254d 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -52,7 +52,7 @@ function method FenEric<T>(t0: T, t1: T): T
   t1

 }

 

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

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

 

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

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

@@ -63,7 +63,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/NoTypeArgs.dfy b/Test/dafny0/NoTypeArgs.dfy
index d658af78..c830e916 100644
--- a/Test/dafny0/NoTypeArgs.dfy
+++ b/Test/dafny0/NoTypeArgs.dfy
@@ -1,7 +1,7 @@
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

-datatype List<T> = Nil | Cons(hd: T, tl: List);

+datatype List<T> = Nil | Cons(hd: T, tl: List)

 

 method M0() {

   var l: List;

diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 054facf4..b3f36b84 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -82,7 +82,7 @@ module Tight refines Loose {
 }

 

 module UnawareClient {

-  import L = Loose;

+  import L = Loose

   method Main0() {

     var n := new L.MyNumber.Init();

     assert n.N == 0;  // error: this is not known

@@ -94,7 +94,7 @@ module UnawareClient {
 }

 

 module AwareClient {

-  import T = Tight;

+  import T = Tight

   method Main1() {

     var n := new T.MyNumber.Init();

     assert n.N == 0;

diff --git a/Test/dafny0/RankNeg.dfy b/Test/dafny0/RankNeg.dfy
index 2ac00196..519d9063 100644
--- a/Test/dafny0/RankNeg.dfy
+++ b/Test/dafny0/RankNeg.dfy
@@ -16,7 +16,7 @@ function seq_loop_s(xs: seq<seq<int>>): int
   else 0

 }

 

-datatype wrap = X | WS(ds: seq<wrap>);

+datatype wrap = X | WS(ds: seq<wrap>)

 function wrap_loop_1(xs: seq<wrap>): int

 {

   if (xs == [WS([X,X])]) then wrap_loop_2(WS([X,X]))

diff --git a/Test/dafny0/RankPos.dfy b/Test/dafny0/RankPos.dfy
index ee582146..d8907b25 100644
--- a/Test/dafny0/RankPos.dfy
+++ b/Test/dafny0/RankPos.dfy
@@ -1,10 +1,10 @@
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

-datatype list<A> = Nil | Cons(head: A, tail: list<A>);

-datatype d = A | B(ds: list<d>);

-datatype d2 = A2 | B2(ds: seq<d2>);

-datatype d3 = A3 | B3(ds: set<d3>);

+datatype list<A> = Nil | Cons(head: A, tail: list<A>)

+datatype d = A | B(ds: list<d>)

+datatype d2 = A2 | B2(ds: seq<d2>)

+datatype d3 = A3 | B3(ds: set<d3>)

 

 function d_size(x: d): int

 {

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index a92e647a..760b090d 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -20,7 +20,7 @@ module A {
 
 module B refines A {
   class C { }
-  datatype Dt = Ax | Bx;
+  datatype Dt = Ax | Bx
   class T {
     method P() returns (p: int)
     {
@@ -165,7 +165,7 @@ module Concrete refines Abstract {
 }
 
 module Client {
-  import C = Concrete;
+  import C = Concrete
   class TheClient {
     method Main() {
       var n := new C.MyNumber.Init();
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 12593b8c..bc9c4eee 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -73,9 +73,9 @@ method TestNameResolution0() {
   y := gg.N(5);

 }

 

-datatype Abc = Abel | Benny | Cecilia(y: int) | David(x: int) | Eleanor;

-datatype Xyz = Alberta | Benny | Constantine(y: int) | David(x: int);

-datatype Rst = David(x: int, y: int);

+datatype Abc = Abel | Benny | Cecilia(y: int) | David(x: int) | Eleanor

+datatype Xyz = Alberta | Benny | Constantine(y: int) | David(x: int)

+datatype Rst = David(x: int, y: int)

 

 function Tuv(arg0: Abc, arg1: bool): int { 10 }

 

@@ -105,7 +105,7 @@ class EE {
 

 datatype GhostDt =

   Nil(ghost extraInfo: int) |

-  Cons(data: int, tail: GhostDt, ghost moreInfo: int);

+  Cons(data: int, tail: GhostDt, ghost moreInfo: int)

 

 class GhostTests {

   method M(dt: GhostDt) returns (r: int) {

@@ -296,7 +296,7 @@ method ConstructorTests()
 

 // ------------------- datatype destructors ---------------------------------------

 

-datatype DTD_List = DTD_Nil | DTD_Cons(Car: int, Cdr: DTD_List, ghost g: int);

+datatype DTD_List = DTD_Nil | DTD_Cons(Car: int, Cdr: DTD_List, ghost g: int)

 

 method DatatypeDestructors(d: DTD_List) {

   if {

@@ -347,7 +347,7 @@ method G_Caller()
   MG0(x, w);  // error: types don't match up

 }

 

-datatype GList<T> = GNil | GCons(hd: T, tl: GList);

+datatype GList<T> = GNil | GCons(hd: T, tl: GList)

 

 method MG1(l: GList, n: nat)

 {

@@ -489,8 +489,8 @@ method AssignSuchThatFromGhost()
 // Put the following tests in a separate module, so that the method bodies will

 // be type checked even if there are resolution errors in other modules.

 module NoTypeArgs0 {

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

-  datatype Tree<A,B> = Leaf(A, B) | Node(Tree, Tree<B,A>);

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

+  datatype Tree<A,B> = Leaf(A, B) | Node(Tree, Tree<B,A>)

 

   method DoAPrefix0<A, B, C>(xs: List) returns (ys: List<A>)

   {

@@ -528,7 +528,7 @@ module NoTypeArgs0 {
 }

 

 module NoTypeArgs1 {

-  datatype Tree<A,B> = Leaf(A, B) | Node(Tree, Tree<B,A>);

+  datatype Tree<A,B> = Leaf(A, B) | Node(Tree, Tree<B,A>)

 

   function FTree3<T>(t: Tree): Tree<T,T>  // error: type of 't' does not have enough type parameters

   {

diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy
index 6c9e56ec..8fc61395 100644
--- a/Test/dafny0/Simple.dfy
+++ b/Test/dafny0/Simple.dfy
@@ -42,12 +42,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) |

-  More(List<int>);

+  More(List<int>)

 

 class C {

   var w: WildData;

diff --git a/Test/dafny0/Simple.dfy.expect b/Test/dafny0/Simple.dfy.expect
index aceb685a..1e6a4f11 100644
--- a/Test/dafny0/Simple.dfy.expect
+++ b/Test/dafny0/Simple.dfy.expect
@@ -1,18 +1,18 @@
 // Simple.dfy

 

 class MyClass<T, U> {

-  var x: int;

+  var x: int

 

   method M(s: bool, lotsaObjects: set<object>)

       returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>)

-    requires s;

-    modifies this, lotsaObjects;

-    ensures t == t;

-    ensures old(null) != this;

+    requires s

+    modifies this, lotsaObjects

+    ensures t == t

+    ensures old(null) != this

   {

     x := 12;

     while x < 100

-      invariant x <= 100;

+      invariant x <= 100

     {

       x := x + 17;

       if x % 20 == 3 {

@@ -49,17 +49,17 @@ datatype List<T> = Nil | Cons(T, List<T>)
 datatype WildData = Something | JustAboutAnything(bool, myName: set<int>, int, WildData) | More(List<int>)

 

 class C {

-  var w: WildData;

-  var list: List<bool>;

+  var w: WildData

+  var list: List<bool>

 }

 

 lemma M(x: int)

-  ensures x < 8;

+  ensures x < 8

 {

 }

 

 colemma M'(x': int)

-  ensures true;

+  ensures true

 {

 }

 

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 13f56383..02335678 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -219,7 +219,7 @@ class AllocatedTests {
 datatype Lindgren =

   Pippi(Node) |

   Longstocking(seq<object>, Lindgren) |

-  HerrNilsson;

+  HerrNilsson

 

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

 

@@ -621,7 +621,7 @@ method AssignSuchThat8(n: int) returns (x: int, y: Lindgren) {
   x :| x in [];  // error

 }

 

-codatatype QuiteFinite = QQA | QQB | QQC;

+codatatype QuiteFinite = QQA | QQB | QQC

 

 method AssignSuchThat9() returns (q: QuiteFinite)

 {

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 0e51ade2..4496f3b7 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -100,7 +100,7 @@ class Termination {
   }

 }

 

-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 1e4f928a..9c75f22a 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -3,9 +3,9 @@
 

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

@@ -50,7 +50,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;

@@ -99,6 +99,6 @@ class State {
 

 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/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index f066d13f..3d40698c 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -218,13 +218,13 @@ method TyKn_Main(k0: TyKn_K) {
 

 module OneLayer

 {

-  datatype wrap<V> = Wrap(V);

+  datatype wrap<V> = Wrap(V)

 }

 

 module TwoLayers

 {

-  import OneLayer;

-  datatype wrap2<T> = Wrap2(get: OneLayer.wrap<T>);

+  import OneLayer

+  datatype wrap2<T> = Wrap2(get: OneLayer.wrap<T>)

   

   function F<U>(w: wrap2<U>) : OneLayer.wrap<U>

   {

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 01c2a0a5..b44f4d68 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -16,26 +16,26 @@ class C {
   }

 }

 

-datatype D = A;

+datatype D = A

 

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

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

 

 datatype MutuallyRecursiveDataType<T> =

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

-  Else(TheCounterpart<T>, C);

+  Else(TheCounterpart<T>, C)

 

 datatype TheCounterpart<T> =

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

-  More(MutuallyRecursiveDataType<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

-  Else(ReverseOrder_TheCounterpart<T>, C);

+  Else(ReverseOrder_TheCounterpart<T>, C)

 

 datatype ReverseOrder_TheCounterpart<T> =

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

-  More(ReverseOrder_MutuallyRecursiveDataType<T>);

+  More(ReverseOrder_MutuallyRecursiveDataType<T>)

 

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

 

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 5dc398f3..28171896 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -156,7 +156,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

@@ -192,7 +192,7 @@ class DatatypeInduction<T> {
 // This is a simple example where the induction hypothesis and the

 // case splits are decoupled.

 

-datatype D = Nothing | Something(D);

+datatype D = Nothing | Something(D)

 

 function FooD(n: nat, d: D): int

   ensures 10 <= FooD(n, d);

diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index a52f994b..41adcf50 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -1,8 +1,8 @@
 // RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

-datatype List<X> = Nil | Cons(Node<X>, List<X>);

-datatype Node<X> = Element(X) | Nary(List<X>);

+datatype List<X> = Nil | Cons(Node<X>, List<X>)

+datatype Node<X> = Element(X) | Nary(List<X>)

 

 function FlattenMain<M>(list: List<M>): List<M>

   ensures IsFlat(FlattenMain(list));

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 0f32d529..55701a93 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -3,17 +3,17 @@
 

 // 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

 

@@ -285,7 +285,7 @@ function mirror(t: Tree): Tree
 // applying some prescribed function (here, a value of the type)

 // to some argument.

 

-type FunctionValue;

+type FunctionValue

 function Apply(f: FunctionValue, x: Nat): Nat  // this function is left uninterpreted

 

 // The following functions stand for the constant "false" and "true" functions,

diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy
index 854af021..3ae1b555 100644
--- a/Test/dafny1/SchorrWaite-stages.dfy
+++ b/Test/dafny1/SchorrWaite-stages.dfy
@@ -17,7 +17,7 @@ abstract module M0 {
     var childrenVisited: nat;

   }

 

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

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

 

   function Reachable(source: Node, sink: Node, S: set<Node>): bool

     requires null !in S;

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index de07fdcc..7a6b051a 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -13,7 +13,7 @@ class Node {
   ghost var pathFromRoot: Path;

 }

 

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

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

 

 

 class Main {

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 174e71c8..da64d004 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -1,12 +1,12 @@
 // RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

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

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

 

 datatype Expr =

   Const(int) |

   Var(int) |

-  Nary(int, List);

+  Nary(int, List)

 

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

 {

@@ -50,7 +50,7 @@ lemma Lemma(l: List, v: int, val: int)
 datatype Expression =

   Const(int) |

   Var(int) |

-  Nary(int, seq<Expression>);

+  Nary(int, seq<Expression>)

 

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

   decreases e;

diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy
index beb1597e..3c836e37 100644
--- a/Test/dafny1/TreeDatatype.dfy
+++ b/Test/dafny1/TreeDatatype.dfy
@@ -3,9 +3,9 @@
 

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

 

 function Inc(t: Tree): Tree

 {

@@ -22,7 +22,7 @@ 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>>)

 

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

 {

@@ -39,9 +39,9 @@ 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)

 

 function XInc(t: OneTree): OneTree

 {

diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy
index 24cd541c..f06c8021 100644
--- a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy
@@ -35,7 +35,7 @@
 // verifies and compiles the program (for this program in less than 2 seconds)

 // without further human intervention.

 

-datatype Tree = Null | Node(Tree, int, Tree);

+datatype Tree = Null | Node(Tree, int, Tree)

 

 function Contains(t: Tree, v: int): bool

 {

diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index 4b8c9b4c..8af0afe9 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -4,7 +4,7 @@
 /* Lists */

 // Here are some standard definitions of List and functions on Lists

 

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

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

 

 function length(l: List): nat

 {

diff --git a/Test/dafny2/MonotonicHeapstate.dfy b/Test/dafny2/MonotonicHeapstate.dfy
index 12e86018..d6817ce9 100644
--- a/Test/dafny2/MonotonicHeapstate.dfy
+++ b/Test/dafny2/MonotonicHeapstate.dfy
@@ -2,7 +2,7 @@
 // RUN: %diff "%s.expect" "%t"

 

 module M0 {

-  datatype Kind = Constant | Ident | Binary;

+  datatype Kind = Constant | Ident | Binary

 

   class Expr {

     var kind: Kind;

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index d5a9d901..e39913a8 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -2,7 +2,7 @@
 // RUN: %diff "%s.expect" "%t"

 

 abstract module A {

-  import L = Library;

+  import L = Library

   class {:autocontracts} StoreAndRetrieve<Thing(==)> {

     ghost var Contents: set<Thing>;

     predicate Valid()

diff --git a/Test/dafny3/CachedContainer.dfy b/Test/dafny3/CachedContainer.dfy
index 18c12862..a3824fbf 100644
--- a/Test/dafny3/CachedContainer.dfy
+++ b/Test/dafny3/CachedContainer.dfy
@@ -117,7 +117,7 @@ module M3 refines M2 {
 

 // here a client of the Container

 module Client {

-  import M as M0 default M2;

+  import M as M0 default M2

   method Test() {

     var c := new M.Container();

     c.Add(56);

@@ -134,7 +134,7 @@ module Client {
 }

 

 module CachedClient refines Client {

-  import M = M3;

+  import M = M3

   method Main() {

     Test();

   }

diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy
index 0d9a7231..24c8e94e 100644
--- a/Test/dafny3/Filter.dfy
+++ b/Test/dafny3/Filter.dfy
@@ -1,7 +1,7 @@
 // RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

-codatatype Stream<T> = Cons(head: T, tail: Stream);

+codatatype Stream<T> = Cons(head: T, tail: Stream)

 

 function Tail(s: Stream, n: nat): Stream

 {

@@ -53,7 +53,7 @@ lemma Lemma_InSubStream<T>(x: T, s: Stream<T>, u: Stream<T>)
   }

 }

 

-type PredicateHandle;

+type PredicateHandle

 predicate P<T>(x: T, h: PredicateHandle)

 

 copredicate AllP(s: Stream, h: PredicateHandle)

diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy
index 47754036..89fa6cc8 100644
--- a/Test/dafny3/InductionVsCoinduction.dfy
+++ b/Test/dafny3/InductionVsCoinduction.dfy
@@ -3,7 +3,7 @@
 

 // A definition of a co-inductive datatype Stream, whose values are possibly

 // infinite lists.

-codatatype Stream<T> = SNil | SCons(head: T, tail: Stream<T>);

+codatatype Stream<T> = SNil | SCons(head: T, tail: Stream<T>)

 

 /*

   A function that returns a stream consisting of all integers upwards of n.

diff --git a/Test/dafny3/Paulson.dfy b/Test/dafny3/Paulson.dfy
index 735963a5..c10c4148 100644
--- a/Test/dafny3/Paulson.dfy
+++ b/Test/dafny3/Paulson.dfy
@@ -5,10 +5,10 @@
 // "Mechanizing Coinduction and Corecursion in Higher-order Logic"

 // by Lawrence C. Paulson, 1996.

 

-codatatype LList<T> = Nil | Cons(head: T, tail: LList);

+codatatype LList<T> = Nil | Cons(head: T, tail: LList)

 

 // Simulate function as arguments

-datatype FunctionHandle<T> = FH(T);

+datatype FunctionHandle<T> = FH(T)

 function Apply<T>(f: FunctionHandle<T>, argument: T): T

 

 // Function composition

diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy
index 00e598c3..6b6d0a9d 100644
--- a/Test/dafny3/SimpleCoinduction.dfy
+++ b/Test/dafny3/SimpleCoinduction.dfy
@@ -1,8 +1,8 @@
 // RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

-codatatype Stream<T> = Cons(head: T, tail: Stream);

-codatatype IList<T> = Nil | ICons(head: T, tail: IList);

+codatatype Stream<T> = Cons(head: T, tail: Stream)

+codatatype IList<T> = Nil | ICons(head: T, tail: IList)

 

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

 

diff --git a/Test/dafny3/SimpleInduction.dfy b/Test/dafny3/SimpleInduction.dfy
index 29660099..83ea6d14 100644
--- a/Test/dafny3/SimpleInduction.dfy
+++ b/Test/dafny3/SimpleInduction.dfy
@@ -56,7 +56,7 @@ ghost method FibLemma_All()
   to fill these in automatically.

   */

 

-datatype List<T> = Nil | Cons(head: T, tail: List<T>);

+datatype List<T> = Nil | Cons(head: T, tail: List<T>)

 

 function Append<T>(xs: List<T>, ys: List<T>): List<T>

   decreases xs;

diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy
index c51f30d4..f45df7ae 100644
--- a/Test/dafny3/Streams.dfy
+++ b/Test/dafny3/Streams.dfy
@@ -3,7 +3,7 @@
 

 // ----- Stream

 

-codatatype Stream<T> = Nil | Cons(head: T, tail: Stream);

+codatatype Stream<T> = Nil | Cons(head: T, tail: Stream)

 

 function append(M: Stream, N: Stream): Stream

 {

@@ -14,7 +14,7 @@ function append(M: Stream, N: Stream): Stream
 

 // ----- f, g, and maps

 

-type X;

+type X

 

 function f(x: X): X

 function g(x: X): X

diff --git a/Test/dafny3/Zip.dfy b/Test/dafny3/Zip.dfy
index 9b1d3671..44342970 100644
--- a/Test/dafny3/Zip.dfy
+++ b/Test/dafny3/Zip.dfy
@@ -17,7 +17,7 @@ of reasoning with quantifiers in SMT solvers make the explicit calls
 necessary.

 */

 

-codatatype Stream<T> = Cons(hd: T, tl: Stream);

+codatatype Stream<T> = Cons(hd: T, tl: Stream)

 

 function zip(xs: Stream, ys: Stream): Stream

   { Cons(xs.hd, Cons(ys.hd, zip(xs.tl, ys.tl))) }

diff --git a/Test/hofs/Fold.dfy b/Test/hofs/Fold.dfy
index 50b5569b..6ca2d3b1 100644
--- a/Test/hofs/Fold.dfy
+++ b/Test/hofs/Fold.dfy
@@ -1,9 +1,9 @@
 // RUN: %dafny /compile:3 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-datatype List<A> = Nil | Cons(A,List<A>);
+datatype List<A> = Nil | Cons(A,List<A>)
 
-datatype Expr = Add(List<Expr>) | Mul(List<Expr>) | Lit(int);
+datatype Expr = Add(List<Expr>) | Mul(List<Expr>) | Lit(int)
 
 function method Eval(e : Expr): int
 {
diff --git a/Test/hofs/Monads.dfy b/Test/hofs/Monads.dfy
index a221f818..3598d2b3 100644
--- a/Test/hofs/Monads.dfy
+++ b/Test/hofs/Monads.dfy
@@ -2,7 +2,7 @@
 // RUN: %diff "%s.expect" "%t"
 
 abstract module Monad {
-  type M<A>;
+  type M<A>
 
   function method Return(x: A): M<A>
   function method Bind(m: M<A>, f:A -> M<B>):M<B>
@@ -30,7 +30,7 @@ abstract module Monad {
 }
 
 module Identity refines Monad {
-  datatype M<A> = I(A);
+  datatype M<A> = I(A)
 
   function method Return<A>(x: A): M<A>
   { I(x) }
@@ -62,7 +62,7 @@ module Identity refines Monad {
 }
 
 module Maybe refines Monad {
-  datatype M<A> = Just(A) | Nothing;
+  datatype M<A> = Just(A) | Nothing
 
   function method Return<A>(x: A): M<A>
   { Just(x) }
@@ -96,7 +96,7 @@ module Maybe refines Monad {
 }
 
 module List refines Monad {
-  datatype M<A> = Cons(hd: A,tl: M<A>) | Nil;
+  datatype M<A> = Cons(hd: A,tl: M<A>) | Nil
 
   function method Return<A>(x: A): M<A>
   { Cons(x,Nil) }
diff --git a/Test/hofs/TreeMapSimple.dfy b/Test/hofs/TreeMapSimple.dfy
index 3c70840e..a853b82c 100644
--- a/Test/hofs/TreeMapSimple.dfy
+++ b/Test/hofs/TreeMapSimple.dfy
@@ -1,9 +1,9 @@
 // RUN: %dafny /compile:3 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-datatype List<A> = Nil | Cons(head: A,tail: List<A>);
+datatype List<A> = Nil | Cons(head: A,tail: List<A>)
 
-datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>);
+datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>)
 
 function ListData(xs : List) : set
   ensures forall x :: x in ListData(xs) ==> x < xs;
diff --git a/Test/vstte2012/Combinators.dfy b/Test/vstte2012/Combinators.dfy
index 37f3bd68..be7bc25f 100644
--- a/Test/vstte2012/Combinators.dfy
+++ b/Test/vstte2012/Combinators.dfy
@@ -11,7 +11,7 @@
 // definition, "car" and "cdr" are declared to be destructors for terms

 // constructed by Apply.

 

-datatype Term = S | K | Apply(car: Term, cdr: Term);

+datatype Term = S | K | Apply(car: Term, cdr: Term)

 

 // The problem defines values to be a subset of the terms.  More precisely,

 // a Value is a Term that fits the following grammar:

@@ -40,7 +40,7 @@ function method IsValue(t: Term): bool
 // A context is essentially a term with one missing subterm, a "hole".  It

 // is defined as follows:

 

-datatype Context = Hole | C_term(Context, Term) | value_C(Term/*Value*/, Context);

+datatype Context = Hole | C_term(Context, Term) | value_C(Term/*Value*/, Context)

 

 // The problem seems to suggest that the value_C form requires a value and

 // a context.  To formalize that notion, we define a predicate that checks this

@@ -270,7 +270,7 @@ ghost method Lemma_ContextPossibilities(t: Term)
 // sequence of terms from "t" to "r", each term reducing to its

 // successor in the trace.

 

-datatype Trace = EmptyTrace | ReductionStep(Trace, Term);

+datatype Trace = EmptyTrace | ReductionStep(Trace, Term)

 

 function IsTrace(trace: Trace, t: Term, r: Term): bool

 {

diff --git a/Test/vstte2012/Tree.dfy b/Test/vstte2012/Tree.dfy
index 82192e6d..4a45d011 100644
--- a/Test/vstte2012/Tree.dfy
+++ b/Test/vstte2012/Tree.dfy
@@ -2,7 +2,7 @@
 // RUN: %diff "%s.expect" "%t"

 

 // The tree datatype

-datatype Tree = Leaf | Node(Tree, Tree);

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

 

 

 // This datatype is used for the result of the build functions.

@@ -11,7 +11,7 @@ datatype Tree = Leaf | Node(Tree, Tree);
 // build_rec, it also has to yield the rest of the sequence,

 // which still needs to be processed. For function build,

 // this part is not used.

-datatype Result = Fail | Res(t: Tree, sOut: seq<int>);

+datatype Result = Fail | Res(t: Tree, sOut: seq<int>)

 

 

 // Function toList converts a tree to a sequence.