From db30cafd94527e73e969457c9c00e8c67300d7d4 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Thu, 5 Mar 2015 12:04:37 -0800 Subject: Stop pretty-print from emitting deprecated semi-colons. --- Source/Dafny/Dafny.atg | 15 +++--- Source/Dafny/Parser.cs | 3 ++ Source/Dafny/Printer.cs | 16 +++--- Test/dafny0/AutoReq.dfy | 4 +- Test/dafny0/CoPrefix.dfy | 8 +-- Test/dafny0/CoResolution.dfy | 6 +-- Test/dafny0/Coinductive.dfy | 62 +++++++++++----------- Test/dafny0/CoinductiveProofs.dfy | 4 +- Test/dafny0/Compilation.dfy | 16 +++--- Test/dafny0/Comprehensions.dfy | 2 +- Test/dafny0/Computations.dfy | 6 +-- Test/dafny0/ControlStructures.dfy | 2 +- Test/dafny0/Corecursion.dfy | 6 +-- Test/dafny0/DTypes.dfy | 4 +- Test/dafny0/DatatypeUpdate.dfy | 2 +- Test/dafny0/Datatypes.dfy | 10 ++-- Test/dafny0/EqualityTypes.dfy | 34 ++++++------ Test/dafny0/FunctionSpecifications.dfy | 2 +- Test/dafny0/MatchBraces.dfy.expect | 6 +-- Test/dafny0/Modules0.dfy | 32 +++++------ Test/dafny0/Modules1.dfy | 8 +-- Test/dafny0/Modules2.dfy | 16 +++--- Test/dafny0/ModulesCycle.dfy | 6 +-- Test/dafny0/NatTypes.dfy | 4 +- Test/dafny0/NoTypeArgs.dfy | 2 +- Test/dafny0/Predicates.dfy | 4 +- Test/dafny0/RankNeg.dfy | 2 +- Test/dafny0/RankPos.dfy | 8 +-- Test/dafny0/Refinement.dfy | 4 +- Test/dafny0/ResolutionErrors.dfy | 18 +++---- Test/dafny0/Simple.dfy | 4 +- Test/dafny0/Simple.dfy.expect | 20 +++---- Test/dafny0/SmallTests.dfy | 4 +- Test/dafny0/Termination.dfy | 2 +- Test/dafny0/TypeAntecedents.dfy | 10 ++-- Test/dafny0/TypeParameters.dfy | 6 +-- Test/dafny0/TypeTests.dfy | 12 ++--- Test/dafny1/Induction.dfy | 4 +- Test/dafny1/MoreInduction.dfy | 4 +- Test/dafny1/Rippling.dfy | 14 ++--- Test/dafny1/SchorrWaite-stages.dfy | 2 +- Test/dafny1/SchorrWaite.dfy | 2 +- Test/dafny1/Substitution.dfy | 6 +-- Test/dafny1/TreeDatatype.dfy | 10 ++-- .../COST-verif-comp-2011-2-MaxTree-datatype.dfy | 2 +- Test/dafny2/Calculations.dfy | 2 +- Test/dafny2/MonotonicHeapstate.dfy | 2 +- Test/dafny2/StoreAndRetrieve.dfy | 2 +- Test/dafny3/CachedContainer.dfy | 4 +- Test/dafny3/Filter.dfy | 4 +- Test/dafny3/InductionVsCoinduction.dfy | 2 +- Test/dafny3/Paulson.dfy | 4 +- Test/dafny3/SimpleCoinduction.dfy | 4 +- Test/dafny3/SimpleInduction.dfy | 2 +- Test/dafny3/Streams.dfy | 4 +- Test/dafny3/Zip.dfy | 2 +- Test/hofs/Fold.dfy | 4 +- Test/hofs/Monads.dfy | 8 +-- Test/hofs/TreeMapSimple.dfy | 4 +- Test/vstte2012/Combinators.dfy | 6 +-- Test/vstte2012/Tree.dfy | 4 +- 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 [ 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(); @@ -678,9 +677,8 @@ DatatypeDecl [ 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 [ 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 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(); @@ -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 = TCons(head: T, tail: TList); +codatatype TList = TCons(head: T, tail: TList) function Next(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 = Cons(head: G, tail: Stream); + codatatype Stream = Cons(head: G, tail: Stream) method UseStream0(s: Stream) { var x := 3; @@ -44,7 +44,7 @@ module GhostCheck0 { } } module GhostCheck1 { - codatatype Stream = Cons(head: G, tail: Stream); + codatatype Stream = Cons(head: G, tail: Stream) method UseStream1(s: Stream) { var x := 3; @@ -54,7 +54,7 @@ module GhostCheck1 { } } module GhostCheck2 { - codatatype Stream = Cons(head: G, tail: Stream); + codatatype Stream = 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 = Ctor(T); + datatype Record = Ctor(T) - datatype RecInt = Ctor(Record); // this is fine - datatype Rec_Forever = Ctor(Record); // error - datatype Rec_Stops = Cons(Record, Rec_Stops) | Nil; // this is okay + datatype RecInt = Ctor(Record) // this is fine + datatype Rec_Forever = Ctor(Record) // error + datatype Rec_Stops = Cons(Record, Rec_Stops) | Nil // this is okay - datatype D = Ctor(E>); // error: illegal cycle - datatype E = Ctor(T); + datatype D = Ctor(E>) // error: illegal cycle + datatype E = Ctor(T) // the following is okay - datatype MD = Ctor(ME); - datatype ME = Ctor(T); + datatype MD = Ctor(ME) + datatype ME = Ctor(T) method M() { var d: MD>; } - datatype A = Ctor(B); // superficially looks like a cycle, but can still be constructed - datatype B = Ctor(List); - datatype List = Nil | Cons(T, List); + datatype A = Ctor(B) // superficially looks like a cycle, but can still be constructed + datatype B = Ctor(List) + datatype List = Nil | Cons(T, List) } module MoreInductive { - datatype Tree = Node(G, List>); - datatype List = Nil | Cons(T, List); + datatype Tree = Node(G, List>) + datatype List = Nil | Cons(T, List) - datatype M = All(List); - datatype H<'a> = HH('a, Tree<'a>); - datatype K<'a> = KK('a, Tree>); // error - datatype L<'a> = LL('a, Tree>>); + datatype M = All(List) + datatype H<'a> = HH('a, Tree<'a>) + datatype K<'a> = KK('a, Tree>) // error + datatype L<'a> = LL('a, Tree>>) } // -------------------------------------------------- module TestCoinductiveDatatypes { - codatatype InfList = Done | Continue(T, InfList); + codatatype InfList = Done | Continue(T, InfList) - codatatype Stream = More(T, Stream); + codatatype Stream = More(T, Stream) - codatatype BinaryTreeForever = BNode(val: T, left: BinaryTreeForever, right: BinaryTreeForever); + codatatype BinaryTreeForever = BNode(val: T, left: BinaryTreeForever, right: BinaryTreeForever) - datatype List = Nil | Cons(T, List); + datatype List = Nil | Cons(T, List) - codatatype BestBushEver = Node(value: T, branches: List>); + codatatype BestBushEver = Node(value: T, branches: List>) - codatatype LazyRecord = Lazy(contents: T); + codatatype LazyRecord = Lazy(contents: T) class MyClass { } - datatype GenericDt = Blue | Green(T); - datatype GenericRecord = Rec(T); + datatype GenericDt = Blue | Green(T) + datatype GenericRecord = Rec(T) - datatype FiniteEnough_Class = Ctor(MyClass); - datatype FiniteEnough_Co = Ctor(LazyRecord); - datatype FiniteEnough_Dt = Ctor(GenericDt); // fine - datatype NotFiniteEnough_Dt = Ctor(GenericRecord); // error + datatype FiniteEnough_Class = Ctor(MyClass) + datatype FiniteEnough_Co = Ctor(LazyRecord) + datatype FiniteEnough_Dt = Ctor(GenericDt) // fine + datatype NotFiniteEnough_Dt = Ctor(GenericRecord) // error } @@ -69,7 +69,7 @@ module TestCoinductiveDatatypes module CoPredicateResolutionErrors { - codatatype Stream = StreamCons(head: T, tail: Stream); + codatatype Stream = StreamCons(head: T, tail: Stream) function Upward(n: int): Stream { @@ -158,7 +158,7 @@ module CoPredicateResolutionErrors { // -------------------------------------------------- module UnfruitfulCoLemmaConclusions { - codatatype Stream = Cons(head: T, tail: Stream); + codatatype Stream = Cons(head: T, tail: Stream) copredicate Positive(s: Stream) { 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 = Cons(head: T, tail: Stream); +codatatype Stream = Cons(head: T, tail: Stream) function Upward(n: int): Stream { @@ -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 = INil | ICons(head: T, tail: IList); +codatatype IList = INil | ICons(head: T, tail: IList) 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 = Nil | Cons(T, MyDt); + datatype MyDt = Nil | Cons(T, MyDt) method M(x: MyDt) { @@ -20,14 +20,14 @@ module OnceBuggy { // -------------------------------------------------- module CoRecursion { - codatatype Stream = More(head: T, rest: Stream); + codatatype Stream = More(head: T, rest: Stream) function method AscendingChain(n: int): Stream { More(n, AscendingChain(n+1)) } - datatype List = Nil | Cons(car: T, cdr: List); + datatype List = 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 = Nil | Cons(head: A, tail: list); +datatype list = 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, 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 = More(head: T, rest: Stream); + codatatype Stream = More(head: T, rest: Stream) function AscendingChain(n: int): Stream { @@ -23,7 +23,7 @@ module CoRecursion { More(n, AscendingChainAndPostcondition(n+1)) // error: cannot prove termination } - datatype List = Nil | Cons(T, List); + datatype List = Nil | Cons(T, List) function Prefix(n: nat, s: Stream): List { @@ -35,7 +35,7 @@ module CoRecursion { // -------------------------------------------------- module CoRecursionNotUsed { - codatatype Stream = More(T, Stream); + codatatype Stream = 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 { } -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 = Leaf(T) | Branch(Tree, Tree); +datatype Tree = Leaf(T) | Branch(Tree, Tree) class DatatypeInduction { function LeafCount(tree: Tree): 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 = Nil | Cons(T, List); +datatype List = Nil | Cons(T, List) 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 = Nil | Cons(set, Explicit); - datatype Inferred = Nil | Cons(set, Inferred); + datatype Explicit = Nil | Cons(set, Explicit) + datatype Inferred = Nil | Cons(set, Inferred) class C { method M(x: Explicit) @@ -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 = Nil | Cons(T, X); // error: not allowed to add a type parameter to type X + datatype X = Nil | Cons(T, X) // error: not allowed to add a type parameter to type X class Y { } // 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 = Nil | Cons(T, Dt); + datatype Dt = Nil | Cons(T, Dt) - datatype BulkyList = Nothing | Wrapper(T, BulkyListAux); - datatype BulkyListAux = Kons(set, BulkyListAuxAux); - datatype BulkyListAuxAux = GoBack(BulkyList); + datatype BulkyList = Nothing | Wrapper(T, BulkyListAux) + datatype BulkyListAux = Kons(set, BulkyListAuxAux) + datatype BulkyListAuxAux = GoBack(BulkyList) - codatatype Stream = Next(head: T, tail: Stream); + codatatype Stream = Next(head: T, tail: Stream) method M(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 = Nil | Cons(T, List); + datatype List = 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) 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(t0: T, t1: T): T t1 } -datatype Pair = Pr(T, T); +datatype Pair = 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 = Nil | Cons(nat, T, List); +datatype List = Nil | Cons(nat, T, List) method MatchIt(list: List) 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 = Nil | Cons(hd: T, tl: List); +datatype List = 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>): int else 0 } -datatype wrap = X | WS(ds: seq); +datatype wrap = X | WS(ds: seq) function wrap_loop_1(xs: seq): 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 = Nil | Cons(head: A, tail: list); -datatype d = A | B(ds: list); -datatype d2 = A2 | B2(ds: seq); -datatype d3 = A3 | B3(ds: set); +datatype list = Nil | Cons(head: A, tail: list) +datatype d = A | B(ds: list) +datatype d2 = A2 | B2(ds: seq) +datatype d3 = A3 | B3(ds: set) 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 = GNil | GCons(hd: T, tl: GList); +datatype GList = 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 = Nil | Cons(T, List); - datatype Tree = Leaf(A, B) | Node(Tree, Tree); + datatype List = Nil | Cons(T, List) + datatype Tree = Leaf(A, B) | Node(Tree, Tree) method DoAPrefix0(xs: List) returns (ys: List) { @@ -528,7 +528,7 @@ module NoTypeArgs0 { } module NoTypeArgs1 { - datatype Tree = Leaf(A, B) | Node(Tree, Tree); + datatype Tree = Leaf(A, B) | Node(Tree, Tree) function FTree3(t: Tree): Tree // 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 { // some datatype stuff: -datatype List = Nil | Cons(T, List); +datatype List = Nil | Cons(T, List) datatype WildData = Something() | JustAboutAnything(bool, myName: set, int, WildData) | - More(List); + More(List) 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 { - var x: int; + var x: int method M(s: bool, lotsaObjects: set) returns (t: object, u: set, v: seq>) - 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 = Nil | Cons(T, List) datatype WildData = Something | JustAboutAnything(bool, myName: set, int, WildData) | More(List) class C { - var w: WildData; - var list: List; + var w: WildData + var list: List } 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, 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 = Nil | Cons(T, List); +datatype List = Nil | Cons(T, List) 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 = Wrap(T); -datatype Unit = It; -datatype Color = Yellow | Blue; +datatype Wrapper = Wrap(T) +datatype Unit = It +datatype Color = Yellow | Blue function F(a: Wrapper): 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) returns (ret: int) modifies S; @@ -99,6 +99,6 @@ class State { function TakesADatatype(a: List): int { 12 } -datatype GenData = Pair(T, T); +datatype GenData = Pair(T, T) function AlsoTakesADatatype(p: GenData): 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 = Wrap(V); + datatype wrap = Wrap(V) } module TwoLayers { - import OneLayer; - datatype wrap2 = Wrap2(get: OneLayer.wrap); + import OneLayer + datatype wrap2 = Wrap2(get: OneLayer.wrap) function F(w: wrap2) : OneLayer.wrap { 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 = FromANumber(int) | // this is the base case - Else(TheCounterpart, C); + Else(TheCounterpart, C) datatype TheCounterpart = TreeLike(TheCounterpart, TheCounterpart) | - More(MutuallyRecursiveDataType); + More(MutuallyRecursiveDataType) // these 'ReverseOrder_' order tests may be called white-box unit tests datatype ReverseOrder_MutuallyRecursiveDataType = FromANumber(int) | // this is the base case - Else(ReverseOrder_TheCounterpart, C); + Else(ReverseOrder_TheCounterpart, C) datatype ReverseOrder_TheCounterpart = TreeLike(ReverseOrder_TheCounterpart, ReverseOrder_TheCounterpart) | - More(ReverseOrder_MutuallyRecursiveDataType); + More(ReverseOrder_MutuallyRecursiveDataType) // --------------------- 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 = Leaf(T) | Branch(Tree, Tree); +datatype Tree = Leaf(T) | Branch(Tree, Tree) class DatatypeInduction { function LeafCount(tree: Tree): int @@ -192,7 +192,7 @@ class DatatypeInduction { // 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 = Nil | Cons(Node, List); -datatype Node = Element(X) | Nary(List); +datatype List = Nil | Cons(Node, List) +datatype Node = Element(X) | Nary(List) function FlattenMain(list: List): List 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): 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); + Nary(int, seq) 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 = Nil | Cons(T, List); +datatype List = Nil | Cons(T, List) -datatype Tree = Node(int, List); +datatype Tree = Node(int, List) function Inc(t: Tree): Tree { @@ -22,7 +22,7 @@ function ForestInc(forest: List): List // ------------------ generic list, generic tree (but GInc defined only for GTree -datatype GTree = Node(T, List>); +datatype GTree = Node(T, List>) function GInc(t: GTree): GTree { @@ -39,9 +39,9 @@ function GForestInc(forest: List>): List> // ------------------ 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 = Nil | Cons(T, List); +datatype List = 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 { ghost var Contents: set; 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 = Cons(head: T, tail: Stream); +codatatype Stream = Cons(head: T, tail: Stream) function Tail(s: Stream, n: nat): Stream { @@ -53,7 +53,7 @@ lemma Lemma_InSubStream(x: T, s: Stream, u: Stream) } } -type PredicateHandle; +type PredicateHandle predicate P(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 = SNil | SCons(head: T, tail: Stream); +codatatype Stream = SNil | SCons(head: T, tail: Stream) /* 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 = Nil | Cons(head: T, tail: LList); +codatatype LList = Nil | Cons(head: T, tail: LList) // Simulate function as arguments -datatype FunctionHandle = FH(T); +datatype FunctionHandle = FH(T) function Apply(f: FunctionHandle, 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 = Cons(head: T, tail: Stream); -codatatype IList = Nil | ICons(head: T, tail: IList); +codatatype Stream = Cons(head: T, tail: Stream) +codatatype IList = 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 = Nil | Cons(head: T, tail: List); +datatype List = Nil | Cons(head: T, tail: List) function Append(xs: List, ys: List): List 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 = Nil | Cons(head: T, tail: Stream); +codatatype Stream = 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 = Cons(hd: T, tl: Stream); +codatatype Stream = 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 = Nil | Cons(A,List); +datatype List = Nil | Cons(A,List) -datatype Expr = Add(List) | Mul(List) | Lit(int); +datatype Expr = Add(List) | Mul(List) | 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; + type M function method Return(x: A): M function method Bind(m: M, f:A -> M):M @@ -30,7 +30,7 @@ abstract module Monad { } module Identity refines Monad { - datatype M = I(A); + datatype M = I(A) function method Return(x: A): M { I(x) } @@ -62,7 +62,7 @@ module Identity refines Monad { } module Maybe refines Monad { - datatype M = Just(A) | Nothing; + datatype M = Just(A) | Nothing function method Return(x: A): M { Just(x) } @@ -96,7 +96,7 @@ module Maybe refines Monad { } module List refines Monad { - datatype M = Cons(hd: A,tl: M) | Nil; + datatype M = Cons(hd: A,tl: M) | Nil function method Return(x: A): M { 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 = Nil | Cons(head: A,tail: List); +datatype List = Nil | Cons(head: A,tail: List) -datatype Tree = Branch(val: A,trees: List>); +datatype Tree = Branch(val: A,trees: List>) 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); +datatype Result = Fail | Res(t: Tree, sOut: seq) // Function toList converts a tree to a sequence. -- cgit v1.2.3