diff options
Diffstat (limited to 'Dafny/Cloner.cs')
| -rw-r--r-- | Dafny/Cloner.cs | 22 |
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));
|