Dafny: support opening modules into the local scope

1 files changed, 57 insertions, 0 deletions

diff --git a/Test/dafny0/Modules2.dfy b/Test/dafny0/Modules2.dfy
new file mode 100644
index 00000000..2a5b2be7
--- /dev/null
+++ b/Test/dafny0/Modules2.dfy
@@ -0,0 +1,57 @@
+

+module A {

+  class C {

+    var f: int;

+  }

+  datatype D = E(int) | F(int);

+  static function f(n:nat): nat

+}

+module B {

+  class C {

+    var f: int;

+  }

+  datatype D = E(int) | F(int);

+  static function f(n:nat): nat

+}

+module Test {

+  import opened A; // nice shorthand for import opened A = A; (see below)

+  method m() {

+    var c := new C;   // fine, as A was opened

+    var c' := new A.C;// also fine, as A is bound

+    var i := 43;

+    var d  := E(i);     // these all refer to the same value

+    var d' := A.E(i);

+    var d'':= A.D.E(i);

+    assert d == d' == d'';

+    assert f(3) >= 0; // true because f(x): nat

+    assert A._default.f(3) >= 0;

+  }

+}

+

+module Test2 {

+  import opened B as A;

+  method m() {

+    var c := new C;   // fine, as A was opened

+    var c' := new B.C;// also fine, as A is bound

+    assert B.f(0) >= 0;

+  }

+}

+

+module Test3 {

+  import opened A;

+  import opened B; // everything in B clashes with A

+  method m() {

+    var c := new C;    // bad, ambiguous between A.C and B.C

+    var c' := new A.C; // good: qualified.

+    var i := 43;

+    var d  := E(i);     // bad, as both A and B give a definition of E

+    var d' := D.E(i);   // bad, as D is still itself ambiguous.

+    var d'':= B.D.E(i); // good, just use the B version

+    assert f(3) >= 0;   // bad because A and be both define f statically.

+  }  

+}

+

+module Test4 {

+  import A = A; // good: looks strange, but A is not bound on the RHS of the equality

+  import B; // the same as the above, but for module B

+}
\ No newline at end of file