diff options
| author |  rustanleino <unknown> | 2011-02-19 04:19:05 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-02-19 04:19:05 +0000 |
| commit | d4fa0b13799c9639b106b909e6d4b5cb36841b9e (patch) | |
| tree | 103f74b5216530ba430290dcab9fde1ae9acb6d2 /Source/Dafny/DafnyAst.cs | |
| parent | b841cb8090c47b0807292c76f591bf38d0bbe9df (diff) | |
Dafny: Improved scheme for splitting expressions. Also, report each split in error messages.
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 43 |
1 files changed, 42 insertions, 1 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 1ae19313..d2536aa4 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1644,7 +1644,48 @@ namespace Microsoft.Dafny { // ------------------------------------------------------------------------------------------------------
- public abstract class Expression {
+ public class NestedToken : IToken
+ {
+ public NestedToken(IToken outer, IToken inner) {
+ Outer = outer;
+ Inner = inner;
+ }
+ public readonly IToken Outer;
+ public readonly IToken Inner;
+
+ public int col {
+ get { return Outer.col; }
+ set { Outer.col = value; }
+ }
+ public string filename {
+ get { return Outer.filename; }
+ set { Outer.filename = value; }
+ }
+ public bool IsValid {
+ get { return Outer.IsValid; }
+ }
+ public int kind {
+ get { return Outer.kind; }
+ set { Outer.kind = value; }
+ }
+ public int line {
+ get { return Outer.line; }
+ set { Outer.line = value; }
+ }
+ public int pos {
+ get { return Outer.pos; }
+ set { Outer.pos = value; }
+ }
+ public string val {
+ get { return Outer.val; }
+ set { Outer.val = value; }
+ }
+ }
+
+ // ------------------------------------------------------------------------------------------------------
+
+ public abstract class Expression
+ {
public readonly IToken tok;
[ContractInvariantMethod]
void ObjectInvariant() {
|