Dafny: added static members of _default to the module level scope, at low priority.

2 files changed, 35 insertions, 11 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 1c5dc070..709074f1 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -840,6 +840,7 @@ namespace Microsoft.Dafny {
     

     public readonly Dictionary<string, TopLevelDecl> TopLevels = new Dictionary<string, TopLevelDecl>();

     public readonly Dictionary<string, Tuple<DatatypeCtor, bool>> Ctors = new Dictionary<string, Tuple<DatatypeCtor, bool>>();

+    public readonly Dictionary<string, MemberDecl> StaticMembers = new Dictionary<string, MemberDecl>();

     public ModuleDefinition ModuleDef; // Note: this is null if this signature does not correspond to a specific definition (i.e.

                                        // it is abstract). Otherwise, it points to that definition.

     public ModuleSignature Refines;

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 2c04d3c4..6f9d5dae 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -363,6 +363,10 @@ namespace Microsoft.Dafny {
       foreach (var kv in m.Ctors) {

         info.Ctors[kv.Key] = kv.Value;

       }

+      foreach (var kv in m.StaticMembers) {

+        info.StaticMembers[kv.Key] = kv.Value;

+      }

+

       return info;

     }

     ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef) {

@@ -403,7 +407,13 @@ namespace Microsoft.Dafny {
             }

           }

           cl.HasConstructor = hasConstructor;

-

+          if (cl.IsDefaultClass) {

+            foreach (MemberDecl m in cl.Members) {

+              if (!sig.StaticMembers.ContainsKey(m.Name) && m.IsStatic && (m is Function || m is Method)) {

+                sig.StaticMembers.Add(m.Name, m);

+              }

+            }

+          }

         } else {

           DatatypeDecl dt = (DatatypeDecl)d;

 

@@ -496,8 +506,9 @@ namespace Microsoft.Dafny {
         var dd = (ClassDecl)d;

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

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

-        var cl = new ClassDecl(dd.tok, dd.Name, m, tps, mm, null);

-        return cl;

+        if (dd is DefaultClassDecl) {

+          return new DefaultClassDecl(m, mm);

+        } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null); 

       } else if (d is ModuleDecl) {

         if (d is LiteralModuleDecl) {

           return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m);

@@ -4413,9 +4424,9 @@ namespace Microsoft.Dafny {
       //       (if two imported types have the same name, an error message is produced here)

       //  - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here)

       //  - imported module name

-      //  - field name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")

-      // Note, at present, modules do not give rise to new namespaces, which is something that should

-      // be changed in the language when modules are given more attention.

+      //  - field, function or method name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")

+      //  - static function or method in the enclosing module.

+      

       Expression r = null;  // resolved version of e

       CallRhs call = null;

 

@@ -4477,18 +4488,20 @@ namespace Microsoft.Dafny {
           }

         }

 

-      } else if (classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member)) {

+      } else if ((classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member))

+                 || moduleInfo.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.

+      {

         // ----- field, function, or method

         Expression receiver;

         if (member.IsStatic) {

-          receiver = new StaticReceiverExpr(id, currentClass);

+          receiver = new StaticReceiverExpr(id, (ClassDecl)member.EnclosingClass);

         } else {

           if (!scope.AllowInstance) {

             Error(id, "'this' is not allowed in a 'static' context");

             // nevertheless, set "receiver" to a value so we can continue resolution

           }

           receiver = new ImplicitThisExpr(id);

-          receiver.Type = GetThisType(id, currentClass);  // resolve here

+          receiver.Type = GetThisType(id, (ClassDecl)member.EnclosingClass);  // resolve here

         }

         r = ResolveSuffix(receiver, e, 0, twoState, allowMethodCall, out call);

 

@@ -4509,10 +4522,11 @@ namespace Microsoft.Dafny {
       return call;

     }

 

-    CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature info, bool twoState, bool allowMethodCall) {

+    CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature sig, bool twoState, bool allowMethodCall) {

       // Look up "id" as follows:

       //  - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or arbitrary-type)

       //       (if two imported types have the same name, an error message is produced here)

+      //  - static function or method of sig.

       // This is used to look up names that appear after a dot in a sequence identifier. For example, in X.M.*, M should be looked up in X, but

       // should not consult the local scope. This distingushes this from the above, in that local scope, imported modules, etc. are ignored.

       Contract.Requires(p < e.Tokens.Count);

@@ -4520,8 +4534,9 @@ namespace Microsoft.Dafny {
       CallRhs call = null;

 

       TopLevelDecl decl;

+      MemberDecl member;

       var id = e.Tokens[p];

-      if (info.TopLevels.TryGetValue(id.val, out decl)) {

+      if (sig.TopLevels.TryGetValue(id.val, out decl)) {

         if (decl is AmbiguousTopLevelDecl) {

           Error(id, "The name {0} ambiguously refers to a something in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames());

         } else if (decl is ClassDecl) {

@@ -4545,6 +4560,14 @@ namespace Microsoft.Dafny {
             r = ResolveSuffix(r, e, p + 2, twoState, allowMethodCall, out call);

           }

         }

+      } else if (sig.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.

+      {

+        // ----- function, or method

+        Expression receiver;

+        Contract.Assert(member.IsStatic);

+        receiver = new StaticReceiverExpr(id, (ClassDecl)member.EnclosingClass);

+        r = ResolveSuffix(receiver, e, p, twoState, allowMethodCall, out call);

+

       } else {

         Error(id, "unresolved identifier: {0}", id.val);

         // resolve arguments, if any