summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2013-03-06 15:09:04 -0800
committerGravatar Rustan Leino <unknown>2013-03-06 15:09:04 -0800
commit172554c51fad4092f2b4e52a921ad0e86fa67ca6 (patch)
treecc3c3430f1a379255f9c4990b26df1c21e06bd38 /Source
parentd584ab2b4240b58cd4ef59e53b970a05d8d13f79 (diff)
Renamed "parallel" statement to "forall" statement, and made the parentheses around the bound variables optional.
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/Cloner.cs6
-rw-r--r--Source/Dafny/Compiler.cs16
-rw-r--r--Source/Dafny/Dafny.atg24
-rw-r--r--Source/Dafny/DafnyAst.cs6
-rw-r--r--Source/Dafny/Parser.cs406
-rw-r--r--Source/Dafny/Printer.cs11
-rw-r--r--Source/Dafny/RefinementTransformer.cs6
-rw-r--r--Source/Dafny/Resolver.cs128
-rw-r--r--Source/Dafny/Scanner.cs72
-rw-r--r--Source/Dafny/Translator.cs54
-rw-r--r--Source/DafnyExtension/IdentifierTagger.cs4
-rw-r--r--Source/DafnyExtension/TokenTagger.cs1
12 files changed, 383 insertions, 351 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 8cd2f4ae..dbbb6a40 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -448,9 +448,9 @@ namespace Microsoft.Dafny
var s = (AlternativeLoopStmt)stmt;
r = new AlternativeLoopStmt(Tok(s.Tok), s.Invariants.ConvertAll(CloneMayBeFreeExpr), CloneSpecExpr(s.Decreases), CloneSpecFrameExpr(s.Mod), s.Alternatives.ConvertAll(CloneGuardedAlternative));
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
- r = new ParallelStmt(Tok(s.Tok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
+ r = new ForallStmt(Tok(s.Tok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
} else if (stmt is CalcStmt) {
var s = (CalcStmt)stmt;
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 60084fb8..6e5dd2ef 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1163,26 +1163,26 @@ namespace Microsoft.Dafny {
wr.WriteLine("}");
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
- if (s.Kind != ParallelStmt.ParBodyKind.Assign) {
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
+ if (s.Kind != ForallStmt.ParBodyKind.Assign) {
// Call and Proof have no side effects, so they can simply be optimized away.
return;
} else if (s.BoundVars.Count == 0) {
- // the bound variables just spell out a single point, so the parallel statement is equivalent to one execution of the body
+ // the bound variables just spell out a single point, so the forall statement is equivalent to one execution of the body
TrStmt(s.Body, indent);
return;
}
var s0 = (AssignStmt)s.S0;
if (s0.Rhs is HavocRhs) {
- // The parallel statement says to havoc a bunch of things. This can be efficiently compiled
+ // The forall statement says to havoc a bunch of things. This can be efficiently compiled
// into doing nothing.
return;
}
var rhs = ((ExprRhs)s0.Rhs).Expr;
// Compile:
- // parallel (w,x,y,z | Range(w,x,y,z)) {
+ // forall (w,x,y,z | Range(w,x,y,z)) {
// LHS(w,x,y,z) := RHS(w,x,y,z);
// }
// where w,x,y,z have types seq<W>,set<X>,int,bool and LHS has L-1 top-level subexpressions
@@ -1206,7 +1206,7 @@ namespace Microsoft.Dafny {
//
// Note, because the .NET Tuple class only supports up to 8 components, the compiler implementation
// here supports arrays only up to 6 dimensions. This does not seem like a serious practical limitation.
- // However, it may be more noticeable if the parallel statement supported parallel assignments in its
+ // However, it may be more noticeable if the forall statement supported forall assignments in its
// body. To support cases where tuples would need more than 8 components, .NET Tuple's would have to
// be nested.
@@ -1231,7 +1231,7 @@ namespace Microsoft.Dafny {
var lhs = (MultiSelectExpr)s0.Lhs;
L = 2 + lhs.Indices.Count;
if (8 < L) {
- Error("compiler currently does not support assignments to more-than-6-dimensional arrays in parallel statements");
+ Error("compiler currently does not support assignments to more-than-6-dimensional arrays in forall statements");
return;
}
tupleTypeArgs = TypeName(lhs.Array.Type);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 11b373cc..c52c33f1 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -881,7 +881,7 @@ OneStmt<out Statement/*!*/ s>
| IfStmt<out s>
| WhileStmt<out s>
| MatchStmt<out s>
- | ParallelStmt<out s>
+ | ForallStmt<out s>
| CalcStmt<out s>
| "label" (. x = t; .)
NoUSIdent<out id> ":"
@@ -1298,9 +1298,10 @@ PrintStmt<out Statement/*!*/ s>
";" (. s = new PrintStmt(x, args); .)
.
-ParallelStmt<out Statement/*!*/ s>
+ForallStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- IToken/*!*/ x;
+ IToken/*!*/ x = Token.NoToken;
+ bool usesOptionalParen = false;
List<BoundVar/*!*/> bvars = null;
Attributes attrs = null;
Expression range = null;
@@ -1310,8 +1311,13 @@ ParallelStmt<out Statement/*!*/ s>
BlockStmt/*!*/ block;
IToken bodyStart, bodyEnd;
.)
- "parallel" (. x = t; .)
- "("
+ ( "forall" (. x = t; .)
+ | "parallel" (. x = t;
+ errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
+ .)
+ )
+ [ "(" (. usesOptionalParen = true; .)
+ ]
[ (. List<BoundVar/*!*/> bvarsX; Attributes attrsX; Expression rangeX; .)
QuantifierDomain<out bvarsX, out attrsX, out rangeX>
(. bvars = bvarsX; attrs = attrsX; range = rangeX;
@@ -1320,14 +1326,16 @@ ParallelStmt<out Statement/*!*/ s>
(. if (bvars == null) { bvars = new List<BoundVar>(); }
if (range == null) { range = new LiteralExpr(x, true); }
.)
- ")"
+ ( ")" (. if (!usesOptionalParen) { SemErr(t, "found but didn't expect a close parenthesis"); } .)
+ | (. if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); } .)
+ )
{ (. isFree = false; .)
[ "free" (. isFree = true; .)
]
"ensures" Expression<out e> ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
}
BlockStmt<out block, out bodyStart, out bodyEnd>
- (. s = new ParallelStmt(x, bvars, attrs, range, ens, block); .)
+ (. s = new ForallStmt(x, bvars, attrs, range, ens, block); .)
.
CalcStmt<out Statement/*!*/ s>
@@ -1929,7 +1937,7 @@ QuantifierDomain<.out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expre
{ ","
IdentTypeOptional<out bv> (. bvars.Add(bv); .)
}
- { Attribute<ref attrs> }
+ { IF(IsAttribute()) Attribute<ref attrs> }
[ "|"
Expression<out range>
]
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index e1b1ed15..281bd466 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2957,7 +2957,7 @@ namespace Microsoft.Dafny {
}
}
- public class ParallelStmt : Statement
+ public class ForallStmt : Statement
{
public readonly List<BoundVar/*!*/> BoundVars; // note, can be the empty list, in which case Range denotes "true"
public readonly Expression/*!*/ Range;
@@ -2980,7 +2980,7 @@ namespace Microsoft.Dafny {
/// * More kinds may be allowed in the future.
/// * One could also allow Call to call non-ghost methods without side effects. However, that
/// would seem pointless in the program, so they are disallowed (to avoid any confusion that
- /// such use of the parallel statement might actually have a point).
+ /// such use of the forall statement might actually have a point).
/// * One could allow Proof even without ensures clauses that "export" what was learned.
/// However, that might give the false impression that the body is nevertheless exported.
/// </summary>
@@ -2996,7 +2996,7 @@ namespace Microsoft.Dafny {
Contract.Invariant(Body != null);
}
- public ParallelStmt(IToken tok, List<BoundVar> boundVars, Attributes attrs, Expression range, List<MaybeFreeExpression/*!*/>/*!*/ ens, Statement body)
+ public ForallStmt(IToken tok, List<BoundVar> boundVars, Attributes attrs, Expression range, List<MaybeFreeExpression/*!*/>/*!*/ ens, Statement body)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(boundVars));
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index ba95908b..7252c56f 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1413,7 +1413,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
PrintStmt(out s);
break;
}
- case 1: case 2: case 24: case 28: case 104: case 105: case 106: case 107: case 108: case 109: {
+ case 1: case 2: case 24: case 28: case 105: case 106: case 107: case 108: case 109: case 110: {
UpdateStmt(out s);
break;
}
@@ -1433,11 +1433,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
MatchStmt(out s);
break;
}
- case 80: {
- ParallelStmt(out s);
+ case 80: case 81: {
+ ForallStmt(out s);
break;
}
- case 81: {
+ case 82: {
CalcStmt(out s);
break;
}
@@ -1782,9 +1782,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
s = new MatchStmt(x, e, cases);
}
- void ParallelStmt(out Statement/*!*/ s) {
+ void ForallStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- IToken/*!*/ x;
+ IToken/*!*/ x = Token.NoToken;
+ bool usesOptionalParen = false;
List<BoundVar/*!*/> bvars = null;
Attributes attrs = null;
Expression range = null;
@@ -1794,9 +1795,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
BlockStmt/*!*/ block;
IToken bodyStart, bodyEnd;
- Expect(80);
- x = t;
- Expect(28);
+ if (la.kind == 80) {
+ Get();
+ x = t;
+ } else if (la.kind == 81) {
+ Get();
+ x = t;
+ errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
+
+ } else SynErr(176);
+ if (la.kind == 28) {
+ Get();
+ usesOptionalParen = true;
+ }
if (la.kind == 1) {
List<BoundVar/*!*/> bvarsX; Attributes attrsX; Expression rangeX;
QuantifierDomain(out bvarsX, out attrsX, out rangeX);
@@ -1806,7 +1817,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (bvars == null) { bvars = new List<BoundVar>(); }
if (range == null) { range = new LiteralExpr(x, true); }
- Expect(30);
+ if (la.kind == 30) {
+ Get();
+ if (!usesOptionalParen) { SemErr(t, "found but didn't expect a close parenthesis"); }
+ } else if (la.kind == 6 || la.kind == 41 || la.kind == 43) {
+ if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); }
+ } else SynErr(177);
while (la.kind == 41 || la.kind == 43) {
isFree = false;
if (la.kind == 41) {
@@ -1819,7 +1835,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ens.Add(new MaybeFreeExpression(e, isFree));
}
BlockStmt(out block, out bodyStart, out bodyEnd);
- s = new ParallelStmt(x, bvars, attrs, range, ens, block);
+ s = new ForallStmt(x, bvars, attrs, range, ens, block);
}
void CalcStmt(out Statement/*!*/ s) {
@@ -1835,7 +1851,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
BlockStmt/*!*/ h;
IToken opTok;
- Expect(81);
+ Expect(82);
x = t;
if (StartOf(19)) {
CalcOp(out opTok, out calcOp);
@@ -1887,7 +1903,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 46) {
Get();
returnTok = t; isYield = true;
- } else SynErr(176);
+ } else SynErr(178);
if (StartOf(21)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
@@ -1993,7 +2009,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(14)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(177);
+ } else SynErr(179);
while (la.kind == 6) {
Attribute(ref attrs);
}
@@ -2014,7 +2030,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (la.kind == 18 || la.kind == 68) {
Suffix(ref e);
}
- } else SynErr(178);
+ } else SynErr(180);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -2059,7 +2075,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(18)) {
BareGuard(out ee);
e = ee;
- } else SynErr(179);
+ } else SynErr(181);
}
void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs) {
@@ -2072,20 +2088,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (StartOf(23)) {
if (la.kind == 41 || la.kind == 76) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 15)) {SynErr(180); Get();}
+ while (!(la.kind == 0 || la.kind == 15)) {SynErr(182); Get();}
Expect(15);
invariants.Add(invariant);
} else if (la.kind == 44) {
- while (!(la.kind == 0 || la.kind == 44)) {SynErr(181); Get();}
+ while (!(la.kind == 0 || la.kind == 44)) {SynErr(183); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 15)) {SynErr(182); Get();}
+ while (!(la.kind == 0 || la.kind == 15)) {SynErr(184); Get();}
Expect(15);
} else {
- while (!(la.kind == 0 || la.kind == 40)) {SynErr(183); Get();}
+ while (!(la.kind == 0 || la.kind == 40)) {SynErr(185); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -2100,7 +2116,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 15)) {SynErr(184); Get();}
+ while (!(la.kind == 0 || la.kind == 15)) {SynErr(186); Get();}
Expect(15);
}
}
@@ -2108,7 +2124,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void Invariant(out MaybeFreeExpression/*!*/ invariant) {
bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null;
- while (!(la.kind == 0 || la.kind == 41 || la.kind == 76)) {SynErr(185); Get();}
+ while (!(la.kind == 0 || la.kind == 41 || la.kind == 76)) {SynErr(187); Get();}
if (la.kind == 41) {
Get();
isFree = true;
@@ -2129,7 +2145,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(14)) {
Expression(out ee);
e = ee;
- } else SynErr(186);
+ } else SynErr(188);
}
void CaseStatement(out MatchCaseStmt/*!*/ c) {
@@ -2168,7 +2184,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(14)) {
Expression(out e);
arg = new Attributes.Argument(t, e);
- } else SynErr(187);
+ } else SynErr(189);
}
void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -2184,7 +2200,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IdentTypeOptional(out bv);
bvars.Add(bv);
}
- while (la.kind == 6) {
+ while (IsAttribute()) {
Attribute(ref attrs);
}
if (la.kind == 24) {
@@ -2214,47 +2230,47 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 82: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 83: {
+ case 84: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 84: {
+ case 85: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 85: {
+ case 86: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 86: {
+ case 87: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 87: {
+ case 88: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 88: case 89: {
+ case 89: case 90: {
EquivOp();
x = t; op = BinaryExpr.Opcode.Iff;
break;
}
- case 90: case 91: {
+ case 91: case 92: {
ImpliesOp();
x = t; op = BinaryExpr.Opcode.Imp;
break;
}
- default: SynErr(188); break;
+ default: SynErr(190); break;
}
}
@@ -2266,7 +2282,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Statement/*!*/ calc;
Token x = la;
- while (la.kind == 6 || la.kind == 81) {
+ while (la.kind == 6 || la.kind == 82) {
if (la.kind == 6) {
BlockStmt(out block, out bodyStart, out bodyEnd);
subhints.Add(block);
@@ -2280,25 +2296,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void EquivOp() {
- if (la.kind == 88) {
+ if (la.kind == 89) {
Get();
- } else if (la.kind == 89) {
+ } else if (la.kind == 90) {
Get();
- } else SynErr(189);
+ } else SynErr(191);
}
void ImpliesOp() {
- if (la.kind == 90) {
+ if (la.kind == 91) {
Get();
- } else if (la.kind == 91) {
+ } else if (la.kind == 92) {
Get();
- } else SynErr(190);
+ } else SynErr(192);
}
void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 88 || la.kind == 89) {
+ while (la.kind == 89 || la.kind == 90) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -2309,7 +2325,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void ImpliesExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
- if (la.kind == 90 || la.kind == 91) {
+ if (la.kind == 91 || la.kind == 92) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -2321,12 +2337,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(24)) {
- if (la.kind == 92 || la.kind == 93) {
+ if (la.kind == 93 || la.kind == 94) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 92 || la.kind == 93) {
+ while (la.kind == 93 || la.kind == 94) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -2337,7 +2353,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 94 || la.kind == 95) {
+ while (la.kind == 95 || la.kind == 96) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -2449,25 +2465,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void AndOp() {
- if (la.kind == 92) {
+ if (la.kind == 93) {
Get();
- } else if (la.kind == 93) {
+ } else if (la.kind == 94) {
Get();
- } else SynErr(191);
+ } else SynErr(193);
}
void OrOp() {
- if (la.kind == 94) {
+ if (la.kind == 95) {
Get();
- } else if (la.kind == 95) {
+ } else if (la.kind == 96) {
Get();
- } else SynErr(192);
+ } else SynErr(194);
}
void Term(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (la.kind == 99 || la.kind == 100) {
+ while (la.kind == 100 || la.kind == 101) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2484,7 +2500,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
case 29: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
- if (la.kind == 96) {
+ if (la.kind == 97) {
Get();
Expect(68);
Expression(out k);
@@ -2502,20 +2518,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 82: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 83: {
+ case 84: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 84: {
+ case 85: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
- if (la.kind == 96) {
+ if (la.kind == 97) {
Get();
Expect(68);
Expression(out k);
@@ -2523,7 +2539,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
break;
}
- case 97: {
+ case 98: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
@@ -2533,10 +2549,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 98: {
+ case 99: {
Get();
x = t; y = Token.NoToken;
- if (la.kind == 98) {
+ if (la.kind == 99) {
Get();
y = t;
}
@@ -2551,29 +2567,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
break;
}
- case 85: {
+ case 86: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 86: {
+ case 87: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 87: {
+ case 88: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(193); break;
+ default: SynErr(195); break;
}
}
void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 58 || la.kind == 101 || la.kind == 102) {
+ while (la.kind == 58 || la.kind == 102 || la.kind == 103) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2582,33 +2598,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 99) {
+ if (la.kind == 100) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 100) {
+ } else if (la.kind == 101) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(194);
+ } else SynErr(196);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 100: {
+ case 101: {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 98: case 103: {
+ case 99: case 104: {
NegOp();
x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 25: case 50: case 60: case 66: case 71: case 77: case 78: case 81: case 112: case 113: case 114: case 115: {
+ case 25: case 50: case 60: case 66: case 71: case 77: case 78: case 80: case 82: case 113: case 114: case 115: {
EndlessExpression(out e);
break;
}
@@ -2645,17 +2661,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
MapComprehensionExpr(x, out e);
} else if (StartOf(26)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(195);
+ } else SynErr(197);
break;
}
- case 2: case 24: case 28: case 104: case 105: case 106: case 107: case 108: case 109: {
+ case 2: case 24: case 28: case 105: case 106: case 107: case 108: case 109: case 110: {
ConstAtomExpression(out e);
while (la.kind == 18 || la.kind == 68) {
Suffix(ref e);
}
break;
}
- default: SynErr(196); break;
+ default: SynErr(198); break;
}
}
@@ -2664,21 +2680,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 58) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 101) {
+ } else if (la.kind == 102) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 102) {
+ } else if (la.kind == 103) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(197);
+ } else SynErr(199);
}
void NegOp() {
- if (la.kind == 98) {
+ if (la.kind == 99) {
Get();
- } else if (la.kind == 103) {
+ } else if (la.kind == 104) {
Get();
- } else SynErr(198);
+ } else SynErr(200);
}
void EndlessExpression(out Expression e) {
@@ -2692,7 +2708,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
x = t;
Expression(out e);
- Expect(110);
+ Expect(111);
Expression(out e0);
Expect(72);
Expression(out e1);
@@ -2703,7 +2719,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
MatchExpression(out e);
break;
}
- case 112: case 113: case 114: case 115: {
+ case 80: case 113: case 114: case 115: {
QuantifierGuts(out e);
break;
}
@@ -2729,7 +2745,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new AssumeExpr(x, e0, e1);
break;
}
- case 81: {
+ case 82: {
CalcStmt(out s);
Expression(out e1);
e = new CalcExpr(s.Tok, (CalcStmt)s, e1);
@@ -2743,7 +2759,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
NamedExpr(out e);
break;
}
- default: SynErr(199); break;
+ default: SynErr(201); break;
}
}
@@ -2759,9 +2775,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out id);
idents.Add(id);
}
- if (la.kind == 28 || la.kind == 96) {
+ if (la.kind == 28 || la.kind == 97) {
args = new List<Expression>();
- if (la.kind == 96) {
+ if (la.kind == 97) {
Get();
id.val = id.val + "#"; Expression k;
Expect(68);
@@ -2788,9 +2804,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 18) {
Get();
Ident(out id);
- if (la.kind == 28 || la.kind == 96) {
+ if (la.kind == 28 || la.kind == 97) {
args = new List<Expression/*!*/>(); func = true;
- if (la.kind == 96) {
+ if (la.kind == 97) {
Get();
id.val = id.val + "#"; Expression k;
Expect(68);
@@ -2813,7 +2829,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (StartOf(14)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 111) {
+ if (la.kind == 112) {
Get();
anyDots = true;
if (StartOf(14)) {
@@ -2835,15 +2851,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
multipleIndices.Add(ee);
}
- } else SynErr(200);
- } else if (la.kind == 111) {
+ } else SynErr(202);
+ } else if (la.kind == 112) {
Get();
anyDots = true;
if (StartOf(14)) {
Expression(out ee);
e1 = ee;
}
- } else SynErr(201);
+ } else SynErr(203);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -2867,7 +2883,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(69);
- } else SynErr(202);
+ } else SynErr(204);
}
void DisplayExpr(out Expression e) {
@@ -2891,7 +2907,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
e = new SeqDisplayExpr(x, elements);
Expect(69);
- } else SynErr(203);
+ } else SynErr(205);
}
void MultiSetExpr(out Expression e) {
@@ -2917,7 +2933,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(30);
} else if (StartOf(27)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(204);
+ } else SynErr(206);
}
void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {
@@ -2958,17 +2974,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = dummyExpr;
switch (la.kind) {
- case 104: {
+ case 105: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 105: {
+ case 106: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 106: {
+ case 107: {
Get();
e = new LiteralExpr(t);
break;
@@ -2978,12 +2994,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new LiteralExpr(t, n);
break;
}
- case 107: {
+ case 108: {
Get();
e = new ThisExpr(t);
break;
}
- case 108: {
+ case 109: {
Get();
x = t;
Expect(28);
@@ -2992,7 +3008,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new FreshExpr(x, e);
break;
}
- case 109: {
+ case 110: {
Get();
x = t;
Expect(28);
@@ -3017,7 +3033,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(30);
break;
}
- default: SynErr(205); break;
+ default: SynErr(207); break;
}
}
@@ -3053,7 +3069,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 117) {
Get();
- } else SynErr(206);
+ } else SynErr(208);
}
void MatchExpression(out Expression/*!*/ e) {
@@ -3078,13 +3094,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression range;
Expression/*!*/ body;
- if (la.kind == 112 || la.kind == 113) {
+ if (la.kind == 80 || la.kind == 113) {
Forall();
x = t; univ = true;
} else if (la.kind == 114 || la.kind == 115) {
Exists();
x = t;
- } else SynErr(207);
+ } else SynErr(209);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body);
@@ -3147,7 +3163,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 65) {
Get();
exact = false;
- } else SynErr(208);
+ } else SynErr(210);
Expression(out e);
letRHSs.Add(e);
while (la.kind == 26) {
@@ -3200,11 +3216,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void Forall() {
- if (la.kind == 112) {
+ if (la.kind == 80) {
Get();
} else if (la.kind == 113) {
Get();
- } else SynErr(209);
+ } else SynErr(211);
}
void Exists() {
@@ -3212,7 +3228,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 115) {
Get();
- } else SynErr(210);
+ } else SynErr(212);
}
void AttributeBody(ref Attributes attrs) {
@@ -3248,7 +3264,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
static readonly bool[,]/*!*/ set = {
- {T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,T,T, T,T,x,x, T,x,x,T, x,x,T,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
+ {T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,T,T, T,T,x,x, T,x,x,T, x,x,T,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
@@ -3258,25 +3274,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,T, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
- {T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
- {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,T, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,x,x,x, x,T,x,x, T,T,T,x, T,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,x, x,x,x,x, x,x,T,T, x,x,x,x, T,T,x,x},
- {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,x,x,x, T,T,x,x, T,T,T,x, T,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,x, x,x,x,x, x,x,T,T, x,x,x,x, T,T,x,x},
- {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x}
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,x,x,x, x,T,x,x, T,T,T,x, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, T,T,x,x},
+ {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,x,x,x, T,T,x,x, T,T,T,x, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, T,T,x,x},
+ {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x}
};
} // end Parser
@@ -3381,39 +3397,39 @@ public class Errors {
case 77: s = "\"match\" expected"; break;
case 78: s = "\"assert\" expected"; break;
case 79: s = "\"print\" expected"; break;
- case 80: s = "\"parallel\" expected"; break;
- case 81: s = "\"calc\" expected"; break;
- case 82: s = "\"<=\" expected"; break;
- case 83: s = "\">=\" expected"; break;
- case 84: s = "\"!=\" expected"; break;
- case 85: s = "\"\\u2260\" expected"; break;
- case 86: s = "\"\\u2264\" expected"; break;
- case 87: s = "\"\\u2265\" expected"; break;
- case 88: s = "\"<==>\" expected"; break;
- case 89: s = "\"\\u21d4\" expected"; break;
- case 90: s = "\"==>\" expected"; break;
- case 91: s = "\"\\u21d2\" expected"; break;
- case 92: s = "\"&&\" expected"; break;
- case 93: s = "\"\\u2227\" expected"; break;
- case 94: s = "\"||\" expected"; break;
- case 95: s = "\"\\u2228\" expected"; break;
- case 96: s = "\"#\" expected"; break;
- case 97: s = "\"in\" expected"; break;
- case 98: s = "\"!\" expected"; break;
- case 99: s = "\"+\" expected"; break;
- case 100: s = "\"-\" expected"; break;
- case 101: s = "\"/\" expected"; break;
- case 102: s = "\"%\" expected"; break;
- case 103: s = "\"\\u00ac\" expected"; break;
- case 104: s = "\"false\" expected"; break;
- case 105: s = "\"true\" expected"; break;
- case 106: s = "\"null\" expected"; break;
- case 107: s = "\"this\" expected"; break;
- case 108: s = "\"fresh\" expected"; break;
- case 109: s = "\"old\" expected"; break;
- case 110: s = "\"then\" expected"; break;
- case 111: s = "\"..\" expected"; break;
- case 112: s = "\"forall\" expected"; break;
+ case 80: s = "\"forall\" expected"; break;
+ case 81: s = "\"parallel\" expected"; break;
+ case 82: s = "\"calc\" expected"; break;
+ case 83: s = "\"<=\" expected"; break;
+ case 84: s = "\">=\" expected"; break;
+ case 85: s = "\"!=\" expected"; break;
+ case 86: s = "\"\\u2260\" expected"; break;
+ case 87: s = "\"\\u2264\" expected"; break;
+ case 88: s = "\"\\u2265\" expected"; break;
+ case 89: s = "\"<==>\" expected"; break;
+ case 90: s = "\"\\u21d4\" expected"; break;
+ case 91: s = "\"==>\" expected"; break;
+ case 92: s = "\"\\u21d2\" expected"; break;
+ case 93: s = "\"&&\" expected"; break;
+ case 94: s = "\"\\u2227\" expected"; break;
+ case 95: s = "\"||\" expected"; break;
+ case 96: s = "\"\\u2228\" expected"; break;
+ case 97: s = "\"#\" expected"; break;
+ case 98: s = "\"in\" expected"; break;
+ case 99: s = "\"!\" expected"; break;
+ case 100: s = "\"+\" expected"; break;
+ case 101: s = "\"-\" expected"; break;
+ case 102: s = "\"/\" expected"; break;
+ case 103: s = "\"%\" expected"; break;
+ case 104: s = "\"\\u00ac\" expected"; break;
+ case 105: s = "\"false\" expected"; break;
+ case 106: s = "\"true\" expected"; break;
+ case 107: s = "\"null\" expected"; break;
+ case 108: s = "\"this\" expected"; break;
+ case 109: s = "\"fresh\" expected"; break;
+ case 110: s = "\"old\" expected"; break;
+ case 111: s = "\"then\" expected"; break;
+ case 112: s = "\"..\" expected"; break;
case 113: s = "\"\\u2200\" expected"; break;
case 114: s = "\"exists\" expected"; break;
case 115: s = "\"\\u2203\" expected"; break;
@@ -3477,41 +3493,43 @@ public class Errors {
case 173: s = "invalid IfStmt"; break;
case 174: s = "invalid WhileStmt"; break;
case 175: s = "invalid WhileStmt"; break;
- case 176: s = "invalid ReturnStmt"; break;
- case 177: s = "invalid Rhs"; break;
- case 178: s = "invalid Lhs"; break;
- case 179: s = "invalid Guard"; break;
- case 180: s = "this symbol not expected in LoopSpec"; break;
- case 181: s = "this symbol not expected in LoopSpec"; break;
+ case 176: s = "invalid ForallStmt"; break;
+ case 177: s = "invalid ForallStmt"; break;
+ case 178: s = "invalid ReturnStmt"; break;
+ case 179: s = "invalid Rhs"; break;
+ case 180: s = "invalid Lhs"; break;
+ case 181: s = "invalid Guard"; break;
case 182: s = "this symbol not expected in LoopSpec"; break;
case 183: s = "this symbol not expected in LoopSpec"; break;
case 184: s = "this symbol not expected in LoopSpec"; break;
- case 185: s = "this symbol not expected in Invariant"; break;
- case 186: s = "invalid BareGuard"; break;
- case 187: s = "invalid AttributeArg"; break;
- case 188: s = "invalid CalcOp"; break;
- case 189: s = "invalid EquivOp"; break;
- case 190: s = "invalid ImpliesOp"; break;
- case 191: s = "invalid AndOp"; break;
- case 192: s = "invalid OrOp"; break;
- case 193: s = "invalid RelOp"; break;
- case 194: s = "invalid AddOp"; break;
- case 195: s = "invalid UnaryExpression"; break;
- case 196: s = "invalid UnaryExpression"; break;
- case 197: s = "invalid MulOp"; break;
- case 198: s = "invalid NegOp"; break;
- case 199: s = "invalid EndlessExpression"; break;
- case 200: s = "invalid Suffix"; break;
- case 201: s = "invalid Suffix"; break;
+ case 185: s = "this symbol not expected in LoopSpec"; break;
+ case 186: s = "this symbol not expected in LoopSpec"; break;
+ case 187: s = "this symbol not expected in Invariant"; break;
+ case 188: s = "invalid BareGuard"; break;
+ case 189: s = "invalid AttributeArg"; break;
+ case 190: s = "invalid CalcOp"; break;
+ case 191: s = "invalid EquivOp"; break;
+ case 192: s = "invalid ImpliesOp"; break;
+ case 193: s = "invalid AndOp"; break;
+ case 194: s = "invalid OrOp"; break;
+ case 195: s = "invalid RelOp"; break;
+ case 196: s = "invalid AddOp"; break;
+ case 197: s = "invalid UnaryExpression"; break;
+ case 198: s = "invalid UnaryExpression"; break;
+ case 199: s = "invalid MulOp"; break;
+ case 200: s = "invalid NegOp"; break;
+ case 201: s = "invalid EndlessExpression"; break;
case 202: s = "invalid Suffix"; break;
- case 203: s = "invalid DisplayExpr"; break;
- case 204: s = "invalid MultiSetExpr"; break;
- case 205: s = "invalid ConstAtomExpression"; break;
- case 206: s = "invalid QSep"; break;
- case 207: s = "invalid QuantifierGuts"; break;
- case 208: s = "invalid LetExpr"; break;
- case 209: s = "invalid Forall"; break;
- case 210: s = "invalid Exists"; break;
+ case 203: s = "invalid Suffix"; break;
+ case 204: s = "invalid Suffix"; break;
+ case 205: s = "invalid DisplayExpr"; break;
+ case 206: s = "invalid MultiSetExpr"; break;
+ case 207: s = "invalid ConstAtomExpression"; break;
+ case 208: s = "invalid QSep"; break;
+ case 209: s = "invalid QuantifierGuts"; break;
+ case 210: s = "invalid LetExpr"; break;
+ case 211: s = "invalid Forall"; break;
+ case 212: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
@@ -3530,6 +3548,12 @@ public class Errors {
count++;
}
+ public void Warning(IToken/*!*/ tok, string/*!*/ msg) { // warnings
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
+ Warning(tok.filename, tok.line, tok.col, msg);
+ }
+
public virtual void Warning(string filename, int line, int col, string msg) {
Contract.Requires(msg != null);
errorStream.WriteLine(warningMsgFormat, filename, line, col, msg);
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 1ed04767..dbb53243 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -629,16 +629,17 @@ namespace Microsoft.Dafny {
Indent(indent);
wr.Write("}");
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
- wr.Write("parallel (");
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
+ wr.Write("forall");
if (s.BoundVars.Count != 0) {
+ wr.Write(" ");
PrintQuantifierDomain(s.BoundVars, s.Attributes, s.Range);
}
if (s.Ens.Count == 0) {
- wr.Write(") ");
+ wr.Write(" ");
} else {
- wr.WriteLine(")");
+ wr.WriteLine();
PrintSpec("ensures", s.Ens, indent + IndentAmount);
Indent(indent);
}
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index a49b3b42..f92620fe 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -1313,9 +1313,9 @@ namespace Microsoft.Dafny
});
} else if (s is CallStmt) {
reporter.Error(s.Tok, "cannot have call statement");
- } else if (s is ParallelStmt) {
- if (((ParallelStmt)s).Kind == ParallelStmt.ParBodyKind.Assign) // allow Proof and Call (as neither touch any existing state)
- reporter.Error(s.Tok, "cannot have parallel statement");
+ } else if (s is ForallStmt) {
+ if (((ForallStmt)s).Kind == ForallStmt.ParBodyKind.Assign) // allow Proof and Call (as neither touch any existing state)
+ reporter.Error(s.Tok, "cannot have forall statement");
} else {
if (s is WhileStmt || s is AlternativeLoopStmt) {
loopLevels++;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index bc8b6c27..0250b2a3 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1625,14 +1625,14 @@ namespace Microsoft.Dafny
return TailRecursionStatus.NotTailRecursive;
}
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
var status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);
if (status != TailRecursionStatus.CanBeFollowedByAnything) {
if (status == TailRecursionStatus.NotTailRecursive) {
// an error has already been reported
} else if (reportErrors) {
- Error(tailCall.Tok, "a recursive call inside a parallel statement is not a tail call");
+ Error(tailCall.Tok, "a recursive call inside a forall statement is not a tail call");
}
return TailRecursionStatus.NotTailRecursive;
}
@@ -1840,8 +1840,8 @@ namespace Microsoft.Dafny
CheckEqualityTypes(alt.Guard);
alt.Body.Iter(CheckEqualityTypes_Stmt);
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
CheckEqualityTypes(s.Range);
CheckEqualityTypes_Stmt(s.Body);
} else if (stmt is MatchStmt) {
@@ -2065,8 +2065,8 @@ namespace Microsoft.Dafny
CheckTypeInference(alt.Guard);
alt.Body.Iter(CheckTypeInference);
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
CheckTypeInference(s.Range);
CheckTypeInference(s.Body);
s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable"));
@@ -3610,7 +3610,7 @@ namespace Microsoft.Dafny
Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
if (!slhs.SelectOne) {
- Error(stmt, "cannot assign to a range of array elements (try the 'parallel' statement)");
+ Error(stmt, "cannot assign to a range of array elements (try the 'forall' statement)");
}
}
@@ -3770,8 +3770,8 @@ namespace Microsoft.Dafny
// any type is fine
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
int prevErrorCount = ErrorCount;
scope.PushMarker();
@@ -3784,7 +3784,7 @@ namespace Microsoft.Dafny
ResolveExpression(s.Range, true, codeContext);
Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(s.Range.Type, Type.Bool)) {
- Error(stmt, "range restriction in parallel statement must be of type bool (instead got {0})", s.Range.Type);
+ Error(stmt, "range restriction in forall statement must be of type bool (instead got {0})", s.Range.Type);
}
foreach (var ens in s.Ens) {
ResolveExpression(ens.E, true, codeContext);
@@ -3807,7 +3807,7 @@ namespace Microsoft.Dafny
}
s.IsGhost = bodyMustBeSpecOnly;
- // clear the labels for the duration of checking the body, because break statements are not allowed to leave a parallel statement
+ // clear the labels for the duration of checking the body, because break statements are not allowed to leave a forall statement
var prevLblStmts = labeledStatements;
var prevLoopStack = loopStack;
labeledStatements = new Scope<Statement>();
@@ -3821,33 +3821,33 @@ namespace Microsoft.Dafny
// determine the Kind and run some additional checks on the body
if (s.Ens.Count != 0) {
// The only supported kind with ensures clauses is Proof.
- s.Kind = ParallelStmt.ParBodyKind.Proof;
+ s.Kind = ForallStmt.ParBodyKind.Proof;
} else {
// There are three special cases:
- // * Assign, which is the only kind of the parallel statement that allows a heap update.
+ // * Assign, which is the only kind of the forall statement that allows a heap update.
// * Call, which is a single call statement with no side effects or output parameters.
// * A single calc statement, which is a special case of Proof where the postcondition can be inferred.
- // The effect of Assign and the postcondition of Call will be seen outside the parallel
+ // The effect of Assign and the postcondition of Call will be seen outside the forall
// statement.
Statement s0 = s.S0;
if (s0 is AssignStmt) {
- s.Kind = ParallelStmt.ParBodyKind.Assign;
+ s.Kind = ForallStmt.ParBodyKind.Assign;
} else if (s0 is CallStmt) {
- s.Kind = ParallelStmt.ParBodyKind.Call;
+ s.Kind = ForallStmt.ParBodyKind.Call;
} else if (s0 is CalcStmt) {
- s.Kind = ParallelStmt.ParBodyKind.Proof;
+ s.Kind = ForallStmt.ParBodyKind.Proof;
// add the conclusion of the calc as a free postcondition
s.Ens.Add(new MaybeFreeExpression(((CalcStmt)s0).Result, true));
} else {
- s.Kind = ParallelStmt.ParBodyKind.Proof;
+ s.Kind = ForallStmt.ParBodyKind.Proof;
if (s.Body is BlockStmt && ((BlockStmt)s.Body).Body.Count == 0) {
// an empty statement, so don't produce any warning
} else {
- Warning(s.Tok, "the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause");
+ Warning(s.Tok, "the conclusion of the body of this forall statement will not be known outside the forall statement; consider using an 'ensures' clause");
}
}
}
- CheckParallelBodyRestrictions(s.Body, s.Kind);
+ CheckForallStatementBodyRestrictions(s.Body, s.Kind);
}
} else if (stmt is CalcStmt) {
@@ -3881,7 +3881,7 @@ namespace Microsoft.Dafny
e0 = e1;
}
- // clear the labels for the duration of checking the hints, because break statements are not allowed to leave a parallel statement
+ // clear the labels for the duration of checking the hints, because break statements are not allowed to leave a forall statement
var prevLblStmts = labeledStatements;
var prevLoopStack = loopStack;
labeledStatements = new Scope<Statement>();
@@ -4016,7 +4016,7 @@ namespace Microsoft.Dafny
Error(lhs, "cannot assign to non-ghost variable in a ghost context");
}
if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {
- Error(lhs, "cannot assign to a range of array elements (try the 'parallel' statement)");
+ Error(lhs, "cannot assign to a range of array elements (try the 'forall' statement)");
}
}
// Resolve RHSs
@@ -4385,47 +4385,47 @@ namespace Microsoft.Dafny
}
/// <summary>
- /// This method performs some additional checks on the body "stmt" of a parallel statement of kind "kind".
+ /// This method performs some additional checks on the body "stmt" of a forall statement of kind "kind".
/// </summary>
- public void CheckParallelBodyRestrictions(Statement stmt, ParallelStmt.ParBodyKind kind) {
+ public void CheckForallStatementBodyRestrictions(Statement stmt, ForallStmt.ParBodyKind kind) {
Contract.Requires(stmt != null);
if (stmt is PredicateStmt) {
// cool
} else if (stmt is PrintStmt) {
- Error(stmt, "print statement is not allowed inside a parallel statement");
+ Error(stmt, "print statement is not allowed inside a forall statement");
} else if (stmt is BreakStmt) {
- // this case is checked already in the first pass through the parallel body, by doing so from an empty set of labeled statements and resetting the loop-stack
+ // this case is checked already in the first pass through the forall-statement body, by doing so from an empty set of labeled statements and resetting the loop-stack
} else if (stmt is ReturnStmt) {
- Error(stmt, "return statement is not allowed inside a parallel statement");
+ Error(stmt, "return statement is not allowed inside a forall statement");
} else if (stmt is YieldStmt) {
- Error(stmt, "yield statement is not allowed inside a parallel statement");
+ Error(stmt, "yield statement is not allowed inside a forall statement");
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
foreach (var lhs in s.Lhss) {
- CheckParallelBodyLhs(s.Tok, lhs.Resolved, kind);
+ CheckForallStatementBodyLhs(s.Tok, lhs.Resolved, kind);
}
} else if (stmt is ConcreteSyntaxStatement) {
var s = (ConcreteSyntaxStatement)stmt;
foreach (var ss in s.ResolvedStatements) {
- CheckParallelBodyRestrictions(ss, kind);
+ CheckForallStatementBodyRestrictions(ss, kind);
}
} else if (stmt is AssignStmt) {
var s = (AssignStmt)stmt;
- CheckParallelBodyLhs(s.Tok, s.Lhs.Resolved, kind);
+ CheckForallStatementBodyLhs(s.Tok, s.Lhs.Resolved, kind);
var rhs = s.Rhs; // ExprRhs and HavocRhs are fine, but TypeRhs is not
if (rhs is TypeRhs) {
- if (kind == ParallelStmt.ParBodyKind.Assign) {
- Error(rhs.Tok, "new allocation not supported in parallel statements");
+ if (kind == ForallStmt.ParBodyKind.Assign) {
+ Error(rhs.Tok, "new allocation not supported in forall statements");
} else {
var t = (TypeRhs)rhs;
if (t.InitCall != null) {
- CheckParallelBodyRestrictions(t.InitCall, kind);
+ CheckForallStatementBodyRestrictions(t.InitCall, kind);
}
}
} else if (rhs is ExprRhs) {
var r = ((ExprRhs)rhs).Expr.Resolved;
- if (kind == ParallelStmt.ParBodyKind.Assign && r is UnaryExpr && ((UnaryExpr)r).Op == UnaryExpr.Opcode.SetChoose) {
- Error(r, "set choose operator not supported inside the enclosing parallel statement");
+ if (kind == ForallStmt.ParBodyKind.Assign && r is UnaryExpr && ((UnaryExpr)r).Op == UnaryExpr.Opcode.SetChoose) {
+ Error(r, "set choose operator not supported inside the enclosing forall statement");
}
}
} else if (stmt is VarDecl) {
@@ -4436,64 +4436,64 @@ namespace Microsoft.Dafny
var idExpr = lhs as IdentifierExpr;
if (idExpr != null) {
if (scope.ContainsDecl(idExpr.Var)) {
- Error(stmt, "body of parallel statement is attempting to update a variable declared outside the parallel statement");
+ Error(stmt, "body of forall statement is attempting to update a variable declared outside the forall statement");
}
} else {
- Error(stmt, "the body of the enclosing parallel statement is not allowed to update heap locations");
+ Error(stmt, "the body of the enclosing forall statement is not allowed to update heap locations");
}
}
if (!s.Method.IsGhost) {
- // The reason for this restriction is that the compiler is going to omit the parallel statement altogether--it has
+ // The reason for this restriction is that the compiler is going to omit the forall statement altogether--it has
// no effect. However, print effects are not documented, so to make sure that the compiler does not omit a call to
// a method that prints something, all calls to non-ghost methods are disallowed. (Note, if this restriction
// is somehow lifted in the future, then it is still necessary to enforce s.Method.Mod.Expressions.Count != 0 for
// calls to non-ghost methods.)
- Error(s, "the body of the enclosing parallel statement is not allowed to call non-ghost methods");
+ Error(s, "the body of the enclosing forall statement is not allowed to call non-ghost methods");
}
} else if (stmt is BlockStmt) {
var s = (BlockStmt)stmt;
scope.PushMarker();
foreach (var ss in s.Body) {
- CheckParallelBodyRestrictions(ss, kind);
+ CheckForallStatementBodyRestrictions(ss, kind);
}
scope.PopMarker();
} else if (stmt is IfStmt) {
var s = (IfStmt)stmt;
- CheckParallelBodyRestrictions(s.Thn, kind);
+ CheckForallStatementBodyRestrictions(s.Thn, kind);
if (s.Els != null) {
- CheckParallelBodyRestrictions(s.Els, kind);
+ CheckForallStatementBodyRestrictions(s.Els, kind);
}
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
foreach (var alt in s.Alternatives) {
foreach (var ss in alt.Body) {
- CheckParallelBodyRestrictions(ss, kind);
+ CheckForallStatementBodyRestrictions(ss, kind);
}
}
} else if (stmt is WhileStmt) {
WhileStmt s = (WhileStmt)stmt;
- CheckParallelBodyRestrictions(s.Body, kind);
+ CheckForallStatementBodyRestrictions(s.Body, kind);
} else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
foreach (var alt in s.Alternatives) {
foreach (var ss in alt.Body) {
- CheckParallelBodyRestrictions(ss, kind);
+ CheckForallStatementBodyRestrictions(ss, kind);
}
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
switch (s.Kind) {
- case ParallelStmt.ParBodyKind.Assign:
- Error(stmt, "a parallel statement with heap updates is not allowed inside the body of another parallel statement");
+ case ForallStmt.ParBodyKind.Assign:
+ Error(stmt, "a forall statement with heap updates is not allowed inside the body of another forall statement");
break;
- case ParallelStmt.ParBodyKind.Call:
- case ParallelStmt.ParBodyKind.Proof:
+ case ForallStmt.ParBodyKind.Call:
+ case ForallStmt.ParBodyKind.Proof:
// these are fine, since they don't update any non-local state
break;
default:
@@ -4508,7 +4508,7 @@ namespace Microsoft.Dafny
var s = (MatchStmt)stmt;
foreach (var kase in s.Cases) {
foreach (var ss in kase.Body) {
- CheckParallelBodyRestrictions(ss, kind);
+ CheckForallStatementBodyRestrictions(ss, kind);
}
}
@@ -4517,14 +4517,14 @@ namespace Microsoft.Dafny
}
}
- void CheckParallelBodyLhs(IToken tok, Expression lhs, ParallelStmt.ParBodyKind kind) {
+ void CheckForallStatementBodyLhs(IToken tok, Expression lhs, ForallStmt.ParBodyKind kind) {
var idExpr = lhs as IdentifierExpr;
if (idExpr != null) {
if (scope.ContainsDecl(idExpr.Var)) {
- Error(tok, "body of parallel statement is attempting to update a variable declared outside the parallel statement");
+ Error(tok, "body of forall statement is attempting to update a variable declared outside the forall statement");
}
- } else if (kind != ParallelStmt.ParBodyKind.Assign) {
- Error(tok, "the body of the enclosing parallel statement is not allowed to update heap locations");
+ } else if (kind != ForallStmt.ParBodyKind.Assign) {
+ Error(tok, "the body of the enclosing forall statement is not allowed to update heap locations");
}
}
@@ -4599,14 +4599,14 @@ namespace Microsoft.Dafny
}
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
switch (s.Kind) {
- case ParallelStmt.ParBodyKind.Assign:
- Error(stmt, "a parallel statement with heap updates is not allowed inside a hint");
+ case ForallStmt.ParBodyKind.Assign:
+ Error(stmt, "a forall statement with heap updates is not allowed inside a hint");
break;
- case ParallelStmt.ParBodyKind.Call:
- case ParallelStmt.ParBodyKind.Proof:
+ case ForallStmt.ParBodyKind.Call:
+ case ForallStmt.ParBodyKind.Proof:
// these are fine, since they don't update any non-local state
break;
default:
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index ca20b113..9802a282 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -542,17 +542,17 @@ public class Scanner {
case "match": t.kind = 77; break;
case "assert": t.kind = 78; break;
case "print": t.kind = 79; break;
- case "parallel": t.kind = 80; break;
- case "calc": t.kind = 81; break;
- case "in": t.kind = 97; break;
- case "false": t.kind = 104; break;
- case "true": t.kind = 105; break;
- case "null": t.kind = 106; break;
- case "this": t.kind = 107; break;
- case "fresh": t.kind = 108; break;
- case "old": t.kind = 109; break;
- case "then": t.kind = 110; break;
- case "forall": t.kind = 112; break;
+ case "forall": t.kind = 80; break;
+ case "parallel": t.kind = 81; break;
+ case "calc": t.kind = 82; break;
+ case "in": t.kind = 98; break;
+ case "false": t.kind = 105; break;
+ case "true": t.kind = 106; break;
+ case "null": t.kind = 107; break;
+ case "this": t.kind = 108; break;
+ case "fresh": t.kind = 109; break;
+ case "old": t.kind = 110; break;
+ case "then": t.kind = 111; break;
case "exists": t.kind = 114; break;
default: break;
}
@@ -695,49 +695,49 @@ public class Scanner {
case 33:
{t.kind = 74; break;}
case 34:
- {t.kind = 83; break;}
- case 35:
{t.kind = 84; break;}
- case 36:
+ case 35:
{t.kind = 85; break;}
- case 37:
+ case 36:
{t.kind = 86; break;}
- case 38:
+ case 37:
{t.kind = 87; break;}
+ case 38:
+ {t.kind = 88; break;}
case 39:
if (ch == '>') {AddCh(); goto case 40;}
else {goto case 0;}
case 40:
- {t.kind = 88; break;}
- case 41:
{t.kind = 89; break;}
- case 42:
+ case 41:
{t.kind = 90; break;}
- case 43:
+ case 42:
{t.kind = 91; break;}
+ case 43:
+ {t.kind = 92; break;}
case 44:
if (ch == '&') {AddCh(); goto case 45;}
else {goto case 0;}
case 45:
- {t.kind = 92; break;}
- case 46:
{t.kind = 93; break;}
- case 47:
+ case 46:
{t.kind = 94; break;}
- case 48:
+ case 47:
{t.kind = 95; break;}
- case 49:
+ case 48:
{t.kind = 96; break;}
+ case 49:
+ {t.kind = 97; break;}
case 50:
- {t.kind = 99; break;}
- case 51:
{t.kind = 100; break;}
- case 52:
+ case 51:
{t.kind = 101; break;}
- case 53:
+ case 52:
{t.kind = 102; break;}
- case 54:
+ case 53:
{t.kind = 103; break;}
+ case 54:
+ {t.kind = 104; break;}
case 55:
{t.kind = 113; break;}
case 56:
@@ -753,10 +753,10 @@ public class Scanner {
else if (ch == ':') {AddCh(); goto case 57;}
else {t.kind = 5; break;}
case 60:
- recEnd = pos; recKind = 98;
+ recEnd = pos; recKind = 99;
if (ch == 'i') {AddCh(); goto case 12;}
else if (ch == '=') {AddCh(); goto case 35;}
- else {t.kind = 98; break;}
+ else {t.kind = 99; break;}
case 61:
recEnd = pos; recKind = 14;
if (ch == '=') {AddCh(); goto case 66;}
@@ -783,13 +783,13 @@ public class Scanner {
if (ch == '>') {AddCh(); goto case 42;}
else {t.kind = 29; break;}
case 67:
- recEnd = pos; recKind = 111;
+ recEnd = pos; recKind = 112;
if (ch == '.') {AddCh(); goto case 26;}
- else {t.kind = 111; break;}
+ else {t.kind = 112; break;}
case 68:
- recEnd = pos; recKind = 82;
+ recEnd = pos; recKind = 83;
if (ch == '=') {AddCh(); goto case 39;}
- else {t.kind = 82; break;}
+ else {t.kind = 83; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 9252cde5..0fef4319 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1957,10 +1957,10 @@ namespace Microsoft.Dafny {
// Also, let Pre be the precondition and VF be the decreases clause.
// Then, insert into the method body what amounts to:
// assume case-analysis-on-parameter[[ y' ]];
- // parallel (this', y' | Pre(this', x, y') && VF(this', x, y') << VF(this, x, y)) {
+ // forall (this', y' | Pre(this', x, y') && VF(this', x, y') << VF(this, x, y)) {
// this'.M(x, y');
// }
- // Generate bound variables for the parallel statement, and a substitution for the Pre and VF
+ // Generate bound variables for the forall statement, and a substitution for the Pre and VF
// assume case-analysis-on-parameter[[ y' ]];
foreach (var inFormal in m.Ins) {
@@ -2047,14 +2047,14 @@ namespace Microsoft.Dafny {
return DecreasesCheck(decrToks, decrTypes, decrCallee, decrCaller, null, null, false, true);
};
-#if VERIFY_CORRECTNESS_OF_TRANSLATION_PARALLEL_RANGE
+#if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE
var definedness = new Bpl.StmtListBuilder();
var exporter = new Bpl.StmtListBuilder();
- TrParallelCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran);
+ TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
#else
- TrParallelCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran);
+ TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran);
#endif
}
}
@@ -4779,10 +4779,10 @@ namespace Microsoft.Dafny {
delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrAlternatives(s.Alternatives, null, new Bpl.BreakCmd(s.Tok, null), bld, locals, e); },
builder, locals, etran);
- } else if (stmt is ParallelStmt) {
- AddComment(builder, stmt, "parallel statement");
- var s = (ParallelStmt)stmt;
- if (s.Kind == ParallelStmt.ParBodyKind.Assign) {
+ } else if (stmt is ForallStmt) {
+ AddComment(builder, stmt, "forall statement");
+ var s = (ForallStmt)stmt;
+ if (s.Kind == ForallStmt.ParBodyKind.Assign) {
Contract.Assert(s.Ens.Count == 0);
if (s.BoundVars.Count == 0) {
TrStmt(s.Body, builder, locals, etran);
@@ -4790,13 +4790,13 @@ namespace Microsoft.Dafny {
var s0 = (AssignStmt)s.S0;
var definedness = new Bpl.StmtListBuilder();
var updater = new Bpl.StmtListBuilder();
- TrParallelAssign(s, s0, definedness, updater, locals, etran);
+ TrForallAssign(s, s0, definedness, updater, locals, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, updater.Collect(s.Tok)));
builder.Add(CaptureState(stmt.Tok));
}
- } else if (s.Kind == ParallelStmt.ParBodyKind.Call) {
+ } else if (s.Kind == ForallStmt.ParBodyKind.Call) {
Contract.Assert(s.Ens.Count == 0);
if (s.BoundVars.Count == 0) {
TrStmt(s.Body, builder, locals, etran);
@@ -4804,16 +4804,16 @@ namespace Microsoft.Dafny {
var s0 = (CallStmt)s.S0;
var definedness = new Bpl.StmtListBuilder();
var exporter = new Bpl.StmtListBuilder();
- TrParallelCall(s.Tok, s.BoundVars, s.Range, null, s0, definedness, exporter, locals, etran);
+ TrForallStmtCall(s.Tok, s.BoundVars, s.Range, null, s0, definedness, exporter, locals, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, exporter.Collect(s.Tok)));
builder.Add(CaptureState(stmt.Tok));
}
- } else if (s.Kind == ParallelStmt.ParBodyKind.Proof) {
+ } else if (s.Kind == ForallStmt.ParBodyKind.Proof) {
var definedness = new Bpl.StmtListBuilder();
var exporter = new Bpl.StmtListBuilder();
- TrParallelProof(s, definedness, exporter, locals, etran);
+ TrForallProof(s, definedness, exporter, locals, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, exporter.Collect(s.Tok)));
builder.Add(CaptureState(stmt.Tok));
@@ -5101,10 +5101,10 @@ namespace Microsoft.Dafny {
return null; // TODO: this can be improved
}
- void TrParallelAssign(ParallelStmt s, AssignStmt s0,
+ void TrForallAssign(ForallStmt s, AssignStmt s0,
Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder updater, Bpl.VariableSeq locals, ExpressionTranslator etran) {
// The statement:
- // parallel (x,y | Range(x,y)) {
+ // forall (x,y | Range(x,y)) {
// (a) E(x,y) . f := G(x,y);
// (b) A(x,y) [ I0(x,y), I1(x,y), ... ] := G(x,y);
// }
@@ -5204,7 +5204,7 @@ namespace Microsoft.Dafny {
GetObjFieldDetails(lhsPrime, etran, out objPrime, out FPrime);
definedness.Add(Assert(s0.Tok,
Bpl.Expr.Or(Bpl.Expr.Neq(obj, objPrime), Bpl.Expr.Neq(F, FPrime)),
- "left-hand sides for different parallel-statement bound variables may refer to the same location"));
+ "left-hand sides for different forall-statement bound variables may refer to the same location"));
definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
@@ -5266,7 +5266,7 @@ namespace Microsoft.Dafny {
delegate Bpl.Expr ExpressionConverter(Dictionary<IVariable, Expression> substMap, ExpressionTranslator etran);
- void TrParallelCall(IToken tok, List<BoundVar> boundVars, Expression range, ExpressionConverter additionalRange, CallStmt s0,
+ void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, Expression range, ExpressionConverter additionalRange, CallStmt s0,
Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {
Contract.Requires(tok != null);
Contract.Requires(boundVars != null);
@@ -5279,7 +5279,7 @@ namespace Microsoft.Dafny {
Contract.Requires(etran != null);
// Translate:
- // parallel (x,y | Range(x,y)) {
+ // forall (x,y | Range(x,y)) {
// E(x,y) . M( Args(x,y) );
// }
// as:
@@ -5327,7 +5327,7 @@ namespace Microsoft.Dafny {
// Now for the other branch, where the postcondition of the call is exported.
{
- var initHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, "$initHeapParallelStmt#" + otherTmpVarCount, predef.HeapType));
+ var initHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, "$initHeapForallStmt#" + otherTmpVarCount, predef.HeapType));
otherTmpVarCount++;
locals.Add(initHeapVar);
var initHeap = new Bpl.IdentifierExpr(tok, initHeapVar);
@@ -5348,7 +5348,7 @@ namespace Microsoft.Dafny {
RecordNewObjectsIn_New(tok, iter, initHeap, heapIdExpr, exporter, locals, etran);
}
} else {
- // As an optimization, create the illusion that the $Heap is unchanged by the parallel body.
+ // As an optimization, create the illusion that the $Heap is unchanged by the forall-statement body.
exporter.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(etran.Tick())));
}
@@ -5410,9 +5410,9 @@ namespace Microsoft.Dafny {
builder.Add(cmd);
}
- void TrParallelProof(ParallelStmt s, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {
+ void TrForallProof(ForallStmt s, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {
// Translate:
- // parallel (x,y | Range(x,y))
+ // forall (x,y | Range(x,y))
// ensures Post(x,y);
// {
// Body;
@@ -5457,7 +5457,7 @@ namespace Microsoft.Dafny {
bool splitHappened; // we actually don't care
foreach (var split in TrSplitExpr(ens.E, etran, out splitHappened)) {
if (split.IsChecked) {
- definedness.Add(Assert(split.E.tok, split.E, "possible violation of postcondition of parallel statement"));
+ definedness.Add(Assert(split.E.tok, split.E, "possible violation of postcondition of forall statement"));
}
}
}
@@ -5467,7 +5467,7 @@ namespace Microsoft.Dafny {
// Now for the other branch, where the ensures clauses are exported.
- var initHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$initHeapParallelStmt#" + otherTmpVarCount, predef.HeapType));
+ var initHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$initHeapForallStmt#" + otherTmpVarCount, predef.HeapType));
otherTmpVarCount++;
locals.Add(initHeapVar);
var initHeap = new Bpl.IdentifierExpr(s.Tok, initHeapVar);
@@ -5483,7 +5483,7 @@ namespace Microsoft.Dafny {
}
}
} else {
- // As an optimization, create the illusion that the $Heap is unchanged by the parallel body.
+ // As an optimization, create the illusion that the $Heap is unchanged by the forall-statement body.
exporter.Add(new Bpl.HavocCmd(s.Tok, new Bpl.IdentifierExprSeq(etran.Tick())));
}
@@ -6509,7 +6509,7 @@ namespace Microsoft.Dafny {
Contract.Requires(tok != null);
Contract.Requires(lhs != null);
Contract.Requires(!(lhs is ConcreteSyntaxExpression));
- Contract.Requires(!(lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne)); // these were once allowed, but their functionality is now provided by 'parallel' statements
+ Contract.Requires(!(lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne)); // these were once allowed, but their functionality is now provided by 'forall' statements
Contract.Requires(rhs != null);
Contract.Requires(builder != null);
Contract.Requires(cce.NonNullElements(locals));
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index b8e8805a..6a612cbd 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -282,8 +282,8 @@ namespace DafnyLanguage
} else if (stmt is VarDecl) {
var s = (VarDecl)stmt;
IdRegion.Add(regions, s.Tok, s, true, module);
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
s.BoundVars.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index a8f63232..45f1c36c 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -271,7 +271,6 @@ namespace DafnyLanguage
case "object":
case "old":
case "opened":
- case "parallel":
case "predicate":
case "print":
case "reads":
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 03:34:57 +0000