From db30cafd94527e73e969457c9c00e8c67300d7d4 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Thu, 5 Mar 2015 12:04:37 -0800
Subject: Stop pretty-print from emitting deprecated semi-colons.

---
 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 +++++-----
 7 files changed, 21 insertions(+), 21 deletions(-)

(limited to 'Test/dafny1')

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
 {
-- 
cgit v1.2.3