From e4da5fcd52bbdd0b8345056a3475333d6e27e65f Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Fri, 29 Jan 2016 13:01:02 -0800
Subject: Implement module export so we can export a subset of items defined in
 the module.

---
 Test/dafny0/ModuleExport.dfy        | 68 +++++++++++++++++++++++++++++++++++++
 Test/dafny0/ModuleExport.dfy.expect |  9 +++++
 2 files changed, 77 insertions(+)
 create mode 100644 Test/dafny0/ModuleExport.dfy
 create mode 100644 Test/dafny0/ModuleExport.dfy.expect

(limited to 'Test')

diff --git a/Test/dafny0/ModuleExport.dfy b/Test/dafny0/ModuleExport.dfy
new file mode 100644
index 00000000..81fe0ed5
--- /dev/null
+++ b/Test/dafny0/ModuleExport.dfy
@@ -0,0 +1,68 @@
+// 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
+  } 
+}
\ No newline at end of file
diff --git a/Test/dafny0/ModuleExport.dfy.expect b/Test/dafny0/ModuleExport.dfy.expect
new file mode 100644
index 00000000..c7444bdb
--- /dev/null
+++ b/Test/dafny0/ModuleExport.dfy.expect
@@ -0,0 +1,9 @@
+ModuleExport.dfy(30,11): Error: unresolved identifier: g
+ModuleExport.dfy(31,11): Error: unresolved identifier: k
+ModuleExport.dfy(32,4): Error: unresolved identifier: T
+ModuleExport.dfy(32,7): Error: expected method call, found expression
+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
-- 
cgit v1.2.3