Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports.

For the following situation
 module LibA {
 // ...things declared here...
 }

 module LibB {
 // ...things declared here...
 }

 module R {
 import opened LibA
 // ...things declared here...
 }

 module S refines R {
 import opened LibB
 // ...declared here...
 }

 1. If module R declares a TopLevelDecl “G”, then we should report an error if S
 attempts to declare an incompatible TopLevelDecl “G”. Dafny does this already.

 2. If LibA declares a TopLevelDecl “G” but R does not directly declare any
 TopLevelDecl G”, then we should also issue an error for any TopLevelDecl “G”
 in S. This behavior is missing in Dafny.

 3. If each of LibA and LibB declares some TopLevelDecl “G”, but neither R nor S
 directly declares any TopLevelDecl “G”, then no error should be issued, and
 any use of “G” in S should resolve to the “G” in LibA. This behavior is missing
 in Dafny.

1 files changed, 15 insertions, 0 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 33186a76..0e4c4751 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1823,6 +1823,21 @@ namespace Microsoft.Dafny {
 

     public int ExclusiveRefinementCount { get; set; }

 

+    private ModuleSignature refinementBaseSig; // module signature of the refinementBase.

+    public ModuleSignature RefinementBaseSig {

+      get {

+        return refinementBaseSig;

+      }

+

+      set {

+        // the refinementBase member may only be changed once.

+        if (null != refinementBaseSig) {

+          throw new InvalidOperationException(string.Format("This module ({0}) already has a refinement base ({1}).", Name, refinementBase.Name));

+        }

+        refinementBaseSig = value;

+      }

+    }

+

     private ModuleDefinition refinementBase; // filled in during resolution via RefinementBase property (null if no refinement base yet or at all).

 

     public ModuleDefinition RefinementBase {