diff options
| author |  rustanleino <unknown> | 2009-11-06 23:54:22 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-06 23:54:22 +0000 |
| commit | 8718c8de05f07ffbb3ccbceee550a9c88a599947 (patch) | |
| tree | 5173a2409c40014effac527837c7b892222a988d /Source/Dafny/Parser.ssc | |
| parent | 660c22dc282ee371fdbd4c97e9289ee016a4aca8 (diff) | |
Added a sequence update expression in Dafny.
Diffstat (limited to 'Source/Dafny/Parser.ssc')
| -rw-r--r-- | Source/Dafny/Parser.ssc | 26 |
1 files changed, 18 insertions, 8 deletions
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index 0fd3e612..6b12d796 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -1312,10 +1312,16 @@ public static int Parse (List<ClassDecl!>! classes) { if (StartOf(5)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 78) {
- Get();
- anyDots = true;
- if (StartOf(5)) {
+ if (t.kind == 35 || t.kind == 78) {
+ if (t.kind == 78) {
+ Get();
+ anyDots = true;
+ if (StartOf(5)) {
+ Expression(out ee);
+ e1 = ee;
+ }
+ } else {
+ Get();
Expression(out ee);
e1 = ee;
}
@@ -1325,12 +1331,16 @@ public static int Parse (List<ClassDecl!>! classes) { Expression(out ee);
anyDots = true; e1 = ee;
} else Error(118);
- if (!anyDots) {
- assert e1 == null;
- e = new SeqSelectExpr(x, true, e, e0, null);
- } else {
+ assert !anyDots ==> e0 != null;
+ if (anyDots) {
assert e0 != null || e1 != null;
e = new SeqSelectExpr(x, false, e, e0, e1);
+ } else if (e1 == null) {
+ assert e0 != null;
+ e = new SeqSelectExpr(x, true, e, e0, null);
+ } else {
+ assert e0 != null;
+ e = new SeqUpdateExpr(x, e, e0, e1);
}
Expect(76);
|