diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-26 21:20:44 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-26 21:20:44 -0700 |
| commit | 8f0b71a95305b32ccded390ec5117462ffcadef0 (patch) | |
| tree | 6ff77c11dd94f38811b2a1b00e6c84798d1e1c76 /Dafny/Dafny.atg | |
| parent | 2b1732bf84b88b5656a305b781fdb818e5738ea6 (diff) | |
Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" statement)
Diffstat (limited to 'Dafny/Dafny.atg')
| -rw-r--r-- | Dafny/Dafny.atg | 32 |
1 files changed, 1 insertions, 31 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 0092b4d9..9de1421b 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -631,7 +631,6 @@ OneStmt<out Statement/*!*/ s> | IfStmt<out s>
| WhileStmt<out s>
| MatchStmt<out s>
- | ForeachStmt<out s>
| ParallelStmt<out s>
| "label" (. x = t; .)
Ident<out id> ":"
@@ -886,36 +885,7 @@ CaseStatement<out MatchCaseStmt/*!*/ c> (. c = new MatchCaseStmt(x, id.val, arguments, body); .)
.
/*------------------------------------------------------------------------*/
-ForeachStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- IToken/*!*/ x, boundVar;
- Type/*!*/ ty;
- Expression/*!*/ collection;
- Expression/*!*/ range;
- List<PredicateStmt/*!*/> bodyPrefix = new List<PredicateStmt/*!*/>();
- Statement bodyAssign = null;
- .)
- "foreach" (. x = t;
- range = new LiteralExpr(x, true);
- ty = new InferredTypeProxy();
- .)
- "(" Ident<out boundVar>
- [ ":" Type<out ty> ]
- "in" Expression<out collection>
- [ "|" Expression<out range> ]
- ")"
- "{"
- { AssertStmt<out s> (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
- | AssumeStmt<out s> (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
- }
- UpdateStmt<out s> (. bodyAssign = s; .)
- "}" (. if (bodyAssign != null) {
- s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
- } else {
- s = dummyStmt; // some error occurred in parsing the bodyAssign
- }
- .)
- .
+
AssertStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
"assert" (. x = t; .)
|