1 files changed, 92 insertions, 5 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 0f3d473a..a13a4dae 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -13,6 +13,7 @@ using System;
 using System.Collections.Generic;
 using System.Numerics;
 using System.Diagnostics.Contracts;
+using IToken = Microsoft.Boogie.IToken;
 
 namespace Microsoft.Dafny {
   public class RefinementTransformer
@@ -57,7 +58,7 @@ namespace Microsoft.Dafny {
       foreach (var d in prev.TopLevelDecls) {
         int index;
         if (!declaredNames.TryGetValue(d.Name, out index)) {
-          m.TopLevelDecls.Add(CreateRefinementCopy(d, m));
+          m.TopLevelDecls.Add(CloneDeclaration(d, m));
         } else {
           var nw = m.TopLevelDecls[index];
           if (d is ArbitraryTypeDecl) {
@@ -82,20 +83,32 @@ namespace Microsoft.Dafny {
       }
     }
 
-    TopLevelDecl CreateRefinementCopy(TopLevelDecl d, ModuleDecl m) {
+    IToken Tok(IToken tok) {
+      // TODO: do something that makes it clear that this token is from a copy
+      return tok;
+    }
+
+    // -------------------------------------------------- Cloning ---------------------------------------------------------------
+
+    TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDecl m) {
       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(dd.tok, dd.Name, m, null);
+        return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, null);
       } else if (d is DatatypeDecl) {
         var dd = (DatatypeDecl)d;
-        var dt = new DatatypeDecl(dd.tok, dd.Name, m, dd.TypeArgs/*TODO*/, dd.Ctors/*TODO*/, null);
+        var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+        var ctors = dd.Ctors.ConvertAll(CloneCtor);
+        var dt = new DatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
         return dt;
       } else if (d is ClassDecl) {
         var dd = (ClassDecl)d;
-        var cl = new ClassDecl(dd.tok, dd.Name, m, dd.TypeArgs/*TODO*/, dd.Members/*TODO*/, null);
+        var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+        var mm = dd.Members.ConvertAll(CloneMember);
+        var cl = new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, null);
         return cl;
       } else {
         Contract.Assert(false);  // unexpected declaration
@@ -103,6 +116,80 @@ 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);
+    }
+
+    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);
+      } else if (member is Function) {
+        var f = (Function)member;
+        var tps = f.TypeArgs.ConvertAll(CloneTypeParam);
+        return new Function(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, f.IsUnlimited, tps, f.Formals.ConvertAll(CloneFormal), CloneType(f.ResultType),
+          f.Req.ConvertAll(CloneExpr), f.Reads.ConvertAll(CloneFrameExpr), f.Ens.ConvertAll(CloneExpr), CloneSpecExpr(f.Decreases), CloneExpr(f.Body), null);
+      } else {
+        var m = (Method)member;
+        var tps = m.TypeArgs.ConvertAll(CloneTypeParam);
+        return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, m.Ins.ConvertAll(CloneFormal), m.Outs.ConvertAll(CloneFormal),
+          m.Req.ConvertAll(CloneMayBeFreeExpr), CloneSpecFrameExpr(m.Mod), m.Ens.ConvertAll(CloneMayBeFreeExpr), CloneSpecExpr(m.Decreases), CloneBlockStmt(m.Body), null);
+      }
+    }
+
+    Type CloneType(Type t) {
+      // TODO
+      return t;
+    }
+
+    Formal CloneFormal(Formal formal) {
+      // TODO
+      return formal;
+    }
+
+    Specification<Expression> CloneSpecExpr(Specification<Expression> spec) {
+      // TODO
+      return spec;
+    }
+
+    Specification<FrameExpression> CloneSpecFrameExpr(Specification<FrameExpression> frame) {
+      // TODO
+      return frame;
+    }
+
+    FrameExpression CloneFrameExpr(FrameExpression frame) {
+      // TODO
+      return frame;
+    }
+
+    MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) {
+      // TODO
+      return expr;
+    }
+
+    Expression CloneExpr(Expression expr) {
+      // TODO
+      return expr;
+    }
+
+    BlockStmt CloneBlockStmt(BlockStmt stmt) {
+      // TODO
+      return stmt;
+    }
+
+    Statement CloneStmt(Statement stmt) {
+      // TODO
+      return stmt;
+    }
+
+    // -------------------------------------------------- Merging ---------------------------------------------------------------
+
     DatatypeDecl MergeDatatype(DatatypeDecl nw, DatatypeDecl prev) {
       // TODO
       return nw;