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

5 files changed, 21 insertions, 44 deletions

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

 }

 

-datatype Tree<T> {

-  Leaf(T);

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

-}

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

 

 class DatatypeInduction<T> {

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

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

 

-datatype Bool { False; True; }

+datatype Bool = False | True;

 

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

+datatype Nat = Zero | Suc(Nat);

 

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

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

 

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

+datatype Pair = Pair(Nat, Nat);

 

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

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

 

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

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

 

 // Boolean functions

 

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

 }

 

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

+

 class Main {

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

     requires root in S;

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

   }

 }

-

-datatype Path {

-  Empty;

-  Extend(Path, Node);

-}

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

-  Nil;

-  Cons(Expr, List);

-}

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

 

-datatype Expr {

-  Const(int);

-  Var(int);

+datatype Expr =

+  Const(int) |

+  Var(int) |

   Nary(int, List);

-}

 

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

 {

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

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

 

-datatype Expression {

-  Const(int);

-  Var(int);

+datatype Expression =

+  Const(int) |

+  Var(int) |

   Nary(int, seq<Expression>);

-}

 

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

   decreases e;

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

 

-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

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

 

-datatype Tree {

-  Node(int, List<Tree>);

-}

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

 

 static function Inc(t: Tree): Tree

 {

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

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

 

-datatype GTree<T> {

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

-}

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

 

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

 {

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

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

 

-datatype TreeList {

-  Nil;

-  Cons(OneTree, TreeList);

-}

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

 

-datatype OneTree {

-  Node(int, TreeList);

-}

+datatype OneTree = Node(int, TreeList);

 

 static function XInc(t: OneTree): OneTree

 {