Dafny: compile iterators

1 files changed, 30 insertions, 0 deletions

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;

+  }

+}