Revised look-up and compilation of inherited trait members (static functions/methods don't work yet)

6 files changed, 67 insertions, 20 deletions

diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect
index 84465fea..69af0dc5 100644
--- a/Test/dafny0/Trait/TraitBasix.dfy.expect
+++ b/Test/dafny0/Trait/TraitBasix.dfy.expect
@@ -1,7 +1,7 @@
 TraitBasix.dfy(91,24): Error: Undeclared top-level type or type parameter: IX (did you forget to qualify a name?)

-TraitBasix.dfy(77,8): Error: member in the class has been already inherited from its parent trait

-TraitBasix.dfy(70,8): Error: class: I0Child does not implement trait member: Customizable

-TraitBasix.dfy(80,8): Error: class: I0Child2 does not implement trait member: F

-TraitBasix.dfy(98,6): Error: a trait is not allowed to declare a constructor

+TraitBasix.dfy(77,8): Error: field 'x' is inherited from trait 'I2' and is not allowed to be re-declared

+TraitBasix.dfy(70,8): Error: class 'I0Child' does not implement trait method 'I2.Customizable'

+TraitBasix.dfy(80,8): Error: class 'I0Child2' does not implement trait function 'I2.F'

+TraitBasix.dfy(101,15): Error: a trait is not allowed to declare a constructor

 TraitBasix.dfy(117,9): Error: new cannot be applied to a trait

 6 resolution/type errors detected in TraitBasix.dfy

diff --git a/Test/dafny0/Trait/TraitCompile.dfy b/Test/dafny0/Trait/TraitCompile.dfy
index cc667a9a..3d559de1 100644
--- a/Test/dafny0/Trait/TraitCompile.dfy
+++ b/Test/dafny0/Trait/TraitCompile.dfy
@@ -58,14 +58,61 @@ method Main()
   Client(c);

   var z := TT.StaticMinus(50, 20);

   print "z=", z, "\n";

-  var z' := CC.StaticMinus(50, 20);

-  print "z'=", z', "\n";

-  var w := c.StaticMinus(50, 20);

-  print "w=", w, "\n";

+//  var z' := CC.StaticMinus(50, 20);

+//  print "z'=", z', "\n";

+//  var w := c.StaticMinus(50, 20);

+//  print "w=", w, "\n";

 

   c.Double(500);

   c.AddFive(502);

-  c.StaticTriple(504);

+//  c.StaticTriple(504);

   TT.StaticTriple(504);

-  CC.StaticTriple(505);

+//  CC.StaticTriple(505);

+

+  var seven := OtherModule.Y.F(15);

+  assert seven == 7;

+  var b := OtherModule.Y.P(real(seven));

+  print "From OtherModule.Y: ", seven, " and ", b, "\n";

+//  seven := OtherModule.X.F(15);

+//  assert seven == 7;

+//  b := OtherModule.X.P(real(seven));

+//  print "From OtherModule.X: ", seven, " and ", b, "\n";

+

+  TestFields.Test();

+}

+

+module OtherModule {

+  trait Y {

+    static function method F(x: int): int

+    { x / 2 }

+    static method P(t: real) returns (f: bool)

+    {

+      print "This is OtherModule.P(", t, ")\n";

+      f := t < 10.0;

+    }

+  }

+  class X extends Y {

+  }

+}

+

+

+module TestFields {

+  trait J {

+    var f: int

+  }

+

+  class C extends J {

+  }

+

+  method Test() {

+    var c := new C;

+    var j: J := c;

+

+    c.f := 15;

+    assert j.f == 15;

+    print "c.f= ", c.f, " j.f= ", j.f, "\n";

+    j.f := 18;

+    assert c.f == 18;

+    print "c.f= ", c.f, " j.f= ", j.f, "\n";

+  }

 }

diff --git a/Test/dafny0/Trait/TraitCompile.dfy.expect b/Test/dafny0/Trait/TraitCompile.dfy.expect
index f4f346de..2b4f82c1 100644
--- a/Test/dafny0/Trait/TraitCompile.dfy.expect
+++ b/Test/dafny0/Trait/TraitCompile.dfy.expect
@@ -1,5 +1,5 @@
 

-Dafny program verifier finished with 23 verified, 0 errors

+Dafny program verifier finished with 22 verified, 0 errors

 Program compiled successfully

 Running...

 

@@ -9,10 +9,10 @@ d=800
 a5=407
 t=1212
 z=30
-z'=30
-w=30
 d=1000
 a5=507
 t=1512
-t=1512
-t=1515
+This is OtherModule.P((7.0 / 1.0))
+From OtherModule.Y: 7 and True
+c.f= 15 j.f= 15
+c.f= 18 j.f= 18
diff --git a/Test/dafny0/Trait/TraitOverride0.dfy.expect b/Test/dafny0/Trait/TraitOverride0.dfy.expect
index 1e7bface..fefed2f2 100644
--- a/Test/dafny0/Trait/TraitOverride0.dfy.expect
+++ b/Test/dafny0/Trait/TraitOverride0.dfy.expect
@@ -1,5 +1,5 @@
-TraitOverride0.dfy(53,20): Error: a class cannot override implemented functions

+TraitOverride0.dfy(53,20): Error: member 'Mul' in class 'C1' overrides fully defined function inherited from trait 'T1'

 TraitOverride0.dfy(48,20): Error: function 'BodyLess1' is declared with a different number of parameter (1 instead of 0) than the corresponding function in the module it overrides

-TraitOverride0.dfy(65,6): Error: class: C2 does not implement trait member: BodyLess1

-TraitOverride0.dfy(65,6): Error: class: C2 does not implement trait member: BodyLess2

+TraitOverride0.dfy(65,6): Error: class 'C2' does not implement trait function 'T1.BodyLess1'

+TraitOverride0.dfy(65,6): Error: class 'C2' does not implement trait function 'T1.BodyLess2'

 4 resolution/type errors detected in TraitOverride0.dfy

diff --git a/Test/dafny0/Trait/TraitOverride1.dfy.expect b/Test/dafny0/Trait/TraitOverride1.dfy.expect
index 85c793d4..26aac19c 100644
--- a/Test/dafny0/Trait/TraitOverride1.dfy.expect
+++ b/Test/dafny0/Trait/TraitOverride1.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 58 verified, 0 errors

+Dafny program verifier finished with 50 verified, 0 errors

diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
index ebda3b9f..9960c1d9 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 9 verified, 1 error

+Dafny program verifier finished with 7 verified, 1 error