Support calls to static trait methods/functions via the class

2 files changed, 44 insertions, 5 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index dadfeb15..75e30b40 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -5267,9 +5267,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(t != null);

       UnresolvedType = t;

     }

-

+    

+    /// <summary>

+    /// Constructs a resolved LiteralExpr representing the 'null' literal whose type is "cl"

+    /// parameterized by the type arguments of "cl" itself.

+    /// </summary>

     public StaticReceiverExpr(IToken tok, ClassDecl cl)

-      : base(tok)  // constructs a LiteralExpr representing the 'null' literal

+      : base(tok)

     {

       Contract.Requires(tok != null);

       Contract.Requires(cl != null);

@@ -5277,6 +5281,36 @@ namespace Microsoft.Dafny {
       Type = new UserDefinedType(tok, cl.Name, cl, typeArgs);

       UnresolvedType = Type;

     }

+

+    /// <summary>

+    /// Constructs a resolved LiteralExpr representing the 'null' literal whose type is "cl"

+    /// parameterized according to the type arguments to "t".  It is assumed that "t" denotes

+    /// a class or trait that (possibly reflexively or transitively) extends "cl".

+    /// Examples:

+    /// * If "t" denotes "C(G)" and "cl" denotes "C", then the type of the StaticReceiverExpr

+    ///   will be "C(G)".

+    /// * Suppose "C" is a class that extends a trait "T"; then, if "t" denotes "C" and "cl" denotes

+    ///   "T", then the type of the StaticReceiverExpr will be "T".

+    /// * In the future, Dafny will support type parameters for traits and for classes that implement

+    ///   traits.  Then, suppose "C(X)" is a class that extends "T(f(X))", and that "T(Y)" is

+    ///   a trait that in turn extends trait "W(g(Y))".  If "t" denotes type "C(G)" and "cl" denotes "W",

+    ///   then type of the StaticReceiverExpr will be "T(g(f(G)))".

+    /// </summary>

+    public StaticReceiverExpr(IToken tok, UserDefinedType t, ClassDecl cl)

+      : base(tok) {

+      Contract.Requires(tok != null);

+      Contract.Requires(t.ResolvedClass != null);

+      Contract.Requires(cl != null);

+      if (t.ResolvedClass != cl) {

+        var orig = (ClassDecl)t.ResolvedClass;

+        Contract.Assert(orig.TraitsObj.Contains(cl));  // Dafny currently supports only one level of inheritance from traits

+        Contract.Assert(orig.TypeArgs.Count == 0);  // Dafny currently only allows type-parameter-less classes to extend traits

+        Contract.Assert(cl.TypeArgs.Count == 0);  // Dafny currently does not support type parameters for traits

+        t = new UserDefinedType(tok, cl.Name, cl, new List<Type>());

+      }

+      Type = t;

+      UnresolvedType = Type;

+    }

   }

 

   public class LiteralExpr : Expression {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 5a5bfb26..299c3abe 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -7786,8 +7786,7 @@ namespace Microsoft.Dafny
               Error(expr.tok, "accessing member '{0}' requires an instance expression", expr.SuffixName);

               // nevertheless, continue creating an expression that approximates a correct one

             }

-            var receiver = new StaticReceiverExpr(expr.tok, ty);

-            receiver.Type = ty;

+            var receiver = new StaticReceiverExpr(expr.tok, (UserDefinedType)ty.NormalizeExpand(), (ClassDecl)member.EnclosingClass);

             r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);

           }

         } else if (ty.IsDatatype) {

@@ -7817,7 +7816,13 @@ namespace Microsoft.Dafny
         NonProxyType nptype;

         member = ResolveMember(expr.tok, expr.Lhs.Type, expr.SuffixName, out nptype);

         if (member != null) {

-          var receiver = expr.Lhs;

+          Expression receiver;

+          if (!member.IsStatic) {

+            receiver = expr.Lhs;

+          } else {

+            Contract.Assert(expr.Lhs.Type.IsRefType);  // only reference types have static methods

+            receiver = new StaticReceiverExpr(expr.tok, (UserDefinedType)expr.Lhs.Type.NormalizeExpand(), (ClassDecl)member.EnclosingClass);

+          }

           r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);

         }

       }