Merge

1 files changed, 14 insertions, 14 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 032e30a0..c94c697d 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -40,7 +40,7 @@ namespace Microsoft.Dafny
       } else if (d is TypeSynonymDecl) {

         var dd = (TypeSynonymDecl)d;

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

-        return new TypeSynonymDecl(Tok(dd.tok), dd.Name, tps, m, CloneType(dd.Rhs), CloneAttributes(dd.Attributes));

+        return new TypeSynonymDecl(Tok(dd.tok), dd.Name, tps, m, CloneType(dd.Rhs), CloneAttributes(dd.Attributes), dd);

       } else if (d is NewtypeDecl) {

         var dd = (NewtypeDecl)d;

         if (dd.Var == null) {

@@ -61,7 +61,7 @@ namespace Microsoft.Dafny
         var dd = (CoDatatypeDecl)d;

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

         var ctors = dd.Ctors.ConvertAll(CloneCtor);

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

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

         return dt;

       } else if (d is IteratorDecl) {

         var dd = (IteratorDecl)d;

@@ -97,7 +97,7 @@ namespace Microsoft.Dafny
               var dd = (TraitDecl)d;

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

               var mm = dd.Members.ConvertAll(CloneMember);

-              var cl = new TraitDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes));

+              var cl = new TraitDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd);

               return cl;

           }

       }

@@ -106,7 +106,7 @@ namespace Microsoft.Dafny
         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

         var mm = dd.Members.ConvertAll(CloneMember);

         if (d is DefaultClassDecl) {

-          return new DefaultClassDecl(m, mm);

+          return new DefaultClassDecl(m, mm, ((DefaultClassDecl)d));

         } else {

           return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType), dd);

         }

@@ -137,7 +137,7 @@ namespace Microsoft.Dafny
     }

 

     public DatatypeCtor CloneCtor(DatatypeCtor ct) {

-      return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), CloneAttributes(ct.Attributes));

+      return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), CloneAttributes(ct.Attributes), ct);

     }

 

     public TypeParameter CloneTypeParam(TypeParameter tp) {

@@ -649,16 +649,16 @@ namespace Microsoft.Dafny
 

       if (f is Predicate) {

         return new Predicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, f.IsGhost, tps, formals,

-          req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, CloneAttributes(f.Attributes), null);

+          req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, CloneAttributes(f.Attributes), null, f);

       } else if (f is InductivePredicate) {

         return new InductivePredicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, tps, formals,

-          req, reads, ens, body, CloneAttributes(f.Attributes), null);

+          req, reads, ens, body, CloneAttributes(f.Attributes), null, f);

       } else if (f is CoPredicate) {

         return new CoPredicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, tps, formals,

-          req, reads, ens, body, CloneAttributes(f.Attributes), null);

+          req, reads, ens, body, CloneAttributes(f.Attributes), null, f);

       } else {

         return new Function(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, f.IsGhost, tps, formals, CloneType(f.ResultType),

-          req, reads, ens, decreases, body, CloneAttributes(f.Attributes), null);

+          req, reads, ens, decreases, body, CloneAttributes(f.Attributes), null, f);

       }

     }

 

@@ -676,19 +676,19 @@ namespace Microsoft.Dafny
       var body = CloneBlockStmt(m.Body);

       if (m is Constructor) {

         return new Constructor(Tok(m.tok), m.Name, tps, ins,

-          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);

+          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m);

       } else if (m is InductiveLemma) {

         return new InductiveLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);

+          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m);

       } else if (m is CoLemma) {

         return new CoLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);

+          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m);

       } else if (m is Lemma) {

         return new Lemma(Tok(m.tok), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);

+          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m);

       } else {

         return new Method(Tok(m.tok), m.Name, m.HasStaticKeyword, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);

+          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m);

       }

     }

     public virtual IToken Tok(IToken tok) {