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.

9 files changed, 225 insertions, 81 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 8971d2c1..6d5e2961 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -23,7 +23,10 @@ namespace Microsoft.Dafny
         nw.TopLevelDecls.Add(CloneDeclaration(d, nw));

       }

       if (null != m.RefinementBase) {

-          nw.RefinementBase = m.RefinementBase;

+        nw.RefinementBase = m.RefinementBase;

+      }

+      if (null != m.RefinementBaseSig) {

+        nw.RefinementBaseSig = m.RefinementBaseSig;

       }

       nw.ClonedFrom = m;

       nw.Height = m.Height;

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 {

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 6281417d..a243ad53 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -141,99 +141,117 @@ namespace Microsoft.Dafny
       }

 

       // Merge the declarations of prev into the declarations of m

+      List<string> processedDecl = new List<string>();

       foreach (var d in prev.TopLevelDecls) {

         int index;

+        processedDecl.Add(d.Name);

         if (!declaredNames.TryGetValue(d.Name, out index)) {

           m.TopLevelDecls.Add(refinementCloner.CloneDeclaration(d, m));

         } else {

           var nw = m.TopLevelDecls[index];

-          if (d is ModuleDecl) {

-            if (!(nw is ModuleDecl)) {

-              reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name);

-            } else if (!(d is ModuleFacadeDecl)) {

-              reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only refine a module facade", nw.Name);

-            } else {

-              ModuleSignature original = ((ModuleFacadeDecl)d).OriginalSignature;

-              ModuleSignature derived = null;

-              if (nw is AliasModuleDecl) {

-                derived = ((AliasModuleDecl)nw).Signature;

-              } else if (nw is ModuleFacadeDecl) {

-                derived = ((ModuleFacadeDecl)nw).Signature;

-              } else {

-                reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only be refined by an alias module or a module facade", d.Name);

+          MergeTopLevelDecls(m, nw, d, index);

+        }

+      }

+

+      // Merge the imports of prev 

+      var prevTopLevelDecls = RefinedSig.TopLevels.Values;

+      foreach (var d in prevTopLevelDecls) {

+        int index;

+        if (!processedDecl.Contains(d.Name) && (declaredNames.TryGetValue(d.Name, out index))) {

+          // if it is redefined, we need to merge them.

+          var nw = m.TopLevelDecls[index];

+          MergeTopLevelDecls(m, nw, d, index);

+        }

+      }

+      m.RefinementBaseSig = RefinedSig;

+

+      Contract.Assert(moduleUnderConstruction == m);  // this should be as it was set earlier in this method

+    }

+

+    private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDecl d, int index) {

+      if (d is ModuleDecl) {

+        if (!(nw is ModuleDecl)) {

+          reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name);

+        } else if (!(d is ModuleFacadeDecl)) {

+          reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only refine a module facade", nw.Name);

+        } else {

+          ModuleSignature original = ((ModuleFacadeDecl)d).OriginalSignature;

+          ModuleSignature derived = null;

+          if (nw is AliasModuleDecl) {

+            derived = ((AliasModuleDecl)nw).Signature;

+          } else if (nw is ModuleFacadeDecl) {

+            derived = ((ModuleFacadeDecl)nw).Signature;

+          } else {

+            reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only be refined by an alias module or a module facade", d.Name);

+          }

+          if (derived != null) {

+            // check that the new module refines the previous declaration

+            if (!CheckIsRefinement(derived, original))

+              reporter.Error(MessageSource.RefinementTransformer, nw.tok, "a module ({0}) can only be replaced by a refinement of the original module", d.Name);

+          }

+        }

+      } else if (d is OpaqueTypeDecl) {

+        if (nw is ModuleDecl) {

+          reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name);

+        } else {

+          bool dDemandsEqualitySupport = ((OpaqueTypeDecl)d).MustSupportEquality;

+          if (nw is OpaqueTypeDecl) {

+            if (dDemandsEqualitySupport != ((OpaqueTypeDecl)nw).MustSupportEquality) {

+              reporter.Error(MessageSource.RefinementTransformer, nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name);

+            }

+            if (nw.TypeArgs.Count != d.TypeArgs.Count) {

+              reporter.Error(MessageSource.RefinementTransformer, nw, "type '{0}' is not allowed to change its number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);

+            }

+          } else if (dDemandsEqualitySupport) {

+            if (nw is ClassDecl) {

+              // fine, as long as "nw" takes the right number of type parameters

+              if (nw.TypeArgs.Count != d.TypeArgs.Count) {

+                reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);

               }

-              if (derived != null) {

-                // check that the new module refines the previous declaration

-                if (!CheckIsRefinement(derived, original))

-                  reporter.Error(MessageSource.RefinementTransformer, nw.tok, "a module ({0}) can only be replaced by a refinement of the original module", d.Name);

+            } else if (nw is NewtypeDecl) {

+              // fine, as long as "nw" does not take any type parameters

+              if (nw.TypeArgs.Count != 0) {

+                reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}', which has {1} type argument{2}, is not allowed to be replaced by a newtype, which takes none", nw.Name, d.TypeArgs.Count, d.TypeArgs.Count == 1 ? "" : "s");

               }

-            }

-          } else if (d is OpaqueTypeDecl) {

-            if (nw is ModuleDecl) {

-              reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name);

+            } else if (nw is CoDatatypeDecl) {

+              reporter.Error(MessageSource.RefinementTransformer, nw, "a type declaration that requires equality support cannot be replaced by a codatatype");

             } else {

-              bool dDemandsEqualitySupport = ((OpaqueTypeDecl)d).MustSupportEquality;

-              if (nw is OpaqueTypeDecl) {

-                if (dDemandsEqualitySupport != ((OpaqueTypeDecl)nw).MustSupportEquality) {

-                  reporter.Error(MessageSource.RefinementTransformer, nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name);

-                }

-                if (nw.TypeArgs.Count != d.TypeArgs.Count) {

-                  reporter.Error(MessageSource.RefinementTransformer, nw, "type '{0}' is not allowed to change its number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);

-                }

-              } else if (dDemandsEqualitySupport) {

-                if (nw is ClassDecl) {

-                  // fine, as long as "nw" takes the right number of type parameters

-                  if (nw.TypeArgs.Count != d.TypeArgs.Count) {

-                    reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);

-                  }

-                } else if (nw is NewtypeDecl) {

-                  // fine, as long as "nw" does not take any type parameters

-                  if (nw.TypeArgs.Count != 0) {

-                    reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}', which has {1} type argument{2}, is not allowed to be replaced by a newtype, which takes none", nw.Name, d.TypeArgs.Count, d.TypeArgs.Count == 1 ? "" : "s");

-                  }

-                } else if (nw is CoDatatypeDecl) {

-                  reporter.Error(MessageSource.RefinementTransformer, nw, "a type declaration that requires equality support cannot be replaced by a codatatype");

-                } else {

-                  Contract.Assert(nw is IndDatatypeDecl || nw is TypeSynonymDecl);

-                  if (nw.TypeArgs.Count != d.TypeArgs.Count) {

-                    reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);

-                  } else {

-                    // Here, we need to figure out if the new type supports equality.  But we won't know about that until resolution has

-                    // taken place, so we defer it until the PostResolve phase.

-                    var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw);

-                    postTasks.Enqueue(() => {

-                      if (!udt.SupportsEquality) {

-                        reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}' is used to refine an opaque type with equality support, but '{0}' does not support equality", udt.Name);

-                      }

-                    });

-                  }

-                }

-              } else if (d.TypeArgs.Count != nw.TypeArgs.Count) {

+              Contract.Assert(nw is IndDatatypeDecl || nw is TypeSynonymDecl);

+              if (nw.TypeArgs.Count != d.TypeArgs.Count) {

                 reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);

+              } else {

+                // Here, we need to figure out if the new type supports equality.  But we won't know about that until resolution has

+                // taken place, so we defer it until the PostResolve phase.

+                var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw);

+                postTasks.Enqueue(() => {

+                  if (!udt.SupportsEquality) {

+                    reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}' is used to refine an opaque type with equality support, but '{0}' does not support equality", udt.Name);

+                  }

+                });

               }

             }

-          } else if (nw is OpaqueTypeDecl) {

-            reporter.Error(MessageSource.RefinementTransformer, nw, "an opaque type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);

-          } else if (nw is DatatypeDecl) {

-            reporter.Error(MessageSource.RefinementTransformer, nw, "a datatype declaration ({0}) in a refinement module can only replace an opaque type declaration", nw.Name);

-          } else if (nw is IteratorDecl) {

-            if (d is IteratorDecl) {

-              m.TopLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d);

-            } else {

-              reporter.Error(MessageSource.RefinementTransformer, nw, "an iterator declaration ({0}) is a refining module cannot replace a different kind of declaration in the refinement base", nw.Name);

-            }

-          } else {

-            Contract.Assert(nw is ClassDecl);

-            if (d is DatatypeDecl) {

-              reporter.Error(MessageSource.RefinementTransformer, nw, "a class declaration ({0}) in a refining module cannot replace a different kind of declaration in the refinement base", nw.Name);

-            } else {

-              m.TopLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d);

-            }

+          } else if (d.TypeArgs.Count != nw.TypeArgs.Count) {

+            reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);

           }

         }

+      } else if (nw is OpaqueTypeDecl) {

+        reporter.Error(MessageSource.RefinementTransformer, nw, "an opaque type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);

+      } else if (nw is DatatypeDecl) {

+        reporter.Error(MessageSource.RefinementTransformer, nw, "a datatype declaration ({0}) in a refinement module can only replace an opaque type declaration", nw.Name);

+      } else if (nw is IteratorDecl) {

+        if (d is IteratorDecl) {

+          m.TopLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d);

+        } else {

+          reporter.Error(MessageSource.RefinementTransformer, nw, "an iterator declaration ({0}) is a refining module cannot replace a different kind of declaration in the refinement base", nw.Name);

+        }

+      } else {

+        Contract.Assert(nw is ClassDecl);

+        if (d is DatatypeDecl) {

+          reporter.Error(MessageSource.RefinementTransformer, nw, "a class declaration ({0}) in a refining module cannot replace a different kind of declaration in the refinement base", nw.Name);

+        } else {

+          m.TopLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d);

+        }

       }

-

-      Contract.Assert(moduleUnderConstruction == m);  // this should be as it was set earlier in this method

     }

 

     public bool CheckIsRefinement(ModuleSignature derived, ModuleSignature original) {

diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs
index 760392ca..b36efc55 100644
--- a/Source/Dafny/Reporting.cs
+++ b/Source/Dafny/Reporting.cs
@@ -37,7 +37,7 @@ namespace Microsoft.Dafny {
     // This is the only thing that needs to be overriden

     public virtual bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {

       bool discard = (ErrorsOnly && level != ErrorLevel.Error) || // Discard non-errors if ErrorsOnly is set

-                     (tok is TokenWrapper && !(tok is NestedToken)); // Discard wrapped tokens, except for nested ones

+                     (tok is TokenWrapper && !(tok is NestedToken) && !(tok is RefinementToken)); // Discard wrapped tokens, except for nested and refinement

       if (!discard) {

         AllMessages[level].Add(new ErrorMessage { token = tok, message = msg });

       }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index e47220d7..99b31923 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1103,6 +1103,17 @@ namespace Microsoft.Dafny
           }

         }

       }

+

+      // second go through and overriding anything from the opened imports with the ones from the refinementBase

+      if (useImports && moduleDef.RefinementBaseSig != null) {

+        foreach (var kv in moduleDef.RefinementBaseSig.TopLevels) {

+          sig.TopLevels[kv.Key] = kv.Value;

+        }

+        foreach (var kv in moduleDef.RefinementBaseSig.StaticMembers) {

+          sig.StaticMembers[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

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index dbbffd87..4b86d848 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -335,3 +335,15 @@ module TopLevelStatics {
   static method M()  // error/warning: static keyword does not belong here

   { }

 }

+

+module Library {

+  class T { }

+}

+

+module AA {

+ import opened Library

+}

+

+module B refines AA {

+  datatype T = MakeT(int)  // illegal

+}

diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect
index e4b46cce..f51e0f6c 100644
--- a/Test/dafny0/Modules0.dfy.expect
+++ b/Test/dafny0/Modules0.dfy.expect
@@ -30,5 +30,6 @@ Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup
 Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon'

 Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)

 Modules0.dfy(324,30): Error: member Create does not exist in class Klassy

+Modules0.dfy(348,11): Error: a datatype declaration (T) in a refinement module can only replace an opaque type declaration

 Modules0.dfy(101,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name or declare a module import 'opened?')

-31 resolution/type errors detected in Modules0.dfy

+32 resolution/type errors detected in Modules0.dfy

diff --git a/Test/dafny4/Bug125.dfy b/Test/dafny4/Bug125.dfy
new file mode 100644
index 00000000..916dd3f8
--- /dev/null
+++ b/Test/dafny4/Bug125.dfy
@@ -0,0 +1,82 @@
+// RUN: %dafny /compile:0  "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+abstract module AbstractModuleA 

+{

+  type T

+} 

+

+abstract module AbstractModuleB 

+{

+  import opened AMA : AbstractModuleA

+

+  method Foo(t:T)

+} 

+

+abstract module AbstractModuleC refines AbstractModuleB 

+{

+  import opened AMA2 : AbstractModuleA

+}

+

+module LibA {

+  class G { 

+    static function f(x:int) : bool {

+      x >= 10

+    }

+  }

+

+  function g() : bool {

+     true

+  }

+}

+

+module LibB {

+  class G { 

+    static function f(x:int) : bool {

+      x < 10

+    }

+  }

+

+  function g() : bool {

+     false

+  }

+}

+

+module R {

+  import opened LibA

+}

+

+module S refines R {

+  import opened LibB

+  method m() {

+    assert g();  // should be LibA.g

+  }

+

+  method m1() {

+   assert G.f(20); // should be LibA.G.f

+  }

+} 

+

+

+module Library {

+

+  class T { }

+

+}

+

+ 

+

+module A {

+

+  import opened Library

+	class T {

+	}

+}

+

+ 

+

+module B refines A {

+

+  datatype T = MakeT(int)  // illegal for the same reason as above, but Dafny fails to issue an error

+

+}

diff --git a/Test/dafny4/Bug125.dfy.expect b/Test/dafny4/Bug125.dfy.expect
new file mode 100644
index 00000000..c87e2af2
--- /dev/null
+++ b/Test/dafny4/Bug125.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 10 verified, 0 errors