Dafny: added iterators; for now, only parsing and resolving (and printing and refining), no compilation or verification

1 files changed, 22 insertions, 0 deletions

diff --git a/Dafny/Cloner.cs b/Dafny/Cloner.cs
index 6d99ce9b..408e9797 100644
--- a/Dafny/Cloner.cs
+++ b/Dafny/Cloner.cs
@@ -42,6 +42,24 @@ namespace Microsoft.Dafny
         var ctors = dd.Ctors.ConvertAll(CloneCtor);

         var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes));

         return dt;

+      } else if (d is IteratorDecl) {

+        var dd = (IteratorDecl)d;

+        var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

+        var ins = dd.Ins.ConvertAll(CloneFormal);

+        var outs = dd.Outs.ConvertAll(CloneFormal);

+        var reads = CloneSpecFrameExpr(dd.Reads);

+        var mod = CloneSpecFrameExpr(dd.Modifies);

+        var decr = CloneSpecExpr(dd.Decreases);

+        var req = dd.Requires.ConvertAll(CloneMayBeFreeExpr);

+        var yreq = dd.YieldRequires.ConvertAll(CloneMayBeFreeExpr);

+        var ens = dd.Ensures.ConvertAll(CloneMayBeFreeExpr);

+        var yens = dd.YieldEnsures.ConvertAll(CloneMayBeFreeExpr);

+        var body = CloneBlockStmt(dd.Body);

+        var iter = new IteratorDecl(Tok(dd.tok), dd.Name, dd.Module,

+          tps, ins, outs, reads, mod, decr,

+          req, ens, yreq, yens,

+          body, CloneAttributes(dd.Attributes), dd.SignatureIsOmitted);

+        return iter;

       } else if (d is ClassDecl) {

         if (d is DefaultClassDecl) {

           var dd = (ClassDecl)d;

@@ -387,6 +405,10 @@ namespace Microsoft.Dafny
         var s = (ReturnStmt)stmt;

         r = new ReturnStmt(Tok(s.Tok), s.rhss == null ? null : s.rhss.ConvertAll(CloneRHS));

 

+      } else if (stmt is YieldStmt) {

+        var s = (YieldStmt)stmt;

+        r = new YieldStmt(Tok(s.Tok), s.rhss == null ? null : s.rhss.ConvertAll(CloneRHS));

+

       } else if (stmt is AssignStmt) {

         var s = (AssignStmt)stmt;

         r = new AssignStmt(Tok(s.Tok), CloneExpr(s.Lhs), CloneRHS(s.Rhs));