summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Dafny/Compiler.cs2
-rw-r--r--Dafny/Dafny.atg22
-rw-r--r--Dafny/Parser.cs404
-rw-r--r--Dafny/RefinementTransformer.cs125
-rw-r--r--Dafny/Resolver.cs5
-rw-r--r--Dafny/Scanner.cs25
-rw-r--r--Dafny/Util.cs2
-rw-r--r--Util/Emacs/dafny-mode.el4
-rw-r--r--Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs3
-rw-r--r--Util/latex/dafny.sty4
-rw-r--r--Util/vim/syntax/dafny.vim4
11 files changed, 318 insertions, 282 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 7f48e551..3864df8b 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -2184,6 +2184,8 @@ namespace Microsoft.Dafny {
var e = (ConcreteSyntaxExpression)expr;
TrExpr(e.ResolvedExpression);
+ } else if (expr is NamedExpr) {
+ TrExpr(((NamedExpr)expr).Body);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 78e7675e..54b9b4a4 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -765,14 +765,24 @@ OneStmt<out Statement/*!*/ s>
SkeletonStmt<out Statement s>
= (. List<IToken> names = null;
List<Expression> exprs = null;
- IToken tok, dotdotdot;
+ IToken tok, dotdotdot, whereTok;
Expression e; .)
"..." (. dotdotdot = t; .)
- ["where" (. names = new List<IToken>(); exprs = new List<Expression>(); .)
- Ident<out tok> "=" Expression<out e> (. names.Add(tok); exprs.Add(e); .)
- {"," Ident<out tok> "=" Expression<out e> } (. names.Add(tok); exprs.Add(e); .)
+ ["where" (. names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;.)
+ Ident<out tok> (. names.Add(tok); .)
+ {"," Ident<out tok> (. names.Add(tok); .)
+ }
+ ":="
+ Expression<out e> (. exprs.Add(e); .)
+ {"," Expression<out e> (. exprs.Add(e); .)
+ }
+ (. if (exprs.Count != names.Count) {
+ SemErr(whereTok, exprs.Count < names.Count ? "not enough expressions" : "too many expressions");
+ names = null; exprs = null;
+ }
+ .)
]
- (. s = new SkeletonStatement(dotdotdot, names, exprs); .)
+ (. s = new SkeletonStatement(dotdotdot, names, exprs); .)
.
ReturnStmt<out Statement/*!*/ s>
= (.
@@ -1527,7 +1537,7 @@ NamedExpr<out Expression e>
e = dummyExpr;
Expression expr;
.)
- "expr" (. x = t; .)
+ "label" (. x = t; .)
NoUSIdent<out d>
":"
Expression<out e> (. expr = e;
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 9c47278b..350ebd8e 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -21,7 +21,7 @@ public class Parser {
public const int _colon = 5;
public const int _lbrace = 6;
public const int _rbrace = 7;
- public const int maxT = 110;
+ public const int maxT = 109;
const bool T = true;
const bool x = false;
@@ -212,7 +212,7 @@ bool IsAttribute() {
defaultModule.TopLevelDecls.Add(at);
} else if (StartOf(2)) {
ClassMemberDecl(membersDefaultClass, isGhost, false);
- } else SynErr(111);
+ } else SynErr(110);
}
DefaultClassDecl defaultClass = null;
foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
@@ -275,7 +275,7 @@ bool IsAttribute() {
module.TopLevelDecls.Add(at);
} else if (StartOf(2)) {
ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false);
- } else SynErr(112);
+ } else SynErr(111);
}
Expect(7);
module.BodyEndTok = t;
@@ -291,7 +291,7 @@ bool IsAttribute() {
QualifiedName(out idPath);
Expect(12);
submodule = new AbstractModuleDecl(idPath, id, parent);
- } else SynErr(113);
+ } else SynErr(112);
}
void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {
@@ -303,7 +303,7 @@ bool IsAttribute() {
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 15)) {SynErr(114); Get();}
+ while (!(la.kind == 0 || la.kind == 15)) {SynErr(113); Get();}
Expect(15);
while (la.kind == 6) {
Attribute(ref attrs);
@@ -334,13 +334,13 @@ bool IsAttribute() {
IToken bodyStart = Token.NoToken; // dummy assignment
bool co = false;
- while (!(la.kind == 0 || la.kind == 17 || la.kind == 18)) {SynErr(115); Get();}
+ while (!(la.kind == 0 || la.kind == 17 || la.kind == 18)) {SynErr(114); Get();}
if (la.kind == 17) {
Get();
} else if (la.kind == 18) {
Get();
co = true;
- } else SynErr(116);
+ } else SynErr(115);
while (la.kind == 6) {
Attribute(ref attrs);
}
@@ -355,7 +355,7 @@ bool IsAttribute() {
Get();
DatatypeMemberDecl(ctors);
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(117); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(116); Get();}
Expect(12);
if (co) {
dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
@@ -384,7 +384,7 @@ bool IsAttribute() {
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(118); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(117); Get();}
Expect(12);
}
@@ -412,7 +412,7 @@ bool IsAttribute() {
} else if (la.kind == 28 || la.kind == 29) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
- } else SynErr(119);
+ } else SynErr(118);
}
void Attribute(ref Attributes attrs) {
@@ -483,7 +483,7 @@ bool IsAttribute() {
Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- while (!(la.kind == 0 || la.kind == 20)) {SynErr(120); Get();}
+ while (!(la.kind == 0 || la.kind == 20)) {SynErr(119); Get();}
Expect(20);
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
@@ -497,7 +497,7 @@ bool IsAttribute() {
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(121); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(120); Get();}
Expect(12);
}
@@ -543,7 +543,7 @@ bool IsAttribute() {
Get();
signatureOmitted = true;
openParen = Token.NoToken;
- } else SynErr(122);
+ } else SynErr(121);
} else if (la.kind == 46) {
Get();
isPredicate = true;
@@ -572,7 +572,7 @@ bool IsAttribute() {
Get();
signatureOmitted = true;
openParen = Token.NoToken;
- } else SynErr(123);
+ } else SynErr(122);
} else if (la.kind == 47) {
Get();
isCoPredicate = true;
@@ -597,8 +597,8 @@ bool IsAttribute() {
Get();
signatureOmitted = true;
openParen = Token.NoToken;
- } else SynErr(124);
- } else SynErr(125);
+ } else SynErr(123);
+ } else SynErr(124);
decreases = isCoPredicate ? null : new List<Expression/*!*/>();
while (StartOf(4)) {
FunctionSpec(reqs, reads, ens, decreases);
@@ -641,7 +641,7 @@ bool IsAttribute() {
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 28 || la.kind == 29)) {SynErr(126); Get();}
+ while (!(la.kind == 0 || la.kind == 28 || la.kind == 29)) {SynErr(125); Get();}
if (la.kind == 28) {
Get();
} else if (la.kind == 29) {
@@ -652,7 +652,7 @@ bool IsAttribute() {
SemErr(t, "constructors are only allowed in classes");
}
- } else SynErr(127);
+ } else SynErr(126);
if (isConstructor) {
if (mmod.IsGhost) {
SemErr(t, "constructors cannot be declared 'ghost'");
@@ -679,7 +679,7 @@ bool IsAttribute() {
} else if (la.kind == 31) {
Get();
signatureOmitted = true; openParen = Token.NoToken;
- } else SynErr(128);
+ } else SynErr(127);
while (StartOf(5)) {
MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
}
@@ -873,7 +873,7 @@ bool IsAttribute() {
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(129); break;
+ default: SynErr(128); break;
}
}
@@ -898,7 +898,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(7))) {SynErr(130); Get();}
+ while (!(StartOf(7))) {SynErr(129); Get();}
if (la.kind == 32) {
Get();
while (IsAttribute()) {
@@ -913,7 +913,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(131); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(130); Get();}
Expect(12);
} else if (la.kind == 33 || la.kind == 34 || la.kind == 35) {
if (la.kind == 33) {
@@ -923,7 +923,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 34) {
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(132); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(131); Get();}
Expect(12);
req.Add(new MaybeFreeExpression(e, isFree));
} else if (la.kind == 35) {
@@ -932,19 +932,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Attribute(ref ensAttrs);
}
Expression(out e);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(133); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(132); Get();}
Expect(12);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- } else SynErr(134);
+ } else SynErr(133);
} else if (la.kind == 36) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(135); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(134); Get();}
Expect(12);
- } else SynErr(136);
+ } else SynErr(135);
}
void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -1045,7 +1045,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt, path);
- } else SynErr(137);
+ } else SynErr(136);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
@@ -1054,10 +1054,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
if (la.kind == 34) {
- while (!(la.kind == 0 || la.kind == 34)) {SynErr(138); Get();}
+ while (!(la.kind == 0 || la.kind == 34)) {SynErr(137); Get();}
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(139); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(138); Get();}
Expect(12);
reqs.Add(e);
} else if (la.kind == 48) {
@@ -1071,12 +1071,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(140); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(139); Get();}
Expect(12);
} else if (la.kind == 35) {
Get();
Expression(out e);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(141); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(140); Get();}
Expect(12);
ens.Add(e);
} else if (la.kind == 36) {
@@ -1087,9 +1087,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(142); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(141); Get();}
Expect(12);
- } else SynErr(143);
+ } else SynErr(142);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -1108,7 +1108,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(8)) {
FrameExpression(out fe);
- } else SynErr(144);
+ } else SynErr(143);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -1119,7 +1119,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new WildcardExpr(t);
} else if (StartOf(8)) {
Expression(out e);
- } else SynErr(145);
+ } else SynErr(144);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1136,7 +1136,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken bodyStart, bodyEnd;
int breakCount;
- while (!(StartOf(11))) {SynErr(146); Get();}
+ while (!(StartOf(11))) {SynErr(145); Get();}
switch (la.kind) {
case 6: {
BlockStmt(out bs, out bodyStart, out bodyEnd);
@@ -1199,13 +1199,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
breakCount++;
}
- } else SynErr(147);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(148); Get();}
+ } else SynErr(146);
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(147); Get();}
Expect(12);
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
}
- case 54: {
+ case 55: {
ReturnStmt(out s);
break;
}
@@ -1214,7 +1214,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(12);
break;
}
- default: SynErr(149); break;
+ default: SynErr(148); break;
}
}
@@ -1231,7 +1231,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression(out e);
} else if (la.kind == 31) {
Get();
- } else SynErr(150);
+ } else SynErr(149);
Expect(12);
if (e == null) {
s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);
@@ -1254,7 +1254,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression(out e);
} else if (la.kind == 31) {
Get();
- } else SynErr(151);
+ } else SynErr(150);
if (e == null) {
s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
} else {
@@ -1299,14 +1299,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(12);
rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 21 || la.kind == 55 || la.kind == 56) {
+ } else if (la.kind == 21 || la.kind == 54 || la.kind == 56) {
lhss.Add(e); lhs0 = e;
while (la.kind == 21) {
Get();
Lhs(out e);
lhss.Add(e);
}
- if (la.kind == 55) {
+ if (la.kind == 54) {
Get();
x = t;
Rhs(out r, lhs0);
@@ -1324,12 +1324,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
suchThatAssume = t;
}
Expression(out suchThat);
- } else SynErr(152);
+ } else SynErr(151);
Expect(12);
} else if (la.kind == 5) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(153);
+ } else SynErr(152);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
} else {
@@ -1364,8 +1364,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d);
}
- if (la.kind == 55 || la.kind == 56) {
- if (la.kind == 55) {
+ if (la.kind == 54 || la.kind == 56) {
+ if (la.kind == 54) {
Get();
assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -1438,7 +1438,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 6) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs;
- } else SynErr(154);
+ } else SynErr(153);
}
if (guardOmitted) {
ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);
@@ -1449,7 +1449,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 6) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(155);
+ } else SynErr(154);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1481,7 +1481,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 31) {
Get();
bodyOmitted = true;
- } else SynErr(156);
+ } else SynErr(155);
if (guardOmitted || bodyOmitted) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -1499,7 +1499,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives);
- } else SynErr(157);
+ } else SynErr(156);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -1563,7 +1563,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<AssignmentRhs> rhss = null;
AssignmentRhs r;
- Expect(54);
+ Expect(55);
returnTok = t;
if (StartOf(13)) {
Rhs(out r, null);
@@ -1581,24 +1581,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void SkeletonStmt(out Statement s) {
List<IToken> names = null;
List<Expression> exprs = null;
- IToken tok, dotdotdot;
+ IToken tok, dotdotdot, whereTok;
Expression e;
Expect(31);
dotdotdot = t;
if (la.kind == 53) {
Get();
- names = new List<IToken>(); exprs = new List<Expression>();
+ names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;
Ident(out tok);
- Expect(11);
- Expression(out e);
- names.Add(tok); exprs.Add(e);
+ names.Add(tok);
while (la.kind == 21) {
Get();
Ident(out tok);
- Expect(11);
+ names.Add(tok);
+ }
+ Expect(54);
+ Expression(out e);
+ exprs.Add(e);
+ while (la.kind == 21) {
+ Get();
Expression(out e);
+ exprs.Add(e);
+ }
+ if (exprs.Count != names.Count) {
+ SemErr(whereTok, exprs.Count < names.Count ? "not enough expressions" : "too many expressions");
+ names = null; exprs = null;
}
- names.Add(tok); exprs.Add(e);
+
}
s = new SkeletonStatement(dotdotdot, names, exprs);
}
@@ -1674,7 +1683,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(8)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(158);
+ } else SynErr(157);
while (la.kind == 6) {
Attribute(ref attrs);
}
@@ -1695,7 +1704,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (la.kind == 14 || la.kind == 59) {
Suffix(ref e);
}
- } else SynErr(159);
+ } else SynErr(158);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1718,7 +1727,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(160);
+ } else SynErr(159);
Expect(25);
}
@@ -1753,20 +1762,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (StartOf(15)) {
if (la.kind == 33 || la.kind == 67) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(161); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(160); Get();}
Expect(12);
invariants.Add(invariant);
} else if (la.kind == 36) {
- while (!(la.kind == 0 || la.kind == 36)) {SynErr(162); Get();}
+ while (!(la.kind == 0 || la.kind == 36)) {SynErr(161); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(163); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(162); Get();}
Expect(12);
} else {
- while (!(la.kind == 0 || la.kind == 32)) {SynErr(164); Get();}
+ while (!(la.kind == 0 || la.kind == 32)) {SynErr(163); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -1781,7 +1790,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(165); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(164); Get();}
Expect(12);
}
}
@@ -1789,7 +1798,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 == 33 || la.kind == 67)) {SynErr(166); Get();}
+ while (!(la.kind == 0 || la.kind == 33 || la.kind == 67)) {SynErr(165); Get();}
if (la.kind == 33) {
Get();
isFree = true;
@@ -1838,7 +1847,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(t, e);
- } else SynErr(167);
+ } else SynErr(166);
}
void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -1890,7 +1899,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 73) {
Get();
- } else SynErr(168);
+ } else SynErr(167);
}
void LogicalExpression(out Expression/*!*/ e0) {
@@ -1928,7 +1937,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 75) {
Get();
- } else SynErr(169);
+ } else SynErr(168);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -2026,7 +2035,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 77) {
Get();
- } else SynErr(170);
+ } else SynErr(169);
}
void OrOp() {
@@ -2034,7 +2043,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 79) {
Get();
- } else SynErr(171);
+ } else SynErr(170);
}
void Term(out Expression/*!*/ e0) {
@@ -2126,7 +2135,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(172); break;
+ default: SynErr(171); break;
}
}
@@ -2148,7 +2157,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 90) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(173);
+ } else SynErr(172);
}
void UnaryExpression(out Expression/*!*/ e) {
@@ -2168,7 +2177,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 20: case 40: case 57: case 62: case 68: case 69: case 102: case 104: case 105: case 106: case 107: {
+ case 20: case 40: case 51: case 57: case 62: case 68: case 69: case 103: case 104: case 105: case 106: {
EndlessExpression(out e);
break;
}
@@ -2198,7 +2207,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
break;
}
- default: SynErr(174); break;
+ default: SynErr(173); break;
}
}
@@ -2213,7 +2222,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 92) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(175);
+ } else SynErr(174);
}
void NegOp() {
@@ -2221,7 +2230,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 93) {
Get();
- } else SynErr(176);
+ } else SynErr(175);
}
void EndlessExpression(out Expression e) {
@@ -2245,7 +2254,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
MatchExpression(out e);
break;
}
- case 104: case 105: case 106: case 107: {
+ case 103: case 104: case 105: case 106: {
QuantifierGuts(out e);
break;
}
@@ -2275,11 +2284,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
LetExpr(out e);
break;
}
- case 102: {
+ case 51: {
NamedExpr(out e);
break;
}
- default: SynErr(177); break;
+ default: SynErr(176); break;
}
}
@@ -2331,14 +2340,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (StartOf(8)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 103) {
+ if (la.kind == 102) {
Get();
anyDots = true;
if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
- } else if (la.kind == 55) {
+ } else if (la.kind == 54) {
Get();
Expression(out ee);
e1 = ee;
@@ -2353,15 +2362,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
multipleIndices.Add(ee);
}
- } else SynErr(178);
- } else if (la.kind == 103) {
+ } else SynErr(177);
+ } else if (la.kind == 102) {
Get();
anyDots = true;
if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
- } else SynErr(179);
+ } else SynErr(178);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -2385,7 +2394,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(60);
- } else SynErr(180);
+ } else SynErr(179);
}
void DisplayExpr(out Expression e) {
@@ -2409,7 +2418,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
e = new SeqDisplayExpr(x, elements);
Expect(60);
- } else SynErr(181);
+ } else SynErr(180);
}
void MultiSetExpr(out Expression e) {
@@ -2435,7 +2444,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(25);
} else if (StartOf(18)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(182);
+ } else SynErr(181);
}
void MapExpr(out Expression e) {
@@ -2469,7 +2478,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new MapComprehension(x, bvars, range, body);
} else if (StartOf(18)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(183);
+ } else SynErr(182);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2546,7 +2555,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(25);
break;
}
- default: SynErr(184); break;
+ default: SynErr(183); break;
}
}
@@ -2565,24 +2574,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression/*!*/ d, r;
elements = new List<ExpressionPair/*!*/>();
Expression(out d);
- Expect(55);
+ Expect(54);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
while (la.kind == 21) {
Get();
Expression(out d);
- Expect(55);
+ Expect(54);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
}
}
void QSep() {
- if (la.kind == 108) {
+ if (la.kind == 107) {
Get();
- } else if (la.kind == 109) {
+ } else if (la.kind == 108) {
Get();
- } else SynErr(185);
+ } else SynErr(184);
}
void MatchExpression(out Expression/*!*/ e) {
@@ -2607,13 +2616,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression range;
Expression/*!*/ body;
- if (la.kind == 104 || la.kind == 105) {
+ if (la.kind == 103 || la.kind == 104) {
Forall();
x = t; univ = true;
- } else if (la.kind == 106 || la.kind == 107) {
+ } else if (la.kind == 105 || la.kind == 106) {
Exists();
x = t;
- } else SynErr(186);
+ } else SynErr(185);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body);
@@ -2644,7 +2653,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(19);
Expression(out range);
- if (la.kind == 108 || la.kind == 109) {
+ if (la.kind == 107 || la.kind == 108) {
QSep();
Expression(out body);
}
@@ -2670,7 +2679,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IdentTypeOptional(out d);
letVars.Add(d);
}
- Expect(55);
+ Expect(54);
Expression(out e);
letRHSs.Add(e);
while (la.kind == 21) {
@@ -2688,7 +2697,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = dummyExpr;
Expression expr;
- Expect(102);
+ Expect(51);
x = t;
NoUSIdent(out d);
Expect(5);
@@ -2723,19 +2732,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void Forall() {
- if (la.kind == 104) {
+ if (la.kind == 103) {
Get();
- } else if (la.kind == 105) {
+ } else if (la.kind == 104) {
Get();
- } else SynErr(187);
+ } else SynErr(186);
}
void Exists() {
- if (la.kind == 106) {
+ if (la.kind == 105) {
Get();
- } else if (la.kind == 107) {
+ } else if (la.kind == 106) {
Get();
- } else SynErr(188);
+ } else SynErr(187);
}
void AttributeBody(ref Attributes attrs) {
@@ -2771,26 +2780,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
static readonly bool[,]/*!*/ set = {
- {T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, T,x,x,T, x,x,x,x, T,T,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,T,x,x, x,x,T,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,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, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {T,x,x,x, x,x,T,T, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,T, x,x,T,x, T,T,x,x, x,x,T,T, T,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,T,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,x,T, x,x,x,x, 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, 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, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,T,x, T,T,T,T, x,x,x,x},
- {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,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, x,x,x,T, T,x,T,x, x,T,x,x, x,x,T,x, x,x,T,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,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,T,x,T, 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,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,T,x, T,T,T,T, x,x,x,x},
- {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,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, x,x,x,T, T,x,T,x, x,T,x,x, x,x,T,x, x,x,T,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,T,T, T,T,T,T, T,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, 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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,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, T,T,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,T,T,T, x,T,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,T,x, T,T,T,T, x,x,x,x},
- {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, 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,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, 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, T,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, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,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,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, T,T,x,x},
- {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,T,x, T,T,T,T, x,x,x,x}
+ {T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, T,x,x,T, x,x,x,x, T,T,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,T,T, T,T,T,T, 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, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {T,x,x,x, x,x,T,T, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,T, x,x,T,x, T,T,x,x, x,x,T,T, T,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,T,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, 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,T,x,T, 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,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, 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,T,T,x, x,x,T,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, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
+ {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,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, x,x,x,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,T,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,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,T,x,T, x,x,x,x, x,T,x,T, 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,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
+ {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,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, x,x,x,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,T,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,T,T, T,T,T,T, 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, 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,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,x, x,x,T,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, T,T,x,T, x,x,x,x, x,T,x,T, x,x,x,x, x,T,T,T, x,T,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
+ {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, 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,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, 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, T,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, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,T,x, x,x,x,x, T,x,x,T, T,T,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,x,x,x, x,x,x,x, x,T,T,x, x,x,x,T, T,x,x},
+ {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,T, 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,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}
};
} // end Parser
@@ -2869,8 +2878,8 @@ public class Errors {
case 51: s = "\"label\" expected"; break;
case 52: s = "\"break\" expected"; break;
case 53: s = "\"where\" expected"; break;
- case 54: s = "\"return\" expected"; break;
- case 55: s = "\":=\" expected"; break;
+ case 54: s = "\":=\" expected"; break;
+ case 55: s = "\"return\" expected"; break;
case 56: s = "\":|\" expected"; break;
case 57: s = "\"assume\" expected"; break;
case 58: s = "\"new\" expected"; break;
@@ -2917,93 +2926,92 @@ public class Errors {
case 99: s = "\"allocated\" expected"; break;
case 100: s = "\"old\" expected"; break;
case 101: s = "\"then\" expected"; break;
- case 102: s = "\"expr\" expected"; break;
- case 103: s = "\"..\" expected"; break;
- case 104: s = "\"forall\" expected"; break;
- case 105: s = "\"\\u2200\" expected"; break;
- case 106: s = "\"exists\" expected"; break;
- case 107: s = "\"\\u2203\" expected"; break;
- case 108: s = "\"::\" expected"; break;
- case 109: s = "\"\\u2022\" expected"; break;
- case 110: s = "??? expected"; break;
- case 111: s = "invalid Dafny"; break;
+ case 102: s = "\"..\" expected"; break;
+ case 103: s = "\"forall\" expected"; break;
+ case 104: s = "\"\\u2200\" expected"; break;
+ case 105: s = "\"exists\" expected"; break;
+ case 106: s = "\"\\u2203\" expected"; break;
+ case 107: s = "\"::\" expected"; break;
+ case 108: s = "\"\\u2022\" expected"; break;
+ case 109: s = "??? expected"; break;
+ case 110: s = "invalid Dafny"; break;
+ case 111: s = "invalid SubModuleDecl"; break;
case 112: s = "invalid SubModuleDecl"; break;
- case 113: s = "invalid SubModuleDecl"; break;
- case 114: s = "this symbol not expected in ClassDecl"; break;
- case 115: s = "this symbol not expected in DatatypeDecl"; break;
- case 116: s = "invalid DatatypeDecl"; break;
- case 117: s = "this symbol not expected in DatatypeDecl"; break;
- case 118: s = "this symbol not expected in ArbitraryTypeDecl"; break;
- case 119: s = "invalid ClassMemberDecl"; break;
+ case 113: s = "this symbol not expected in ClassDecl"; break;
+ case 114: s = "this symbol not expected in DatatypeDecl"; break;
+ case 115: s = "invalid DatatypeDecl"; break;
+ case 116: s = "this symbol not expected in DatatypeDecl"; break;
+ case 117: s = "this symbol not expected in ArbitraryTypeDecl"; break;
+ case 118: s = "invalid ClassMemberDecl"; break;
+ case 119: s = "this symbol not expected in FieldDecl"; break;
case 120: s = "this symbol not expected in FieldDecl"; break;
- case 121: s = "this symbol not expected in FieldDecl"; break;
+ case 121: s = "invalid FunctionDecl"; break;
case 122: s = "invalid FunctionDecl"; break;
case 123: s = "invalid FunctionDecl"; break;
case 124: s = "invalid FunctionDecl"; break;
- case 125: s = "invalid FunctionDecl"; break;
- case 126: s = "this symbol not expected in MethodDecl"; break;
+ case 125: s = "this symbol not expected in MethodDecl"; break;
+ case 126: s = "invalid MethodDecl"; break;
case 127: s = "invalid MethodDecl"; break;
- case 128: s = "invalid MethodDecl"; break;
- case 129: s = "invalid TypeAndToken"; break;
+ case 128: s = "invalid TypeAndToken"; break;
+ case 129: s = "this symbol not expected in MethodSpec"; break;
case 130: s = "this symbol not expected in MethodSpec"; break;
case 131: s = "this symbol not expected in MethodSpec"; break;
case 132: s = "this symbol not expected in MethodSpec"; break;
- case 133: s = "this symbol not expected in MethodSpec"; break;
- case 134: s = "invalid MethodSpec"; break;
- case 135: s = "this symbol not expected in MethodSpec"; break;
- case 136: s = "invalid MethodSpec"; break;
- case 137: s = "invalid ReferenceType"; break;
+ case 133: s = "invalid MethodSpec"; break;
+ case 134: s = "this symbol not expected in MethodSpec"; break;
+ case 135: s = "invalid MethodSpec"; break;
+ case 136: s = "invalid ReferenceType"; break;
+ case 137: s = "this symbol not expected in FunctionSpec"; break;
case 138: s = "this symbol not expected in FunctionSpec"; break;
case 139: s = "this symbol not expected in FunctionSpec"; break;
case 140: s = "this symbol not expected in FunctionSpec"; break;
case 141: s = "this symbol not expected in FunctionSpec"; break;
- case 142: s = "this symbol not expected in FunctionSpec"; break;
- case 143: s = "invalid FunctionSpec"; break;
- case 144: s = "invalid PossiblyWildFrameExpression"; break;
- case 145: s = "invalid PossiblyWildExpression"; break;
- case 146: s = "this symbol not expected in OneStmt"; break;
- case 147: s = "invalid OneStmt"; break;
- case 148: s = "this symbol not expected in OneStmt"; break;
- case 149: s = "invalid OneStmt"; break;
- case 150: s = "invalid AssertStmt"; break;
- case 151: s = "invalid AssumeStmt"; break;
+ case 142: s = "invalid FunctionSpec"; break;
+ case 143: s = "invalid PossiblyWildFrameExpression"; break;
+ case 144: s = "invalid PossiblyWildExpression"; break;
+ case 145: s = "this symbol not expected in OneStmt"; break;
+ case 146: s = "invalid OneStmt"; break;
+ case 147: s = "this symbol not expected in OneStmt"; break;
+ case 148: s = "invalid OneStmt"; break;
+ case 149: s = "invalid AssertStmt"; break;
+ case 150: s = "invalid AssumeStmt"; break;
+ case 151: s = "invalid UpdateStmt"; break;
case 152: s = "invalid UpdateStmt"; break;
- case 153: s = "invalid UpdateStmt"; break;
+ case 153: s = "invalid IfStmt"; break;
case 154: s = "invalid IfStmt"; break;
- case 155: s = "invalid IfStmt"; break;
+ case 155: s = "invalid WhileStmt"; break;
case 156: s = "invalid WhileStmt"; break;
- case 157: s = "invalid WhileStmt"; break;
- case 158: s = "invalid Rhs"; break;
- case 159: s = "invalid Lhs"; break;
- case 160: s = "invalid Guard"; break;
+ case 157: s = "invalid Rhs"; break;
+ case 158: s = "invalid Lhs"; break;
+ case 159: s = "invalid Guard"; break;
+ case 160: s = "this symbol not expected in LoopSpec"; break;
case 161: s = "this symbol not expected in LoopSpec"; break;
case 162: s = "this symbol not expected in LoopSpec"; break;
case 163: s = "this symbol not expected in LoopSpec"; break;
case 164: s = "this symbol not expected in LoopSpec"; break;
- case 165: s = "this symbol not expected in LoopSpec"; break;
- case 166: s = "this symbol not expected in Invariant"; break;
- case 167: s = "invalid AttributeArg"; break;
- case 168: s = "invalid EquivOp"; break;
- case 169: s = "invalid ImpliesOp"; break;
- case 170: s = "invalid AndOp"; break;
- case 171: s = "invalid OrOp"; break;
- case 172: s = "invalid RelOp"; break;
- case 173: s = "invalid AddOp"; break;
- case 174: s = "invalid UnaryExpression"; break;
- case 175: s = "invalid MulOp"; break;
- case 176: s = "invalid NegOp"; break;
- case 177: s = "invalid EndlessExpression"; break;
+ case 165: s = "this symbol not expected in Invariant"; break;
+ case 166: s = "invalid AttributeArg"; break;
+ case 167: s = "invalid EquivOp"; break;
+ case 168: s = "invalid ImpliesOp"; break;
+ case 169: s = "invalid AndOp"; break;
+ case 170: s = "invalid OrOp"; break;
+ case 171: s = "invalid RelOp"; break;
+ case 172: s = "invalid AddOp"; break;
+ case 173: s = "invalid UnaryExpression"; break;
+ case 174: s = "invalid MulOp"; break;
+ case 175: s = "invalid NegOp"; break;
+ case 176: s = "invalid EndlessExpression"; break;
+ case 177: s = "invalid Suffix"; break;
case 178: s = "invalid Suffix"; break;
case 179: s = "invalid Suffix"; break;
- case 180: s = "invalid Suffix"; break;
- case 181: s = "invalid DisplayExpr"; break;
- case 182: s = "invalid MultiSetExpr"; break;
- case 183: s = "invalid MapExpr"; break;
- case 184: s = "invalid ConstAtomExpression"; break;
- case 185: s = "invalid QSep"; break;
- case 186: s = "invalid QuantifierGuts"; break;
- case 187: s = "invalid Forall"; break;
- case 188: s = "invalid Exists"; break;
+ case 180: s = "invalid DisplayExpr"; break;
+ case 181: s = "invalid MultiSetExpr"; break;
+ case 182: s = "invalid MapExpr"; break;
+ case 183: s = "invalid ConstAtomExpression"; break;
+ case 184: s = "invalid QSep"; break;
+ case 185: s = "invalid QuantifierGuts"; break;
+ case 186: s = "invalid Forall"; break;
+ case 187: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index 5ddc1fac..a5fab242 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -809,15 +809,15 @@ namespace Microsoft.Dafny {
return nw;
}
- private Statement SubstituteNamedExpr(Statement s, IToken p, Expression E, ref int subCount) {
+ private Statement SubstituteNamedExpr(Statement s, Dictionary<string, Expression> sub, SortedSet<string> subs) {
if (s == null) {
return null;
} else if (s is AssertStmt) {
AssertStmt stmt = (AssertStmt)s;
- return new AssertStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, p, E, ref subCount), null);
+ return new AssertStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, sub, subs), null);
} else if (s is AssumeStmt) {
AssumeStmt stmt = (AssumeStmt)s;
- return new AssumeStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, p, E, ref subCount), null);
+ return new AssumeStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, sub, subs), null);
} else if (s is PrintStmt) {
throw new NotImplementedException();
} else if (s is BreakStmt) {
@@ -833,16 +833,16 @@ namespace Microsoft.Dafny {
List<Expression> lhs = new List<Expression>();
List<AssignmentRhs> rhs = new List<AssignmentRhs>();
foreach (Expression l in stmt.Lhss) {
- lhs.Add(SubstituteNamedExpr(l, p, E, ref subCount));
+ lhs.Add(SubstituteNamedExpr(l, sub, subs));
}
foreach (AssignmentRhs r in stmt.Rhss) {
if (r is HavocRhs) {
rhs.Add(r); // no substitution on Havoc (*);
} else if (r is ExprRhs) {
- rhs.Add(new ExprRhs(SubstituteNamedExpr(((ExprRhs)r).Expr, p, E, ref subCount)));
+ rhs.Add(new ExprRhs(SubstituteNamedExpr(((ExprRhs)r).Expr, sub, subs)));
} else if (r is CallRhs) {
CallRhs rr = (CallRhs)r;
- rhs.Add(new CallRhs(rr.Tok, SubstituteNamedExpr(rr.Receiver, p, E, ref subCount), rr.MethodName, SubstituteNamedExprList(rr.Args, p, E, ref subCount)));
+ rhs.Add(new CallRhs(rr.Tok, SubstituteNamedExpr(rr.Receiver, sub, subs), rr.MethodName, SubstituteNamedExprList(rr.Args, sub, subs)));
} else if (r is TypeRhs) {
rhs.Add(r);
} else {
@@ -862,19 +862,19 @@ namespace Microsoft.Dafny {
BlockStmt stmt = (BlockStmt)s;
List<Statement> res = new List<Statement>();
foreach (Statement ss in stmt.Body) {
- res.Add(SubstituteNamedExpr(ss, p, E, ref subCount));
+ res.Add(SubstituteNamedExpr(ss, sub, subs));
}
return new BlockStmt(stmt.Tok, res);
} else if (s is IfStmt) {
IfStmt stmt = (IfStmt)s;
- return new IfStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, p, E, ref subCount),
- (BlockStmt)SubstituteNamedExpr(stmt.Thn, p, E, ref subCount),
- SubstituteNamedExpr(stmt.Els, p, E, ref subCount));
+ return new IfStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, sub, subs),
+ (BlockStmt)SubstituteNamedExpr(stmt.Thn, sub, subs),
+ SubstituteNamedExpr(stmt.Els, sub, subs));
} else if (s is AlternativeStmt) {
return s;
} else if (s is WhileStmt) {
WhileStmt stmt = (WhileStmt)s;
- return new WhileStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, p, E, ref subCount), stmt.Invariants, stmt.Decreases, stmt.Mod, (BlockStmt)SubstituteNamedExpr(stmt.Body, p, E, ref subCount));
+ return new WhileStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, sub, subs), stmt.Invariants, stmt.Decreases, stmt.Mod, (BlockStmt)SubstituteNamedExpr(stmt.Body, sub, subs));
} else if (s is AlternativeLoopStmt) {
return s;
} else if (s is ParallelStmt) {
@@ -889,21 +889,22 @@ namespace Microsoft.Dafny {
}
}
- private Expression SubstituteNamedExpr(Expression expr, IToken p, Expression E, ref int subCount) {
+ private Expression SubstituteNamedExpr(Expression expr, Dictionary<string, Expression> sub, SortedSet<string> subs) {
if (expr == null) {
return null;
}
if (expr is NamedExpr) {
NamedExpr n = (NamedExpr)expr;
- if (n.Name == p.val) {
- subCount++;
- return new NamedExpr(n.tok, n.Name, E, CloneExpr(n.Body), p);
- } else return new NamedExpr(n.tok, n.Name, SubstituteNamedExpr(n.Body, p, E, ref subCount));
+ Expression E;
+ if (sub.TryGetValue(n.Name, out E)) {
+ subs.Add(n.Name);
+ return new NamedExpr(n.tok, n.Name, E, CloneExpr(n.Body), E.tok);
+ } else return new NamedExpr(n.tok, n.Name, SubstituteNamedExpr(n.Body, sub, subs));
} else if (expr is LiteralExpr || expr is WildcardExpr | expr is ThisExpr || expr is IdentifierExpr) {
return expr;
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
- List<Expression> newElements = SubstituteNamedExprList(e.Elements, p, E, ref subCount);
+ List<Expression> newElements = SubstituteNamedExprList(e.Elements, sub, subs);
if (expr is SetDisplayExpr) {
return new SetDisplayExpr(expr.tok, newElements);
} else if (expr is MultiSetDisplayExpr) {
@@ -913,65 +914,65 @@ namespace Microsoft.Dafny {
}
} else if (expr is FieldSelectExpr) {
FieldSelectExpr fse = (FieldSelectExpr)expr;
- Expression substE = SubstituteNamedExpr(fse.Obj, p, E, ref subCount);
+ Expression substE = SubstituteNamedExpr(fse.Obj, sub, subs);
return new FieldSelectExpr(fse.tok, substE, fse.FieldName);
} else if (expr is SeqSelectExpr) {
SeqSelectExpr sse = (SeqSelectExpr)expr;
- Expression seq = SubstituteNamedExpr(sse.Seq, p, E, ref subCount);
- Expression e0 = sse.E0 == null ? null : SubstituteNamedExpr(sse.E0, p, E, ref subCount);
- Expression e1 = sse.E1 == null ? null : SubstituteNamedExpr(sse.E1, p, E, ref subCount);
+ Expression seq = SubstituteNamedExpr(sse.Seq, sub, subs);
+ Expression e0 = sse.E0 == null ? null : SubstituteNamedExpr(sse.E0, sub, subs);
+ Expression e1 = sse.E1 == null ? null : SubstituteNamedExpr(sse.E1, sub, subs);
return new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr sse = (SeqUpdateExpr)expr;
- Expression seq = SubstituteNamedExpr(sse.Seq, p, E, ref subCount);
- Expression index = SubstituteNamedExpr(sse.Index, p, E, ref subCount);
- Expression val = SubstituteNamedExpr(sse.Value, p, E, ref subCount);
+ Expression seq = SubstituteNamedExpr(sse.Seq, sub, subs);
+ Expression index = SubstituteNamedExpr(sse.Index, sub, subs);
+ Expression val = SubstituteNamedExpr(sse.Value, sub, subs);
return new SeqUpdateExpr(sse.tok, seq, index, val);
} else if (expr is MultiSelectExpr) {
MultiSelectExpr mse = (MultiSelectExpr)expr;
- Expression array = SubstituteNamedExpr(mse.Array, p, E, ref subCount);
- List<Expression> newArgs = SubstituteNamedExprList(mse.Indices, p, E, ref subCount);
+ Expression array = SubstituteNamedExpr(mse.Array, sub, subs);
+ List<Expression> newArgs = SubstituteNamedExprList(mse.Indices, sub, subs);
return new MultiSelectExpr(mse.tok, array, newArgs);
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
- Expression receiver = SubstituteNamedExpr(e.Receiver, p, E, ref subCount);
- List<Expression> newArgs = SubstituteNamedExprList(e.Args, p, E, ref subCount);
+ Expression receiver = SubstituteNamedExpr(e.Receiver, sub, subs);
+ List<Expression> newArgs = SubstituteNamedExprList(e.Args, sub, subs);
return new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs);
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
- List<Expression> newArgs = SubstituteNamedExprList(dtv.Arguments, p, E, ref subCount);
+ List<Expression> newArgs = SubstituteNamedExprList(dtv.Arguments, sub, subs);
return new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArgs);
} else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
- Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);
+ Expression se = SubstituteNamedExpr(e.E, sub, subs);
return new OldExpr(expr.tok, se);
} else if (expr is FreshExpr) {
FreshExpr e = (FreshExpr)expr;
- Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);
+ Expression se = SubstituteNamedExpr(e.E, sub, subs);
return new FreshExpr(expr.tok, se);
} else if (expr is AllocatedExpr) {
AllocatedExpr e = (AllocatedExpr)expr;
- Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);
+ Expression se = SubstituteNamedExpr(e.E, sub, subs);
return new AllocatedExpr(expr.tok, se);
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
- Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);
+ Expression se = SubstituteNamedExpr(e.E, sub, subs);
return new UnaryExpr(expr.tok, e.Op, se);
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
- Expression e0 = SubstituteNamedExpr(e.E0, p, E, ref subCount);
- Expression e1 = SubstituteNamedExpr(e.E1, p, E, ref subCount);
+ Expression e0 = SubstituteNamedExpr(e.E0, sub, subs);
+ Expression e1 = SubstituteNamedExpr(e.E1, sub, subs);
return new BinaryExpr(expr.tok, e.Op, e0, e1);
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
- var rhss = SubstituteNamedExprList(e.RHSs, p, E, ref subCount);
- var body = SubstituteNamedExpr(e.Body, p, E, ref subCount);
+ var rhss = SubstituteNamedExprList(e.RHSs, sub, subs);
+ var body = SubstituteNamedExpr(e.Body, sub, subs);
return new LetExpr(e.tok, e.Vars, rhss, body);
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
- Expression newRange = e.Range == null ? null : SubstituteNamedExpr(e.Range, p, E, ref subCount);
- Expression newTerm = SubstituteNamedExpr(e.Term, p, E, ref subCount);
- Attributes newAttrs = e.Attributes;//SubstituteNamedExpr(e.Attributes, p, E, ref subCount);
+ Expression newRange = e.Range == null ? null : SubstituteNamedExpr(e.Range, sub, subs);
+ Expression newTerm = SubstituteNamedExpr(e.Term, sub, subs);
+ Attributes newAttrs = e.Attributes;//SubstituteNamedExpr(e.Attributes, sub, ref subCount);
if (e is SetComprehension) {
return new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm);
} else if (e is MapComprehension) {
@@ -990,8 +991,8 @@ namespace Microsoft.Dafny {
} else if (expr is PredicateExpr) {
var e = (PredicateExpr)expr;
- Expression g = SubstituteNamedExpr(e.Guard, p, E, ref subCount);
- Expression b = SubstituteNamedExpr(e.Body, p, E, ref subCount);
+ Expression g = SubstituteNamedExpr(e.Guard, sub, subs);
+ Expression b = SubstituteNamedExpr(e.Body, sub, subs);
if (expr is AssertExpr) {
return new AssertExpr(e.tok, g, b);
} else {
@@ -999,21 +1000,21 @@ namespace Microsoft.Dafny {
}
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
- Expression test = SubstituteNamedExpr(e.Test, p, E, ref subCount);
- Expression thn = SubstituteNamedExpr(e.Thn, p, E, ref subCount);
- Expression els = SubstituteNamedExpr(e.Els, p, E, ref subCount);
+ Expression test = SubstituteNamedExpr(e.Test, sub, subs);
+ Expression thn = SubstituteNamedExpr(e.Thn, sub, subs);
+ Expression els = SubstituteNamedExpr(e.Els, sub, subs);
return new ITEExpr(expr.tok, test, thn, els);
} else if (expr is ConcreteSyntaxExpression) {
if (expr is ParensExpression) {
- return SubstituteNamedExpr(((ParensExpression)expr).E, p, E, ref subCount);
+ return SubstituteNamedExpr(((ParensExpression)expr).E, sub, subs);
} else if (expr is IdentifierSequence) {
return expr;
} else if (expr is ExprDotName) {
ExprDotName edn = (ExprDotName)expr;
- return new ExprDotName(edn.tok, SubstituteNamedExpr(edn.Obj, p, E, ref subCount), edn.SuffixName);
+ return new ExprDotName(edn.tok, SubstituteNamedExpr(edn.Obj, sub, subs), edn.SuffixName);
} else if (expr is ChainingExpression) {
ChainingExpression ch = (ChainingExpression)expr;
- return SubstituteNamedExpr(ch.E, p, E, ref subCount);
+ return SubstituteNamedExpr(ch.E, sub, subs);
} else {
Contract.Assert(false);
throw new cce.UnreachableException();
@@ -1024,10 +1025,10 @@ namespace Microsoft.Dafny {
}
}
- private List<Expression> SubstituteNamedExprList(List<Expression> list, IToken p, Expression E, ref int subCount) {
+ private List<Expression> SubstituteNamedExprList(List<Expression> list, Dictionary<string, Expression> sub, SortedSet<string> subCount) {
List<Expression> res = new List<Expression>();
foreach (Expression e in list) {
- res.Add(SubstituteNamedExpr(e, p, E, ref subCount));
+ res.Add(SubstituteNamedExpr(e, sub, subCount));
}
return res;
}
@@ -1162,20 +1163,34 @@ namespace Microsoft.Dafny {
if (nxt != null && nxt is SkeletonStatement && ((SkeletonStatement)nxt).S == null) {
// "...; ...;" is the same as just "...;", so skip this one
} else {
- int subCount = 0;
+ SortedSet<string> substitutions = null;
+ Dictionary<string, Expression> subExprs = null;
+ if (c.NameReplacements != null) {
+ subExprs = new Dictionary<string, Expression>();
+ substitutions = new SortedSet<string>();
+ Contract.Assert(c.NameReplacements.Count == c.ExprReplacements.Count);
+ for (int k = 0; k < c.NameReplacements.Count; k++) {
+ if (subExprs.ContainsKey(c.NameReplacements[k].val)) {
+ reporter.Error(c.NameReplacements[k], "replacement definition must contain at most one definition for a given label");
+ } else subExprs.Add(c.NameReplacements[k].val, c.ExprReplacements[k]);
+ }
+ }
// skip up until the next thing that matches "nxt"
while (nxt == null || !PotentialMatch(nxt, oldS)) {
// loop invariant: oldS == oldStmt.Body[j]
var s = CloneStmt(oldS);
- if (c.NameReplacements != null)
- s = SubstituteNamedExpr(s, c.NameReplacements[0], c.ExprReplacements[0], ref subCount);
+ if (subExprs != null)
+ s = SubstituteNamedExpr(s, subExprs, substitutions);
body.Add(s);
j++;
if (j == oldStmt.Body.Count) { break; }
oldS = oldStmt.Body[j];
}
- if (c.NameReplacements != null && subCount == 0)
- reporter.Error(c.NameReplacements[0], "did not find expression labeled {0}", c.NameReplacements[0].val);
+ if (subExprs != null && substitutions.Count < subExprs.Count) {
+ foreach (var s in substitutions)
+ subExprs.Remove(s);
+ reporter.Error(c.Tok, "could not find labeled expression(s): " + Util.Comma(", ", subExprs.Keys, x => x));
+ }
}
i++;
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 71210c9f..16804d8c 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -4421,8 +4421,9 @@ namespace Microsoft.Dafny {
return;
}
} else if (expr is NamedExpr) {
- if (moduleInfo.IsGhost) return;
- else CheckIsNonGhost(((NamedExpr)expr).Body);
+ if (!moduleInfo.IsGhost)
+ CheckIsNonGhost(((NamedExpr)expr).Body);
+ return;
}
foreach (var ee in expr.SubExpressions) {
diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index 1bfa80a0..0433519d 100644
--- a/Dafny/Scanner.cs
+++ b/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 = 110;
- const int noSym = 110;
+ const int maxT = 109;
+ const int noSym = 109;
[ContractInvariantMethod]
@@ -521,7 +521,7 @@ public class Scanner {
case "label": t.kind = 51; break;
case "break": t.kind = 52; break;
case "where": t.kind = 53; break;
- case "return": t.kind = 54; break;
+ case "return": t.kind = 55; break;
case "assume": t.kind = 57; break;
case "new": t.kind = 58; break;
case "choose": t.kind = 61; break;
@@ -543,9 +543,8 @@ public class Scanner {
case "allocated": t.kind = 99; break;
case "old": t.kind = 100; break;
case "then": t.kind = 101; break;
- case "expr": t.kind = 102; break;
- case "forall": t.kind = 104; break;
- case "exists": t.kind = 106; break;
+ case "forall": t.kind = 103; break;
+ case "exists": t.kind = 105; break;
default: break;
}
}
@@ -665,7 +664,7 @@ public class Scanner {
case 25:
{t.kind = 50; break;}
case 26:
- {t.kind = 55; break;}
+ {t.kind = 54; break;}
case 27:
{t.kind = 56; break;}
case 28:
@@ -719,13 +718,13 @@ public class Scanner {
case 51:
{t.kind = 93; break;}
case 52:
- {t.kind = 105; break;}
+ {t.kind = 104; break;}
case 53:
- {t.kind = 107; break;}
+ {t.kind = 106; break;}
case 54:
- {t.kind = 108; break;}
+ {t.kind = 107; break;}
case 55:
- {t.kind = 109; break;}
+ {t.kind = 108; break;}
case 56:
recEnd = pos; recKind = 5;
if (ch == '=') {AddCh(); goto case 26;}
@@ -763,9 +762,9 @@ public class Scanner {
if (ch == '>') {AddCh(); goto case 34;}
else {t.kind = 24; break;}
case 64:
- recEnd = pos; recKind = 103;
+ recEnd = pos; recKind = 102;
if (ch == '.') {AddCh(); goto case 23;}
- else {t.kind = 103; break;}
+ else {t.kind = 102; break;}
case 65:
recEnd = pos; recKind = 80;
if (ch == '=') {AddCh(); goto case 31;}
diff --git a/Dafny/Util.cs b/Dafny/Util.cs
index e057727a..8db3ebc8 100644
--- a/Dafny/Util.cs
+++ b/Dafny/Util.cs
@@ -7,7 +7,7 @@ namespace Microsoft.Dafny {
class Util
{
public delegate string ToString<T>(T t);
- public static string Comma<T>(string comma, List<T> l, ToString<T> f) {
+ public static string Comma<T>(string comma, IEnumerable<T> l, ToString<T> f) {
string res = "";
string c = "";
foreach(var t in l) {
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index cf2b357f..e4a8c5d0 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -37,10 +37,10 @@
"invariant" "decreases"
)) . font-lock-builtin-face)
`(,(dafny-regexp-opt '(
- "assert" "assume" "break" "choose" "then" "else" "havoc" "if" "label" "return" "while" "print"
+ "assert" "assume" "break" "choose" "then" "else" "havoc" "if" "label" "return" "while" "print" "where"
"old" "forall" "exists" "new" "parallel" "in" "this" "fresh" "allocated"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
- `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "nat" "int" "object" "set" "seq")) . font-lock-type-face)
+ `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "int" "object" "set" "seq")) . font-lock-type-face)
)
"Minimal highlighting for Dafny mode")
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 01767ca6..4d8e2df1 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -28,7 +28,7 @@ namespace Demo
"in", "forall", "exists",
"seq", "set", "map", "multiset", "array", "array2", "array3",
"match", "case",
- "fresh", "allocated", "old", "choose"
+ "fresh", "allocated", "old", "choose", "where"
);
StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote);
@@ -321,6 +321,7 @@ namespace Demo
| "allocated"
| "old"
| "choose"
+ | "where"
| ident
| "}"
| "{"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index cfd8863f..74bfa65a 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -5,7 +5,7 @@
\usepackage{listings}
\lstdefinelanguage{dafny}{
- morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,%
+ morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,map%
function,predicate,copredicate,
ghost,var,static,refines,
method,constructor,returns,module,imports,in,
@@ -13,7 +13,7 @@
% expressions
match,case,false,true,null,old,fresh,allocated,choose,this,
% statements
- assert,assume,print,new,havoc,if,then,else,while,invariant,break,label,return,parallel,
+ assert,assume,print,new,havoc,if,then,else,while,invariant,break,label,return,parallel,where
},
literate=%
{:}{$\colon$}1
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index 33d447fe..37ec7be0 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -9,9 +9,9 @@ syntax keyword dafnyFunction function predicate copredicate method constructor
syntax keyword dafnyTypeDef class datatype codatatype type
syntax keyword dafnyConditional if then else match case
syntax keyword dafnyRepeat while parallel
-syntax keyword dafnyStatement havoc assume assert return new print break label
+syntax keyword dafnyStatement havoc assume assert return new print break label where
syntax keyword dafnyKeyword var ghost returns null static this refines
-syntax keyword dafnyType bool nat int seq set multiset object array array2 array3
+syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map
syntax keyword dafnyLogic requires ensures modifies reads decreases invariant
syntax keyword dafnyOperator forall exists old fresh allocated choose
syntax keyword dafnyBoolean true false
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 03:25:31 +0000