Dafny: filled in more cloning for the refinement transformations

3 files changed, 614 insertions, 80 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 357b2b60..9e69b432 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3086,7 +3086,7 @@ namespace Microsoft.Dafny {
 

   public class Specification<T> where T : class

   {

-    public List<T/*!*/> Expressions;

+    public List<T> Expressions;

 

     [ContractInvariantMethod]

     private void ObjectInvariant()

@@ -3095,7 +3095,7 @@ namespace Microsoft.Dafny {
     }

 

 

-    public Specification(List<T/*!*/> exprs, Attributes attrs)

+    public Specification(List<T> exprs, Attributes attrs)

     {

       Contract.Requires(exprs == null || cce.NonNullElements<T>(exprs));

       Expressions = exprs;

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index a13a4dae..8b46c897 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -7,6 +7,9 @@
 // constructed as a refinement of another.  It is invoked during program resolution,

 // so the transformation is done syntactically.  Upon return from the RefinementTransformer,

 // the caller is expected to resolve the resulting module.

+//

+// As for now (and perhaps this is always the right thing to do), attributes do

+// not survive the transformation.

 //-----------------------------------------------------------------------------

 

 using System;

@@ -16,6 +19,43 @@ using System.Diagnostics.Contracts;
 using IToken = Microsoft.Boogie.IToken;

 

 namespace Microsoft.Dafny {

+  public class RefinementToken : IToken

+  {

+    IToken tok;

+    public RefinementToken(IToken tok)

+    {

+      this.tok = tok;

+    }

+

+    public int kind {

+      get { return tok.kind; }

+      set { throw new NotSupportedException(); }

+    }

+    public string filename {

+      get { return tok.filename; }

+      set { throw new NotSupportedException(); }

+    }

+    public int pos {

+      get { return tok.pos; }

+      set { throw new NotSupportedException(); }

+    }

+    public int col {

+      get { return tok.col; }

+      set { throw new NotSupportedException(); }

+    }

+    public int line {

+      get { return tok.line; }

+      set { throw new NotSupportedException(); }

+    }

+    public string/*!*/ val {

+      get { return tok.val; }

+      set { throw new NotSupportedException(); }

+    }

+    public bool IsValid {

+      get { return tok.IsValid; }

+    }

+  }

+

   public class RefinementTransformer

   {

     ResolutionErrorReporter reporter;

@@ -30,8 +70,6 @@ namespace Microsoft.Dafny {
 

       var prev = m.RefinementBase;

 

-      // TODO: What to do with the attributes of prev?  Should they be copied as well?

-

       // Include the imports of the base.  Note, prev is itself NOT added as an import

       // of m; instead, the contents from prev is merged directly into m.

       // (Here, we change the import declarations.  But edges for these imports will

@@ -84,8 +122,7 @@ namespace Microsoft.Dafny {
     }

 

     IToken Tok(IToken tok) {

-      // TODO: do something that makes it clear that this token is from a copy

-      return tok;

+      return new RefinementToken(tok);

     }

 

     // -------------------------------------------------- Cloning ---------------------------------------------------------------

@@ -94,7 +131,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(d != null);

       Contract.Requires(m != null);

 

-      // top-level declarations clone their tokens

       if (d is ArbitraryTypeDecl) {

         var dd = (ArbitraryTypeDecl)d;

         return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, null);

@@ -117,16 +153,14 @@ namespace Microsoft.Dafny {
     }

 

     DatatypeCtor CloneCtor(DatatypeCtor ct) {

-      // datatype constructors clone their tokens

       return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), null);

     }

 

     TypeParameter CloneTypeParam(TypeParameter tp) {

-      return new TypeParameter(tp.tok, tp.Name);

+      return new TypeParameter(Tok(tp.tok), tp.Name);

     }

 

     MemberDecl CloneMember(MemberDecl member) {

-      // members clone their tokens

       if (member is Field) {

         var f = (Field)member;

         return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null);

@@ -144,48 +178,553 @@ namespace Microsoft.Dafny {
     }

 

     Type CloneType(Type t) {

-      // TODO

-      return t;

+      if (t is BasicType) {

+        return t;

+      } else if (t is SetType) {

+        var tt = (SetType)t;

+        return new SetType(tt.Arg);

+      } else if (t is SeqType) {

+        var tt = (SeqType)t;

+        return new SeqType(tt.Arg);

+      } else if (t is MultiSetType) {

+        var tt = (MultiSetType)t;

+        return new MultiSetType(tt.Arg);

+      } else if (t is UserDefinedType) {

+        var tt = (UserDefinedType)t;

+        return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType));

+      } else if (t is InferredTypeProxy) {

+        return new InferredTypeProxy();

+      } else {

+        Contract.Assert(false);  // unexpected type (e.g., no other type proxies are expected at this time)

+        return null;  // to please compiler

+      }

     }

 

     Formal CloneFormal(Formal formal) {

-      // TODO

-      return formal;

+      return new Formal(Tok(formal.tok), formal.Name, formal.Type, formal.InParam, formal.IsGhost);

+    }

+

+    BoundVar CloneBoundVar(BoundVar bv) {

+      return new BoundVar(Tok(bv.tok), bv.Name, bv.Type);

     }

 

     Specification<Expression> CloneSpecExpr(Specification<Expression> spec) {

-      // TODO

-      return spec;

+      var ee = spec.Expressions == null ? null : spec.Expressions.ConvertAll(CloneExpr);

+      return new Specification<Expression>(ee, null);

     }

 

     Specification<FrameExpression> CloneSpecFrameExpr(Specification<FrameExpression> frame) {

-      // TODO

-      return frame;

+      var ee = frame.Expressions == null ? null : frame.Expressions.ConvertAll(CloneFrameExpr);

+      return new Specification<FrameExpression>(ee, null);

     }

 

     FrameExpression CloneFrameExpr(FrameExpression frame) {

-      // TODO

-      return frame;

+      return new FrameExpression(CloneExpr(frame.E), frame.FieldName);

+    }

+

+    Attributes.Argument CloneAttrArg(Attributes.Argument aa) {

+      if (aa.E != null) {

+        return new Attributes.Argument(Tok(aa.Tok), CloneExpr(aa.E));

+      } else {

+        return new Attributes.Argument(Tok(aa.Tok), aa.S);

+      }

     }

 

     MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) {

-      // TODO

-      return expr;

+      return new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree);

     }

 

     Expression CloneExpr(Expression expr) {

-      // TODO

-      return expr;

+#if SOON

+      if (expr is LiteralExpr) {

+        var e = (LiteralExpr)expr;

+        if (e.Value == null) {

+          return new LiteralExpr(Tok(e.tok));

+        } else if (e.Value is bool) {

+          return new LiteralExpr(Tok(e.tok), (bool)e.Value);

+        } else {

+          return new LiteralExpr(Tok(e.tok), (BigInteger)e.Value);

+        }

+

+      } else if (expr is ThisExpr) {

+        wr.Write("this");

+

+      } else if (expr is IdentifierExpr) {

+        wr.Write(((IdentifierExpr)expr).Name);

+

+      } else if (expr is DatatypeValue) {

+        DatatypeValue dtv = (DatatypeValue)expr;

+        wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName);

+        if (dtv.Arguments.Count != 0) {

+          wr.Write("(");

+          PrintExpressionList(dtv.Arguments);

+          wr.Write(")");

+        }

+

+      } else if (expr is DisplayExpression) {

+        DisplayExpression e = (DisplayExpression)expr;

+        if (e is MultiSetDisplayExpr) wr.Write("multiset");

+        wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "{" : "[");

+        PrintExpressionList(e.Elements);

+        wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "}" : "]");

+

+      } else if (expr is FieldSelectExpr) {

+        FieldSelectExpr e = (FieldSelectExpr)expr;

+        // determine if parens are needed

+        int opBindingStrength = 0x70;

+        bool parensNeeded = !(e.Obj is ImplicitThisExpr) &&

+          opBindingStrength < contextBindingStrength ||

+          (fragileContext && opBindingStrength == contextBindingStrength);

+

+        if (parensNeeded) { wr.Write("("); }

+        if (!(e.Obj is ImplicitThisExpr)) {

+          PrintExpr(e.Obj, opBindingStrength, false, false, -1);

+          wr.Write(".");

+        }

+        wr.Write(e.FieldName);

+        if (parensNeeded) { wr.Write(")"); }

+

+      } else if (expr is SeqSelectExpr) {

+        SeqSelectExpr e = (SeqSelectExpr)expr;

+        // determine if parens are needed

+        int opBindingStrength = 0x70;

+        bool parensNeeded = opBindingStrength < contextBindingStrength ||

+          (fragileContext && opBindingStrength == contextBindingStrength);

+

+        if (parensNeeded) { wr.Write("("); }

+        PrintExpr(e.Seq, 0x00, false, false, indent);  // BOGUS: fix me

+        wr.Write("[");

+        if (e.SelectOne) {

+          Contract.Assert( e.E0 != null);

+          PrintExpression(e.E0);

+        } else {

+          if (e.E0 != null) {

+            PrintExpression(e.E0);

+          }

+          wr.Write(e.E0 != null && e.E1 != null ? " .. " : "..");

+          if (e.E1 != null) {

+            PrintExpression(e.E1);

+          }

+        }

+        wr.Write("]");

+        if (parensNeeded) { wr.Write(")"); }

+

+      } else if (expr is MultiSelectExpr) {

+        MultiSelectExpr e = (MultiSelectExpr)expr;

+        // determine if parens are needed

+        int opBindingStrength = 0x70;

+        bool parensNeeded = opBindingStrength < contextBindingStrength ||

+          (fragileContext && opBindingStrength == contextBindingStrength);

+

+        if (parensNeeded) { wr.Write("("); }

+        PrintExpr(e.Array, 0x00, false, false, indent);  // BOGUS: fix me

+        string prefix = "[";

+        foreach (Expression idx in e.Indices) {

+          Contract.Assert(idx != null);

+          wr.Write(prefix);

+          PrintExpression(idx);

+          prefix = ", ";

+        }

+        wr.Write("]");

+        if (parensNeeded) { wr.Write(")"); }

+

+      } else if (expr is SeqUpdateExpr) {

+        SeqUpdateExpr e = (SeqUpdateExpr)expr;

+        // determine if parens are needed

+        int opBindingStrength = 0x70;

+        bool parensNeeded = opBindingStrength < contextBindingStrength ||

+          (fragileContext && opBindingStrength == contextBindingStrength);

+

+        if (parensNeeded) { wr.Write("("); }

+        PrintExpr(e.Seq, 00, false, false, indent);  // BOGUS: fix me

+        wr.Write("[");

+        PrintExpression(e.Index);

+        wr.Write(" := ");

+        PrintExpression(e.Value);

+        wr.Write("]");

+        if (parensNeeded) { wr.Write(")"); }

+

+      } else if (expr is FunctionCallExpr) {

+        FunctionCallExpr e = (FunctionCallExpr)expr;

+        // determine if parens are needed

+        int opBindingStrength = 0x70;

+        bool parensNeeded = !(e.Receiver is ImplicitThisExpr) &&

+          opBindingStrength < contextBindingStrength ||

+          (fragileContext && opBindingStrength == contextBindingStrength);

+

+        if (parensNeeded) { wr.Write("("); }

+        if (!(e.Receiver is ImplicitThisExpr)) {

+          PrintExpr(e.Receiver, opBindingStrength, false, false, -1);

+          wr.Write(".");

+        }

+        wr.Write(e.Name);

+        wr.Write("(");

+        PrintExpressionList(e.Args);

+        wr.Write(")");

+        if (parensNeeded) { wr.Write(")"); }

+

+      } else if (expr is OldExpr) {

+        wr.Write("old(");

+        PrintExpression(((OldExpr)expr).E);

+        wr.Write(")");

+

+      } else if (expr is MultiSetFormingExpr) {

+        wr.Write("multiset(");

+        PrintExpression(((MultiSetFormingExpr)expr).E);

+        wr.Write(")");

+

+      } else if (expr is FreshExpr) {

+        wr.Write("fresh(");

+        PrintExpression(((FreshExpr)expr).E);

+        wr.Write(")");

+

+      } else if (expr is AllocatedExpr) {

+        wr.Write("allocated(");

+        PrintExpression(((AllocatedExpr)expr).E);

+        wr.Write(")");

+

+      } else if (expr is UnaryExpr) {

+        UnaryExpr e = (UnaryExpr)expr;

+        if (e.Op == UnaryExpr.Opcode.SeqLength) {

+          wr.Write("|");

+          PrintExpression(e.E);

+          wr.Write("|");

+        } else {

+          // Prefix operator.

+          // determine if parens are needed

+          string op;

+          int opBindingStrength;

+          switch (e.Op) {

+            case UnaryExpr.Opcode.SetChoose:

+              op = "choose ";  opBindingStrength = 0;  break;

+            case UnaryExpr.Opcode.Not:

+              op = "!";  opBindingStrength = 0x60;  break;

+            default:

+              Contract.Assert(false); throw new cce.UnreachableException();  // unexpected unary opcode

+          }

+          bool parensNeeded = opBindingStrength < contextBindingStrength ||

+            (fragileContext && opBindingStrength == contextBindingStrength);

+

+          bool containsNestedNot = e.E is ParensExpression &&

+                                ((ParensExpression)e.E).E is UnaryExpr &&

+                                ((UnaryExpr)((ParensExpression)e.E).E).Op == UnaryExpr.Opcode.Not;

+

+          if (parensNeeded) { wr.Write("("); }

+          wr.Write(op);

+          PrintExpr(e.E, opBindingStrength, containsNestedNot, parensNeeded || isRightmost, -1);

+          if (parensNeeded) { wr.Write(")"); }

+        }

+

+      } else if (expr is BinaryExpr) {

+        BinaryExpr e = (BinaryExpr)expr;

+        // determine if parens are needed

+        int opBindingStrength;

+        bool fragileLeftContext = false;  // false means "allow same binding power on left without parens"

+        bool fragileRightContext = false;  // false means "allow same binding power on right without parens"

+        switch (e.Op)

+        {

+          case BinaryExpr.Opcode.Add:

+            opBindingStrength = 0x40; break;

+          case BinaryExpr.Opcode.Sub:

+            opBindingStrength = 0x40; fragileRightContext = true; break;

+          case BinaryExpr.Opcode.Mul:

+            opBindingStrength = 0x50; break;

+          case BinaryExpr.Opcode.Div:

+          case BinaryExpr.Opcode.Mod:

+            opBindingStrength = 0x50; fragileRightContext = true; break;

+          case BinaryExpr.Opcode.Eq:

+          case BinaryExpr.Opcode.Neq:

+          case BinaryExpr.Opcode.Gt:

+          case BinaryExpr.Opcode.Ge:

+          case BinaryExpr.Opcode.Lt:

+          case BinaryExpr.Opcode.Le:

+          case BinaryExpr.Opcode.Disjoint:

+          case BinaryExpr.Opcode.In:

+          case BinaryExpr.Opcode.NotIn:

+            opBindingStrength = 0x30; fragileLeftContext = fragileRightContext = true; break;

+          case BinaryExpr.Opcode.And:

+            opBindingStrength = 0x20; break;

+          case BinaryExpr.Opcode.Or:

+            opBindingStrength = 0x21; break;

+          case BinaryExpr.Opcode.Imp:

+            opBindingStrength = 0x10; fragileLeftContext = true; break;

+          case BinaryExpr.Opcode.Iff:

+            opBindingStrength = 0x08; break;

+          default:

+            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected binary operator

+        }

+        int opBS = opBindingStrength & 0xF8;

+        int ctxtBS = contextBindingStrength & 0xF8;

+        bool parensNeeded = opBS < ctxtBS ||

+          (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));

+

+        string op = BinaryExpr.OpcodeString(e.Op);

+        if (parensNeeded) { wr.Write("("); }

+        if (0 <= indent && e.Op == BinaryExpr.Opcode.And) {

+          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, indent);

+          wr.WriteLine(" {0}", op);

+          Indent(indent);

+          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, indent);

+        } else if (0 <= indent && e.Op == BinaryExpr.Opcode.Imp) {

+          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, indent);

+          wr.WriteLine(" {0}", op);

+          int ind = indent + IndentAmount;

+          Indent(ind);

+          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, ind);

+        } else {

+          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, -1);

+          wr.Write(" {0} ", op);

+          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, -1);

+        }

+        if (parensNeeded) { wr.Write(")"); }

+

+      } else if (expr is ChainingExpression) {

+        var e = (ChainingExpression)expr;

+        // determine if parens are needed

+        int opBindingStrength = 0x30;

+        int opBS = opBindingStrength & 0xF8;

+        int ctxtBS = contextBindingStrength & 0xF8;

+        bool parensNeeded = opBS < ctxtBS ||

+          (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));

+

+        if (parensNeeded) { wr.Write("("); }

+        PrintExpr(e.Operands[0], opBindingStrength, true, false, -1);

+        for (int i = 0; i < e.Operators.Count; i++) {

+          string op = BinaryExpr.OpcodeString(e.Operators[i]);

+          wr.Write(" {0} ", op);

+          PrintExpr(e.Operands[i+1], opBindingStrength, true, i == e.Operators.Count - 1 && (parensNeeded || isRightmost), -1);

+        }

+        if (parensNeeded) { wr.Write(")"); }

+

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        bool parensNeeded = !isRightmost;

+        if (parensNeeded) { wr.Write("("); }

+        string sep = "";

+        foreach (var v in e.Vars) {

+          wr.Write("{0}{1}", sep, v.Name);

+          PrintType(": ", v.Type);

+          sep = ", ";

+        }

+        wr.Write(" := ");

+        PrintExpressionList(e.RHSs);

+        wr.Write("; ");

+        PrintExpression(e.Body);

+        if (parensNeeded) { wr.Write(")"); }

+

+

+      } else if (expr is QuantifierExpr) {

+        QuantifierExpr e = (QuantifierExpr)expr;

+        bool parensNeeded = !isRightmost;

+        if (parensNeeded) { wr.Write("("); }

+        wr.Write(e is ForallExpr ? "forall " : "exists ");

+        PrintQuantifierDomain(e.BoundVars, e.Attributes, e.Range);

+        wr.Write(" :: ");

+        if (0 <= indent) {

+          int ind = indent + IndentAmount;

+          wr.WriteLine();

+          Indent(ind);

+          PrintExpression(e.Term, ind);

+        } else {

+          PrintExpression(e.Term);

+        }

+        if (parensNeeded) { wr.Write(")"); }

+

+      } else if (expr is SetComprehension) {

+        var e = (SetComprehension)expr;

+        bool parensNeeded = !isRightmost;

+        if (parensNeeded) { wr.Write("("); }

+        wr.Write("set ");

+        string sep = "";

+        foreach (BoundVar bv in e.BoundVars) {

+          wr.Write("{0}{1}", sep, bv.Name);

+          sep = ", ";

+          PrintType(": ", bv.Type);

+        }

+        PrintAttributes(e.Attributes);

+        wr.Write(" | ");

+        PrintExpression(e.Range);

+        if (!e.TermIsImplicit) {

+          wr.Write(" :: ");

+          PrintExpression(e.Term);

+        }

+        if (parensNeeded) { wr.Write(")"); }

+

+      } else if (expr is WildcardExpr) {

+        wr.Write("*");

+

+      } else if (expr is PredicateExpr) {

+        var e = (PredicateExpr)expr;

+        bool parensNeeded = !isRightmost;

+        if (parensNeeded) { wr.Write("("); }

+        wr.Write("{0} ", e.Kind);

+        PrintExpression(e.Guard);

+        wr.Write("; ");

+        PrintExpression(e.Body);

+        if (parensNeeded) { wr.Write(")"); }

+

+      } else if (expr is ITEExpr) {

+        ITEExpr ite = (ITEExpr)expr;

+        bool parensNeeded = !isRightmost;

+        if (parensNeeded) { wr.Write("("); }

+        wr.Write("if ");

+        PrintExpression(ite.Test);

+        wr.Write(" then ");

+        PrintExpression(ite.Thn);

+        wr.Write(" else ");

+        PrintExpression(ite.Els);

+        if (parensNeeded) { wr.Write(")"); }

+

+      } else if (expr is ParensExpression) {

+        var e = (ParensExpression)expr;

+        // printing of parentheses is done optimally, not according to the parentheses in the given program

+        PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, indent);

+

+      } else if (expr is IdentifierSequence) {

+        var e = (IdentifierSequence)expr;

+        string sep = "";

+        foreach (var id in e.Tokens) {

+          wr.Write("{0}{1}", sep, id.val);

+          sep = ".";

+        }

+        if (e.Arguments != null) {

+          wr.Write("(");

+          PrintExpressionList(e.Arguments);

+          wr.Write(")");

+        }

+

+      } else if (expr is MatchExpr) {

+        Contract.Assert(false); throw new cce.UnreachableException();  // MatchExpr is an extended expression and should be printed only using PrintExtendedExpr

+      } else {

+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

+      }

+#else

+      return expr;  // TODO

+#endif

+    }

+

+    AssignmentRhs CloneRHS(AssignmentRhs rhs) {

+      if (rhs is ExprRhs) {

+        var r = (ExprRhs)rhs;

+        return new ExprRhs(r.Expr);

+      } else if (rhs is HavocRhs) {

+        return new HavocRhs(Tok(rhs.Tok));

+      } else {

+        var r = (TypeRhs)rhs;

+        if (r.ArrayDimensions != null) {

+          return new TypeRhs(Tok(r.Tok), r.EType, r.ArrayDimensions.ConvertAll(CloneExpr));

+        } else if (r.InitCall != null) {

+          return new TypeRhs(Tok(r.Tok), r.EType, (CallStmt)CloneStmt(r.InitCall));

+        } else {

+          return new TypeRhs(Tok(r.Tok), r.EType);

+        }

+      }

     }

 

     BlockStmt CloneBlockStmt(BlockStmt stmt) {

-      // TODO

-      return stmt;

+      if (stmt == null) {

+        return null;

+      } else {

+        return new BlockStmt(Tok(stmt.Tok), stmt.Body.ConvertAll(CloneStmt));

+      }

     }

 

     Statement CloneStmt(Statement stmt) {

-      // TODO

-      return stmt;

+      if (stmt == null) {

+        return null;

+      }

+

+      Statement r;

+      if (stmt is AssertStmt) {

+        var s = (AssertStmt)stmt;

+        r = new AssertStmt(Tok(s.Tok), s.Expr);

+

+      } else if (stmt is AssumeStmt) {

+        var s = (AssumeStmt)stmt;

+        r = new AssumeStmt(Tok(s.Tok), s.Expr);

+

+      } else if (stmt is PrintStmt) {

+        var s = (PrintStmt)stmt;

+        r = new PrintStmt(Tok(s.Tok), s.Args.ConvertAll(CloneAttrArg));

+

+      } else if (stmt is BreakStmt) {

+        var s = (BreakStmt)stmt;

+        if (s.TargetLabel != null) {

+          r = new BreakStmt(Tok(s.Tok), s.TargetLabel);

+        } else {

+          r = new BreakStmt(Tok(s.Tok), s.BreakCount);

+        }

+

+      } else if (stmt is ReturnStmt) {

+        var s = (ReturnStmt)stmt;

+        r = new ReturnStmt(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));

+

+      } else if (stmt is VarDecl) {

+        var s = (VarDecl)stmt;

+        r = new VarDecl(Tok(s.Tok), s.Name, s.OptionalType, s.IsGhost);

+

+      } else if (stmt is CallStmt) {

+        var s = (CallStmt)stmt;

+        r = new CallStmt(Tok(s.Tok), s.Lhs.ConvertAll(CloneExpr), CloneExpr(s.Receiver), s.MethodName, s.Args.ConvertAll(CloneExpr));

+

+      } else if (stmt is BlockStmt) {

+        r = CloneBlockStmt((BlockStmt)stmt);

+

+      } else if (stmt is IfStmt) {

+        var s = (IfStmt)stmt;

+        r = new IfStmt(Tok(s.Tok), CloneExpr(s.Guard), CloneStmt(s.Thn), CloneStmt(s.Els));

+

+      } else if (stmt is AlternativeStmt) {

+        var s = (AlternativeStmt)stmt;

+        r = new AlternativeStmt(Tok(s.Tok), s.Alternatives.ConvertAll(CloneGuardedAlternative));

+

+      } else if (stmt is WhileStmt) {

+        var s = (WhileStmt)stmt;

+        r = new WhileStmt(Tok(s.Tok), CloneExpr(s.Guard), s.Invariants.ConvertAll(CloneMayBeFreeExpr), CloneSpecExpr(s.Decreases), CloneSpecFrameExpr(s.Mod), CloneStmt(s.Body));

+

+      } else if (stmt is AlternativeLoopStmt) {

+        var s = (AlternativeLoopStmt)stmt;

+        r = new AlternativeLoopStmt(Tok(s.Tok), s.Invariants.ConvertAll(CloneMayBeFreeExpr), CloneSpecExpr(s.Decreases), CloneSpecFrameExpr(s.Mod), s.Alternatives.ConvertAll(CloneGuardedAlternative));

+

+      } else if (stmt is ParallelStmt) {

+        var s = (ParallelStmt)stmt;

+        r = new ParallelStmt(Tok(s.Tok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));

+

+      } else if (stmt is MatchStmt) {

+        var s = (MatchStmt)stmt;

+        r = new MatchStmt(Tok(s.Tok), CloneExpr(s.Source), s.Cases.ConvertAll(c => new MatchCaseStmt(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), c.Body.ConvertAll(CloneStmt))));

+

+      } else if (stmt is UpdateStmt) {

+        var s = (UpdateStmt)stmt;

+        r = new UpdateStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), s.Rhss.ConvertAll(CloneRHS), s.CanMutateKnownState);

+

+      } else if (stmt is VarDeclStmt) {

+        var s = (VarDeclStmt)stmt;

+        r = new VarDeclStmt(Tok(s.Tok), s.Lhss.ConvertAll(c => (VarDecl)CloneStmt(c)), (UpdateStmt)CloneStmt(s.Update));

+

+      } else {

+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement

+      }

+

+      // add labels to the cloned statement

+      AddStmtLabels(r, stmt.Labels);

+

+      return r;

+    }

+

+    void AddStmtLabels(Statement s, LabelNode node) {

+      if (node != null) {

+        AddStmtLabels(s, node.Next);

+        s.Labels = new LabelNode(Tok(node.Tok), node.Label, s.Labels);

+      }

+    }

+

+    GuardedAlternative CloneGuardedAlternative(GuardedAlternative alt) {

+      return new GuardedAlternative(Tok(alt.Tok), CloneExpr(alt.Guard), alt.Body.ConvertAll(CloneStmt));

     }

 

     // -------------------------------------------------- Merging ---------------------------------------------------------------

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index c9b877c9..af3fe0a7 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -177,6 +177,11 @@ namespace Microsoft.Dafny {
           var transformer = new RefinementTransformer(this);

           transformer.Construct(m);

         }

+#if TEST_REFINEMENT_TRANSFORMATION

+        var tm = new ModuleDecl(m.tok, "CloneTesting_" + m.Name, m.Name, new List<string>(), null);

+        tm.RefinementBase = m;

+        new RefinementTransformer(this).Construct(tm);

+#endif

         moduleNameInfo[m.Height] = RegisterTopLevelDecls(m.TopLevelDecls);

       }

 

@@ -1267,7 +1272,7 @@ namespace Microsoft.Dafny {
               ident.Type = ident.Var.Type;

               Contract.Assert(f.Type != null);

               formals.Add(ident);

-              // link the reciever parameter properly:

+              // link the receiver parameter properly:

               if (s.rhss[i] is TypeRhs) {

                 var r = (TypeRhs)s.rhss[i];

                 if (r.InitCall != null) {

@@ -1759,70 +1764,60 @@ namespace Microsoft.Dafny {
         if (s.Lhss.Count == 0) {

           Contract.Assert(s.Rhss.Count == 1);  // guaranteed by the parser

           Error(s, "expected method call, found expression");

-        }

-        else if (s.Lhss.Count != s.Rhss.Count) {

+        } else if (s.Lhss.Count != s.Rhss.Count) {

           Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);

-        }

-        else if (arrayRangeLhs != null && s.Lhss.Count != 1) {

+        } else if (arrayRangeLhs != null && s.Lhss.Count != 1) {

           Error(arrayRangeLhs, "array-range may not be used as LHS of multi-assignment; use separate assignment statements for each array-range assignment");

-        }

-        else if (ErrorCount == prevErrorCount) {

+        } else if (ErrorCount == prevErrorCount) {

           // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment)

           for (int i = 0; i < s.Lhss.Count; i++) {

             var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, s.Rhss[i]);

             s.ResolvedStatements.Add(a);

           }

         }

-      }

-      else {

-        if (s.CanMutateKnownState) {

-          if (1 < s.Rhss.Count)

-            Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");

-          else { // it might be ok, if it is a TypeExpr

-            Contract.Assert(s.Rhss.Count == 1);

-            if (callRhs != null) {

-              Error(callRhs.Tok, "cannot have method call in return statement.");

-            }

-            else {

-              // we have a TypeExpr

-              Contract.Assert(s.Rhss[0] is TypeRhs);

-              var tr = (TypeRhs)s.Rhss[0];

-              Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call.

-              if (tr.CanAffectPreviouslyKnownExpressions) {

-                Error(tr.Tok, "can only have initialization methods which modify at most 'this'.");

-              }

+

+      } else if (s.CanMutateKnownState) {

+        if (1 < s.Rhss.Count) {

+          Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");

+        } else { // it might be ok, if it is a TypeRhs

+          Contract.Assert(s.Rhss.Count == 1);

+          if (callRhs != null) {

+            Error(callRhs.Tok, "cannot have method call in return statement.");

+          } else {

+            // we have a TypeRhs

+            Contract.Assert(s.Rhss[0] is TypeRhs);

+            var tr = (TypeRhs)s.Rhss[0];

+            Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call.

+            if (tr.CanAffectPreviouslyKnownExpressions) {

+              Error(tr.Tok, "can only have initialization methods which modify at most 'this'.");

             }

           }

         }

-        else {

-          // if there was an effectful RHS, that must be the only RHS

-          if (s.Rhss.Count != 1) {

-            Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");

-          }

-          else if (arrayRangeLhs != null) {

-            Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");

-          }

-          else if (callRhs == null) {

-            // must be a single TypeRhs

-            if (s.Lhss.Count != 1) {

-              Contract.Assert(2 <= s.Lhss.Count);  // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)

-              Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);

-            }

-            else if (ErrorCount == prevErrorCount) {

-              var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, s.Rhss[0]);

-              s.ResolvedStatements.Add(a);

-            }

+

+      } else {

+        // if there was an effectful RHS, that must be the only RHS

+        if (s.Rhss.Count != 1) {

+          Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");

+        } else if (arrayRangeLhs != null) {

+          Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");

+        } else if (callRhs == null) {

+          // must be a single TypeRhs

+          if (s.Lhss.Count != 1) {

+            Contract.Assert(2 <= s.Lhss.Count);  // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)

+            Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);

+          } else if (ErrorCount == prevErrorCount) {

+            var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, s.Rhss[0]);

+            s.ResolvedStatements.Add(a);

           }

-          else {

-            // a call statement

-            if (ErrorCount == prevErrorCount) {

-              var resolvedLhss = new List<Expression>();

-              foreach (var ll in s.Lhss) {

-                resolvedLhss.Add(ll.Resolved);

-              }

-              var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);

-              s.ResolvedStatements.Add(a);

+        } else {

+          // a call statement

+          if (ErrorCount == prevErrorCount) {

+            var resolvedLhss = new List<Expression>();

+            foreach (var ll in s.Lhss) {

+              resolvedLhss.Add(ll.Resolved);

             }

+            var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);

+            s.ResolvedStatements.Add(a);

           }

         }

       }