Dafny: compile iterators

8 files changed, 156 insertions, 17 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index a6e05c22..91e6d6f4 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -93,9 +93,86 @@ namespace Microsoft.Dafny {
             CompileDatatypeConstructors(dt, indent);

             CompileDatatypeStruct(dt, indent);

           } else if (d is IteratorDecl) {

-            throw new NotImplementedException();  // TODO

+            var iter = (IteratorDecl)d;

+            // An iterator is compiled as follows:

+            //   public class MyIteratorExample<T>

+            //   {

+            //     public T q;  // in-parameter

+            //     public T x;  // yield-parameter

+            //     public int y;  // yield-parameter

+            //     IEnumerator<object> _iter;

+            //   

+            //     public void _MyIteratorExample(T q) {

+            //       this.q = q;

+            //       _iter = TheIterator();

+            //     }

+            //   

+            //     public void MoveNext(out bool more) {

+            //       more =_iter.MoveNext();

+            //     }

+            //   

+            //     private IEnumerator<object> TheIterator() {

+            //       // the translation of the body of the iterator, with each "yield" turning into a "yield return null;"

+            //       yield break;

+            //     }

+            //   }

+

+            Indent(indent);

+            wr.Write("public class @{0}", iter.CompileName);

+            if (iter.TypeArgs.Count != 0) {

+              wr.Write("<{0}>", TypeParameters(iter.TypeArgs));

+            }

+            wr.WriteLine(" {");

+            var ind = indent + IndentAmount;

+            // here come the fields

+            Constructor ct = null;

+            foreach (var member in iter.Members) {

+              var f = member as Field;

+              if (f != null && !f.IsGhost) {

+                Indent(ind);

+                wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.CompileName, DefaultValue(f.Type));

+              } else if (member is Constructor) {

+                Contract.Assert(ct == null);  // we're expecting just one constructor

+                ct = (Constructor)member;

+              }

+            }

+            Contract.Assert(ct != null);  // we do expect a constructor

+            Indent(ind); wr.WriteLine("System.Collections.Generic.IEnumerator<object> __iter;");

+

+            // here's the initializer method

+            Indent(ind); wr.Write("public void @{0}(", ct.CompileName);

+            string sep = "";

+            foreach (var p in ct.Ins) {

+              if (!p.IsGhost) {

+                // here we rely on the parameters and the corresponding fields having the same names

+                wr.Write("{0}{1} @{2}", sep, TypeName(p.Type), p.CompileName);

+                sep = ", ";

+              }

+            }

+            wr.WriteLine(") {");

+            foreach (var p in ct.Ins) {

+              if (!p.IsGhost) {

+                Indent(ind + IndentAmount);

+                wr.WriteLine("this.@{0} = @{0};", p.CompileName);

+              }

+            }

+            Indent(ind + IndentAmount); wr.WriteLine("__iter = TheIterator();");

+            Indent(ind);  wr.WriteLine("}");

+            // here are the enumerator methods

+            Indent(ind); wr.WriteLine("public void MoveNext(out bool more) { more = __iter.MoveNext(); }");

+            Indent(ind); wr.WriteLine("private System.Collections.Generic.IEnumerator<object> TheIterator() {");

+            if (iter.Body == null) {

+              Error("Iterator {0} has no body", iter.FullName);

+            } else {

+              TrStmt(iter.Body, ind + IndentAmount);

+            }

+            Indent(ind + IndentAmount); wr.WriteLine("yield break;");

+            Indent(ind); wr.WriteLine("}");

+            // end of the class

+            Indent(indent); wr.WriteLine("}");

+

           } else if (d is ClassDecl) {

-            ClassDecl cl = (ClassDecl)d;

+            var cl = (ClassDecl)d;

             Indent(indent);

             wr.Write("public class @{0}", cl.CompileName);

             if (cl.TypeArgs.Count != 0) {

@@ -939,13 +1016,16 @@ namespace Microsoft.Dafny {
         var s = (BreakStmt)stmt;

         Indent(indent);

         wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.Data.UniqueId);

-      } else if (stmt is ReturnStmt) {

-        var s = (ReturnStmt)stmt;

+      } else if (stmt is ProduceStmt) {

+        var s = (ProduceStmt)stmt;

         if (s.hiddenUpdate != null)

           TrStmt(s.hiddenUpdate, indent);

-        Indent(indent); wr.WriteLine("return;");

-      } else if (stmt is YieldStmt) {

-        throw new NotImplementedException();  // TODO

+        Indent(indent);

+        if (s is YieldStmt) {

+          wr.WriteLine("yield return null;");

+        } else {

+          wr.WriteLine("return;");

+        }

       } else if (stmt is UpdateStmt) {

         var s = (UpdateStmt)stmt;

         var resolved = s.ResolvedStatements;

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index dd190b6c..012619ee 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -744,7 +744,7 @@ namespace Microsoft.Dafny {
     public IToken BodyEndTok = Token.NoToken;

     public readonly string/*!*/ Name;

     string compileName;

-    public string CompileName {

+    public virtual string CompileName {

       get {

         if (compileName == null) {

           compileName = NonglobalVariable.CompilerizeName(Name);

@@ -1253,6 +1253,15 @@ namespace Microsoft.Dafny {
 

       return EnclosingClass.FullNameInContext(context) + "." + Name;

     }

+    public override string CompileName {

+      get {

+        var nm = base.CompileName;

+        if (this.Name == EnclosingClass.Name) {

+          nm = "_" + nm;

+        }

+        return nm;

+      }

+    }

     public string FullCompileName {

       get {

         Contract.Requires(EnclosingClass != null);

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index d568ab0e..1fd828a0 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -546,15 +546,25 @@ namespace Microsoft.Dafny
           // Also add "Valid" and "MoveNext"

           var init = new Constructor(iter.tok, iter.Name, new List<TypeParameter>(), iter.Ins,

             /* TODO: Fill in the spec here */

-            new List<MaybeFreeExpression>(), new Specification<FrameExpression>(null, null), new List<MaybeFreeExpression>(), new Specification<Expression>(null, null),

+            new List<MaybeFreeExpression>(),

+            new Specification<FrameExpression>(new List<FrameExpression>(), null),

+            new List<MaybeFreeExpression>(),

+            new Specification<Expression>(new List<Expression>(), null),

             null, null, false);

           var valid = new Predicate(iter.tok, "Valid", false, true, new List<TypeParameter>(), iter.tok,

-            new List<Formal>(), new List<Expression>(), new List<FrameExpression>()/*TODO: does this need to be filled?*/, new List<Expression>(), new Specification<Expression>(null, null),

+            new List<Formal>(),

+            new List<Expression>(),

+            new List<FrameExpression>()/*TODO: does this need to be filled?*/,

+            new List<Expression>(),

+            new Specification<Expression>(new List<Expression>(), null),

             null/*TODO: does this need to be fileld?*/, Predicate.BodyOriginKind.OriginalOrInherited, null, false);

           var moveNext = new Method(iter.tok, "MoveNext", false, false, new List<TypeParameter>(),

             new List<Formal>(), new List<Formal>() { new Formal(iter.tok, "more", Type.Bool, false, false) },

             /* TODO: Do the first 3 of the specification components on the next line need to be filled in? */

-            new List<MaybeFreeExpression>(), new Specification<FrameExpression>(null, null), new List<MaybeFreeExpression>(), new Specification<Expression>(null, null),

+            new List<MaybeFreeExpression>(),

+            new Specification<FrameExpression>(new List<FrameExpression>(), null),

+            new List<MaybeFreeExpression>(),

+            new Specification<Expression>(new List<Expression>(), null),

             null, null, false);

           init.EnclosingClass = iter;

           valid.EnclosingClass = iter;

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 54a4bec5..8d2eff05 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -345,10 +345,13 @@ namespace Microsoft.Dafny {
             AddDatatype((DatatypeDecl)d);

           } else if (d is ModuleDecl) {

             // submodules have already been added as a top level module, ignore this.

-          } else if (d is IteratorDecl) {

-            throw new NotImplementedException();  // TODO

           } else if (d is ClassDecl) {

             AddClassMembers((ClassDecl)d);

+            var iter = d as IteratorDecl;

+            if (iter != null && iter.Body != null) {

+              // also translate the body of the iterator

+              //KRML  throw new NotImplementedException();  // TODO

+            }

           } else {

             Contract.Assert(false);

           }

@@ -1034,7 +1037,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr.Neq(o, predef.Null)),

           etran.IsAlloced(f.tok, o));

         Bpl.Expr body = Bpl.Expr.Imp(ante, wh);

-        Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(oDotF));

+        Bpl.Trigger tr = f.IsMutable ? new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(oDotF)) : null;  // the trigger must include both "o" and "h"

         Bpl.Expr ax = new Bpl.ForallExpr(f.tok, new Bpl.VariableSeq(hVar, oVar), tr, body);

         sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));

       }

@@ -3769,7 +3772,7 @@ namespace Microsoft.Dafny {
         }

         builder.Add(new Bpl.ReturnCmd(stmt.Tok));

       } else if (stmt is YieldStmt) {

-        throw new NotImplementedException(); // TODO

+        //KRML   throw new NotImplementedException(); // TODO

       } else if (stmt is AssignSuchThatStmt) {

         var s = (AssignSuchThatStmt)stmt;

         AddComment(builder, s, "assign-such-that statement");

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