From f877453f13a60e8a1d08da9cf017b35c772dddc9 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 9 Jul 2012 22:27:41 -0700 Subject: Dafny: rebuilt parser/scanner after previous merge --- Source/Dafny/Parser.cs | 788 ++++++++++++++++++++++++++---------------------- Source/Dafny/Scanner.cs | 122 ++++---- 2 files changed, 482 insertions(+), 428 deletions(-) (limited to 'Source/Dafny') diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index f82f5e88..9c47278b 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/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 = 108; + public const int maxT = 110; 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(109); + } else SynErr(111); } 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(110); + } else SynErr(112); } Expect(7); module.BodyEndTok = t; @@ -291,7 +291,7 @@ bool IsAttribute() { QualifiedName(out idPath); Expect(12); submodule = new AbstractModuleDecl(idPath, id, parent); - } else SynErr(111); + } else SynErr(113); } void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) { @@ -303,7 +303,7 @@ bool IsAttribute() { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 15)) {SynErr(112); Get();} + while (!(la.kind == 0 || la.kind == 15)) {SynErr(114); 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(113); Get();} + while (!(la.kind == 0 || la.kind == 17 || la.kind == 18)) {SynErr(115); Get();} if (la.kind == 17) { Get(); } else if (la.kind == 18) { Get(); co = true; - } else SynErr(114); + } else SynErr(116); while (la.kind == 6) { Attribute(ref attrs); } @@ -355,7 +355,7 @@ bool IsAttribute() { Get(); DatatypeMemberDecl(ctors); } - while (!(la.kind == 0 || la.kind == 12)) {SynErr(115); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(117); 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(116); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(118); 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(117); + } else SynErr(119); } 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(118); Get();} + while (!(la.kind == 0 || la.kind == 20)) {SynErr(120); 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(119); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(121); Get();} Expect(12); } @@ -543,7 +543,7 @@ bool IsAttribute() { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(120); + } else SynErr(122); } else if (la.kind == 46) { Get(); isPredicate = true; @@ -572,7 +572,7 @@ bool IsAttribute() { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(121); + } else SynErr(123); } else if (la.kind == 47) { Get(); isCoPredicate = true; @@ -597,8 +597,8 @@ bool IsAttribute() { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(122); - } else SynErr(123); + } else SynErr(124); + } else SynErr(125); decreases = isCoPredicate ? null : new List(); 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(124); Get();} + while (!(la.kind == 0 || la.kind == 28 || la.kind == 29)) {SynErr(126); 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(125); + } else SynErr(127); 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(126); + } else SynErr(128); 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(127); break; + default: SynErr(129); break; } } @@ -898,7 +898,7 @@ List/*!*/ 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(128); Get();} + while (!(StartOf(7))) {SynErr(130); Get();} if (la.kind == 32) { Get(); while (IsAttribute()) { @@ -913,7 +913,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 12)) {SynErr(129); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(131); Get();} Expect(12); } else if (la.kind == 33 || la.kind == 34 || la.kind == 35) { if (la.kind == 33) { @@ -923,7 +923,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 34) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 12)) {SynErr(130); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(132); Get();} Expect(12); req.Add(new MaybeFreeExpression(e, isFree)); } else if (la.kind == 35) { @@ -932,19 +932,19 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Attribute(ref ensAttrs); } Expression(out e); - while (!(la.kind == 0 || la.kind == 12)) {SynErr(131); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(133); Get();} Expect(12); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); - } else SynErr(132); + } else SynErr(134); } else if (la.kind == 36) { Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 12)) {SynErr(133); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(135); Get();} Expect(12); - } else SynErr(134); + } else SynErr(136); } void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -1013,8 +1013,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) { Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ - IToken moduleName = null; List/*!*/ gt; + List path; if (la.kind == 44) { Get(); @@ -1034,17 +1034,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 1) { Ident(out tok); - gt = new List(); - if (la.kind == 14) { - moduleName = tok; + gt = new List(); + path = new List(); + while (la.kind == 14) { + path.Add(tok); Get(); Ident(out tok); } if (la.kind == 26) { GenericInstantiation(gt); } - ty = new UserDefinedType(tok, tok.val, gt, moduleName); - } else SynErr(135); + ty = new UserDefinedType(tok, tok.val, gt, path); + } else SynErr(137); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List decreases) { @@ -1053,10 +1054,10 @@ List/*!*/ 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(136); Get();} + while (!(la.kind == 0 || la.kind == 34)) {SynErr(138); Get();} Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 12)) {SynErr(137); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(139); Get();} Expect(12); reqs.Add(e); } else if (la.kind == 48) { @@ -1070,12 +1071,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe); } } - while (!(la.kind == 0 || la.kind == 12)) {SynErr(138); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(140); Get();} Expect(12); } else if (la.kind == 35) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 12)) {SynErr(139); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(141); Get();} Expect(12); ens.Add(e); } else if (la.kind == 36) { @@ -1086,9 +1087,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 12)) {SynErr(140); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(142); Get();} Expect(12); - } else SynErr(141); + } else SynErr(143); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -1107,7 +1108,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo fe = new FrameExpression(new WildcardExpr(t), null); } else if (StartOf(8)) { FrameExpression(out fe); - } else SynErr(142); + } else SynErr(144); } void PossiblyWildExpression(out Expression/*!*/ e) { @@ -1118,7 +1119,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new WildcardExpr(t); } else if (StartOf(8)) { Expression(out e); - } else SynErr(143); + } else SynErr(145); } void Stmt(List/*!*/ ss) { @@ -1135,26 +1136,26 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd; int breakCount; - while (!(StartOf(11))) {SynErr(144); Get();} + while (!(StartOf(11))) {SynErr(146); Get();} switch (la.kind) { case 6: { BlockStmt(out bs, out bodyStart, out bodyEnd); s = bs; break; } - case 68: { + case 69: { AssertStmt(out s); break; } - case 56: { + case 57: { AssumeStmt(out s); break; } - case 69: { + case 70: { PrintStmt(out s); break; } - case 1: case 2: case 19: case 23: case 93: case 94: case 95: case 96: case 97: case 98: case 99: { + case 1: case 2: case 19: case 23: case 94: case 95: case 96: case 97: case 98: case 99: case 100: { UpdateStmt(out s); break; } @@ -1162,19 +1163,19 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo VarDeclStatement(out s); break; } - case 61: { + case 62: { IfStmt(out s); break; } - case 65: { + case 66: { WhileStmt(out s); break; } - case 67: { + case 68: { MatchStmt(out s); break; } - case 70: { + case 71: { ParallelStmt(out s); break; } @@ -1198,23 +1199,22 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); breakCount++; } - } else SynErr(145); - while (!(la.kind == 0 || la.kind == 12)) {SynErr(146); Get();} + } else SynErr(147); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(148); Get();} Expect(12); s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); break; } - case 53: { + case 54: { ReturnStmt(out s); break; } case 31: { - Get(); - s = new SkeletonStatement(t); + SkeletonStmt(out s); Expect(12); break; } - default: SynErr(147); break; + default: SynErr(149); break; } } @@ -1222,7 +1222,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression e = null; Attributes attrs = null; - Expect(68); + Expect(69); x = t; while (IsAttribute()) { Attribute(ref attrs); @@ -1231,7 +1231,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e); } else if (la.kind == 31) { Get(); - } else SynErr(148); + } else SynErr(150); Expect(12); if (e == null) { s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false); @@ -1245,7 +1245,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression e = null; Attributes attrs = null; - Expect(56); + Expect(57); x = t; while (IsAttribute()) { Attribute(ref attrs); @@ -1254,7 +1254,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e); } else if (la.kind == 31) { Get(); - } else SynErr(149); + } else SynErr(151); if (e == null) { s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false); } else { @@ -1268,7 +1268,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg; List args = new List(); - Expect(69); + Expect(70); x = t; AttributeArg(out arg); args.Add(arg); @@ -1299,14 +1299,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(12); rhss.Add(new ExprRhs(e, attrs)); - } else if (la.kind == 21 || la.kind == 54 || la.kind == 55) { + } else if (la.kind == 21 || la.kind == 55 || la.kind == 56) { lhss.Add(e); lhs0 = e; while (la.kind == 21) { Get(); Lhs(out e); lhss.Add(e); } - if (la.kind == 54) { + if (la.kind == 55) { Get(); x = t; Rhs(out r, lhs0); @@ -1316,20 +1316,20 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0); rhss.Add(r); } - } else if (la.kind == 55) { + } else if (la.kind == 56) { Get(); x = t; - if (la.kind == 56) { + if (la.kind == 57) { Get(); suchThatAssume = t; } Expression(out suchThat); - } else SynErr(150); + } else SynErr(152); Expect(12); } else if (la.kind == 5) { Get(); SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); - } else SynErr(151); + } else SynErr(153); if (suchThat != null) { s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume); } else { @@ -1364,8 +1364,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LocalIdentTypeOptional(out d, isGhost); lhss.Add(d); } - if (la.kind == 54 || la.kind == 55) { - if (la.kind == 54) { + if (la.kind == 55 || la.kind == 56) { + if (la.kind == 55) { Get(); assignTok = t; lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); @@ -1381,7 +1381,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else { Get(); assignTok = t; - if (la.kind == 56) { + if (la.kind == 57) { Get(); suchThatAssume = t; } @@ -1420,7 +1420,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List alternatives; ifStmt = dummyStmt; // to please the compiler - Expect(61); + Expect(62); x = t; if (la.kind == 23 || la.kind == 31) { if (la.kind == 23) { @@ -1430,15 +1430,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo guardOmitted = true; } BlockStmt(out thn, out bodyStart, out bodyEnd); - if (la.kind == 62) { + if (la.kind == 63) { Get(); - if (la.kind == 61) { + if (la.kind == 62) { IfStmt(out s); els = s; } else if (la.kind == 6) { BlockStmt(out bs, out bodyStart, out bodyEnd); els = bs; - } else SynErr(152); + } else SynErr(154); } if (guardOmitted) { ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false); @@ -1449,7 +1449,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 6) { AlternativeBlock(out alternatives); ifStmt = new AlternativeStmt(x, alternatives); - } else SynErr(153); + } else SynErr(155); } void WhileStmt(out Statement/*!*/ stmt) { @@ -1465,7 +1465,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List alternatives; stmt = dummyStmt; // to please the compiler - Expect(65); + Expect(66); x = t; if (la.kind == 23 || la.kind == 31) { if (la.kind == 23) { @@ -1481,7 +1481,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 31) { Get(); bodyOmitted = true; - } else SynErr(154); + } else SynErr(156); if (guardOmitted || bodyOmitted) { if (mod != null) { SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops"); @@ -1499,18 +1499,18 @@ List/*!*/ 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(decreases, decAttrs), new Specification(mod, modAttrs), alternatives); - } else SynErr(155); + } else SynErr(157); } void MatchStmt(out Statement/*!*/ s) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c; List cases = new List(); - Expect(67); + Expect(68); x = t; Expression(out e); Expect(6); - while (la.kind == 63) { + while (la.kind == 64) { CaseStatement(out c); cases.Add(c); } @@ -1530,7 +1530,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BlockStmt/*!*/ block; IToken bodyStart, bodyEnd; - Expect(70); + Expect(71); x = t; Expect(23); if (la.kind == 1) { @@ -1563,7 +1563,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List rhss = null; AssignmentRhs r; - Expect(53); + Expect(54); returnTok = t; if (StartOf(13)) { Rhs(out r, null); @@ -1578,6 +1578,31 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s = new ReturnStmt(returnTok, rhss); } + void SkeletonStmt(out Statement s) { + List names = null; + List exprs = null; + IToken tok, dotdotdot; + Expression e; + Expect(31); + dotdotdot = t; + if (la.kind == 53) { + Get(); + names = new List(); exprs = new List(); + Ident(out tok); + Expect(11); + Expression(out e); + names.Add(tok); exprs.Add(e); + while (la.kind == 21) { + Get(); + Ident(out tok); + Expect(11); + Expression(out e); + } + names.Add(tok); exprs.Add(e); + } + s = new SkeletonStatement(dotdotdot, names, exprs); + } + void Rhs(out AssignmentRhs r, Expression receiverForInitCall) { IToken/*!*/ x, newToken; Expression/*!*/ e; List ee = null; @@ -1587,16 +1612,16 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = null; // to please compiler Attributes attrs = null; - if (la.kind == 57) { + if (la.kind == 58) { Get(); newToken = t; TypeAndToken(out x, out ty); - if (la.kind == 14 || la.kind == 23 || la.kind == 58) { - if (la.kind == 58) { + if (la.kind == 14 || la.kind == 23 || la.kind == 59) { + if (la.kind == 59) { Get(); ee = new List(); Expressions(ee); - Expect(59); + Expect(60); UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true); } else if (la.kind == 14) { @@ -1612,11 +1637,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else { Get(); var udf = ty as UserDefinedType; - if (udf != null && udf.ModuleName != null && udf.TypeArgs.Count == 0) { - // The parsed name had the form "A.B", so treat "A" as the name of the type and "B" as + if (udf != null && 0 < udf.Path.Count && udf.TypeArgs.Count == 0) { + // The parsed name had the form "A.B.Ctr", so treat "A.B" as the name of the type and "Ctr" as // the name of the constructor that's being invoked. x = udf.tok; - ty = new UserDefinedType(udf.ModuleName, udf.ModuleName.val, new List(), null); + ty = new UserDefinedType(udf.Path[0], udf.Path[udf.Path.Count-1].val, new List(), udf.Path.GetRange(0,udf.Path.Count-1)); } else { SemErr(t, "expected '.'"); x = null; @@ -1638,7 +1663,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = new TypeRhs(newToken, ty, initCall); } - } else if (la.kind == 60) { + } else if (la.kind == 61) { Get(); x = t; Expression(out e); @@ -1649,7 +1674,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(8)) { Expression(out e); r = new ExprRhs(e); - } else SynErr(156); + } else SynErr(158); while (la.kind == 6) { Attribute(ref attrs); } @@ -1661,16 +1686,16 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) { DottedIdentifiersAndFunction(out e); - while (la.kind == 14 || la.kind == 58) { + while (la.kind == 14 || la.kind == 59) { Suffix(ref e); } } else if (StartOf(14)) { ConstAtomExpression(out e); Suffix(ref e); - while (la.kind == 14 || la.kind == 58) { + while (la.kind == 14 || la.kind == 59) { Suffix(ref e); } - } else SynErr(157); + } else SynErr(159); } void Expressions(List/*!*/ args) { @@ -1693,7 +1718,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(8)) { Expression(out ee); e = ee; - } else SynErr(158); + } else SynErr(160); Expect(25); } @@ -1704,11 +1729,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List body; Expect(6); - while (la.kind == 63) { + while (la.kind == 64) { Get(); x = t; Expression(out e); - Expect(64); + Expect(65); body = new List(); while (StartOf(9)) { Stmt(body); @@ -1726,22 +1751,22 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod = null; while (StartOf(15)) { - if (la.kind == 33 || la.kind == 66) { + if (la.kind == 33 || la.kind == 67) { Invariant(out invariant); - while (!(la.kind == 0 || la.kind == 12)) {SynErr(159); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(161); Get();} Expect(12); invariants.Add(invariant); } else if (la.kind == 36) { - while (!(la.kind == 0 || la.kind == 36)) {SynErr(160); Get();} + while (!(la.kind == 0 || la.kind == 36)) {SynErr(162); Get();} Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, true); - while (!(la.kind == 0 || la.kind == 12)) {SynErr(161); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(163); Get();} Expect(12); } else { - while (!(la.kind == 0 || la.kind == 32)) {SynErr(162); Get();} + while (!(la.kind == 0 || la.kind == 32)) {SynErr(164); Get();} Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -1756,7 +1781,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 12)) {SynErr(163); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(165); Get();} Expect(12); } } @@ -1764,12 +1789,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Invariant(out MaybeFreeExpression/*!*/ invariant) { bool isFree = false; Expression/*!*/ e; List ids = new List(); invariant = null; Attributes attrs = null; - while (!(la.kind == 0 || la.kind == 33 || la.kind == 66)) {SynErr(164); Get();} + while (!(la.kind == 0 || la.kind == 33 || la.kind == 67)) {SynErr(166); Get();} if (la.kind == 33) { Get(); isFree = true; } - Expect(66); + Expect(67); while (IsAttribute()) { Attribute(ref attrs); } @@ -1784,7 +1809,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv; List body = new List(); - Expect(63); + Expect(64); x = t; Ident(out id); if (la.kind == 23) { @@ -1798,7 +1823,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(25); } - Expect(64); + Expect(65); while (StartOf(9)) { Stmt(body); } @@ -1813,7 +1838,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(8)) { Expression(out e); arg = new Attributes.Argument(t, e); - } else SynErr(165); + } else SynErr(167); } void QuantifierDomain(out List bvars, out Attributes attrs, out Expression range) { @@ -1841,7 +1866,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void EquivExpression(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; ImpliesExpression(out e0); - while (la.kind == 71 || la.kind == 72) { + while (la.kind == 72 || la.kind == 73) { EquivOp(); x = t; ImpliesExpression(out e1); @@ -1852,7 +1877,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ImpliesExpression(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; LogicalExpression(out e0); - if (la.kind == 73 || la.kind == 74) { + if (la.kind == 74 || la.kind == 75) { ImpliesOp(); x = t; ImpliesExpression(out e1); @@ -1861,23 +1886,23 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } void EquivOp() { - if (la.kind == 71) { + if (la.kind == 72) { Get(); - } else if (la.kind == 72) { + } else if (la.kind == 73) { Get(); - } else SynErr(166); + } else SynErr(168); } void LogicalExpression(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; RelationalExpression(out e0); if (StartOf(16)) { - if (la.kind == 75 || la.kind == 76) { + if (la.kind == 76 || la.kind == 77) { AndOp(); x = t; RelationalExpression(out e1); e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); - while (la.kind == 75 || la.kind == 76) { + while (la.kind == 76 || la.kind == 77) { AndOp(); x = t; RelationalExpression(out e1); @@ -1888,7 +1913,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; RelationalExpression(out e1); e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); - while (la.kind == 77 || la.kind == 78) { + while (la.kind == 78 || la.kind == 79) { OrOp(); x = t; RelationalExpression(out e1); @@ -1899,11 +1924,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } void ImpliesOp() { - if (la.kind == 73) { + if (la.kind == 74) { Get(); - } else if (la.kind == 74) { + } else if (la.kind == 75) { Get(); - } else SynErr(167); + } else SynErr(169); } void RelationalExpression(out Expression/*!*/ e) { @@ -1997,25 +2022,25 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } void AndOp() { - if (la.kind == 75) { + if (la.kind == 76) { Get(); - } else if (la.kind == 76) { + } else if (la.kind == 77) { Get(); - } else SynErr(168); + } else SynErr(170); } void OrOp() { - if (la.kind == 77) { + if (la.kind == 78) { Get(); - } else if (la.kind == 78) { + } else if (la.kind == 79) { Get(); - } else SynErr(169); + } else SynErr(171); } void Term(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; Factor(out e0); - while (la.kind == 88 || la.kind == 89) { + while (la.kind == 89 || la.kind == 90) { AddOp(out x, out op); Factor(out e1); e0 = new BinaryExpr(x, op, e0, e1); @@ -2043,35 +2068,35 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Gt; break; } - case 79: { + case 80: { Get(); x = t; op = BinaryExpr.Opcode.Le; break; } - case 80: { + case 81: { Get(); x = t; op = BinaryExpr.Opcode.Ge; break; } - case 81: { + case 82: { Get(); x = t; op = BinaryExpr.Opcode.Neq; break; } - case 82: { + case 83: { Get(); x = t; op = BinaryExpr.Opcode.Disjoint; break; } - case 83: { + case 84: { Get(); x = t; op = BinaryExpr.Opcode.In; break; } - case 84: { + case 85: { Get(); x = t; y = Token.NoToken; - if (la.kind == 83) { + if (la.kind == 84) { Get(); y = t; } @@ -2086,29 +2111,29 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break; } - case 85: { + case 86: { Get(); x = t; op = BinaryExpr.Opcode.Neq; break; } - case 86: { + case 87: { Get(); x = t; op = BinaryExpr.Opcode.Le; break; } - case 87: { + case 88: { Get(); x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(170); break; + default: SynErr(172); break; } } void Factor(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; UnaryExpression(out e0); - while (la.kind == 49 || la.kind == 90 || la.kind == 91) { + while (la.kind == 49 || la.kind == 91 || la.kind == 92) { MulOp(out x, out op); UnaryExpression(out e1); e0 = new BinaryExpr(x, op, e0, e1); @@ -2117,44 +2142,44 @@ List/*!*/ 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 == 88) { + if (la.kind == 89) { Get(); x = t; op = BinaryExpr.Opcode.Add; - } else if (la.kind == 89) { + } else if (la.kind == 90) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(171); + } else SynErr(173); } void UnaryExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; switch (la.kind) { - case 89: { + case 90: { Get(); x = t; UnaryExpression(out e); e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); break; } - case 84: case 92: { + case 85: case 93: { NegOp(); x = t; UnaryExpression(out e); e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); break; } - case 20: case 40: case 56: case 61: case 67: case 68: case 102: case 103: case 104: case 105: { + case 20: case 40: case 57: case 62: case 68: case 69: case 102: case 104: case 105: case 106: case 107: { EndlessExpression(out e); break; } case 1: { DottedIdentifiersAndFunction(out e); - while (la.kind == 14 || la.kind == 58) { + while (la.kind == 14 || la.kind == 59) { Suffix(ref e); } break; } - case 6: case 58: { + case 6: case 59: { DisplayExpr(out e); break; } @@ -2166,14 +2191,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo MapExpr(out e); break; } - case 2: case 19: case 23: case 93: case 94: case 95: case 96: case 97: case 98: case 99: { + case 2: case 19: case 23: case 94: case 95: case 96: case 97: case 98: case 99: case 100: { ConstAtomExpression(out e); - while (la.kind == 14 || la.kind == 58) { + while (la.kind == 14 || la.kind == 59) { Suffix(ref e); } break; } - default: SynErr(172); break; + default: SynErr(174); break; } } @@ -2182,47 +2207,45 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 49) { Get(); x = t; op = BinaryExpr.Opcode.Mul; - } else if (la.kind == 90) { + } else if (la.kind == 91) { Get(); x = t; op = BinaryExpr.Opcode.Div; - } else if (la.kind == 91) { + } else if (la.kind == 92) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(173); + } else SynErr(175); } void NegOp() { - if (la.kind == 84) { + if (la.kind == 85) { Get(); - } else if (la.kind == 92) { + } else if (la.kind == 93) { Get(); - } else SynErr(174); + } else SynErr(176); } void EndlessExpression(out Expression e) { IToken/*!*/ x; Expression e0, e1; e = dummyExpr; - BoundVar d; - List letVars; List letRHSs; switch (la.kind) { - case 61: { + case 62: { Get(); x = t; Expression(out e); - Expect(100); + Expect(101); Expression(out e0); - Expect(62); + Expect(63); Expression(out e1); e = new ITEExpr(x, e, e0, e1); break; } - case 67: { + case 68: { MatchExpression(out e); break; } - case 102: case 103: case 104: case 105: { + case 104: case 105: case 106: case 107: { QuantifierGuts(out e); break; } @@ -2230,7 +2253,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ComprehensionExpr(out e); break; } - case 68: { + case 69: { Get(); x = t; Expression(out e0); @@ -2239,7 +2262,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new AssertExpr(x, e0, e1); break; } - case 56: { + case 57: { Get(); x = t; Expression(out e0); @@ -2249,31 +2272,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break; } case 20: { - Get(); - x = t; - letVars = new List(); - letRHSs = new List(); - IdentTypeOptional(out d); - letVars.Add(d); - while (la.kind == 21) { - Get(); - IdentTypeOptional(out d); - letVars.Add(d); - } - Expect(54); - Expression(out e); - letRHSs.Add(e); - while (la.kind == 21) { - Get(); - Expression(out e); - letRHSs.Add(e); - } - Expect(12); - Expression(out e); - e = new LetExpr(x, letVars, letRHSs, e); + LetExpr(out e); break; } - default: SynErr(175); break; + case 102: { + NamedExpr(out e); + break; + } + default: SynErr(177); break; } } @@ -2319,24 +2325,24 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new FunctionCallExpr(id, id.val, e, openParen, args); } if (!func) { e = new ExprDotName(id, e, id.val); } - } else if (la.kind == 58) { + } else if (la.kind == 59) { Get(); x = t; if (StartOf(8)) { Expression(out ee); e0 = ee; - if (la.kind == 101) { + if (la.kind == 103) { Get(); anyDots = true; if (StartOf(8)) { Expression(out ee); e1 = ee; } - } else if (la.kind == 54) { + } else if (la.kind == 55) { Get(); Expression(out ee); e1 = ee; - } else if (la.kind == 21 || la.kind == 59) { + } else if (la.kind == 21 || la.kind == 60) { while (la.kind == 21) { Get(); Expression(out ee); @@ -2347,15 +2353,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee); } - } else SynErr(176); - } else if (la.kind == 101) { + } else SynErr(178); + } else if (la.kind == 103) { Get(); anyDots = true; if (StartOf(8)) { Expression(out ee); e1 = ee; } - } else SynErr(177); + } else SynErr(179); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -2378,8 +2384,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } - Expect(59); - } else SynErr(178); + Expect(60); + } else SynErr(180); } void DisplayExpr(out Expression e) { @@ -2395,15 +2401,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } e = new SetDisplayExpr(x, elements); Expect(7); - } else if (la.kind == 58) { + } else if (la.kind == 59) { Get(); x = t; elements = new List(); if (StartOf(8)) { Expressions(elements); } e = new SeqDisplayExpr(x, elements); - Expect(59); - } else SynErr(179); + Expect(60); + } else SynErr(181); } void MultiSetExpr(out Expression e) { @@ -2429,7 +2435,7 @@ List/*!*/ 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(180); + } else SynErr(182); } void MapExpr(out Expression e) { @@ -2440,14 +2446,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(43); x = t; - if (la.kind == 58) { + if (la.kind == 59) { Get(); elements = new List(); if (StartOf(8)) { MapLiteralExpressions(out elements); } e = new MapDisplayExpr(x, elements); - Expect(59); + Expect(60); } else if (la.kind == 1) { BoundVar/*!*/ bv; List bvars = new List(); @@ -2463,7 +2469,7 @@ List/*!*/ 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(181); + } else SynErr(183); } void ConstAtomExpression(out Expression/*!*/ e) { @@ -2472,17 +2478,17 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr; switch (la.kind) { - case 93: { + case 94: { Get(); e = new LiteralExpr(t, false); break; } - case 94: { + case 95: { Get(); e = new LiteralExpr(t, true); break; } - case 95: { + case 96: { Get(); e = new LiteralExpr(t); break; @@ -2492,12 +2498,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LiteralExpr(t, n); break; } - case 96: { + case 97: { Get(); e = new ThisExpr(t); break; } - case 97: { + case 98: { Get(); x = t; Expect(23); @@ -2506,7 +2512,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new FreshExpr(x, e); break; } - case 98: { + case 99: { Get(); x = t; Expect(23); @@ -2515,7 +2521,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new AllocatedExpr(x, e); break; } - case 99: { + case 100: { Get(); x = t; Expect(23); @@ -2540,7 +2546,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(25); break; } - default: SynErr(182); break; + default: SynErr(184); break; } } @@ -2559,34 +2565,34 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ d, r; elements = new List(); Expression(out d); - Expect(54); + Expect(55); Expression(out r); elements.Add(new ExpressionPair(d,r)); while (la.kind == 21) { Get(); Expression(out d); - Expect(54); + Expect(55); Expression(out r); elements.Add(new ExpressionPair(d,r)); } } void QSep() { - if (la.kind == 106) { + if (la.kind == 108) { Get(); - } else if (la.kind == 107) { + } else if (la.kind == 109) { Get(); - } else SynErr(183); + } else SynErr(185); } void MatchExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c; List cases = new List(); - Expect(67); + Expect(68); x = t; Expression(out e); - while (la.kind == 63) { + while (la.kind == 64) { CaseExpression(out c); cases.Add(c); } @@ -2601,13 +2607,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression range; Expression/*!*/ body; - if (la.kind == 102 || la.kind == 103) { + if (la.kind == 104 || la.kind == 105) { Forall(); x = t; univ = true; - } else if (la.kind == 104 || la.kind == 105) { + } else if (la.kind == 106 || la.kind == 107) { Exists(); x = t; - } else SynErr(184); + } else SynErr(186); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body); @@ -2638,7 +2644,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(19); Expression(out range); - if (la.kind == 106 || la.kind == 107) { + if (la.kind == 108 || la.kind == 109) { QSep(); Expression(out body); } @@ -2647,13 +2653,57 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } + void LetExpr(out Expression e) { + IToken/*!*/ x; + e = dummyExpr; + BoundVar d; + List letVars; List letRHSs; + + Expect(20); + x = t; + letVars = new List(); + letRHSs = new List(); + IdentTypeOptional(out d); + letVars.Add(d); + while (la.kind == 21) { + Get(); + IdentTypeOptional(out d); + letVars.Add(d); + } + Expect(55); + Expression(out e); + letRHSs.Add(e); + while (la.kind == 21) { + Get(); + Expression(out e); + letRHSs.Add(e); + } + Expect(12); + Expression(out e); + e = new LetExpr(x, letVars, letRHSs, e); + } + + void NamedExpr(out Expression e) { + IToken/*!*/ x, d; + e = dummyExpr; + Expression expr; + + Expect(102); + x = t; + NoUSIdent(out d); + Expect(5); + Expression(out e); + expr = e; + e = new NamedExpr(x, d.val, expr); + } + void CaseExpression(out MatchCaseExpr/*!*/ c) { Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id; List arguments = new List(); BoundVar/*!*/ bv; Expression/*!*/ body; - Expect(63); + Expect(64); x = t; Ident(out id); if (la.kind == 23) { @@ -2667,25 +2717,25 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(25); } - Expect(64); + Expect(65); Expression(out body); c = new MatchCaseExpr(x, id.val, arguments, body); } void Forall() { - if (la.kind == 102) { + if (la.kind == 104) { Get(); - } else if (la.kind == 103) { + } else if (la.kind == 105) { Get(); - } else SynErr(185); + } else SynErr(187); } void Exists() { - if (la.kind == 104) { + if (la.kind == 106) { Get(); - } else if (la.kind == 105) { + } else if (la.kind == 107) { Get(); - } else SynErr(186); + } else SynErr(188); } void AttributeBody(ref Attributes attrs) { @@ -2721,26 +2771,26 @@ List/*!*/ 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,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, 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, 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}, - {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,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, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,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}, - {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,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, 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,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,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, 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,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,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,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,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,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,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,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,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,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,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, 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} }; } // end Parser @@ -2818,140 +2868,142 @@ public class Errors { case 50: s = "\"`\" expected"; break; case 51: s = "\"label\" expected"; break; case 52: s = "\"break\" expected"; break; - case 53: s = "\"return\" expected"; break; - case 54: s = "\":=\" expected"; break; - case 55: s = "\":|\" expected"; break; - case 56: s = "\"assume\" expected"; break; - case 57: s = "\"new\" expected"; break; - case 58: s = "\"[\" expected"; break; - case 59: s = "\"]\" expected"; break; - case 60: s = "\"choose\" expected"; break; - case 61: s = "\"if\" expected"; break; - case 62: s = "\"else\" expected"; break; - case 63: s = "\"case\" expected"; break; - case 64: s = "\"=>\" expected"; break; - case 65: s = "\"while\" expected"; break; - case 66: s = "\"invariant\" expected"; break; - case 67: s = "\"match\" expected"; break; - case 68: s = "\"assert\" expected"; break; - case 69: s = "\"print\" expected"; break; - case 70: s = "\"parallel\" expected"; break; - case 71: s = "\"<==>\" expected"; break; - case 72: s = "\"\\u21d4\" expected"; break; - case 73: s = "\"==>\" expected"; break; - case 74: s = "\"\\u21d2\" expected"; break; - case 75: s = "\"&&\" expected"; break; - case 76: s = "\"\\u2227\" expected"; break; - case 77: s = "\"||\" expected"; break; - case 78: s = "\"\\u2228\" expected"; break; - case 79: s = "\"<=\" expected"; break; - case 80: s = "\">=\" expected"; break; - case 81: s = "\"!=\" expected"; break; - case 82: s = "\"!!\" expected"; break; - case 83: s = "\"in\" expected"; break; - case 84: s = "\"!\" expected"; break; - case 85: s = "\"\\u2260\" expected"; break; - case 86: s = "\"\\u2264\" expected"; break; - case 87: s = "\"\\u2265\" expected"; break; - case 88: s = "\"+\" expected"; break; - case 89: s = "\"-\" expected"; break; - case 90: s = "\"/\" expected"; break; - case 91: s = "\"%\" expected"; break; - case 92: s = "\"\\u00ac\" expected"; break; - case 93: s = "\"false\" expected"; break; - case 94: s = "\"true\" expected"; break; - case 95: s = "\"null\" expected"; break; - case 96: s = "\"this\" expected"; break; - case 97: s = "\"fresh\" expected"; break; - case 98: s = "\"allocated\" expected"; break; - case 99: s = "\"old\" expected"; break; - case 100: s = "\"then\" expected"; break; - case 101: s = "\"..\" expected"; break; - case 102: s = "\"forall\" expected"; break; - case 103: s = "\"\\u2200\" expected"; break; - case 104: s = "\"exists\" expected"; break; - case 105: s = "\"\\u2203\" expected"; break; - case 106: s = "\"::\" expected"; break; - case 107: s = "\"\\u2022\" expected"; break; - case 108: s = "??? expected"; break; - case 109: s = "invalid Dafny"; break; - case 110: s = "invalid SubModuleDecl"; break; - case 111: s = "invalid SubModuleDecl"; break; - case 112: s = "this symbol not expected in ClassDecl"; break; - case 113: s = "this symbol not expected in DatatypeDecl"; break; - case 114: s = "invalid DatatypeDecl"; break; + case 53: s = "\"where\" expected"; break; + case 54: s = "\"return\" expected"; break; + case 55: s = "\":=\" expected"; break; + case 56: s = "\":|\" expected"; break; + case 57: s = "\"assume\" expected"; break; + case 58: s = "\"new\" expected"; break; + case 59: s = "\"[\" expected"; break; + case 60: s = "\"]\" expected"; break; + case 61: s = "\"choose\" expected"; break; + case 62: s = "\"if\" expected"; break; + case 63: s = "\"else\" expected"; break; + case 64: s = "\"case\" expected"; break; + case 65: s = "\"=>\" expected"; break; + case 66: s = "\"while\" expected"; break; + case 67: s = "\"invariant\" expected"; break; + case 68: s = "\"match\" expected"; break; + case 69: s = "\"assert\" expected"; break; + case 70: s = "\"print\" expected"; break; + case 71: s = "\"parallel\" expected"; break; + case 72: s = "\"<==>\" expected"; break; + case 73: s = "\"\\u21d4\" expected"; break; + case 74: s = "\"==>\" expected"; break; + case 75: s = "\"\\u21d2\" expected"; break; + case 76: s = "\"&&\" expected"; break; + case 77: s = "\"\\u2227\" expected"; break; + case 78: s = "\"||\" expected"; break; + case 79: s = "\"\\u2228\" expected"; break; + case 80: s = "\"<=\" expected"; break; + case 81: s = "\">=\" expected"; break; + case 82: s = "\"!=\" expected"; break; + case 83: s = "\"!!\" expected"; break; + case 84: s = "\"in\" expected"; break; + case 85: s = "\"!\" expected"; break; + case 86: s = "\"\\u2260\" expected"; break; + case 87: s = "\"\\u2264\" expected"; break; + case 88: s = "\"\\u2265\" expected"; break; + case 89: s = "\"+\" expected"; break; + case 90: s = "\"-\" expected"; break; + case 91: s = "\"/\" expected"; break; + case 92: s = "\"%\" expected"; break; + case 93: s = "\"\\u00ac\" expected"; break; + case 94: s = "\"false\" expected"; break; + case 95: s = "\"true\" expected"; break; + case 96: s = "\"null\" expected"; break; + case 97: s = "\"this\" expected"; break; + case 98: s = "\"fresh\" expected"; break; + 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 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 = "this symbol not expected in ArbitraryTypeDecl"; break; - case 117: s = "invalid ClassMemberDecl"; break; - case 118: s = "this symbol not expected in FieldDecl"; break; - case 119: s = "this symbol not expected in FieldDecl"; break; - case 120: s = "invalid FunctionDecl"; break; - case 121: s = "invalid FunctionDecl"; 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 120: s = "this symbol not expected in FieldDecl"; break; + case 121: s = "this symbol not expected in FieldDecl"; break; case 122: s = "invalid FunctionDecl"; break; case 123: s = "invalid FunctionDecl"; break; - case 124: s = "this symbol not expected in MethodDecl"; break; - case 125: s = "invalid MethodDecl"; break; - case 126: s = "invalid MethodDecl"; break; - case 127: s = "invalid TypeAndToken"; break; - case 128: s = "this symbol not expected in MethodSpec"; break; - case 129: s = "this symbol not expected in MethodSpec"; break; + case 124: s = "invalid FunctionDecl"; break; + case 125: s = "invalid FunctionDecl"; break; + case 126: s = "this symbol not expected in MethodDecl"; break; + case 127: s = "invalid MethodDecl"; break; + case 128: s = "invalid MethodDecl"; break; + case 129: s = "invalid TypeAndToken"; break; case 130: s = "this symbol not expected in MethodSpec"; break; case 131: s = "this symbol not expected in MethodSpec"; break; - case 132: s = "invalid 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 = "invalid ReferenceType"; break; - case 136: s = "this symbol not expected in FunctionSpec"; break; - case 137: s = "this symbol not expected in FunctionSpec"; break; + case 135: s = "this symbol not expected in MethodSpec"; break; + case 136: s = "invalid MethodSpec"; break; + case 137: s = "invalid ReferenceType"; 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 = "invalid FunctionSpec"; break; - case 142: s = "invalid PossiblyWildFrameExpression"; break; - case 143: s = "invalid PossiblyWildExpression"; break; - case 144: s = "this symbol not expected in OneStmt"; break; - case 145: s = "invalid OneStmt"; 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 = "invalid AssertStmt"; break; - case 149: s = "invalid AssumeStmt"; break; - case 150: s = "invalid UpdateStmt"; break; - case 151: s = "invalid UpdateStmt"; break; - case 152: s = "invalid IfStmt"; break; - case 153: s = "invalid IfStmt"; break; - case 154: s = "invalid WhileStmt"; break; - case 155: s = "invalid WhileStmt"; break; - case 156: s = "invalid Rhs"; break; - case 157: s = "invalid Lhs"; break; - case 158: s = "invalid Guard"; break; - case 159: s = "this symbol not expected in LoopSpec"; break; - case 160: s = "this symbol not expected in LoopSpec"; 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 152: s = "invalid UpdateStmt"; break; + case 153: s = "invalid UpdateStmt"; break; + case 154: s = "invalid IfStmt"; break; + case 155: s = "invalid IfStmt"; 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 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 Invariant"; break; - case 165: s = "invalid AttributeArg"; break; - case 166: s = "invalid EquivOp"; break; - case 167: s = "invalid ImpliesOp"; break; - case 168: s = "invalid AndOp"; break; - case 169: s = "invalid OrOp"; break; - case 170: s = "invalid RelOp"; break; - case 171: s = "invalid AddOp"; break; - case 172: s = "invalid UnaryExpression"; break; - case 173: s = "invalid MulOp"; break; - case 174: s = "invalid NegOp"; break; - case 175: s = "invalid EndlessExpression"; break; - case 176: s = "invalid Suffix"; break; - case 177: s = "invalid Suffix"; 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 178: s = "invalid Suffix"; break; - case 179: s = "invalid DisplayExpr"; break; - case 180: s = "invalid MultiSetExpr"; break; - case 181: s = "invalid MapExpr"; break; - case 182: s = "invalid ConstAtomExpression"; break; - case 183: s = "invalid QSep"; break; - case 184: s = "invalid QuantifierGuts"; break; - case 185: s = "invalid Forall"; break; - case 186: s = "invalid Exists"; 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; default: s = "error " + n; break; } diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index e2d1b438..1bfa80a0 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 = 108; - const int noSym = 108; + const int maxT = 110; + const int noSym = 110; [ContractInvariantMethod] @@ -520,30 +520,32 @@ public class Scanner { case "reads": t.kind = 48; break; case "label": t.kind = 51; break; case "break": t.kind = 52; break; - case "return": t.kind = 53; break; - case "assume": t.kind = 56; break; - case "new": t.kind = 57; break; - case "choose": t.kind = 60; break; - case "if": t.kind = 61; break; - case "else": t.kind = 62; break; - case "case": t.kind = 63; break; - case "while": t.kind = 65; break; - case "invariant": t.kind = 66; break; - case "match": t.kind = 67; break; - case "assert": t.kind = 68; break; - case "print": t.kind = 69; break; - case "parallel": t.kind = 70; break; - case "in": t.kind = 83; break; - case "false": t.kind = 93; break; - case "true": t.kind = 94; break; - case "null": t.kind = 95; break; - case "this": t.kind = 96; break; - case "fresh": t.kind = 97; break; - case "allocated": t.kind = 98; break; - case "old": t.kind = 99; break; - case "then": t.kind = 100; break; - case "forall": t.kind = 102; break; - case "exists": t.kind = 104; break; + case "where": t.kind = 53; break; + case "return": t.kind = 54; break; + case "assume": t.kind = 57; break; + case "new": t.kind = 58; break; + case "choose": t.kind = 61; break; + case "if": t.kind = 62; break; + case "else": t.kind = 63; break; + case "case": t.kind = 64; break; + case "while": t.kind = 66; break; + case "invariant": t.kind = 67; break; + case "match": t.kind = 68; break; + case "assert": t.kind = 69; break; + case "print": t.kind = 70; break; + case "parallel": t.kind = 71; break; + case "in": t.kind = 84; break; + case "false": t.kind = 94; break; + case "true": t.kind = 95; break; + case "null": t.kind = 96; break; + case "this": t.kind = 97; break; + case "fresh": t.kind = 98; break; + 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; default: break; } } @@ -663,67 +665,67 @@ public class Scanner { case 25: {t.kind = 50; break;} case 26: - {t.kind = 54; break;} - case 27: {t.kind = 55; break;} + case 27: + {t.kind = 56; break;} case 28: - {t.kind = 58; break;} - case 29: {t.kind = 59; break;} + case 29: + {t.kind = 60; break;} case 30: - {t.kind = 64; break;} + {t.kind = 65; break;} case 31: if (ch == '>') {AddCh(); goto case 32;} else {goto case 0;} case 32: - {t.kind = 71; break;} - case 33: {t.kind = 72; break;} - case 34: + case 33: {t.kind = 73; break;} - case 35: + case 34: {t.kind = 74; break;} + case 35: + {t.kind = 75; break;} case 36: if (ch == '&') {AddCh(); goto case 37;} else {goto case 0;} case 37: - {t.kind = 75; break;} - case 38: {t.kind = 76; break;} - case 39: + case 38: {t.kind = 77; break;} - case 40: + case 39: {t.kind = 78; break;} + case 40: + {t.kind = 79; break;} case 41: - {t.kind = 80; break;} - case 42: {t.kind = 81; break;} - case 43: + case 42: {t.kind = 82; break;} + case 43: + {t.kind = 83; break;} case 44: - {t.kind = 85; break;} - case 45: {t.kind = 86; break;} - case 46: + case 45: {t.kind = 87; break;} - case 47: + case 46: {t.kind = 88; break;} - case 48: + case 47: {t.kind = 89; break;} - case 49: + case 48: {t.kind = 90; break;} - case 50: + case 49: {t.kind = 91; break;} - case 51: + case 50: {t.kind = 92; break;} + case 51: + {t.kind = 93; break;} case 52: - {t.kind = 103; break;} - case 53: {t.kind = 105; break;} + case 53: + {t.kind = 107; break;} case 54: - {t.kind = 106; break;} + {t.kind = 108; break;} case 55: - {t.kind = 107; break;} + {t.kind = 109; break;} case 56: recEnd = pos; recKind = 5; if (ch == '=') {AddCh(); goto case 26;} @@ -752,22 +754,22 @@ public class Scanner { if (ch == '=') {AddCh(); goto case 41;} else {t.kind = 27; break;} case 62: - recEnd = pos; recKind = 84; + recEnd = pos; recKind = 85; if (ch == '=') {AddCh(); goto case 42;} else if (ch == '!') {AddCh(); goto case 43;} - else {t.kind = 84; break;} + else {t.kind = 85; break;} case 63: recEnd = pos; recKind = 24; if (ch == '>') {AddCh(); goto case 34;} else {t.kind = 24; break;} case 64: - recEnd = pos; recKind = 101; + recEnd = pos; recKind = 103; if (ch == '.') {AddCh(); goto case 23;} - else {t.kind = 101; break;} + else {t.kind = 103; break;} case 65: - recEnd = pos; recKind = 79; + recEnd = pos; recKind = 80; if (ch == '=') {AddCh(); goto case 31;} - else {t.kind = 79; break;} + else {t.kind = 80; break;} } t.val = new String(tval, 0, tlen); -- cgit v1.2.3