diff options
| author |  rustanleino <unknown> | 2009-11-06 23:54:22 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-06 23:54:22 +0000 |
| commit | 2efa59dea051803bc716d02070aa013397cfccc4 (patch) | |
| tree | bea0fe3564ee6b336db622f8c24a13552f68d10d /Dafny/Dafny.atg | |
| parent | 61993a0cf682448770a0e3223ba560171635c3af (diff) | |
Added a sequence update expression in Dafny.
Diffstat (limited to 'Dafny/Dafny.atg')
| -rw-r--r-- | Dafny/Dafny.atg | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 022dc912..5da2b44b 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -847,14 +847,20 @@ SelectOrCallSuffix<ref Expression! e> [ ".." (. anyDots = true; .)
[ Expression<out ee> (. e1 = ee; .)
]
+ | ":="
+ Expression<out ee> (. e1 = ee; .)
]
| ".." Expression<out ee> (. anyDots = true; e1 = ee; .)
- ) (. 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);
}
.)
"]"
|