- fixed a bug in merging fields that come from a parent trait

- added one more test

7 files changed, 69 insertions, 4 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 60e737b1..978bf5c4 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -147,14 +147,17 @@ namespace Microsoft.Dafny
         Contract.Assert(!(member is SpecialField));  // we don't expect a SpecialField to be cloned (or do we?)

         var f = (Field)member;

         Field field = new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), CloneAttributes(f.Attributes));

+        field.Inherited = member.Inherited;

         return field;

       } else if (member is Function) {

         var f = (Function)member;

         Function func = CloneFunction(f);

+        func.Inherited = member.Inherited;

         return func;

       } else {

         var m = (Method)member;

         Method method = CloneMethod(m);

+        method.Inherited = member.Inherited;

         return method;

       }

     }

@@ -202,6 +205,8 @@ namespace Microsoft.Dafny
 

     public Formal CloneFormal(Formal formal) {

       Formal f = new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost);

+      if (f.Type is UserDefinedType && formal.Type is UserDefinedType)

+          ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(formal.Type)).ResolvedClass;

       return f;

     }

 

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 0b8c4254..547b48d6 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -249,7 +249,7 @@ namespace Microsoft.Dafny {
             Indent(indent);

             if (cl.TraitObj != null && cl.TraitObj is TraitDecl)

             {

-                wr.WriteLine("public class @{0} : @{1}", cl.CompileName, ((UserDefinedType)cl.TraitTyp).tok);

+                wr.WriteLine("public class @{0} : @{1}", cl.CompileName, cl.TraitObj.Name);

             }

             else

                 wr.Write("public class @{0}", cl.CompileName);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 167b56c2..49a71fb0 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2730,6 +2730,7 @@ namespace Microsoft.Dafny
     void InheritTraitMembers(ClassDecl cl) {

       Contract.Requires(cl != null);

 

+      RefinementCloner cloner = new RefinementCloner(cl.Module);

       //merging class members with parent members if any

       if (cl.TraitObj != null) {

         var clMembers = classMembers[cl];

@@ -2809,7 +2810,18 @@ namespace Microsoft.Dafny
           } else {

             //the member is not already in the class

             // enter the trait member in the symbol table for the class

-            clMembers.Add(traitMem.Key, traitMem.Value);

+            //clMembers.Add(traitMem.Key, traitMem.Value);

+              MemberDecl classNewMember = cloner.CloneMember(traitMem.Value);

+              if (classNewMember is Field)

+              {

+                  Field f = (Field)classNewMember;

+                  if (f.Type is UserDefinedType)

+                      ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(((Field)(traitMem.Value)).Type)).ResolvedClass;

+              }

+              classNewMember.EnclosingClass = cl;

+              classNewMember.Inherited = true;

+              classMembers[cl].Add(traitMem.Key, classNewMember);

+              cl.Members.Add(classNewMember);

           }

         }//foreach

 

@@ -4027,6 +4039,9 @@ namespace Microsoft.Dafny
             successSoFar = UnifyTypes(aa.TypeArgs[i], bb.TypeArgs[i]);

           }

           return successSoFar;

+        }

+        else if ((bb.ResolvedClass is TraitDecl) && (aa.ResolvedClass is TraitDecl)) {

+            return ((TraitDecl)bb.ResolvedClass).FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName;

         } else if ((bb.ResolvedClass is ClassDecl) && (aa.ResolvedClass is TraitDecl)) {

           return ((ClassDecl)bb.ResolvedClass).TraitObj.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName;

         } else if ((aa.ResolvedClass is ClassDecl) && (bb.ResolvedClass is TraitDecl)) {

diff --git a/Test/dafny0/Trait/TraitOverride1.dfy.expect b/Test/dafny0/Trait/TraitOverride1.dfy.expect
index c90560b0..0f7b49e3 100644
--- a/Test/dafny0/Trait/TraitOverride1.dfy.expect
+++ b/Test/dafny0/Trait/TraitOverride1.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 52 verified, 0 errors

+Dafny program verifier finished with 62 verified, 0 errors

diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
index b59d7b80..6849499c 100644
--- a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
+++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
@@ -5,4 +5,4 @@ Execution trace:
     (0,0): anon2

     (0,0): anon6_Then

 

-Dafny program verifier finished with 7 verified, 1 error

+Dafny program verifier finished with 9 verified, 1 error

diff --git a/Test/dafny0/Trait/Traits-Fields.dfy b/Test/dafny0/Trait/Traits-Fields.dfy
new file mode 100644
index 00000000..c215ecf8
--- /dev/null
+++ b/Test/dafny0/Trait/Traits-Fields.dfy
@@ -0,0 +1,38 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+trait J

+{

+  var x: int;

+}

+

+class C extends J

+{

+

+}

+

+method Main() 

+{

+  var c := new C;

+  var j: J := new C;

+

+  j.x := 8;

+  c.x := 9;

+  assert j.x + 1 == c.x;

+

+  j := c;

+  //assert j.x == 9;

+

+  print "j"; Print(j);

+  print "c"; Print(c);

+

+  c := null;

+  assert j != null;

+  j := null;

+}

+

+method Print(j: J)

+  requires j != null;

+{

+  print ".x = ", j.x, "\n";

+}

diff --git a/Test/dafny0/Trait/Traits-Fields.dfy.expect b/Test/dafny0/Trait/Traits-Fields.dfy.expect
new file mode 100644
index 00000000..4e367bf5
--- /dev/null
+++ b/Test/dafny0/Trait/Traits-Fields.dfy.expect
@@ -0,0 +1,7 @@
+

+Dafny program verifier finished with 4 verified, 0 errors

+Program compiled successfully

+Running...

+

+j.x = 9

+c.x = 9