Support calls to static trait methods/functions via the class

2 files changed, 16 insertions, 10 deletions

diff --git a/Test/dafny0/Trait/TraitCompile.dfy b/Test/dafny0/Trait/TraitCompile.dfy
index 3d559de1..3de5a6d2 100644
--- a/Test/dafny0/Trait/TraitCompile.dfy
+++ b/Test/dafny0/Trait/TraitCompile.dfy
@@ -58,25 +58,25 @@ 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";

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

+  assert seven == 7;

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

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

 

   TestFields.Test();

 }

diff --git a/Test/dafny0/Trait/TraitCompile.dfy.expect b/Test/dafny0/Trait/TraitCompile.dfy.expect
index 2b4f82c1..1838fbc3 100644
--- a/Test/dafny0/Trait/TraitCompile.dfy.expect
+++ b/Test/dafny0/Trait/TraitCompile.dfy.expect
@@ -9,10 +9,16 @@ 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
+This is OtherModule.P((7.0 / 1.0))
+From OtherModule.X: 7 and True
 c.f= 15 j.f= 15
 c.f= 18 j.f= 18