From dcaef29ffbe2570632e7368d27377fb9ac282d7b Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Fri, 22 Apr 2011 22:57:58 -0700
Subject: Dafny: include source location for array types supplied in input

---
 Source/Dafny/Dafny.atg   | 4 ++--
 Source/Dafny/DafnyAst.cs | 9 +++++----
 Source/Dafny/Parser.cs   | 4 ++--
 3 files changed, 9 insertions(+), 8 deletions(-)

(limited to 'Source/Dafny')

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 23582495..c630d67e 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -555,7 +555,7 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
                                        if (tok.val.Length != 5) {
                                          dims = int.Parse(tok.val.Substring(5));
                                        }
-                                       ty = theBuiltIns.ArrayType(dims, gt[0], true);
+                                       ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
                                     .)
   | Ident<out tok>                  (. gt = new List<Type/*!*/>(); .)
     [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt); .)
@@ -808,7 +808,7 @@ AssignRhs<.out List<Expression> ee, out Type ty, out CallStmt initCall, Expressi
     [ "["                              (. ee = new List<Expression>(); .)
       Expressions<ee>
       "]"                              (. // make sure an array class with this dimensionality exists
-                                          UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
+                                          UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
                                        .)
     | "." Ident<out x>
       "("                              (. args = new List<Expression/*!*/>(); .)
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index d923e5dc..f76f24de 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -40,20 +40,21 @@ namespace Microsoft.Dafny {
       ClassDecl obj = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), null);
       SystemModule.TopLevelDecls.Add(obj);
       // add one-dimensional arrays, since they may arise during type checking
-      UserDefinedType tmp = ArrayType(1, Type.Int, true);
+      UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true);
     }
 
     public UserDefinedType ArrayType(int dims, Type arg) {
-      return ArrayType(dims, arg, false);
+      return ArrayType(Token.NoToken, dims, arg, false);
     }
-    public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) {
+    public UserDefinedType ArrayType(IToken tok, int dims, Type arg, bool allowCreationOfNewClass) {
+      Contract.Requires(tok != null);
       Contract.Requires(1 <= dims);
       Contract.Requires(arg != null);
       Contract.Ensures(Contract.Result<UserDefinedType>() != null);
 
       List<Type/*!*/> typeArgs = new List<Type/*!*/>();
       typeArgs.Add(arg);
-      UserDefinedType udt = new UserDefinedType(Token.NoToken, ArrayClassName(dims), typeArgs);
+      UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs);
       if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {
         ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule);
         for (int d = 0; d < dims; d++) {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 180f15ab..e2a45ceb 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -877,7 +877,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (tok.val.Length != 5) {
 			  dims = int.Parse(tok.val.Substring(5));
 			}
-			ty = theBuiltIns.ArrayType(dims, gt[0], true);
+			ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
 			
 		} else if (la.kind == 1) {
 			Ident(out tok);
@@ -1419,7 +1419,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 					ee = new List<Expression>(); 
 					Expressions(ee);
 					Expect(53);
-					UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
+					UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
 					
 				} else {
 					Get();
-- 
cgit v1.2.3