Fixed scoping to allow a datatype to have a constructor with the same name.

Allow conversions to qualify type with module names.

4 files changed, 25 insertions, 4 deletions

diff --git a/Test/dafny0/DerivedTypes.dfy b/Test/dafny0/DerivedTypes.dfy
index 34c91447..09e43d32 100644
--- a/Test/dafny0/DerivedTypes.dfy
+++ b/Test/dafny0/DerivedTypes.dfy
@@ -117,7 +117,6 @@ module PredicateTests {
   }

 }

 

-/*

 module Module0 {

   import Module1

   method M(x: int) returns (n: Module1.N9) {

@@ -128,4 +127,14 @@ module Module0 {
 module Module1 {

   newtype N9 = int

 }

-*/

+

+module DatatypeCtorResolution {

+  datatype Pair = Pair(int, int)

+

+  method M() {

+    var p := Pair(5, 6);

+    var q: Pair;

+    q := p;

+    q := Pair.Pair(10, 20);

+  }

+}

diff --git a/Test/dafny0/DerivedTypes.dfy.expect b/Test/dafny0/DerivedTypes.dfy.expect
index abe01f96..41c21410 100644
--- a/Test/dafny0/DerivedTypes.dfy.expect
+++ b/Test/dafny0/DerivedTypes.dfy.expect
@@ -20,4 +20,4 @@ DerivedTypes.dfy(104,16): Error: result of operation might violate newtype const
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 20 verified, 6 errors

+Dafny program verifier finished with 24 verified, 6 errors

diff --git a/Test/dafny0/DerivedTypesResolution.dfy b/Test/dafny0/DerivedTypesResolution.dfy
index dd9d58e5..b1407f10 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy
+++ b/Test/dafny0/DerivedTypesResolution.dfy
@@ -110,3 +110,14 @@ module CyclicDependencies {
 module SelfCycleTest {

   newtype SelfCycle = x: int where var s: SelfCycle := 4; s < 10  // error: cyclic dependency on itself

 }

+

+module Module0 {

+  import Module1

+  method M(x: int) returns (n: Module1.N9) {

+    var x := Module1.N9;  // error

+  }

+}

+

+module Module1 {

+  newtype N9 = int

+}

diff --git a/Test/dafny0/DerivedTypesResolution.dfy.expect b/Test/dafny0/DerivedTypesResolution.dfy.expect
index 11dd556b..2f5682ac 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy.expect
+++ b/Test/dafny0/DerivedTypesResolution.dfy.expect
@@ -11,4 +11,5 @@ DerivedTypesResolution.dfy(57,25): Error: first argument to % must be of type in
 DerivedTypesResolution.dfy(98,24): Error: Wrong number of type arguments (1 instead of 0) passed to newtype: N

 DerivedTypesResolution.dfy(102,10): Error: recursive dependency involving a newtype: _default.BadLemma -> Cycle

 DerivedTypesResolution.dfy(111,10): Error: recursive dependency involving a newtype: SelfCycle -> SelfCycle

-13 resolution/type errors detected in DerivedTypesResolution.dfy

+DerivedTypesResolution.dfy(117,21): Error: unresolved identifier: N9

+14 resolution/type errors detected in DerivedTypesResolution.dfy