Dafny: support opening modules into the local scope

10 files changed, 185 insertions, 44 deletions

diff --git a/Dafny/Cloner.cs b/Dafny/Cloner.cs
index 506df4c6..2f254135 100644
--- a/Dafny/Cloner.cs
+++ b/Dafny/Cloner.cs
@@ -63,13 +63,13 @@ namespace Microsoft.Dafny
           return l;

         } else if (d is AliasModuleDecl) {

           var a = (AliasModuleDecl)d;

-          var alias = new AliasModuleDecl(a.Path, a.tok, m);

+          var alias = new AliasModuleDecl(a.Path, a.tok, m, a.Opened);

           alias.ModuleReference = a.ModuleReference;

           alias.Signature = a.Signature;

           return alias;

         } else if (d is AbstractModuleDecl) {

           var a = (AbstractModuleDecl)d;

-          var abs = new AbstractModuleDecl(a.Path, a.tok, m, a.CompilePath);

+          var abs = new AbstractModuleDecl(a.Path, a.tok, m, a.CompilePath, a.Opened);

           abs.Signature = a.Signature;

           abs.OriginalSignature = a.OriginalSignature;

           return abs;

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 748b3090..ce0ccf16 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -203,11 +203,11 @@ SubModuleDecl<ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl
      | 

     "import" ["opened" (.opened = true;.)]

       ( NoUSIdent<out id> (   "=" QualifiedName<out idPath> ";"

-                                 (. submodule = new AliasModuleDecl(idPath, id, parent); .)

+                                 (. submodule = new AliasModuleDecl(idPath, id, parent, opened); .)

                             | ";" 

-                                 (. idPath = new List<IToken>(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent); .)

+                                 (. idPath = new List<IToken>(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent, opened); .)

                             | "as" QualifiedName<out idPath>  ["default" QualifiedName<out idAssignment> ] ";"

-                                 (.submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment); .)

+                                 (.submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment, opened); .)

                           )

       )

   )

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index a019f068..0dcbcf11 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -804,10 +804,12 @@ namespace Microsoft.Dafny {
   {

     public ModuleSignature Signature; // filled in by resolution, in topological order.

     public int Height;

-    public ModuleDecl(IToken tok, string name, ModuleDefinition parent)

+    public readonly bool Opened;

+    public ModuleDecl(IToken tok, string name, ModuleDefinition parent, bool opened)

       : base(tok, name, parent, new List<TypeParameter>(), null) {

         Height = -1;

-        Signature = null;

+      Signature = null;

+      Opened = opened;

     }

   }

   // Represents module X { ... }

@@ -815,7 +817,7 @@ namespace Microsoft.Dafny {
   {

     public readonly ModuleDefinition ModuleDef;

     public LiteralModuleDecl(ModuleDefinition module, ModuleDefinition parent)

-      : base(module.tok, module.Name, parent) {

+      : base(module.tok, module.Name, parent, false) {

       ModuleDef = module;

     }

   }

@@ -826,8 +828,8 @@ namespace Microsoft.Dafny {
                                        // be detected and warned.

     public readonly List<IToken> Path; // generated by the parser, this is looked up

     public ModuleDecl Root;            // the moduleDecl that Path[0] refers to.

-    public AliasModuleDecl(List<IToken> path, IToken name, ModuleDefinition parent)

-      : base(name, name.val, parent) {

+    public AliasModuleDecl(List<IToken> path, IToken name, ModuleDefinition parent, bool opened)

+      : base(name, name.val, parent, opened) {

        Contract.Requires(path != null && path.Count > 0);

        Path = path;

        ModuleReference = null;

@@ -842,8 +844,8 @@ namespace Microsoft.Dafny {
     public readonly List<IToken> CompilePath;

     public ModuleSignature OriginalSignature;

     

-    public AbstractModuleDecl(List<IToken> path, IToken name, ModuleDefinition parent, List<IToken> compilePath)

-      : base(name, name.val, parent) {

+    public AbstractModuleDecl(List<IToken> path, IToken name, ModuleDefinition parent, List<IToken> compilePath, bool opened)

+      : base(name, name.val, parent, opened) {

       Path = path;

       Root = null;

       CompilePath = compilePath;

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 244fe550..a7de690e 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -293,10 +293,10 @@ bool IsAttribute() {
 				Get();

 				QualifiedName(out idPath);

 				Expect(14);

-				submodule = new AliasModuleDecl(idPath, id, parent); 

+				submodule = new AliasModuleDecl(idPath, id, parent, opened); 

 			} else if (la.kind == 14) {

 				Get();

-				idPath = new List<IToken>(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent); 

+				idPath = new List<IToken>(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent, opened); 

 			} else if (la.kind == 15) {

 				Get();

 				QualifiedName(out idPath);

@@ -305,7 +305,7 @@ bool IsAttribute() {
 					QualifiedName(out idAssignment);

 				}

 				Expect(14);

-				submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment); 

+				submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment, opened); 

 			} else SynErr(114);

 		} else SynErr(115);

 	}

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index c1f41b6e..7a84f86e 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -84,11 +84,11 @@ namespace Microsoft.Dafny {
               wr.WriteLine("}");

             }

           } else if (d is AliasModuleDecl) {

-            wr.Write("module");

+            wr.Write("import"); if (((AliasModuleDecl)d).Opened) wr.Write(" opened");

             wr.Write(" {0} ", ((AliasModuleDecl)d).Name);

             wr.WriteLine("= {0};", Util.Comma(".", ((AliasModuleDecl)d).Path, id => id.val));

           } else if (d is AbstractModuleDecl) {

-            wr.Write("module");

+            wr.Write("import"); if (((AbstractModuleDecl)d).Opened) wr.Write(" opened");

             wr.Write(" {0} ", ((AbstractModuleDecl)d).Name);

             wr.WriteLine("as {0};", Util.Comma(".", ((AbstractModuleDecl)d).Path, id => id.val));

           }

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index b131912c..118e540f 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -93,6 +93,31 @@ namespace Microsoft.Dafny
         return nm;

       }

     }

+

+    class AmbiguousMemberDecl : MemberDecl  // only used with "classes"

+    {

+      readonly MemberDecl A;

+      readonly MemberDecl B;

+      public AmbiguousMemberDecl(ModuleDefinition m, MemberDecl a, MemberDecl b)

+        : base(a.tok, a.Name + "/" + b.Name, a.IsStatic, a.IsGhost, null) {

+        A = a;

+        B = b;

+      }

+      public string ModuleNames() {

+        string nm;

+        if (A is AmbiguousMemberDecl) {

+          nm = ((AmbiguousMemberDecl)A).ModuleNames();

+        } else {

+          nm = A.EnclosingClass.Module.Name;

+        }

+        if (B is AmbiguousMemberDecl) {

+          nm += ", " + ((AmbiguousMemberDecl)B).ModuleNames();

+        } else {

+          nm += ", " + B.EnclosingClass.Module.Name;

+        }

+        return nm;

+      }

+    }

     //Dictionary<string/*!*/, Tuple<DatatypeCtor, bool>> allDatatypeCtors;

 

     readonly Dictionary<ClassDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>/*!*/ classMembers = new Dictionary<ClassDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>();

@@ -147,7 +172,7 @@ namespace Microsoft.Dafny
       var refinementTransformer = new RefinementTransformer(this, prog);

 

       IRewriter rewriter = new AutoContractsRewriter();

-      systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);

+      systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false);

       foreach (var decl in sortedDecls) {

         if (decl is LiteralModuleDecl) {

           // The declaration is a literal module, so it has members and such that we need

@@ -176,7 +201,7 @@ namespace Microsoft.Dafny
               Error(m.RefinementBaseName[0], "module ({0}) named as refinement base does not exist", Util.Comma(".", m.RefinementBaseName, x => x.val));

             }

           }

-          literalDecl.Signature = RegisterTopLevelDecls(m);

+          literalDecl.Signature = RegisterTopLevelDecls(m, true);

           literalDecl.Signature.Refines = refinedSig;

           var sig = literalDecl.Signature;

           // set up environment

@@ -191,7 +216,7 @@ namespace Microsoft.Dafny
           if (ErrorCount == errorCount && !m.IsGhost) {

             // compilation should only proceed if everything is good, including the signature (which preResolveErrorCount does not include);

             var nw = (new Cloner()).CloneModuleDefinition(m, m.CompileName + "_Compile");

-            var compileSig = RegisterTopLevelDecls(nw);

+            var compileSig = RegisterTopLevelDecls(nw, true);

             compileSig.Refines = refinedSig;

             sig.CompileSignature = compileSig;

             useCompileSignatures = true;

@@ -285,10 +310,12 @@ namespace Microsoft.Dafny
           return parent.TryLookup(name, out m);

         } else return false;

       }

-      public bool TryLookupLocal(IToken name, out ModuleDecl m) {

+      public bool TryLookupIgnore(IToken name, out ModuleDecl m, ModuleDecl ignore) {

         Contract.Requires(name != null);

-        if (modules.TryGetValue(name.val, out m)) {

+        if (modules.TryGetValue(name.val, out m) && m != ignore) {

           return true;

+        } else if (parent != null) {

+          return parent.TryLookup(name, out m);

         } else return false;

       }

       public IEnumerable<ModuleDecl> ModuleList {

@@ -354,7 +381,7 @@ namespace Microsoft.Dafny
       } else if (moduleDecl is AliasModuleDecl) {

         var alias = moduleDecl as AliasModuleDecl;

         ModuleDecl root;

-        if (!bindings.TryLookup(alias.Path[0], out root))

+        if (!bindings.TryLookupIgnore(alias.Path[0], out root, alias))

           Error(alias.tok, ModuleNotFoundErrorMessage(0, alias.Path));

         else {

           dependencies.AddEdge(moduleDecl, root);

@@ -407,20 +434,62 @@ namespace Microsoft.Dafny
       info.IsGhost = m.IsGhost;

       return info;

     }

-    ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef) {

+    ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImports) {

       Contract.Requires(moduleDef != null);

       var sig = new ModuleSignature();

       sig.ModuleDef = moduleDef;

       sig.IsGhost = moduleDef.IsGhost;

       List<TopLevelDecl> declarations = moduleDef.TopLevelDecls;

 

+      if (useImports) {

+        // First go through and add anything from the opened imports

+        foreach (var im in declarations) {

+          if (im is ModuleDecl && ((ModuleDecl)im).Opened) {

+            var s = ((ModuleDecl)im).Signature;

+            // classes:

+            foreach (var kv in s.TopLevels) {

+              TopLevelDecl d;

+              if (sig.TopLevels.TryGetValue(kv.Key, out d)) {

+                sig.TopLevels[kv.Key] = new AmbiguousTopLevelDecl(moduleDef, d, kv.Value);

+              } else {

+                sig.TopLevels.Add(kv.Key, kv.Value);

+              }

+            }

+            // constructors:

+            foreach (var kv in s.Ctors) {

+              Tuple<DatatypeCtor, bool> pair;

+              if (sig.Ctors.TryGetValue(kv.Key, out pair)) {

+                // mark it as a duplicate

+                sig.Ctors[kv.Key] = new Tuple<DatatypeCtor, bool>(pair.Item1, true);

+              } else {

+                // add new

+                sig.Ctors.Add(kv.Key, kv.Value);

+              }

+            }

+            // static members:

+            foreach (var kv in s.StaticMembers) {

+              MemberDecl md;

+              if (sig.StaticMembers.TryGetValue(kv.Key, out md)) {

+                sig.StaticMembers[kv.Key] = new AmbiguousMemberDecl(moduleDef, md, kv.Value);

+              } else {

+                // add new

+                sig.StaticMembers.Add(kv.Key, kv.Value);

+              }

+            }

+          }

+        }

+      }

+      // This is solely used to detect duplicates amongst the various e

+      Dictionary<string, TopLevelDecl> toplevels = new Dictionary<string, TopLevelDecl>();

+      // Now add the things present

       foreach (TopLevelDecl d in declarations) {

         Contract.Assert(d != null);

         // register the class/datatype/module name

-        if (sig.TopLevels.ContainsKey(d.Name)) {

+        if (toplevels.ContainsKey(d.Name)) {

           Error(d, "Duplicate name of top-level declaration: {0}", d.Name);

         } else {

-          sig.TopLevels.Add(d.Name, d);

+          toplevels[d.Name] = d;

+          sig.TopLevels[d.Name] = d;

         }

         if (d is ModuleDecl) {

           // nothing to do

@@ -448,8 +517,8 @@ 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);

+              if (m.IsStatic && (m is Function || m is Method)) {

+                sig.StaticMembers[m.Name] = m;

               }

             }

           }

@@ -516,7 +585,7 @@ namespace Microsoft.Dafny
       foreach (var kv in p.TopLevels) {

         mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod, mods, Name));

       }

-      var sig = RegisterTopLevelDecls(mod);

+      var sig = RegisterTopLevelDecls(mod, false);

       sig.Refines = p.Refines;

       sig.CompileSignature = p;

       sig.IsGhost = p.IsGhost;

@@ -555,14 +624,14 @@ namespace Microsoft.Dafny
           return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m);

         } else if (d is AliasModuleDecl) {

           var a = (AliasModuleDecl)d;

-          var alias = new AliasModuleDecl(a.Path, a.tok, m);

+          var alias = new AliasModuleDecl(a.Path, a.tok, m, a.Opened);

           alias.ModuleReference = a.ModuleReference;

           alias.Signature = a.Signature;

           return alias;

         } else if (d is AbstractModuleDecl) {

           var abs = (AbstractModuleDecl)d;

           var sig = MakeAbstractSignature(abs.OriginalSignature, Name + "." + abs.Name, abs.Height, mods);

-          var a = new AbstractModuleDecl(abs.Path, abs.tok, m, abs.CompilePath);

+          var a = new AbstractModuleDecl(abs.Path, abs.tok, m, abs.CompilePath, abs.Opened);

           a.Signature = sig;

           a.OriginalSignature = abs.OriginalSignature;

           return a;

@@ -4652,7 +4721,7 @@ namespace Microsoft.Dafny
       //  - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here)

       //  - imported module name

       //  - 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.

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

 

       Expression r = null;  // resolved version of e

       CallRhs call = null;

@@ -4719,18 +4788,23 @@ namespace Microsoft.Dafny
                  || 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, (ClassDecl)member.EnclosingClass);

+        if (member is AmbiguousMemberDecl) {

+          Contract.Assert(member.IsStatic); // currently, static members of _default are the only thing which can be ambiguous.

+          Error(id, "The name {0} ambiguously refers to a static member in one of the modules {1}", id.val, ((AmbiguousMemberDecl)member).ModuleNames());

         } 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

+          Expression receiver;

+          if (member.IsStatic) {

+            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, (ClassDecl)member.EnclosingClass);  // resolve here

           }

-          receiver = new ImplicitThisExpr(id);

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

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

         }

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

 

       } else {

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

diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs
index 82a0e8ed..672124b1 100644
--- a/DafnyDriver/DafnyDriver.cs
+++ b/DafnyDriver/DafnyDriver.cs
@@ -638,8 +638,8 @@ namespace Microsoft.Dafny
             {

                 if (CommandLineOptions.Clo.Trace)

                 {

-                    int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;

-                    timeIndication = string.Format("  [{0} s, {1} proof obligation{2}]  ", elapsed.TotalSeconds, poCount, poCount == 1 ? "" : "s");

+                  int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;

+                  timeIndication = string.Format("  [{0:F3} s, {1} proof obligation{2}]  ", elapsed.TotalSeconds, poCount, poCount == 1 ? "" : "s");

                 }

             }

 

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index e3246f8f..3899b6df 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -757,6 +757,14 @@ Execution trace:
 

 Dafny program verifier finished with 22 verified, 5 errors

 

+-------------------- Modules2.dfy --------------------

+Modules2.dfy(44,17): Error: The name C ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)

+Modules2.dfy(44,10): Error: new can be applied only to reference types (got C)

+Modules2.dfy(47,14): Error: the name 'E' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'D.E')

+Modules2.dfy(48,14): Error: The name D ambiguously refers to a type in one of the modules A, B

+Modules2.dfy(50,11): Error: The name f ambiguously refers to a static member in one of the modules A, B

+5 resolution/type errors detected in Modules2.dfy

+

 -------------------- BadFunction.dfy --------------------

 BadFunction.dfy(6,3): Error: failure to decrease termination measure

 Execution trace:

diff --git a/Test/dafny0/Modules2.dfy b/Test/dafny0/Modules2.dfy
new file mode 100644
index 00000000..2a5b2be7
--- /dev/null
+++ b/Test/dafny0/Modules2.dfy
@@ -0,0 +1,57 @@
+

+module A {

+  class C {

+    var f: int;

+  }

+  datatype D = E(int) | F(int);

+  static function f(n:nat): nat

+}

+module B {

+  class C {

+    var f: int;

+  }

+  datatype D = E(int) | F(int);

+  static function f(n:nat): nat

+}

+module Test {

+  import opened A; // nice shorthand for import opened A = A; (see below)

+  method m() {

+    var c := new C;   // fine, as A was opened

+    var c' := new A.C;// also fine, as A is bound

+    var i := 43;

+    var d  := E(i);     // these all refer to the same value

+    var d' := A.E(i);

+    var d'':= A.D.E(i);

+    assert d == d' == d'';

+    assert f(3) >= 0; // true because f(x): nat

+    assert A._default.f(3) >= 0;

+  }

+}

+

+module Test2 {

+  import opened B as A;

+  method m() {

+    var c := new C;   // fine, as A was opened

+    var c' := new B.C;// also fine, as A is bound

+    assert B.f(0) >= 0;

+  }

+}

+

+module Test3 {

+  import opened A;

+  import opened B; // everything in B clashes with A

+  method m() {

+    var c := new C;    // bad, ambiguous between A.C and B.C

+    var c' := new A.C; // good: qualified.

+    var i := 43;

+    var d  := E(i);     // bad, as both A and B give a definition of E

+    var d' := D.E(i);   // bad, as D is still itself ambiguous.

+    var d'':= B.D.E(i); // good, just use the B version

+    assert f(3) >= 0;   // bad because A and be both define f statically.

+  }  

+}

+

+module Test4 {

+  import A = A; // good: looks strange, but A is not bound on the RHS of the equality

+  import B; // the same as the above, but for module B

+}
\ No newline at end of file
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 3b4e6e19..7a836c5a 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -13,7 +13,7 @@ for %%f in (Simple.dfy) do (
 for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy

             FunctionSpecifications.dfy ResolutionErrors.dfy ParseErrors.dfy

             Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

-            ModulesCycle.dfy Modules0.dfy Modules1.dfy BadFunction.dfy

+            ModulesCycle.dfy Modules0.dfy Modules1.dfy Modules2.dfy BadFunction.dfy

             Comprehensions.dfy Basics.dfy ControlStructures.dfy

             Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy

             TypeParameters.dfy Datatypes.dfy