summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Cloner.cs5
-rw-r--r--Source/Dafny/Compiler.cs3
-rw-r--r--Source/Dafny/Dafny.atg14
-rw-r--r--Source/Dafny/DafnyAst.cs22
-rw-r--r--Source/Dafny/Parser.cs679
-rw-r--r--Source/Dafny/Printer.cs8
-rw-r--r--Source/Dafny/Resolver.cs10
-rw-r--r--Source/Dafny/Scanner.cs89
-rw-r--r--Source/Dafny/Translator.cs45
-rw-r--r--Source/DafnyExtension/TokenTagger.cs1
-rw-r--r--Test/dafny0/Answer54
-rw-r--r--Test/dafny0/ModifyStmt.dfy160
-rw-r--r--Test/dafny0/ResolutionErrors.dfy10
-rw-r--r--Test/dafny0/runtest.bat2
-rw-r--r--Util/Emacs/dafny-mode.el2
-rw-r--r--Util/latex/dafny.sty2
-rw-r--r--Util/vim/dafny.vim2
17 files changed, 726 insertions, 382 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 8ac0b3a8..8aff4bc6 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -487,6 +487,11 @@ namespace Microsoft.Dafny
var lhss = s.Locals.ConvertAll(c => new LocalVariable(Tok(c.Tok), Tok(c.EndTok), c.Name, CloneType(c.OptionalType), c.IsGhost));
r = new VarDeclStmt(Tok(s.Tok), Tok(s.EndTok), lhss, (ConcreteUpdateStatement)CloneStmt(s.Update));
+ } else if (stmt is ModifyStmt) {
+ var s = (ModifyStmt)stmt;
+ var mod = CloneSpecFrameExpr(s.Mod);
+ r = new ModifyStmt(Tok(s.Tok), Tok(s.EndTok), mod.Expressions, mod.Attributes);
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 77bbd6bf..2d517021 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1563,6 +1563,9 @@ namespace Microsoft.Dafny {
TrStmt(s.Update, indent);
}
+ } else if (stmt is ModifyStmt) {
+ // do nothing
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 70ea9ae8..78360361 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1011,6 +1011,7 @@ OneStmt<out Statement/*!*/ s>
| MatchStmt<out s>
| ForallStmt<out s>
| CalcStmt<out s>
+ | ModifyStmt<out s>
| "label" (. x = t; .)
NoUSIdent<out id> ":"
OneStmt<out s> (. s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); .)
@@ -1460,6 +1461,19 @@ ForallStmt<out Statement/*!*/ s>
(. s = new ForallStmt(x, block.EndTok, bvars, attrs, range, ens, block); .)
.
+ModifyStmt<out Statement s>
+= (. IToken tok; FrameExpression fe; var mod = new List<FrameExpression>();
+ Attributes attrs = null;
+ .)
+ "modify" (. tok = t; .)
+ { IF(IsAttribute()) Attribute<ref attrs> }
+ [ FrameExpression<out fe> (. mod.Add(fe); .)
+ { "," FrameExpression<out fe> (. mod.Add(fe); .)
+ }
+ ]
+ SYNC ";" (. s = new ModifyStmt(tok, t, mod, attrs); .)
+ .
+
CalcStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index a7fc7122..c3ff26db 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3507,6 +3507,28 @@ namespace Microsoft.Dafny {
}
}
+ public class ModifyStmt : Statement
+ {
+ public readonly Specification<FrameExpression> Mod;
+
+ public ModifyStmt(IToken tok, IToken endTok, List<FrameExpression> mod, Attributes attrs)
+ : base(tok, endTok)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(endTok != null);
+ Contract.Requires(mod != null);
+ Mod = new Specification<FrameExpression>(mod, attrs);
+ }
+
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ foreach (var fe in Mod.Expressions) {
+ yield return fe.E;
+ }
+ }
+ }
+ }
+
public class CalcStmt : Statement
{
public abstract class CalcOp {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 24d7d25d..ec498837 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -27,7 +27,7 @@ public class Parser {
public const int _openparen = 11;
public const int _star = 12;
public const int _notIn = 13;
- public const int maxT = 125;
+ public const int maxT = 126;
const bool T = true;
const bool x = false;
@@ -386,7 +386,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
}
}
if (la.kind == 8) {
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(126); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(127); Get();}
Get();
}
if (submodule == null) {
@@ -395,7 +395,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
submodule = new AliasModuleDecl(idPath, id, parent, opened);
}
- } else SynErr(127);
+ } else SynErr(128);
}
void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {
@@ -407,7 +407,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 23)) {SynErr(128); Get();}
+ while (!(la.kind == 0 || la.kind == 23)) {SynErr(129); Get();}
Expect(23);
while (la.kind == 9) {
Attribute(ref attrs);
@@ -438,13 +438,13 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
IToken bodyStart = Token.NoToken; // dummy assignment
bool co = false;
- while (!(la.kind == 0 || la.kind == 26 || la.kind == 27)) {SynErr(129); Get();}
+ while (!(la.kind == 0 || la.kind == 26 || la.kind == 27)) {SynErr(130); Get();}
if (la.kind == 26) {
Get();
} else if (la.kind == 27) {
Get();
co = true;
- } else SynErr(130);
+ } else SynErr(131);
while (la.kind == 9) {
Attribute(ref attrs);
}
@@ -460,7 +460,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
DatatypeMemberDecl(ctors);
}
if (la.kind == 8) {
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(131); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(132); Get();}
Get();
}
if (co) {
@@ -491,7 +491,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
}
at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);
if (la.kind == 8) {
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(132); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(133); Get();}
Get();
}
}
@@ -520,7 +520,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 34)) {SynErr(133); Get();}
+ while (!(la.kind == 0 || la.kind == 34)) {SynErr(134); Get();}
Expect(34);
while (la.kind == 9) {
Attribute(ref attrs);
@@ -543,7 +543,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
} else if (la.kind == 37) {
Get();
signatureEllipsis = t; openParen = Token.NoToken;
- } else SynErr(134);
+ } else SynErr(135);
while (StartOf(3)) {
IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs);
}
@@ -584,7 +584,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
} else if (StartOf(4)) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
- } else SynErr(135);
+ } else SynErr(136);
}
void Attribute(ref Attributes attrs) {
@@ -654,7 +654,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
}
}
- } else SynErr(136);
+ } else SynErr(137);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -692,7 +692,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- while (!(la.kind == 0 || la.kind == 29)) {SynErr(137); Get();}
+ while (!(la.kind == 0 || la.kind == 29)) {SynErr(138); Get();}
Expect(29);
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
@@ -706,7 +706,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
FIdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(138); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(139); Get();}
Expect(8);
}
@@ -752,7 +752,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
Get();
signatureEllipsis = t;
openParen = Token.NoToken;
- } else SynErr(139);
+ } else SynErr(140);
} else if (la.kind == 63) {
Get();
isPredicate = true;
@@ -781,7 +781,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
Get();
signatureEllipsis = t;
openParen = Token.NoToken;
- } else SynErr(140);
+ } else SynErr(141);
} else if (la.kind == 64) {
Get();
isCoPredicate = true;
@@ -806,8 +806,8 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
Get();
signatureEllipsis = t;
openParen = Token.NoToken;
- } else SynErr(141);
- } else SynErr(142);
+ } else SynErr(142);
+ } else SynErr(143);
decreases = isCoPredicate ? null : new List<Expression/*!*/>();
while (StartOf(6)) {
FunctionSpec(reqs, reads, ens, decreases);
@@ -865,7 +865,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(StartOf(7))) {SynErr(143); Get();}
+ while (!(StartOf(7))) {SynErr(144); Get();}
if (la.kind == 40) {
Get();
} else if (la.kind == 41) {
@@ -887,7 +887,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
SemErr(t, "constructors are only allowed in classes");
}
- } else SynErr(144);
+ } else SynErr(145);
keywordToken = t;
if (isLemma) {
if (mmod.IsGhost) {
@@ -933,7 +933,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
} else if (la.kind == 37) {
Get();
signatureEllipsis = t; openParen = Token.NoToken;
- } else SynErr(145);
+ } else SynErr(146);
while (StartOf(8)) {
MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
}
@@ -1016,7 +1016,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
} else if (la.kind == 2) {
Get();
id = t;
- } else SynErr(146);
+ } else SynErr(147);
Expect(7);
Type(out ty);
}
@@ -1110,7 +1110,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
id = t; name = id.val;
Expect(7);
Type(out ty);
- } else SynErr(147);
+ } else SynErr(148);
if (name != null) {
identName = name;
} else {
@@ -1204,7 +1204,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(148); break;
+ default: SynErr(149); break;
}
}
@@ -1230,7 +1230,7 @@ List<MaybeFreeExpression/*!*/>/*!*/ yieldReq, List<MaybeFreeExpression/*!*/>/*!*
ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;
- while (!(StartOf(11))) {SynErr(149); Get();}
+ while (!(StartOf(11))) {SynErr(150); Get();}
if (la.kind == 50) {
Get();
while (IsAttribute()) {
@@ -1245,7 +1245,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(150); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(151); Get();}
Expect(8);
} else if (la.kind == 45) {
Get();
@@ -1261,7 +1261,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(151); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(152); Get();}
Expect(8);
} else if (StartOf(13)) {
if (la.kind == 46) {
@@ -1275,7 +1275,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
if (la.kind == 47) {
Get();
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(152); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(153); Get();}
Expect(8);
if (isYield) {
yieldReq.Add(new MaybeFreeExpression(e, isFree));
@@ -1289,7 +1289,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
Attribute(ref ensAttrs);
}
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(153); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(154); Get();}
Expect(8);
if (isYield) {
yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
@@ -1297,16 +1297,16 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
}
- } else SynErr(154);
+ } else SynErr(155);
} else if (la.kind == 49) {
Get();
while (IsAttribute()) {
Attribute(ref decrAttrs);
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(155); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(156); Get();}
Expect(8);
- } else SynErr(156);
+ } else SynErr(157);
}
void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -1328,7 +1328,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null;
- while (!(StartOf(15))) {SynErr(157); Get();}
+ while (!(StartOf(15))) {SynErr(158); Get();}
if (la.kind == 45) {
Get();
while (IsAttribute()) {
@@ -1343,7 +1343,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(158); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(159); Get();}
Expect(8);
} else if (la.kind == 46 || la.kind == 47 || la.kind == 48) {
if (la.kind == 46) {
@@ -1353,7 +1353,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 47) {
Get();
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(159); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(160); Get();}
Expect(8);
req.Add(new MaybeFreeExpression(e, isFree));
} else if (la.kind == 48) {
@@ -1362,19 +1362,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Attribute(ref ensAttrs);
}
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(160); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(161); Get();}
Expect(8);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- } else SynErr(161);
+ } else SynErr(162);
} else if (la.kind == 49) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(162); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(163); Get();}
Expect(8);
- } else SynErr(163);
+ } else SynErr(164);
}
void FrameExpression(out FrameExpression/*!*/ fe) {
@@ -1398,7 +1398,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out id);
fieldName = id.val;
fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName);
- } else SynErr(164);
+ } else SynErr(165);
}
void Expression(out Expression e, bool allowSemi) {
@@ -1484,7 +1484,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
GenericInstantiation(gt);
}
ty = (tok.val == "real") ? (Type)Microsoft.Dafny.Type.Real : new UserDefinedType(tok, tok.val, gt, path);
- } else SynErr(165);
+ } else SynErr(166);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
@@ -1493,10 +1493,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
if (la.kind == 47) {
- while (!(la.kind == 0 || la.kind == 47)) {SynErr(166); Get();}
+ while (!(la.kind == 0 || la.kind == 47)) {SynErr(167); Get();}
Get();
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(167); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(168); Get();}
Expect(8);
reqs.Add(e);
} else if (la.kind == 50) {
@@ -1510,12 +1510,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(168); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(169); Get();}
Expect(8);
} else if (la.kind == 48) {
Get();
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(169); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(170); Get();}
Expect(8);
ens.Add(e);
} else if (la.kind == 49) {
@@ -1526,9 +1526,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(170); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(171); Get();}
Expect(8);
- } else SynErr(171);
+ } else SynErr(172);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -1547,7 +1547,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
fe = new FrameExpression(t, new WildcardExpr(t), null);
} else if (StartOf(12)) {
FrameExpression(out fe);
- } else SynErr(172);
+ } else SynErr(173);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -1558,7 +1558,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new WildcardExpr(t);
} else if (StartOf(16)) {
Expression(out e, false);
- } else SynErr(173);
+ } else SynErr(174);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1575,7 +1575,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken bodyStart, bodyEnd;
int breakCount;
- while (!(StartOf(18))) {SynErr(174); Get();}
+ while (!(StartOf(18))) {SynErr(175); Get();}
switch (la.kind) {
case 9: {
BlockStmt(out bs, out bodyStart, out bodyEnd);
@@ -1594,7 +1594,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
PrintStmt(out s);
break;
}
- case 1: case 2: case 3: case 4: case 11: case 28: case 54: case 55: case 112: case 113: case 114: case 115: case 116: case 117: {
+ case 1: case 2: case 3: case 4: case 11: case 28: case 54: case 55: case 113: case 114: case 115: case 116: case 117: case 118: {
UpdateStmt(out s);
break;
}
@@ -1618,10 +1618,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ForallStmt(out s);
break;
}
- case 87: {
+ case 88: {
CalcStmt(out s);
break;
}
+ case 87: {
+ ModifyStmt(out s);
+ break;
+ }
case 66: {
Get();
x = t;
@@ -1642,8 +1646,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
breakCount++;
}
- } else SynErr(175);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(176); Get();}
+ } else SynErr(176);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(177); Get();}
Expect(8);
s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount);
break;
@@ -1656,7 +1660,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
SkeletonStmt(out s);
break;
}
- default: SynErr(177); break;
+ default: SynErr(178); break;
}
}
@@ -1675,7 +1679,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 37) {
Get();
dotdotdot = t;
- } else SynErr(178);
+ } else SynErr(179);
Expect(8);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
@@ -1700,7 +1704,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 37) {
Get();
dotdotdot = t;
- } else SynErr(179);
+ } else SynErr(180);
Expect(8);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
@@ -1770,13 +1774,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
suchThatAssume = t;
}
Expression(out suchThat, false);
- } else SynErr(180);
+ } else SynErr(181);
Expect(8);
endTok = t;
} else if (la.kind == 7) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(181);
+ } else SynErr(182);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume);
} else {
@@ -1897,7 +1901,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 9) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs; endTok = bs.EndTok;
- } else SynErr(182);
+ } else SynErr(183);
}
if (guardEllipsis != null) {
ifStmt = new SkeletonStatement(new IfStmt(x, endTok, guard, thn, els), guardEllipsis, null);
@@ -1905,7 +1909,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ifStmt = new IfStmt(x, endTok, guard, thn, els);
}
- } else SynErr(183);
+ } else SynErr(184);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1942,7 +1946,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 37) {
Get();
bodyEllipsis = t; endTok = t;
- } else SynErr(184);
+ } else SynErr(185);
if (guardEllipsis != null || bodyEllipsis != null) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -1958,7 +1962,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
}
- } else SynErr(185);
+ } else SynErr(186);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -1998,7 +2002,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
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(186);
+ } else SynErr(187);
if (la.kind == 11) {
Get();
usesOptionalParen = true;
@@ -2017,7 +2021,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (!usesOptionalParen) { SemErr(t, "found but didn't expect a close parenthesis"); }
} else if (la.kind == 9 || la.kind == 46 || la.kind == 48) {
if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); }
- } else SynErr(187);
+ } else SynErr(188);
while (la.kind == 46 || la.kind == 48) {
isFree = false;
if (la.kind == 46) {
@@ -2047,7 +2051,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken opTok;
IToken danglingOperator = null;
- Expect(87);
+ Expect(88);
x = t;
if (StartOf(21)) {
CalcOp(out opTok, out calcOp);
@@ -2093,6 +2097,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
+ void ModifyStmt(out Statement s) {
+ IToken tok; FrameExpression fe; var mod = new List<FrameExpression>();
+ Attributes attrs = null;
+
+ Expect(87);
+ tok = t;
+ while (IsAttribute()) {
+ Attribute(ref attrs);
+ }
+ if (StartOf(12)) {
+ FrameExpression(out fe);
+ mod.Add(fe);
+ while (la.kind == 30) {
+ Get();
+ FrameExpression(out fe);
+ mod.Add(fe);
+ }
+ }
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(189); Get();}
+ Expect(8);
+ s = new ModifyStmt(tok, t, mod, attrs);
+ }
+
void ReturnStmt(out Statement/*!*/ s) {
IToken returnTok = null;
List<AssignmentRhs> rhss = null;
@@ -2105,7 +2132,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 51) {
Get();
returnTok = t; isYield = true;
- } else SynErr(188);
+ } else SynErr(190);
if (StartOf(22)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
@@ -2207,7 +2234,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(16)) {
Expression(out e, false);
r = new ExprRhs(e);
- } else SynErr(189);
+ } else SynErr(191);
while (la.kind == 9) {
Attribute(ref attrs);
}
@@ -2228,7 +2255,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
- } else SynErr(190);
+ } else SynErr(192);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -2277,7 +2304,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(16)) {
Expression(out ee, true);
e = ee;
- } else SynErr(191);
+ } else SynErr(193);
}
void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs) {
@@ -2290,20 +2317,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (StartOf(24)) {
if (la.kind == 46 || la.kind == 81) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(192); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(194); Get();}
Expect(8);
invariants.Add(invariant);
} else if (la.kind == 49) {
- while (!(la.kind == 0 || la.kind == 49)) {SynErr(193); Get();}
+ while (!(la.kind == 0 || la.kind == 49)) {SynErr(195); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(194); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(196); Get();}
Expect(8);
} else {
- while (!(la.kind == 0 || la.kind == 45)) {SynErr(195); Get();}
+ while (!(la.kind == 0 || la.kind == 45)) {SynErr(197); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -2318,7 +2345,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(196); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(198); Get();}
Expect(8);
}
}
@@ -2326,7 +2353,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 == 46 || la.kind == 81)) {SynErr(197); Get();}
+ while (!(la.kind == 0 || la.kind == 46 || la.kind == 81)) {SynErr(199); Get();}
if (la.kind == 46) {
Get();
isFree = true;
@@ -2375,7 +2402,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(16)) {
Expression(out e, allowSemi);
arg = new Attributes.Argument(t, e);
- } else SynErr(198);
+ } else SynErr(200);
}
void QuantifierDomain(out List<BoundVar> bvars, out Attributes attrs, out Expression range) {
@@ -2409,7 +2436,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
case 32: {
Get();
x = t; binOp = BinaryExpr.Opcode.Eq;
- if (la.kind == 88) {
+ if (la.kind == 89) {
Get();
Expect(74);
Expression(out k, true);
@@ -2427,52 +2454,52 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; binOp = BinaryExpr.Opcode.Gt;
break;
}
- case 89: {
+ case 90: {
Get();
x = t; binOp = BinaryExpr.Opcode.Le;
break;
}
- case 90: {
+ case 91: {
Get();
x = t; binOp = BinaryExpr.Opcode.Ge;
break;
}
- case 91: {
+ case 92: {
Get();
x = t; binOp = BinaryExpr.Opcode.Neq;
break;
}
- case 92: {
+ case 93: {
Get();
x = t; binOp = BinaryExpr.Opcode.Neq;
break;
}
- case 93: {
+ case 94: {
Get();
x = t; binOp = BinaryExpr.Opcode.Le;
break;
}
- case 94: {
+ case 95: {
Get();
x = t; binOp = BinaryExpr.Opcode.Ge;
break;
}
- case 95: case 96: {
+ case 96: case 97: {
EquivOp();
x = t; binOp = BinaryExpr.Opcode.Iff;
break;
}
- case 97: case 98: {
+ case 98: case 99: {
ImpliesOp();
x = t; binOp = BinaryExpr.Opcode.Imp;
break;
}
- case 99: case 100: {
+ case 100: case 101: {
ExpliesOp();
x = t; binOp = BinaryExpr.Opcode.Exp;
break;
}
- default: SynErr(199); break;
+ default: SynErr(201); break;
}
if (k == null) {
op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
@@ -2491,7 +2518,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Token x = la;
IToken endTok = x;
- while (la.kind == 9 || la.kind == 87) {
+ while (la.kind == 9 || la.kind == 88) {
if (la.kind == 9) {
BlockStmt(out block, out bodyStart, out bodyEnd);
endTok = block.EndTok; subhints.Add(block);
@@ -2505,33 +2532,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void EquivOp() {
- if (la.kind == 95) {
+ if (la.kind == 96) {
Get();
- } else if (la.kind == 96) {
+ } else if (la.kind == 97) {
Get();
- } else SynErr(200);
+ } else SynErr(202);
}
void ImpliesOp() {
- if (la.kind == 97) {
+ if (la.kind == 98) {
Get();
- } else if (la.kind == 98) {
+ } else if (la.kind == 99) {
Get();
- } else SynErr(201);
+ } else SynErr(203);
}
void ExpliesOp() {
- if (la.kind == 99) {
+ if (la.kind == 100) {
Get();
- } else if (la.kind == 100) {
+ } else if (la.kind == 101) {
Get();
- } else SynErr(202);
+ } else SynErr(204);
}
void EquivExpression(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpliesExpression(out e0, allowSemi);
- while (la.kind == 95 || la.kind == 96) {
+ while (la.kind == 96 || la.kind == 97) {
EquivOp();
x = t;
ImpliesExpliesExpression(out e1, allowSemi);
@@ -2543,7 +2570,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0, allowSemi);
if (StartOf(25)) {
- if (la.kind == 97 || la.kind == 98) {
+ if (la.kind == 98 || la.kind == 99) {
ImpliesOp();
x = t;
ImpliesExpression(out e1, allowSemi);
@@ -2553,7 +2580,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t;
LogicalExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1);
- while (la.kind == 99 || la.kind == 100) {
+ while (la.kind == 100 || la.kind == 101) {
ExpliesOp();
x = t;
LogicalExpression(out e1, allowSemi);
@@ -2567,12 +2594,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0, allowSemi);
if (StartOf(26)) {
- if (la.kind == 101 || la.kind == 102) {
+ if (la.kind == 102 || la.kind == 103) {
AndOp();
x = t;
RelationalExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 101 || la.kind == 102) {
+ while (la.kind == 102 || la.kind == 103) {
AndOp();
x = t;
RelationalExpression(out e1, allowSemi);
@@ -2583,7 +2610,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t;
RelationalExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 103 || la.kind == 104) {
+ while (la.kind == 104 || la.kind == 105) {
OrOp();
x = t;
RelationalExpression(out e1, allowSemi);
@@ -2596,7 +2623,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void ImpliesExpression(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0, allowSemi);
- if (la.kind == 97 || la.kind == 98) {
+ if (la.kind == 98 || la.kind == 99) {
ImpliesOp();
x = t;
ImpliesExpression(out e1, allowSemi);
@@ -2706,25 +2733,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void AndOp() {
- if (la.kind == 101) {
+ if (la.kind == 102) {
Get();
- } else if (la.kind == 102) {
+ } else if (la.kind == 103) {
Get();
- } else SynErr(203);
+ } else SynErr(205);
}
void OrOp() {
- if (la.kind == 103) {
+ if (la.kind == 104) {
Get();
- } else if (la.kind == 104) {
+ } else if (la.kind == 105) {
Get();
- } else SynErr(204);
+ } else SynErr(206);
}
void Term(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0, allowSemi);
- while (la.kind == 107 || la.kind == 108) {
+ while (la.kind == 108 || la.kind == 109) {
AddOp(out x, out op);
Factor(out e1, allowSemi);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2741,7 +2768,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
case 32: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
- if (la.kind == 88) {
+ if (la.kind == 89) {
Get();
Expect(74);
Expression(out k, true);
@@ -2759,20 +2786,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 89: {
+ case 90: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 90: {
+ case 91: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 91: {
+ case 92: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
- if (la.kind == 88) {
+ if (la.kind == 89) {
Get();
Expect(74);
Expression(out k, true);
@@ -2780,7 +2807,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
break;
}
- case 105: {
+ case 106: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
@@ -2790,10 +2817,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 106: {
+ case 107: {
Get();
x = t; y = Token.NoToken;
- if (la.kind == 106) {
+ if (la.kind == 107) {
Get();
y = t;
}
@@ -2808,29 +2835,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
break;
}
- case 92: {
+ case 93: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 93: {
+ case 94: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 94: {
+ case 95: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(205); break;
+ default: SynErr(207); break;
}
}
void Factor(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0, allowSemi);
- while (la.kind == 12 || la.kind == 109 || la.kind == 110) {
+ while (la.kind == 12 || la.kind == 110 || la.kind == 111) {
MulOp(out x, out op);
UnaryExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2839,33 +2866,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 == 107) {
+ if (la.kind == 108) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 108) {
+ } else if (la.kind == 109) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(206);
+ } else SynErr(208);
}
void UnaryExpression(out Expression e, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 108: {
+ case 109: {
Get();
x = t;
UnaryExpression(out e, allowSemi);
e = new NegationExpression(x, e);
break;
}
- case 106: case 111: {
+ case 107: case 112: {
NegOp();
x = t;
UnaryExpression(out e, allowSemi);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 24: case 29: case 56: case 66: case 72: case 76: case 82: case 83: case 85: case 87: case 120: case 121: case 122: {
+ case 24: case 29: case 56: case 66: case 72: case 76: case 82: case 83: case 85: case 88: case 121: case 122: case 123: {
EndlessExpression(out e, allowSemi);
break;
}
@@ -2902,17 +2929,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
MapComprehensionExpr(x, out e, allowSemi);
} else if (StartOf(28)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(207);
+ } else SynErr(209);
break;
}
- case 2: case 3: case 4: case 11: case 28: case 54: case 55: case 112: case 113: case 114: case 115: case 116: case 117: {
+ case 2: case 3: case 4: case 11: case 28: case 54: case 55: case 113: case 114: case 115: case 116: case 117: case 118: {
ConstAtomExpression(out e);
while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
break;
}
- default: SynErr(208); break;
+ default: SynErr(210); break;
}
}
@@ -2921,21 +2948,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 12) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 109) {
+ } else if (la.kind == 110) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 110) {
+ } else if (la.kind == 111) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(209);
+ } else SynErr(211);
}
void NegOp() {
- if (la.kind == 106) {
+ if (la.kind == 107) {
Get();
- } else if (la.kind == 111) {
+ } else if (la.kind == 112) {
Get();
- } else SynErr(210);
+ } else SynErr(212);
}
void EndlessExpression(out Expression e, bool allowSemi) {
@@ -2949,7 +2976,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
x = t;
Expression(out e, true);
- Expect(118);
+ Expect(119);
Expression(out e0, true);
Expect(77);
Expression(out e1, allowSemi);
@@ -2960,7 +2987,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
MatchExpression(out e, allowSemi);
break;
}
- case 85: case 120: case 121: case 122: {
+ case 85: case 121: case 122: case 123: {
QuantifierGuts(out e, allowSemi);
break;
}
@@ -2968,7 +2995,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ComprehensionExpr(out e, allowSemi);
break;
}
- case 72: case 83: case 87: {
+ case 72: case 83: case 88: {
StmtInExpr(out s);
Expression(out e, allowSemi);
e = new StmtExpr(s.Tok, s, e);
@@ -2982,7 +3009,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
NamedExpr(out e, allowSemi);
break;
}
- default: SynErr(211); break;
+ default: SynErr(213); break;
}
}
@@ -2999,9 +3026,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (idPrime != null) { idents.Add(idPrime); id = idPrime; }
}
- if (la.kind == 11 || la.kind == 88) {
+ if (la.kind == 11 || la.kind == 89) {
args = new List<Expression>();
- if (la.kind == 88) {
+ if (la.kind == 89) {
Get();
id.val = id.val + "#"; Expression k;
Expect(74);
@@ -3033,9 +3060,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
id = x; // move to the next Suffix
}
- if (la.kind == 11 || la.kind == 88) {
+ if (la.kind == 11 || la.kind == 89) {
args = new List<Expression/*!*/>(); func = true;
- if (la.kind == 88) {
+ if (la.kind == 89) {
Get();
id.val = id.val + "#"; Expression k;
Expect(74);
@@ -3058,7 +3085,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (StartOf(16)) {
Expression(out ee, true);
e0 = ee;
- if (la.kind == 119) {
+ if (la.kind == 120) {
Get();
anyDots = true;
if (StartOf(16)) {
@@ -3080,15 +3107,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
multipleIndices.Add(ee);
}
- } else SynErr(212);
- } else if (la.kind == 119) {
+ } else SynErr(214);
+ } else if (la.kind == 120) {
Get();
anyDots = true;
if (StartOf(16)) {
Expression(out ee, true);
e1 = ee;
}
- } else SynErr(213);
+ } else SynErr(215);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -3112,7 +3139,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(75);
- } else SynErr(214);
+ } else SynErr(216);
}
void DisplayExpr(out Expression e) {
@@ -3136,7 +3163,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
e = new SeqDisplayExpr(x, elements);
Expect(75);
- } else SynErr(215);
+ } else SynErr(217);
}
void MultiSetExpr(out Expression e) {
@@ -3162,7 +3189,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(33);
} else if (StartOf(29)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(216);
+ } else SynErr(218);
}
void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {
@@ -3203,17 +3230,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = dummyExpr;
switch (la.kind) {
- case 112: {
+ case 113: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 113: {
+ case 114: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 114: {
+ case 115: {
Get();
e = new LiteralExpr(t);
break;
@@ -3228,12 +3255,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new LiteralExpr(t, d);
break;
}
- case 115: {
+ case 116: {
Get();
e = new ThisExpr(t);
break;
}
- case 116: {
+ case 117: {
Get();
x = t;
Expect(11);
@@ -3242,7 +3269,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new FreshExpr(x, e);
break;
}
- case 117: {
+ case 118: {
Get();
x = t;
Expect(11);
@@ -3295,7 +3322,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
break;
}
- default: SynErr(217); break;
+ default: SynErr(219); break;
}
}
@@ -3320,7 +3347,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
n = BigInteger.Zero;
}
- } else SynErr(218);
+ } else SynErr(220);
}
void Dec(out Basetypes.BigDec d) {
@@ -3352,11 +3379,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void QSep() {
- if (la.kind == 123) {
+ if (la.kind == 124) {
Get();
- } else if (la.kind == 124) {
+ } else if (la.kind == 125) {
Get();
- } else SynErr(219);
+ } else SynErr(221);
}
void MatchExpression(out Expression e, bool allowSemi) {
@@ -3381,13 +3408,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression range;
Expression/*!*/ body;
- if (la.kind == 85 || la.kind == 120) {
+ if (la.kind == 85 || la.kind == 121) {
Forall();
x = t; univ = true;
- } else if (la.kind == 121 || la.kind == 122) {
+ } else if (la.kind == 122 || la.kind == 123) {
Exists();
x = t;
- } else SynErr(220);
+ } else SynErr(222);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body, allowSemi);
@@ -3418,7 +3445,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(28);
Expression(out range, allowSemi);
- if (la.kind == 123 || la.kind == 124) {
+ if (la.kind == 124 || la.kind == 125) {
QSep();
Expression(out body, allowSemi);
}
@@ -3433,9 +3460,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
AssertStmt(out s);
} else if (la.kind == 72) {
AssumeStmt(out s);
- } else if (la.kind == 87) {
+ } else if (la.kind == 88) {
CalcStmt(out s);
- } else SynErr(221);
+ } else SynErr(223);
}
void LetExpr(out Expression e, bool allowSemi) {
@@ -3475,7 +3502,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
- } else SynErr(222);
+ } else SynErr(224);
Expression(out e, false);
letRHSs.Add(e);
while (la.kind == 30) {
@@ -3526,7 +3553,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IdentTypeOptional(out bv);
pat = new CasePattern(bv.tok, bv);
- } else SynErr(223);
+ } else SynErr(225);
}
void CaseExpression(out MatchCaseExpr c, bool allowSemi) {
@@ -3557,17 +3584,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void Forall() {
if (la.kind == 85) {
Get();
- } else if (la.kind == 120) {
+ } else if (la.kind == 121) {
Get();
- } else SynErr(224);
+ } else SynErr(226);
}
void Exists() {
- if (la.kind == 121) {
+ if (la.kind == 122) {
Get();
- } else if (la.kind == 122) {
+ } else if (la.kind == 123) {
Get();
- } else SynErr(225);
+ } else SynErr(227);
}
void AttributeBody(ref Attributes attrs) {
@@ -3603,37 +3630,37 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
static readonly bool[,]/*!*/ set = {
- {T,T,T,T, T,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,T, T,T,x,x, x,x,T,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,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,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,T, T,x,T,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,T,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,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, T,T,x,x, x,T,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,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, 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,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x,x, x,x,x},
- {T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,T, T,x,T,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,T, T,T,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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, 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,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,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, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,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, 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,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,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,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,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, 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,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,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, 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,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,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, 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,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,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,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,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, 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,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,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, 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, 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,x,x, x,T,T,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,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,T,T,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, 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,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, 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,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, 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,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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x, x,T,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,x,x, x,T,T,T, T,T,T,x, 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,x, T,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,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,T, x,T,T,T, x,T,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,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,x,x, T,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,x,x, x,x,T,T, x,T,T,T, x,T,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,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,T, T,x,T,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,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, 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,T, T,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,T, T,T,x,x, x,x,T,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, 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,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,T, T,x,T,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,T,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,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, T,T,x,x, x,T,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,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,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,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x,x, x,x,x,x},
+ {T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,T, T,x,T,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,T, T,T,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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, 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,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,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, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,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,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,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,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,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, 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,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,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,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,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,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,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,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,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,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,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, 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,x,x, x,x,T,T, 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,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,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,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, 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,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,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,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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x, x,T,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,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,x, 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, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,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,T, x,T,T,T, x,T,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,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,x,x, T,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,x,x, x,x,T,T, x,T,T,T, x,T,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,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,T, T,x,T,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,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
@@ -3745,145 +3772,147 @@ public class Errors {
case 84: s = "\"print\" expected"; break;
case 85: s = "\"forall\" expected"; break;
case 86: s = "\"parallel\" expected"; break;
- case 87: s = "\"calc\" expected"; break;
- case 88: s = "\"#\" expected"; break;
- case 89: s = "\"<=\" expected"; break;
- case 90: s = "\">=\" expected"; break;
- case 91: s = "\"!=\" expected"; break;
- case 92: s = "\"\\u2260\" expected"; break;
- case 93: s = "\"\\u2264\" expected"; break;
- case 94: s = "\"\\u2265\" expected"; break;
- case 95: s = "\"<==>\" expected"; break;
- case 96: s = "\"\\u21d4\" expected"; break;
- case 97: s = "\"==>\" expected"; break;
- case 98: s = "\"\\u21d2\" expected"; break;
- case 99: s = "\"<==\" expected"; break;
- case 100: s = "\"\\u21d0\" expected"; break;
- case 101: s = "\"&&\" expected"; break;
- case 102: s = "\"\\u2227\" expected"; break;
- case 103: s = "\"||\" expected"; break;
- case 104: s = "\"\\u2228\" expected"; break;
- case 105: s = "\"in\" expected"; break;
- case 106: s = "\"!\" expected"; break;
- case 107: s = "\"+\" expected"; break;
- case 108: s = "\"-\" expected"; break;
- case 109: s = "\"/\" expected"; break;
- case 110: s = "\"%\" expected"; break;
- case 111: s = "\"\\u00ac\" expected"; break;
- case 112: s = "\"false\" expected"; break;
- case 113: s = "\"true\" expected"; break;
- case 114: s = "\"null\" expected"; break;
- case 115: s = "\"this\" expected"; break;
- case 116: s = "\"fresh\" expected"; break;
- case 117: s = "\"old\" expected"; break;
- case 118: s = "\"then\" expected"; break;
- case 119: s = "\"..\" expected"; break;
- case 120: s = "\"\\u2200\" expected"; break;
- case 121: s = "\"exists\" expected"; break;
- case 122: s = "\"\\u2203\" expected"; break;
- case 123: s = "\"::\" expected"; break;
- case 124: s = "\"\\u2022\" expected"; break;
- case 125: s = "??? expected"; break;
- case 126: s = "this symbol not expected in SubModuleDecl"; break;
- case 127: s = "invalid SubModuleDecl"; break;
- case 128: s = "this symbol not expected in ClassDecl"; break;
- case 129: s = "this symbol not expected in DatatypeDecl"; break;
- case 130: s = "invalid DatatypeDecl"; break;
- case 131: s = "this symbol not expected in DatatypeDecl"; break;
- case 132: s = "this symbol not expected in ArbitraryTypeDecl"; break;
- case 133: s = "this symbol not expected in IteratorDecl"; break;
- case 134: s = "invalid IteratorDecl"; break;
- case 135: s = "invalid ClassMemberDecl"; break;
- case 136: s = "invalid IdentOrDigitsSuffix"; break;
- case 137: s = "this symbol not expected in FieldDecl"; break;
+ case 87: s = "\"modify\" expected"; break;
+ case 88: s = "\"calc\" expected"; break;
+ case 89: s = "\"#\" expected"; break;
+ case 90: s = "\"<=\" expected"; break;
+ case 91: s = "\">=\" expected"; break;
+ case 92: s = "\"!=\" expected"; break;
+ case 93: s = "\"\\u2260\" expected"; break;
+ case 94: s = "\"\\u2264\" expected"; break;
+ case 95: s = "\"\\u2265\" expected"; break;
+ case 96: s = "\"<==>\" expected"; break;
+ case 97: s = "\"\\u21d4\" expected"; break;
+ case 98: s = "\"==>\" expected"; break;
+ case 99: s = "\"\\u21d2\" expected"; break;
+ case 100: s = "\"<==\" expected"; break;
+ case 101: s = "\"\\u21d0\" expected"; break;
+ case 102: s = "\"&&\" expected"; break;
+ case 103: s = "\"\\u2227\" expected"; break;
+ case 104: s = "\"||\" expected"; break;
+ case 105: s = "\"\\u2228\" expected"; break;
+ case 106: s = "\"in\" expected"; break;
+ case 107: s = "\"!\" expected"; break;
+ case 108: s = "\"+\" expected"; break;
+ case 109: s = "\"-\" expected"; break;
+ case 110: s = "\"/\" expected"; break;
+ case 111: s = "\"%\" expected"; break;
+ case 112: s = "\"\\u00ac\" expected"; break;
+ case 113: s = "\"false\" expected"; break;
+ case 114: s = "\"true\" expected"; break;
+ case 115: s = "\"null\" expected"; break;
+ case 116: s = "\"this\" expected"; break;
+ case 117: s = "\"fresh\" expected"; break;
+ case 118: s = "\"old\" expected"; break;
+ case 119: s = "\"then\" expected"; break;
+ case 120: s = "\"..\" expected"; break;
+ case 121: s = "\"\\u2200\" expected"; break;
+ case 122: s = "\"exists\" expected"; break;
+ case 123: s = "\"\\u2203\" expected"; break;
+ case 124: s = "\"::\" expected"; break;
+ case 125: s = "\"\\u2022\" expected"; break;
+ case 126: s = "??? expected"; break;
+ case 127: s = "this symbol not expected in SubModuleDecl"; break;
+ case 128: s = "invalid SubModuleDecl"; break;
+ case 129: s = "this symbol not expected in ClassDecl"; break;
+ case 130: s = "this symbol not expected in DatatypeDecl"; break;
+ case 131: s = "invalid DatatypeDecl"; break;
+ case 132: s = "this symbol not expected in DatatypeDecl"; break;
+ case 133: s = "this symbol not expected in ArbitraryTypeDecl"; break;
+ case 134: s = "this symbol not expected in IteratorDecl"; break;
+ case 135: s = "invalid IteratorDecl"; break;
+ case 136: s = "invalid ClassMemberDecl"; break;
+ case 137: s = "invalid IdentOrDigitsSuffix"; break;
case 138: s = "this symbol not expected in FieldDecl"; break;
- case 139: s = "invalid FunctionDecl"; break;
+ case 139: s = "this symbol not expected in FieldDecl"; break;
case 140: s = "invalid FunctionDecl"; break;
case 141: s = "invalid FunctionDecl"; break;
case 142: s = "invalid FunctionDecl"; break;
- case 143: s = "this symbol not expected in MethodDecl"; break;
- case 144: s = "invalid MethodDecl"; break;
+ case 143: s = "invalid FunctionDecl"; break;
+ case 144: s = "this symbol not expected in MethodDecl"; break;
case 145: s = "invalid MethodDecl"; break;
- case 146: s = "invalid FIdentType"; break;
- case 147: s = "invalid TypeIdentOptional"; break;
- case 148: s = "invalid TypeAndToken"; break;
- case 149: s = "this symbol not expected in IteratorSpec"; break;
+ case 146: s = "invalid MethodDecl"; break;
+ case 147: s = "invalid FIdentType"; break;
+ case 148: s = "invalid TypeIdentOptional"; break;
+ case 149: s = "invalid TypeAndToken"; break;
case 150: s = "this symbol not expected in IteratorSpec"; break;
case 151: s = "this symbol not expected in IteratorSpec"; break;
case 152: s = "this symbol not expected in IteratorSpec"; break;
case 153: s = "this symbol not expected in IteratorSpec"; break;
- case 154: s = "invalid IteratorSpec"; break;
- case 155: s = "this symbol not expected in IteratorSpec"; break;
- case 156: s = "invalid IteratorSpec"; break;
- case 157: s = "this symbol not expected in MethodSpec"; break;
+ case 154: s = "this symbol not expected in IteratorSpec"; break;
+ case 155: s = "invalid IteratorSpec"; break;
+ case 156: s = "this symbol not expected in IteratorSpec"; break;
+ case 157: s = "invalid IteratorSpec"; break;
case 158: s = "this symbol not expected in MethodSpec"; break;
case 159: s = "this symbol not expected in MethodSpec"; break;
case 160: s = "this symbol not expected in MethodSpec"; break;
- case 161: s = "invalid MethodSpec"; break;
- case 162: s = "this symbol not expected in MethodSpec"; break;
- case 163: s = "invalid MethodSpec"; break;
- case 164: s = "invalid FrameExpression"; break;
- case 165: s = "invalid ReferenceType"; break;
- case 166: s = "this symbol not expected in FunctionSpec"; break;
+ case 161: s = "this symbol not expected in MethodSpec"; break;
+ case 162: s = "invalid MethodSpec"; break;
+ case 163: s = "this symbol not expected in MethodSpec"; break;
+ case 164: s = "invalid MethodSpec"; break;
+ case 165: s = "invalid FrameExpression"; break;
+ case 166: s = "invalid ReferenceType"; break;
case 167: s = "this symbol not expected in FunctionSpec"; break;
case 168: s = "this symbol not expected in FunctionSpec"; break;
case 169: s = "this symbol not expected in FunctionSpec"; break;
case 170: s = "this symbol not expected in FunctionSpec"; break;
- case 171: s = "invalid FunctionSpec"; break;
- case 172: s = "invalid PossiblyWildFrameExpression"; break;
- case 173: s = "invalid PossiblyWildExpression"; break;
- case 174: s = "this symbol not expected in OneStmt"; break;
- case 175: s = "invalid OneStmt"; break;
- case 176: s = "this symbol not expected in OneStmt"; break;
- case 177: s = "invalid OneStmt"; break;
- case 178: s = "invalid AssertStmt"; break;
- case 179: s = "invalid AssumeStmt"; break;
- case 180: s = "invalid UpdateStmt"; break;
+ case 171: s = "this symbol not expected in FunctionSpec"; break;
+ case 172: s = "invalid FunctionSpec"; break;
+ case 173: s = "invalid PossiblyWildFrameExpression"; break;
+ case 174: s = "invalid PossiblyWildExpression"; break;
+ case 175: s = "this symbol not expected in OneStmt"; break;
+ case 176: s = "invalid OneStmt"; break;
+ case 177: s = "this symbol not expected in OneStmt"; break;
+ case 178: s = "invalid OneStmt"; break;
+ case 179: s = "invalid AssertStmt"; break;
+ case 180: s = "invalid AssumeStmt"; break;
case 181: s = "invalid UpdateStmt"; break;
- case 182: s = "invalid IfStmt"; break;
+ case 182: s = "invalid UpdateStmt"; break;
case 183: s = "invalid IfStmt"; break;
- case 184: s = "invalid WhileStmt"; break;
+ case 184: s = "invalid IfStmt"; break;
case 185: s = "invalid WhileStmt"; break;
- case 186: s = "invalid ForallStmt"; break;
+ case 186: s = "invalid WhileStmt"; break;
case 187: s = "invalid ForallStmt"; break;
- case 188: s = "invalid ReturnStmt"; break;
- case 189: s = "invalid Rhs"; break;
- case 190: s = "invalid Lhs"; break;
- case 191: s = "invalid Guard"; break;
- case 192: s = "this symbol not expected in LoopSpec"; break;
- case 193: s = "this symbol not expected in LoopSpec"; break;
+ case 188: s = "invalid ForallStmt"; break;
+ case 189: s = "this symbol not expected in ModifyStmt"; break;
+ case 190: s = "invalid ReturnStmt"; break;
+ case 191: s = "invalid Rhs"; break;
+ case 192: s = "invalid Lhs"; break;
+ case 193: s = "invalid Guard"; break;
case 194: s = "this symbol not expected in LoopSpec"; break;
case 195: s = "this symbol not expected in LoopSpec"; break;
case 196: s = "this symbol not expected in LoopSpec"; break;
- case 197: s = "this symbol not expected in Invariant"; break;
- case 198: s = "invalid AttributeArg"; break;
- case 199: s = "invalid CalcOp"; break;
- case 200: s = "invalid EquivOp"; break;
- case 201: s = "invalid ImpliesOp"; break;
- case 202: s = "invalid ExpliesOp"; break;
- case 203: s = "invalid AndOp"; break;
- case 204: s = "invalid OrOp"; break;
- case 205: s = "invalid RelOp"; break;
- case 206: s = "invalid AddOp"; break;
- case 207: s = "invalid UnaryExpression"; break;
- case 208: s = "invalid UnaryExpression"; break;
- case 209: s = "invalid MulOp"; break;
- case 210: s = "invalid NegOp"; break;
- case 211: s = "invalid EndlessExpression"; break;
- case 212: s = "invalid Suffix"; break;
- case 213: s = "invalid Suffix"; break;
+ case 197: s = "this symbol not expected in LoopSpec"; break;
+ case 198: s = "this symbol not expected in LoopSpec"; break;
+ case 199: s = "this symbol not expected in Invariant"; break;
+ case 200: s = "invalid AttributeArg"; break;
+ case 201: s = "invalid CalcOp"; break;
+ case 202: s = "invalid EquivOp"; break;
+ case 203: s = "invalid ImpliesOp"; break;
+ case 204: s = "invalid ExpliesOp"; break;
+ case 205: s = "invalid AndOp"; break;
+ case 206: s = "invalid OrOp"; break;
+ case 207: s = "invalid RelOp"; break;
+ case 208: s = "invalid AddOp"; break;
+ case 209: s = "invalid UnaryExpression"; break;
+ case 210: s = "invalid UnaryExpression"; break;
+ case 211: s = "invalid MulOp"; break;
+ case 212: s = "invalid NegOp"; break;
+ case 213: s = "invalid EndlessExpression"; break;
case 214: s = "invalid Suffix"; break;
- case 215: s = "invalid DisplayExpr"; break;
- case 216: s = "invalid MultiSetExpr"; break;
- case 217: s = "invalid ConstAtomExpression"; break;
- case 218: s = "invalid Nat"; break;
- case 219: s = "invalid QSep"; break;
- case 220: s = "invalid QuantifierGuts"; break;
- case 221: s = "invalid StmtInExpr"; break;
- case 222: s = "invalid LetExpr"; break;
- case 223: s = "invalid CasePattern"; break;
- case 224: s = "invalid Forall"; break;
- case 225: s = "invalid Exists"; break;
+ case 215: s = "invalid Suffix"; break;
+ case 216: s = "invalid Suffix"; break;
+ case 217: s = "invalid DisplayExpr"; break;
+ case 218: s = "invalid MultiSetExpr"; break;
+ case 219: s = "invalid ConstAtomExpression"; break;
+ case 220: s = "invalid Nat"; break;
+ case 221: s = "invalid QSep"; break;
+ case 222: s = "invalid QuantifierGuts"; break;
+ case 223: s = "invalid StmtInExpr"; break;
+ case 224: s = "invalid LetExpr"; break;
+ case 225: s = "invalid CasePattern"; break;
+ case 226: s = "invalid Forall"; break;
+ case 227: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index c4e8d7db..845200a3 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -726,6 +726,14 @@ namespace Microsoft.Dafny {
}
PrintStatement(s.Body, indent);
+ } else if (stmt is ModifyStmt) {
+ var s = (ModifyStmt)stmt;
+ wr.Write("modify");
+ PrintAttributes(s.Mod.Attributes);
+ wr.Write(" ");
+ PrintFrameExpressionList(s.Mod.Expressions);
+ wr.Write(";");
+
} else if (stmt is CalcStmt) {
CalcStmt s = (CalcStmt)stmt;
wr.Write("calc ");
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 3b19b11c..5f2c5411 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1979,6 +1979,7 @@ namespace Microsoft.Dafny
return CheckTailRecursive(s.hiddenUpdate, enclosingMethod, ref tailCall, reportErrors);
}
} else if (stmt is AssignStmt) {
+ } else if (stmt is ModifyStmt) {
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
if (s.Method == enclosingMethod) {
@@ -4472,6 +4473,15 @@ namespace Microsoft.Dafny
CheckForallStatementBodyRestrictions(s.Body, s.Kind);
}
+ } else if (stmt is ModifyStmt) {
+ var s = (ModifyStmt)stmt;
+ ResolveAttributes(s.Mod.Attributes, true, codeContext);
+ foreach (FrameExpression fe in s.Mod.Expressions) {
+ // (yes, say "modifies", not "modify", in the next line -- it seems to give a more readable error message
+ ResolveFrameExpression(fe, "modifies", codeContext);
+ }
+ s.IsGhost = specContextOnly;
+
} else if (stmt is CalcStmt) {
var prevErrorCount = ErrorCount;
CalcStmt s = (CalcStmt)stmt;
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 92809143..4b473e9d 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 125;
- const int noSym = 125;
+ const int maxT = 126;
+ const int noSym = 126;
[ContractInvariantMethod]
@@ -549,16 +549,17 @@ public class Scanner {
case "print": t.kind = 84; break;
case "forall": t.kind = 85; break;
case "parallel": t.kind = 86; break;
- case "calc": t.kind = 87; break;
- case "in": t.kind = 105; break;
- case "false": t.kind = 112; break;
- case "true": t.kind = 113; break;
- case "null": t.kind = 114; break;
- case "this": t.kind = 115; break;
- case "fresh": t.kind = 116; break;
- case "old": t.kind = 117; break;
- case "then": t.kind = 118; break;
- case "exists": t.kind = 121; break;
+ case "modify": t.kind = 87; break;
+ case "calc": t.kind = 88; break;
+ case "in": t.kind = 106; break;
+ case "false": t.kind = 113; break;
+ case "true": t.kind = 114; break;
+ case "null": t.kind = 115; break;
+ case "this": t.kind = 116; break;
+ case "fresh": t.kind = 117; break;
+ case "old": t.kind = 118; break;
+ case "then": t.kind = 119; break;
+ case "exists": t.kind = 122; break;
default: break;
}
}
@@ -721,56 +722,56 @@ public class Scanner {
case 38:
{t.kind = 79; break;}
case 39:
- {t.kind = 88; break;}
+ {t.kind = 89; break;}
case 40:
- {t.kind = 90; break;}
- case 41:
{t.kind = 91; break;}
- case 42:
+ case 41:
{t.kind = 92; break;}
- case 43:
+ case 42:
{t.kind = 93; break;}
- case 44:
+ case 43:
{t.kind = 94; break;}
- case 45:
+ case 44:
{t.kind = 95; break;}
- case 46:
+ case 45:
{t.kind = 96; break;}
- case 47:
+ case 46:
{t.kind = 97; break;}
- case 48:
+ case 47:
{t.kind = 98; break;}
+ case 48:
+ {t.kind = 99; break;}
case 49:
- {t.kind = 100; break;}
+ {t.kind = 101; break;}
case 50:
if (ch == '&') {AddCh(); goto case 51;}
else {goto case 0;}
case 51:
- {t.kind = 101; break;}
- case 52:
{t.kind = 102; break;}
- case 53:
+ case 52:
{t.kind = 103; break;}
- case 54:
+ case 53:
{t.kind = 104; break;}
+ case 54:
+ {t.kind = 105; break;}
case 55:
- {t.kind = 107; break;}
- case 56:
{t.kind = 108; break;}
- case 57:
+ case 56:
{t.kind = 109; break;}
- case 58:
+ case 57:
{t.kind = 110; break;}
- case 59:
+ case 58:
{t.kind = 111; break;}
+ case 59:
+ {t.kind = 112; break;}
case 60:
- {t.kind = 120; break;}
+ {t.kind = 121; break;}
case 61:
- {t.kind = 122; break;}
- case 62:
{t.kind = 123; break;}
- case 63:
+ case 62:
{t.kind = 124; break;}
+ case 63:
+ {t.kind = 125; break;}
case 64:
recEnd = pos; recKind = 7;
if (ch == '=') {AddCh(); goto case 34;}
@@ -778,10 +779,10 @@ public class Scanner {
else if (ch == ':') {AddCh(); goto case 62;}
else {t.kind = 7; break;}
case 65:
- recEnd = pos; recKind = 106;
+ recEnd = pos; recKind = 107;
if (ch == 'i') {AddCh(); goto case 18;}
else if (ch == '=') {AddCh(); goto case 41;}
- else {t.kind = 106; break;}
+ else {t.kind = 107; break;}
case 66:
recEnd = pos; recKind = 20;
if (ch == '=') {AddCh(); goto case 71;}
@@ -808,17 +809,17 @@ public class Scanner {
if (ch == '>') {AddCh(); goto case 47;}
else {t.kind = 32; break;}
case 72:
- recEnd = pos; recKind = 119;
+ recEnd = pos; recKind = 120;
if (ch == '.') {AddCh(); goto case 32;}
- else {t.kind = 119; break;}
+ else {t.kind = 120; break;}
case 73:
- recEnd = pos; recKind = 89;
+ recEnd = pos; recKind = 90;
if (ch == '=') {AddCh(); goto case 74;}
- else {t.kind = 89; break;}
+ else {t.kind = 90; break;}
case 74:
- recEnd = pos; recKind = 99;
+ recEnd = pos; recKind = 100;
if (ch == '>') {AddCh(); goto case 45;}
- else {t.kind = 99; break;}
+ else {t.kind = 100; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e4472f67..8b1d42d7 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2607,7 +2607,7 @@ namespace Microsoft.Dafny {
builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));
}
- void CheckFrameSubset(IToken tok, List<FrameExpression> calleeFrame,
+ void CheckFrameSubset(IToken tok, List<FrameExpression> calleeFrame, bool calleeIsGhost,
Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/> substMap,
ExpressionTranslator/*!*/ etran, Bpl.StmtListBuilder/*!*/ builder, string errorMessage,
Bpl.QKeyValue kv)
@@ -2620,13 +2620,17 @@ namespace Microsoft.Dafny {
Contract.Requires(errorMessage != null);
Contract.Requires(predef != null);
- // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in subFrame ==> $_Frame[o,f]);
+ // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && GhostCheck(f) && (o,f) in subFrame ==> $_Frame[o,f]);
+ // where GhostCheck(f) is "true" for a non-ghost context and is $IsGhostField(f) for a ghost context.
Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));
Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);
Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o));
+ if (calleeIsGhost) {
+ ante = Bpl.Expr.And(ante, FunctionCall(tok, BuiltinFunction.IsGhostField, alpha, f));
+ }
Bpl.Expr oInCallee = InRWClause(tok, o, f, calleeFrame, etran, receiverReplacement, substMap);
Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(etran.TheFrame(tok), o, f);
Bpl.Expr q = new Bpl.ForallExpr(tok, new List<TypeVariable> { alpha }, new List<Variable> { oVar, fVar },
@@ -3629,7 +3633,7 @@ namespace Microsoft.Dafny {
}
if (options.DoReadsChecks) {
// check that the callee reads only what the caller is already allowed to read
- CheckFrameSubset(expr.tok, e.Function.Reads, e.Receiver, substMap, etran, builder, "insufficient reads clause to invoke function", options.AssertKv);
+ CheckFrameSubset(expr.tok, e.Function.Reads, e.Function.IsGhost, e.Receiver, substMap, etran, builder, "insufficient reads clause to invoke function", options.AssertKv);
}
Bpl.Expr allowance = null;
@@ -4371,7 +4375,7 @@ namespace Microsoft.Dafny {
}
// Check modifies clause of a subcall is a subset of the current frame.
- CheckFrameSubset(method.tok, method.Mod.Expressions, receiver, substMap, etran, builder, "call may modify locations not in the refined method's modifies clause", null);
+ CheckFrameSubset(method.tok, method.Mod.Expressions, method.IsGhost, receiver, substMap, etran, builder, "call may modify locations not in the refined method's modifies clause", null);
// Create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.
var outs = new List<Bpl.IdentifierExpr>();
@@ -5220,6 +5224,31 @@ 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 ModifyStmt) {
+ AddComment(builder, stmt, "modify statement");
+ var s = (ModifyStmt)stmt;
+ // check that the modifies is a subset
+ CheckFrameSubset(s.Tok, s.Mod.Expressions, s.IsGhost, null, null, etran, builder, "modify statement may violate context's modifies clause", null);
+ // cause the change of the heap according to the given frame
+ int modifyId = loopHeapVarCount;
+ loopHeapVarCount++;
+ string modifyFrameName = "#_Frame#" + modifyId;
+ DefineFrame(s.Tok, s.Mod.Expressions, builder, locals, modifyFrameName);
+ var preModifyHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$PreModifyHeap" + modifyId, predef.HeapType));
+ locals.Add(preModifyHeapVar);
+ var preModifyHeap = new Bpl.IdentifierExpr(s.Tok, preModifyHeapVar);
+ // preModifyHeap := $Heap;
+ builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preModifyHeap, etran.HeapExpr));
+ // havoc $Heap;
+ builder.Add(new Bpl.HavocCmd(s.Tok, new List<Bpl.IdentifierExpr> { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr }));
+ // assume $HeapSucc(preModifyHeap, $Heap); OR $HeapSuccGhost
+ builder.Add(new Bpl.AssumeCmd(s.Tok, FunctionCall(s.Tok, s.IsGhost ? BuiltinFunction.HeapSuccGhost : BuiltinFunction.HeapSucc, null, preModifyHeap, etran.HeapExpr)));
+ // assume nothing outside the frame was changed
+ var etranPreLoop = new ExpressionTranslator(this, predef, preModifyHeap);
+ var updatedFrameEtran = new ExpressionTranslator(etran, modifyFrameName);
+ builder.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));
+ builder.Add(CaptureState(stmt));
+
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
if (s.Kind == ForallStmt.ParBodyKind.Assign) {
@@ -6048,13 +6077,13 @@ namespace Microsoft.Dafny {
ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap);
ExpressionTranslator updatedFrameEtran;
string loopFrameName = "#_Frame#" + loopId;
- if(s.Mod.Expressions != null)
+ if (s.Mod.Expressions != null)
updatedFrameEtran = new ExpressionTranslator(etran, loopFrameName);
else
updatedFrameEtran = etran;
- if (s.Mod.Expressions != null) { // check that the modifies is a strict subset
- CheckFrameSubset(s.Tok, s.Mod.Expressions, null, null, etran, builder, "loop modifies clause may violate context's modifies clause", null);
+ if (s.Mod.Expressions != null) { // check that the modifies is a subset
+ CheckFrameSubset(s.Tok, s.Mod.Expressions, s.IsGhost, null, null, etran, builder, "loop modifies clause may violate context's modifies clause", null);
DefineFrame(s.Tok, s.Mod.Expressions, builder, locals, loopFrameName);
}
builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr));
@@ -6395,7 +6424,7 @@ namespace Microsoft.Dafny {
// Check modifies clause of a subcall is a subset of the current frame.
if (codeContext is IMethodCodeContext) {
- CheckFrameSubset(tok, callee.Mod.Expressions, receiver, substMap, etran, builder, "call may violate context's modifies clause", null);
+ CheckFrameSubset(tok, callee.Mod.Expressions, callee.IsGhost, receiver, substMap, etran, builder, "call may violate context's modifies clause", null);
}
// Check termination
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index 889da2c0..48f5d1b4 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -291,6 +291,7 @@ namespace DafnyLanguage
case "match":
case "method":
case "modifies":
+ case "modify":
case "module":
case "multiset":
case "nat":
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c68568ab..4d39d989 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -498,6 +498,7 @@ ResolutionErrors.dfy(433,14): Error: when allocating an object of type 'YHWH', o
ResolutionErrors.dfy(438,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
ResolutionErrors.dfy(439,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
ResolutionErrors.dfy(441,9): Error: class Lamb does not have a default constructor
+ResolutionErrors.dfy(836,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(23,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)
@@ -549,7 +550,7 @@ ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specifi
ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts
ResolutionErrors.dfy(544,18): Error: unresolved identifier: w
ResolutionErrors.dfy(651,11): Error: lemmas are not allowed to have modifies clauses
-120 resolution/type errors detected in ResolutionErrors.dfy
+121 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -2148,6 +2149,57 @@ Execution trace:
Dafny program verifier finished with 52 verified, 8 errors
+-------------------- ModifyStmt.dfy --------------------
+ModifyStmt.dfy(24,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ModifyStmt.dfy(39,5): Error: modify statement may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+ModifyStmt.dfy(45,5): Error: modify statement may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+ModifyStmt.dfy(58,5): Error: modify statement may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+ModifyStmt.dfy(67,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ModifyStmt.dfy(111,11): Error: assignment may update an object not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon18_Then
+ ModifyStmt.dfy(107,7): anon19_LoopHead
+ (0,0): anon19_LoopBody
+ ModifyStmt.dfy(107,7): anon20_Else
+ ModifyStmt.dfy(107,7): anon21_Else
+ (0,0): anon22_Then
+ModifyStmt.dfy(124,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon18_Then
+ ModifyStmt.dfy(107,7): anon19_LoopHead
+ (0,0): anon19_LoopBody
+ ModifyStmt.dfy(107,7): anon20_Else
+ (0,0): anon21_Then
+ ModifyStmt.dfy(116,7): anon23_LoopHead
+ (0,0): anon23_LoopBody
+ ModifyStmt.dfy(116,7): anon24_Else
+ (0,0): anon25_Then
+ (0,0): anon17
+ModifyStmt.dfy(134,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ModifyStmt.dfy(145,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ModifyStmt.dfy(157,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+
+Dafny program verifier finished with 23 verified, 10 errors
+
-------------------- Superposition.dfy --------------------
Verifying CheckWellformed$$_0_M0.C.M ...
diff --git a/Test/dafny0/ModifyStmt.dfy b/Test/dafny0/ModifyStmt.dfy
new file mode 100644
index 00000000..49ced294
--- /dev/null
+++ b/Test/dafny0/ModifyStmt.dfy
@@ -0,0 +1,160 @@
+class MyClass {
+ var x: int;
+ var y: int;
+ ghost var g: int;
+
+ method M(S: set<MyClass>, mc: MyClass)
+ requires this == mc;
+ modifies this, S;
+ {
+ if mc == this {
+ modify mc, this;
+ }
+ modify {this}, this, {this}, S;
+ modify this;
+ modify {:myAttribute} {:another true} {this}, this, S;
+ modify ;
+ }
+
+ method N()
+ modifies this;
+ {
+ x := 18;
+ modify this;
+ assert x == 18; // error: cannot conclude this here
+ }
+
+ method P(other: MyClass)
+ modifies this;
+ {
+ x := 18;
+ var previous := if other == null then 0 else other.x;
+ modify this;
+ assert other != null && other != this ==> other.x == previous;
+ }
+
+ method FieldSpecific0()
+ modifies `x;
+ {
+ modify this; // error: this is a larger frame than what FieldSpecific0 is allowed to modify
+ }
+
+ method FieldSpecific1()
+ modifies `x, `y;
+ {
+ modify this; // error: this is a larger frame than what FieldSpecific0 is allowed to modify
+ }
+
+ method FieldSpecific2()
+ modifies this;
+ {
+ modify `x;
+ }
+
+ method FieldSpecific3()
+ modifies `x;
+ {
+ modify this`x;
+ modify `y; // error: this is a larger frame than what FieldSpecific3 is allowed to modify
+ }
+
+ method FieldSpecific4()
+ modifies `x;
+ {
+ var xx, yy := x, y;
+ modify this`x;
+ assert y == yy; // fine
+ assert x == xx; // error: x just changed
+ }
+
+ ghost method GhostFrame0()
+ modifies `x, `g; // the `x has no effect, since this is a ghost context
+ {
+ modify `x, `g;
+ }
+
+ ghost method GhostFrame1()
+ modifies `g;
+ {
+ modify `x, `g; // the `x has no effect, since this is a ghost context
+ }
+
+ ghost method GhostFrame2()
+ {
+ var xx := x;
+ modify `x; // fine, since we're in a ghost context, so `x doesn't count
+ assert xx == x; // fine
+ }
+
+ method GhostFrame3()
+ {
+ var xx := x;
+ if g < 100 {
+ // we're now in a ghost context
+ modify `x; // fine, since `x doesn't count here
+ }
+ assert xx == x; // fine
+ }
+
+ method GhostFrame4()
+ modifies this;
+ {
+ var xx := x;
+ ghost var gg := g;
+ if g < 100 {
+ // we're now in a ghost context
+ var n := 0;
+ while n < y
+ modifies `x;
+ {
+ if * {
+ g := g + 1; // error: this is an error here, since it violates the loop's modifies clause
+ }
+ n := n + 1;
+ }
+ n := 0;
+ while n < y
+ modifies `x, `g;
+ {
+ g := g + 1;
+ n := n + 1;
+ }
+ }
+ assert x == xx; // fine, since only ghost state is allowed to be modified inside the ghost if
+ assert g == gg; // error
+ }
+
+ ghost method Ghost0()
+ modifies this;
+ {
+ var xx := x;
+ var gg := g;
+ modify this; // since we're in the context of a ghost method, this will only modify ghost fields
+ assert x == xx; // fine
+ assert g == gg; // error
+ }
+
+ ghost method Ghost1()
+ modifies this;
+ {
+ var xx := x;
+ var gg := g;
+ modify `x, `g; // since we're in the context of a ghost method, this will only modify
+ // ghost fields, despite the specific mention of non-ghost fields
+ assert x == xx; // fine
+ assert g == gg; // error
+ }
+
+ method Ghost2()
+ modifies this;
+ {
+ var xx := x;
+ ghost var gg := g;
+ if g < 100 {
+ // the if guard mentions a ghost field, so we're now in a ghost context
+ modify this;
+ assert x == xx; // fine, since the 'modify' statement only modified ghost fields
+ assert g == gg; // error: the 'modify' statement can affect the ghost field 'g'
+ }
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index f7a7ed3e..1eb69a8e 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -826,3 +826,13 @@ module ObjectType {
o := co; // error
}
}
+
+// ------------------ modify statment ---------------------------
+
+class ModifyStatementClass {
+ var x: int;
+ method M()
+ {
+ modify x; // error: type error
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 581f5068..a4c3914f 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -29,7 +29,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy RealTypes.dfy Definedness.dfy
IteratorResolution.dfy Iterators.dfy
RankPos.dfy RankNeg.dfy
Computations.dfy ComputationsNeg.dfy
- Include.dfy AutoReq.dfy) do (
+ Include.dfy AutoReq.dfy ModifyStmt.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index d663665b..6c59c50a 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -40,7 +40,7 @@
`(,(dafny-regexp-opt '(
"assert" "assume" "break" "then" "else" "if" "label" "return" "yield"
"while" "print" "where"
- "old" "forall" "exists" "new" "calc" "in" "this" "fresh"
+ "old" "forall" "exists" "new" "calc" "modify" "in" "this" "fresh"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
`(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "int" "real" "object" "set" "seq")) . font-lock-type-face)
)
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 361b72d2..785cf6f1 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -16,7 +16,7 @@
match,case,false,true,null,old,fresh,this,
% statements
assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,
- where,calc
+ where,calc,modify
},
literate=%
{:}{$\colon$}1
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim
index f533a621..d6e6bac5 100644
--- a/Util/vim/dafny.vim
+++ b/Util/vim/dafny.vim
@@ -11,7 +11,7 @@ syntax keyword dafnyTypeDef class datatype codatatype type iterator
syntax keyword abstract module import opened as default
syntax keyword dafnyConditional if then else match case
syntax keyword dafnyRepeat while
-syntax keyword dafnyStatement assume assert return yield new print break label where calc
+syntax keyword dafnyStatement assume assert return yield new print break label where calc modify
syntax keyword dafnyKeyword var ghost returns yields null static this refines include
syntax keyword dafnyType bool nat int real seq set multiset object array array2 array3 map
syntax keyword dafnyLogic requires ensures modifies reads decreases invariant
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 00:11:38 +0000