Dafny: types can now be qualified with full module paths

6 files changed, 68 insertions, 59 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index d0dd4169..8f9a7717 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -536,8 +536,8 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
 ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>

 = (. Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);

      tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

-     IToken moduleName = null;

      List<Type/*!*/>/*!*/ gt;

+     List<IToken> path;

   .)

   ( "object"                        (. tok = t;  ty = new ObjectType(); .)

   | arrayToken                      (. tok = t;  gt = new List<Type/*!*/>(); .)

@@ -550,11 +550,12 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
                                        }

                                        ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);

                                     .)

-  | Ident<out tok>                  (. gt = new List<Type/*!*/>(); .)

-    [                               (. moduleName = tok; .)

-      "." Ident<out tok>

-    ]

-    [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt, moduleName); .)

+  | Ident<out tok>                  (. gt = new List<Type/*!*/>();

+                                       path = new List<IToken>(); .)

+    {                               (. path.Add(tok); .)

+      "." Ident<out tok>           

+    }

+    [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt, path); .)

   )

   .

 GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>

@@ -802,16 +803,18 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
       "]"                              (. // make sure an array class with this dimensionality exists

                                           UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);

                                        .)

-    | "." Ident<out x>

-      "("                              (. args = new List<Expression/*!*/>(); .)

+    | "." Ident<out x>                 

+      "("                              (. // This case happens when we have type<typeargs>.Constructor(args)

+                                          // There is no ambiguity about where the constructor is or whether one exists.

+                                          args = new List<Expression/*!*/>(); .)

         [ Expressions<args> ]

       ")"                              (. initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args); .)

     | "("                              (. var udf = ty as UserDefinedType;

-                                          if (udf != null && udf.ModuleName != null && udf.TypeArgs.Count == 0) {

-                                            // The parsed name had the form "A.B", so treat "A" as the name of the type and "B" as

+                                          if (udf != null && 0 < udf.Path.Count && udf.TypeArgs.Count == 0) {

+                                            // The parsed name had the form "A.B.Ctr", so treat "A.B" as the name of the type and "Ctr" as

                                             // the name of the constructor that's being invoked.

                                             x = udf.tok;

-                                            ty = new UserDefinedType(udf.ModuleName, udf.ModuleName.val, new List<Type>(), null);

+                                            ty = new UserDefinedType(udf.Path[0], udf.Path[udf.Path.Count-1].val, new List<Type>(), udf.Path.GetRange(0,udf.Path.Count-1));

                                           } else {

                                             SemErr(t, "expected '.'");

                                             x = null;

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index e6a693fa..9d426421 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -414,9 +414,10 @@ namespace Microsoft.Dafny {
       Contract.Invariant(tok != null);

       Contract.Invariant(Name != null);

       Contract.Invariant(cce.NonNullElements(TypeArgs));

+      Contract.Invariant(cce.NonNullElements(Path));

     }

 

-    public readonly IToken ModuleName;  // may be null

+    public readonly List<IToken> Path;  // may be null

     public readonly IToken tok;  // token of the Name

     public readonly string Name;

     [Rep]

@@ -454,11 +455,13 @@ namespace Microsoft.Dafny {
     public TopLevelDecl ResolvedClass;  // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype

     public TypeParameter ResolvedParam;  // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list

 

-    public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Type/*!*/>/*!*/ typeArgs, IToken moduleName) {

+    public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Type/*!*/>/*!*/ typeArgs, List<IToken> moduleName) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(cce.NonNullElements(typeArgs));

-      this.ModuleName = moduleName;

+      Contract.Requires(moduleName == null || cce.NonNullElements(moduleName));

+      if (moduleName != null) this.Path = moduleName;

+      else this.Path = new List<IToken>();

       this.tok = tok;

       this.Name = name;

       this.TypeArgs = typeArgs;

@@ -476,6 +479,7 @@ namespace Microsoft.Dafny {
       this.Name = name;

       this.TypeArgs = typeArgs;

       this.ResolvedClass = cd;

+      this.Path = new List<IToken>();

     }

 

     /// <summary>

@@ -489,6 +493,7 @@ namespace Microsoft.Dafny {
       this.Name = name;

       this.TypeArgs = new List<Type/*!*/>();

       this.ResolvedParam = tp;

+      this.Path = new List<IToken>();

     }

 

     /// <summary>

@@ -522,19 +527,10 @@ namespace Microsoft.Dafny {
     [Pure]

     public override string ToString() {

       Contract.Ensures(Contract.Result<string>() != null);

-

-      string s = Name;

-      if (ModuleName != null) {

-        s = ModuleName.val + "." + s;

-      }

+      

+      string s = Util.Comma(".", Path, i => i.val) + (Path.Count == 0 ? "" : ".") + Name;

       if (TypeArgs.Count != 0) {

-        string sep = "<";

-        foreach (Type t in TypeArgs) {

-          Contract.Assume(cce.IsPeerConsistent(t));

-          s += sep + t;

-          sep = ",";

-        }

-        s += ">";

+        s += "<" + Util.Comma(",", TypeArgs, ty => ty.ToString()) + ">";

       }

       return s;

     }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 0c6cc993..15ea873c 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -984,8 +984,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {

 		Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);

 		tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

-		IToken moduleName = null;

 		List<Type/*!*/>/*!*/ gt;

+		List<IToken> path;

 		

 		if (la.kind == 44) {

 			Get();

@@ -1005,16 +1005,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			

 		} else if (la.kind == 1) {

 			Ident(out tok);

-			gt = new List<Type/*!*/>(); 

-			if (la.kind == 14) {

-				moduleName = tok; 

+			gt = new List<Type/*!*/>();

+			path = new List<IToken>(); 

+			while (la.kind == 14) {

+				path.Add(tok); 

 				Get();

 				Ident(out tok);

 			}

 			if (la.kind == 26) {

 				GenericInstantiation(gt);

 			}

-			ty = new UserDefinedType(tok, tok.val, gt, moduleName); 

+			ty = new UserDefinedType(tok, tok.val, gt, path); 

 		} else SynErr(133);

 	}

 

@@ -1576,11 +1577,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				} else {

 					Get();

 					var udf = ty as UserDefinedType;

-					if (udf != null && udf.ModuleName != null && udf.TypeArgs.Count == 0) {

-					 // The parsed name had the form "A.B", so treat "A" as the name of the type and "B" as

+					if (udf != null && 0 < udf.Path.Count && udf.TypeArgs.Count == 0) {

+					 // The parsed name had the form "A.B.Ctr", so treat "A.B" as the name of the type and "Ctr" as

 					 // the name of the constructor that's being invoked.

 					 x = udf.tok;

-					 ty = new UserDefinedType(udf.ModuleName, udf.ModuleName.val, new List<Type>(), null);

+					 ty = new UserDefinedType(udf.Path[0], udf.Path[udf.Path.Count-1].val, new List<Type>(), udf.Path.GetRange(0,udf.Path.Count-1));

 					} else {

 					 SemErr(t, "expected '.'");

 					 x = null;

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 0d32e24e..0a653f6c 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -279,7 +279,7 @@ namespace Microsoft.Dafny {
         return new MapType(CloneType(tt.Domain), CloneType(tt.Range));

       } else if (t is UserDefinedType) {

         var tt = (UserDefinedType)t;

-        return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.ModuleName == null ? null : Tok(tt.ModuleName));

+        return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(x => Tok(x)));

       } else if (t is InferredTypeProxy) {

         return new InferredTypeProxy();

       } else {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 05cbc74f..0a18b783 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -577,7 +577,7 @@ namespace Microsoft.Dafny {
         return new MapType(CloneType(tt.Domain), CloneType(tt.Range));

       } else if (t is UserDefinedType) {

         var tt = (UserDefinedType)t;

-        return new UserDefinedType(tt.tok, tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.ModuleName == null ? null : tt.ModuleName);

+        return new UserDefinedType(tt.tok, tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(x => x));

       } else if (t is InferredTypeProxy) {

         return new InferredTypeProxy();

       } else {

@@ -1885,7 +1885,7 @@ namespace Microsoft.Dafny {
             Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type");

           }

         }

-        TypeParameter tp = t.ModuleName == null ? allTypeParameters.Find(t.Name) : null;

+        TypeParameter tp = t.Path.Count == 0 ? allTypeParameters.Find(t.Name) : null;

         if (tp != null) {

           if (t.TypeArgs.Count == 0) {

             t.ResolvedParam = tp;

@@ -1894,17 +1894,26 @@ namespace Microsoft.Dafny {
           }

         } else if (t.ResolvedClass == null) {  // this test is because 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string')

           TopLevelDecl d = null;

-          if (t.ModuleName != null) {

-            ModuleSignature sig;

-            if (moduleInfo.FindSubmodule(t.ModuleName.val, out sig)) {

-              if (!sig.TopLevels.TryGetValue(t.Name, out d)) {

-                Error(t.tok, "The name does not exist in the given module");

-              }

+

+          int j = 0;

+          var sig = moduleInfo;

+          while (j < t.Path.Count) {

+            if (sig.FindSubmodule(t.Path[j].val, out sig)) {

+              j++;

             } else {

-              Error(t.ModuleName, "Undeclared module name: {0} (did you forget a module import?)", t.ModuleName.val);

+              Error(t.Path[j], "module {0} does not exist", t.Path[j].val);

+              break;

             }

-          } else if (!moduleInfo.TopLevels.TryGetValue(t.Name, out d)) {

-            Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget a module import?)", t.Name);

+          }

+          if (j == t.Path.Count) {

+            if (!sig.TopLevels.TryGetValue(t.Name, out d)) {

+              if (j == 0)

+                Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget to qualify a name?)", t.Name);

+              else

+                Error(t.tok, "Undeclared type {0} in module {1}", t.Name, t.Path[t.Path.Count - 1].val);

+            }

+          } else {

+            // error has already been reported

           }

 

           if (d == null) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 85958099..a55d68a8 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -714,28 +714,28 @@ Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA
 Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB

 Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB

 Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(53,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)

-Modules0.dfy(54,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

-Modules0.dfy(65,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

-Modules0.dfy(72,20): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)

-Modules0.dfy(72,34): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget a module import?)

-Modules0.dfy(75,23): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget a module import?)

-Modules0.dfy(80,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget a module import?)

-Modules0.dfy(89,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)

-Modules0.dfy(221,15): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)

+Modules0.dfy(53,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)

+Modules0.dfy(54,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

+Modules0.dfy(65,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

+Modules0.dfy(72,20): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)

+Modules0.dfy(72,34): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?)

+Modules0.dfy(75,23): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?)

+Modules0.dfy(80,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)

+Modules0.dfy(89,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)

+Modules0.dfy(221,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

 Modules0.dfy(221,8): Error: new can be applied only to reference types (got X)

-Modules0.dfy(230,13): Error: The name does not exist in the given module

+Modules0.dfy(230,13): Error: Undeclared type X in module B

 Modules0.dfy(240,13): Error: unresolved identifier: X

 Modules0.dfy(241,15): Error: member DoesNotExist does not exist in class X

-Modules0.dfy(280,19): Error: Undeclared top-level type or type parameter: D (did you forget a module import?)

+Modules0.dfy(280,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)

 Modules0.dfy(280,12): Error: new can be applied only to reference types (got D)

 Modules0.dfy(283,25): Error: type of the receiver is not fully determined at this program point

 Modules0.dfy(284,16): Error: type of the receiver is not fully determined at this program point

 Modules0.dfy(284,6): Error: expected method call, found expression

 Modules0.dfy(285,16): Error: type of the receiver is not fully determined at this program point

 Modules0.dfy(285,6): Error: expected method call, found expression

-Modules0.dfy(307,24): Error: Undeclared module name: Q_Imp (did you forget a module import?)

-Modules0.dfy(97,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget a module import?)

+Modules0.dfy(307,24): Error: module Q_Imp does not exist

+Modules0.dfy(97,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)

 28 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------