diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-04-22 22:57:58 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-04-22 22:57:58 -0700 |
| commit | dcaef29ffbe2570632e7368d27377fb9ac282d7b (patch) | |
| tree | a26c6cc36c473c789affea73c81485369a6dbb39 /Source/Dafny | |
| parent | e6609f4aa8c29d32a3b590bf2b4337148a686bf5 (diff) | |
Dafny: include source location for array types supplied in input
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 4 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 9 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 4 |
3 files changed, 9 insertions, 8 deletions
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();
|