Dafny: support opening modules into the local scope

3 files changed, 66 insertions, 1 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index e3246f8f..3899b6df 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -757,6 +757,14 @@ Execution trace:
 

 Dafny program verifier finished with 22 verified, 5 errors

 

+-------------------- Modules2.dfy --------------------

+Modules2.dfy(44,17): Error: The name C ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)

+Modules2.dfy(44,10): Error: new can be applied only to reference types (got C)

+Modules2.dfy(47,14): Error: the name 'E' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'D.E')

+Modules2.dfy(48,14): Error: The name D ambiguously refers to a type in one of the modules A, B

+Modules2.dfy(50,11): Error: The name f ambiguously refers to a static member in one of the modules A, B

+5 resolution/type errors detected in Modules2.dfy

+

 -------------------- BadFunction.dfy --------------------

 BadFunction.dfy(6,3): Error: failure to decrease termination measure

 Execution trace:

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
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 3b4e6e19..7a836c5a 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -13,7 +13,7 @@ for %%f in (Simple.dfy) do (
 for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy

             FunctionSpecifications.dfy ResolutionErrors.dfy ParseErrors.dfy

             Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

-            ModulesCycle.dfy Modules0.dfy Modules1.dfy BadFunction.dfy

+            ModulesCycle.dfy Modules0.dfy Modules1.dfy Modules2.dfy BadFunction.dfy

             Comprehensions.dfy Basics.dfy ControlStructures.dfy

             Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy

             TypeParameters.dfy Datatypes.dfy