Update module export error messages. Also for "import Y" if there is at least

one exported view, but no exported view is marked as default, then it is an
error.

3 files changed, 56 insertions, 5 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index d3b59b51..aa9ce148 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -742,7 +742,7 @@ namespace Microsoft.Dafny
               d.ExtendDecls.Add(extend);

               exportDependencies.AddEdge(d, extend);

             } else {

-              reporter.Error(MessageSource.Resolver, m.tok, s + " must be an export of" + m + " to be extended");

+              reporter.Error(MessageSource.Resolver, m.tok, s + " must be an export of " + m.Name + " to be extended");

             }

           }

           foreach (ExportSignature export in d.Exports) {

@@ -757,7 +757,7 @@ namespace Microsoft.Dafny
             } else if (sig.StaticMembers.TryGetValue(name, out member)) {

               export.Decl = member;

             } else {

-              reporter.Error(MessageSource.Resolver, d.tok, name + " must be a member of " + m + " to be exported");

+              reporter.Error(MessageSource.Resolver, d.tok, name + " must be a member of " + m.Name + " to be exported");

             }

           }

         }

@@ -779,7 +779,7 @@ namespace Microsoft.Dafny
           if (defaultExport == null) {

             defaultExport = decl;

           } else {

-            reporter.Error(MessageSource.Resolver, m.tok, "more than one default export declared: {0}, {1}", defaultExport, decl);

+            reporter.Error(MessageSource.Resolver, m.tok, "more than one default export declared in module {0}", m.Name);

           }

         }

         // fill in export signature

@@ -811,9 +811,14 @@ namespace Microsoft.Dafny
         }

       }

 

-      // set the default export if it exists, otherwise, default is export everything     

+      // set the default export if it exists

       if (defaultExport != null) {

         literalDecl.DefaultExport = defaultExport.Signature;

+      } else {

+        // if there is at least one exported view, but no exported view marked as default, then defaultExport should be null.

+        if (sortedDecls.Count > 0) {

+          literalDecl.DefaultExport = null;       

+        }

       }

     }

 

@@ -1437,6 +1442,11 @@ namespace Microsoft.Dafny
         // use the default export when the importing the root

         LiteralModuleDecl decl = (LiteralModuleDecl)root;

         p = decl.DefaultExport;

+        if (p == null) {

+          // no default view is specified. 

+          reporter.Error(MessageSource.Resolver, decl.tok, "no default export declared in module: {0}", decl.Name);

+          return false;

+        }

         return true;

       }

 

diff --git a/Test/dafny0/ModuleExport.dfy b/Test/dafny0/ModuleExport.dfy
index 81fe0ed5..1e69764f 100644
--- a/Test/dafny0/ModuleExport.dfy
+++ b/Test/dafny0/ModuleExport.dfy
@@ -65,4 +65,41 @@ module E {
     case Kiwi(x) => 7

 		case Orang => 8  // error

   } 

+}

+

+module F {

+  default export Public { f, h}

+	default export E1 { f, g}

+	export E2 extends Public2, E1 {T}		// error: Public2 is not a exported view of F

+  export Friend extends Public {g2, T}  // error: g2 is not a member of F

+	export Fruit {Data}

+

+  method h() {}

+  function f(): int { 818 }

+  function g() : int { 819 }

+	function k() : int { 820 }

+  

+	class T 

+	{

+	  static method l() {}

+	}

+

+	datatype Data = Lemon | Kiwi(int)

+}

+

+module G {

+  export Public { f, h}

+

+	method h() {}

+  function f(): int { 818 }

+  function g() : int { 819 }

+	function k() : int { 820 }

+}

+

+module H {

+  import G  // error: G has no default export

+}

+

+module I {

+  import G.Public  // OK

 }
\ No newline at end of file
diff --git a/Test/dafny0/ModuleExport.dfy.expect b/Test/dafny0/ModuleExport.dfy.expect
index c7444bdb..274c8f31 100644
--- a/Test/dafny0/ModuleExport.dfy.expect
+++ b/Test/dafny0/ModuleExport.dfy.expect
@@ -6,4 +6,8 @@ ModuleExport.dfy(42,11): Error: unresolved identifier: k
 ModuleExport.dfy(52,9): Error: unresolved identifier: g

 ModuleExport.dfy(53,9): Error: unresolved identifier: k

 ModuleExport.dfy(66,2): Error: member Orang does not exist in datatype Data

-8 resolution/type errors detected in ModuleExport.dfy

+ModuleExport.dfy(70,7): Error: Public2 must be an export of F to be extended

+ModuleExport.dfy(74,9): Error: g2 must be a member of F to be exported

+ModuleExport.dfy(70,7): Error: more than one default export declared in module F

+ModuleExport.dfy(90,7): Error: no default export declared in module: G

+12 resolution/type errors detected in ModuleExport.dfy