summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/Dafny/Dafny.atg15
-rw-r--r--Source/Dafny/Parser.cs3
-rw-r--r--Source/Dafny/Printer.cs16
-rw-r--r--Test/dafny0/AutoReq.dfy4
-rw-r--r--Test/dafny0/CoPrefix.dfy8
-rw-r--r--Test/dafny0/CoResolution.dfy6
-rw-r--r--Test/dafny0/Coinductive.dfy62
-rw-r--r--Test/dafny0/CoinductiveProofs.dfy4
-rw-r--r--Test/dafny0/Compilation.dfy16
-rw-r--r--Test/dafny0/Comprehensions.dfy2
-rw-r--r--Test/dafny0/Computations.dfy6
-rw-r--r--Test/dafny0/ControlStructures.dfy2
-rw-r--r--Test/dafny0/Corecursion.dfy6
-rw-r--r--Test/dafny0/DTypes.dfy4
-rw-r--r--Test/dafny0/DatatypeUpdate.dfy2
-rw-r--r--Test/dafny0/Datatypes.dfy10
-rw-r--r--Test/dafny0/EqualityTypes.dfy34
-rw-r--r--Test/dafny0/FunctionSpecifications.dfy2
-rw-r--r--Test/dafny0/MatchBraces.dfy.expect6
-rw-r--r--Test/dafny0/Modules0.dfy32
-rw-r--r--Test/dafny0/Modules1.dfy8
-rw-r--r--Test/dafny0/Modules2.dfy16
-rw-r--r--Test/dafny0/ModulesCycle.dfy6
-rw-r--r--Test/dafny0/NatTypes.dfy4
-rw-r--r--Test/dafny0/NoTypeArgs.dfy2
-rw-r--r--Test/dafny0/Predicates.dfy4
-rw-r--r--Test/dafny0/RankNeg.dfy2
-rw-r--r--Test/dafny0/RankPos.dfy8
-rw-r--r--Test/dafny0/Refinement.dfy4
-rw-r--r--Test/dafny0/ResolutionErrors.dfy18
-rw-r--r--Test/dafny0/Simple.dfy4
-rw-r--r--Test/dafny0/Simple.dfy.expect20
-rw-r--r--Test/dafny0/SmallTests.dfy4
-rw-r--r--Test/dafny0/Termination.dfy2
-rw-r--r--Test/dafny0/TypeAntecedents.dfy10
-rw-r--r--Test/dafny0/TypeParameters.dfy6
-rw-r--r--Test/dafny0/TypeTests.dfy12
-rw-r--r--Test/dafny1/Induction.dfy4
-rw-r--r--Test/dafny1/MoreInduction.dfy4
-rw-r--r--Test/dafny1/Rippling.dfy14
-rw-r--r--Test/dafny1/SchorrWaite-stages.dfy2
-rw-r--r--Test/dafny1/SchorrWaite.dfy2
-rw-r--r--Test/dafny1/Substitution.dfy6
-rw-r--r--Test/dafny1/TreeDatatype.dfy10
-rw-r--r--Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy2
-rw-r--r--Test/dafny2/Calculations.dfy2
-rw-r--r--Test/dafny2/MonotonicHeapstate.dfy2
-rw-r--r--Test/dafny2/StoreAndRetrieve.dfy2
-rw-r--r--Test/dafny3/CachedContainer.dfy4
-rw-r--r--Test/dafny3/Filter.dfy4
-rw-r--r--Test/dafny3/InductionVsCoinduction.dfy2
-rw-r--r--Test/dafny3/Paulson.dfy4
-rw-r--r--Test/dafny3/SimpleCoinduction.dfy4
-rw-r--r--Test/dafny3/SimpleInduction.dfy2
-rw-r--r--Test/dafny3/Streams.dfy4
-rw-r--r--Test/dafny3/Zip.dfy2
-rw-r--r--Test/hofs/Fold.dfy4
-rw-r--r--Test/hofs/Monads.dfy8
-rw-r--r--Test/hofs/TreeMapSimple.dfy4
-rw-r--r--Test/vstte2012/Combinators.dfy6
-rw-r--r--Test/vstte2012/Tree.dfy4
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.