1 files changed, 105 insertions, 0 deletions
diff --git a/Test/dafny0/ModuleExport.dfy b/Test/dafny0/ModuleExport.dfy
new file mode 100644
index 00000000..1e69764f
--- /dev/null
+++ b/Test/dafny0/ModuleExport.dfy
@@ -0,0 +1,105 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module A {
+	default export Public { f, h}
+	export E1 { f, g}
+	export E2 extends Public, E1 {T}
+  export Friend extends Public {g, T}
+	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 B {
+  import X = A.Public
+	method m() {
+	  X.h();  // OK
+	  assert X.f() == 818; // OK
+		assert X.g() == 819; // error
+		assert X.k() == 820; // error
+		X.T.l(); // error
+	}
+}
+
+module C {
+  import X = A.Friend
+	method m() {
+	  X.h();  // OK
+	  assert X.f() == 818; // OK
+		assert X.g() == 819; // OK
+		assert X.k() == 820; // error
+		X.T.l(); // OK
+	}
+}
+
+module D {
+  import opened A
+	method m() {
+	  h();  // OK
+	  assert f() == 818; // OK
+		assert g() == 819; // error
+		assert k() == 820; // error
+	 }
+}
+
+module E {
+  import opened A.Fruit
+
+  function G(d: Data): int
+    requires d != Data.Lemon
+  {
+    match d
+    case Lemon => G(d)
+    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