From 225930765d1f6c11dcf6c523ce0730457c07ec47 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 26 Sep 2012 00:09:04 -0700
Subject: Dafny: compile iterators

---
 Test/dafny0/Answer                 |  7 ++++++-
 Test/dafny0/IteratorResolution.dfy |  2 ++
 Test/dafny0/Iterators.dfy          | 30 ++++++++++++++++++++++++++++++
 Test/dafny0/runtest.bat            |  2 +-
 4 files changed, 39 insertions(+), 2 deletions(-)
 create mode 100644 Test/dafny0/Iterators.dfy

(limited to 'Test/dafny0')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 9025e206..bde6a07c 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1620,7 +1620,12 @@ IteratorResolution.dfy(56,11): Error: LHS of assignment does not denote a mutabl
 IteratorResolution.dfy(57,11): Error: LHS of assignment does not denote a mutable field
 IteratorResolution.dfy(61,18): Error: arguments must have the same type (got _T0 and int)
 IteratorResolution.dfy(73,19): Error: RHS (of type bool) not assignable to LHS (of type int)
-4 resolution/type errors detected in IteratorResolution.dfy
+IteratorResolution.dfy(76,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called
+5 resolution/type errors detected in IteratorResolution.dfy
+
+-------------------- Iterators.dfy --------------------
+
+Dafny program verifier finished with 8 verified, 0 errors
 
 -------------------- Superposition.dfy --------------------
 
diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy
index f45dd764..fe9e2563 100644
--- a/Test/dafny0/IteratorResolution.dfy
+++ b/Test/dafny0/IteratorResolution.dfy
@@ -72,6 +72,8 @@ module Mx {
       } else {
         var x: int := h1.t;  // error: h1 would have to be a GenericIteratorResult<int>
       }
+
+      var h2 := new GenericIteratorResult;  // error: constructor is not mentioned
     }
   }
 
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy
new file mode 100644
index 00000000..76a30330
--- /dev/null
+++ b/Test/dafny0/Iterators.dfy
@@ -0,0 +1,30 @@
+iterator MyIter<T>(q: T) yields (x: T, y: T)
+{
+}
+
+iterator MyIntIter() yields (x: int, y: int)
+{
+  x, y := 0, 0;
+  yield;
+  yield 2, 3;
+  x, y := y, x;
+  yield;
+}
+
+method Main() {
+  var m := new MyIter.MyIter(12);
+  var a := m.x;
+  // assert !a;  // error: type mismatch
+  if (a <= 13) {
+    print "-- ", m.x, " --\n";
+  }
+
+  var n := new MyIntIter.MyIntIter();
+  var patience := 10;
+  while (patience != 0) {
+    var more := n.MoveNext();
+    if (!more) { break; }
+    print n.x, ", ", n.y, "\n";
+    patience := patience - 1;
+  }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index b602f089..9789e7d7 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -24,7 +24,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
             Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy
             RefinementModificationChecking.dfy TailCalls.dfy
-            IteratorResolution.dfy) do (
+            IteratorResolution.dfy Iterators.dfy) do (
   echo.
   echo -------------------- %%f --------------------
   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
-- 
cgit v1.2.3