From a89b9aee05dff74345a79f8fb4fe0fe3fdbb17ad Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Mon, 21 Mar 2016 11:45:14 -0700
Subject: 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.

---
 Test/dafny0/ModuleExport.dfy        | 37 +++++++++++++++++++++++++++++++++++++
 Test/dafny0/ModuleExport.dfy.expect |  6 +++++-
 2 files changed, 42 insertions(+), 1 deletion(-)

(limited to 'Test/dafny0')

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
-- 
cgit v1.2.3