diff options
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.
|