Dafny: allow types to be qualified with the name of the module that declares them (for now, this is supported only in type expressions and "new" allocations, not in places where the type name is used to qualify some other type member)

1 files changed, 20 insertions, 0 deletions

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 5e2d0fff..e8a88749 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -89,3 +89,23 @@ module B_Visibility imports A_Visibility {
     }

   }

 }

+

+// ------ qualified type names ----------------------------------

+

+module Q_Imp {

+  class Node { }

+  class Klassy {

+    method Init()

+  }

+}

+

+module Q_M imports Q_Imp {

+  method MyMethod(root: Q_Imp.Node, S: set<Q_Imp.Node>)

+    requires root in S;

+  {

+    var i := new Q_Imp.Node;

+    var j := new Node;

+    assert i != j;  // fine

+    var q := new Q_Imp.Klassy.Init();

+  }

+}