From e07d86d6cc4423703dbfb479f09b44c80f877ef9 Mon Sep 17 00:00:00 2001 From: leino Date: Sat, 3 Oct 2015 02:40:41 -0700 Subject: Parsing and pretty printing of the new "existential guards" of the two kinds of "if" statements. --- Source/Dafny/Cloner.cs | 4 +- Source/Dafny/Dafny.atg | 64 +- Source/Dafny/DafnyAst.cs | 12 +- Source/Dafny/Parser.cs | 1268 ++++++++++++++++-------------- Source/Dafny/Printer.cs | 60 +- Source/Dafny/RefinementTransformer.cs | 8 +- Source/Dafny/Resolver.cs | 2 +- Source/Dafny/Rewriter.cs | 2 +- Source/Dafny/Scanner.cs | 264 +++---- Source/Dafny/Translator.cs | 4 +- Test/dafny0/ExistentialGuards.dfy | 89 +++ Test/dafny0/ExistentialGuards.dfy.expect | 94 +++ Test/dafny0/Simple.dfy | 27 + Test/dafny0/Simple.dfy.expect | 29 + 14 files changed, 1137 insertions(+), 790 deletions(-) create mode 100644 Test/dafny0/ExistentialGuards.dfy create mode 100644 Test/dafny0/ExistentialGuards.dfy.expect diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 45d8a2c9..9a93a340 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -531,7 +531,7 @@ namespace Microsoft.Dafny } else if (stmt is IfStmt) { var s = (IfStmt)stmt; - r = new IfStmt(Tok(s.Tok), Tok(s.EndTok), CloneExpr(s.Guard), CloneBlockStmt(s.Thn), CloneStmt(s.Els)); + r = new IfStmt(Tok(s.Tok), Tok(s.EndTok), s.IsExistentialGuard, CloneExpr(s.Guard), CloneBlockStmt(s.Thn), CloneStmt(s.Els)); } else if (stmt is AlternativeStmt) { var s = (AlternativeStmt)stmt; @@ -631,7 +631,7 @@ namespace Microsoft.Dafny } public GuardedAlternative CloneGuardedAlternative(GuardedAlternative alt) { - return new GuardedAlternative(Tok(alt.Tok), CloneExpr(alt.Guard), alt.Body.ConvertAll(CloneStmt)); + return new GuardedAlternative(Tok(alt.Tok), alt.IsExistentialGuard, CloneExpr(alt.Guard), alt.Body.ConvertAll(CloneStmt)); } public Function CloneFunction(Function f, string newName = null) { diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 954448af..66dff8a2 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -104,6 +104,25 @@ bool IsAlternative() { return la.kind == _lbrace && x.kind == _case; } +// an existential guard starts with an identifier and is then followed by +// * a colon (if the first identifier is given an explicit type), +// * a comma (if there's a list a bound variables and the first one is not given an explicit type), +// * a start-attribute (if there's one bound variable and it is not given an explicit type and there are attributes), or +// * a bored smiley (if there's one bound variable and it is not given an explicit type). +bool IsExistentialGuard() { + scanner.ResetPeek(); + if (la.kind == _ident) { + Token x = scanner.Peek(); + if (x.kind == _colon || x.kind == _comma || x.kind == _boredSmiley) { + return true; + } else if (x.kind == _lbrace) { + x = scanner.Peek(); + return x.kind == _colon; + } + } + return false; +} + bool IsLoopSpec() { return la.kind == _invariant | la.kind == _decreases | la.kind == _modifies; } @@ -456,6 +475,7 @@ TOKENS comma = ','. verticalbar = '|'. doublecolon = "::". + boredSmiley = ":|". bullet = '\u2022'. dot = '.'. semi = ';'. @@ -1651,7 +1671,7 @@ VarDeclStatement<.out Statement/*!*/ s.> . IfStmt = (. Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x; - Expression guard = null; IToken guardEllipsis = null; + Expression guard = null; IToken guardEllipsis = null; bool isExistentialGuard = false; BlockStmt/*!*/ thn; BlockStmt/*!*/ bs; Statement/*!*/ s; @@ -1663,11 +1683,13 @@ IfStmt "if" (. x = t; .) ( IF(IsAlternative()) - AlternativeBlock + AlternativeBlock (. ifStmt = new AlternativeStmt(x, endTok, alternatives); .) | - ( Guard - | "..." (. guardEllipsis = t; .) + ( IF(IsExistentialGuard()) + ExistentialGuard (. isExistentialGuard = true; .) + | Guard + | "..." (. guardEllipsis = t; .) ) BlockStmt (. endTok = thn.EndTok; .) [ "else" @@ -1676,26 +1698,29 @@ IfStmt ) ] (. if (guardEllipsis != null) { - ifStmt = new SkeletonStatement(new IfStmt(x, endTok, guard, thn, els), guardEllipsis, null); + ifStmt = new SkeletonStatement(new IfStmt(x, endTok, isExistentialGuard, guard, thn, els), guardEllipsis, null); } else { - ifStmt = new IfStmt(x, endTok, guard, thn, els); + ifStmt = new IfStmt(x, endTok, isExistentialGuard, guard, thn, els); } .) ) . -AlternativeBlock<.out List alternatives, out IToken endTok.> +AlternativeBlock<.bool allowExistentialGuards, out List alternatives, out IToken endTok.> = (. alternatives = new List(); IToken x; - Expression e; + Expression e; bool isExistentialGuard; List body; .) "{" - { "case" (. x = t; .) - Expression // NB: don't allow lambda here + { "case" (. x = t; isExistentialGuard = false; e = dummyExpr; .) + ( IF(allowExistentialGuards && IsExistentialGuard()) + ExistentialGuard (. isExistentialGuard = true; .) // NB: don't allow lambda here + | Expression // NB: don't allow lambda here + ) "=>" (. body = new List(); .) { Stmt } - (. alternatives.Add(new GuardedAlternative(x, e, body)); .) + (. alternatives.Add(new GuardedAlternative(x, isExistentialGuard, e, body)); .) } "}" (. endTok = t; .) . @@ -1719,7 +1744,7 @@ WhileStmt ( IF(IsLoopSpec() || IsAlternative()) { LoopSpec } - AlternativeBlock + AlternativeBlock (. stmt = new AlternativeLoopStmt(x, endTok, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), alternatives); .) | ( Guard (. Contract.Assume(guard == null || cce.Owner.None(guard)); .) @@ -1799,6 +1824,21 @@ Guard /* null represents demonic-choice */ | Expression (. e = ee; .) ) . +ExistentialGuard += (. var bvars = new List(); + BoundVar bv; IToken x; + Attributes attrs = null; + Expression body; + .) + IdentTypeOptional (. bvars.Add(bv); x = bv.tok; .) + { "," + IdentTypeOptional (. bvars.Add(bv); .) + } + { Attribute } + ":|" + Expression + (. e = new ExistsExpr(x, bvars, null, body, attrs); .) + . MatchStmt = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c; diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 4fc48f2f..64af1425 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4411,20 +4411,24 @@ namespace Microsoft.Dafny { } public class IfStmt : Statement { + public readonly bool IsExistentialGuard; public readonly Expression Guard; public readonly BlockStmt Thn; public readonly Statement Els; [ContractInvariantMethod] void ObjectInvariant() { + Contract.Invariant(!IsExistentialGuard || (Guard is ExistsExpr && ((ExistsExpr)Guard).Range == null)); Contract.Invariant(Thn != null); Contract.Invariant(Els == null || Els is BlockStmt || Els is IfStmt || Els is SkeletonStatement); } - public IfStmt(IToken tok, IToken endTok, Expression guard, BlockStmt thn, Statement els) + public IfStmt(IToken tok, IToken endTok, bool isExistentialGuard, Expression guard, BlockStmt thn, Statement els) : base(tok, endTok) { Contract.Requires(tok != null); Contract.Requires(endTok != null); + Contract.Requires(!isExistentialGuard || (guard is ExistsExpr && ((ExistsExpr)guard).Range == null)); Contract.Requires(thn != null); Contract.Requires(els == null || els is BlockStmt || els is IfStmt || els is SkeletonStatement); + this.IsExistentialGuard = isExistentialGuard; this.Guard = guard; this.Thn = thn; this.Els = els; @@ -4450,20 +4454,24 @@ namespace Microsoft.Dafny { public class GuardedAlternative { public readonly IToken Tok; + public readonly bool IsExistentialGuard; public readonly Expression Guard; public readonly List Body; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Tok != null); Contract.Invariant(Guard != null); + Contract.Invariant(!IsExistentialGuard || (Guard is ExistsExpr && ((ExistsExpr)Guard).Range == null)); Contract.Invariant(Body != null); } - public GuardedAlternative(IToken tok, Expression guard, List body) + public GuardedAlternative(IToken tok, bool isExistentialGuard, Expression guard, List body) { Contract.Requires(tok != null); Contract.Requires(guard != null); + Contract.Requires(!isExistentialGuard || (guard is ExistsExpr && ((ExistsExpr)guard).Range == null)); Contract.Requires(body != null); this.Tok = tok; + this.IsExistentialGuard = isExistentialGuard; this.Guard = guard; this.Body = body; } diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 7dafb572..c79c1051 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -38,40 +38,41 @@ public class Parser { public const int _comma = 22; public const int _verticalbar = 23; public const int _doublecolon = 24; - public const int _bullet = 25; - public const int _dot = 26; - public const int _semi = 27; - public const int _darrow = 28; - public const int _arrow = 29; - public const int _assume = 30; - public const int _calc = 31; - public const int _case = 32; - public const int _then = 33; - public const int _else = 34; - public const int _decreases = 35; - public const int _invariant = 36; - public const int _function = 37; - public const int _predicate = 38; - public const int _inductive = 39; - public const int _lemma = 40; - public const int _copredicate = 41; - public const int _modifies = 42; - public const int _reads = 43; - public const int _requires = 44; - public const int _lbrace = 45; - public const int _rbrace = 46; - public const int _lbracket = 47; - public const int _rbracket = 48; - public const int _openparen = 49; - public const int _closeparen = 50; - public const int _openAngleBracket = 51; - public const int _closeAngleBracket = 52; - public const int _eq = 53; - public const int _neq = 54; - public const int _neqAlt = 55; - public const int _star = 56; - public const int _notIn = 57; - public const int _ellipsis = 58; + public const int _boredSmiley = 25; + public const int _bullet = 26; + public const int _dot = 27; + public const int _semi = 28; + public const int _darrow = 29; + public const int _arrow = 30; + public const int _assume = 31; + public const int _calc = 32; + public const int _case = 33; + public const int _then = 34; + public const int _else = 35; + public const int _decreases = 36; + public const int _invariant = 37; + public const int _function = 38; + public const int _predicate = 39; + public const int _inductive = 40; + public const int _lemma = 41; + public const int _copredicate = 42; + public const int _modifies = 43; + public const int _reads = 44; + public const int _requires = 45; + public const int _lbrace = 46; + public const int _rbrace = 47; + public const int _lbracket = 48; + public const int _rbracket = 49; + public const int _openparen = 50; + public const int _closeparen = 51; + public const int _openAngleBracket = 52; + public const int _closeAngleBracket = 53; + public const int _eq = 54; + public const int _neq = 55; + public const int _neqAlt = 56; + public const int _star = 57; + public const int _notIn = 58; + public const int _ellipsis = 59; public const int maxT = 138; const bool _T = true; @@ -175,6 +176,25 @@ bool IsAlternative() { return la.kind == _lbrace && x.kind == _case; } +// an existential guard starts with an identifier and is then followed by +// * a colon (if the first identifier is given an explicit type), +// * a comma (if there's a list a bound variables and the first one is not given an explicit type), +// * a start-attribute (if there's one bound variable and it is not given an explicit type and there are attributes), or +// * a bored smiley (if there's one bound variable and it is not given an explicit type). +bool IsExistentialGuard() { + scanner.ResetPeek(); + if (la.kind == _ident) { + Token x = scanner.Peek(); + if (x.kind == _colon || x.kind == _comma || x.kind == _boredSmiley) { + return true; + } else if (x.kind == _lbrace) { + x = scanner.Peek(); + return x.kind == _colon; + } + } + return false; +} + bool IsLoopSpec() { return la.kind == _invariant | la.kind == _decreases | la.kind == _modifies; } @@ -532,7 +552,7 @@ bool IsType(ref IToken pt) { TraitDecl/*!*/ trait; Contract.Assert(defaultModule != null); - while (la.kind == 59) { + while (la.kind == 60) { Get(); Expect(20); { @@ -552,42 +572,42 @@ bool IsType(ref IToken pt) { } while (StartOf(1)) { switch (la.kind) { - case 60: case 61: case 64: { + case 61: case 62: case 65: { SubModuleDecl(defaultModule, out submodule); defaultModule.TopLevelDecls.Add(submodule); break; } - case 69: { + case 70: { ClassDecl(defaultModule, out c); defaultModule.TopLevelDecls.Add(c); break; } - case 75: case 76: { + case 76: case 77: { DatatypeDecl(defaultModule, out dt); defaultModule.TopLevelDecls.Add(dt); break; } - case 78: { + case 79: { NewtypeDecl(defaultModule, out td); defaultModule.TopLevelDecls.Add(td); break; } - case 79: { + case 80: { OtherTypeDecl(defaultModule, out td); defaultModule.TopLevelDecls.Add(td); break; } - case 80: { + case 81: { IteratorDecl(defaultModule, out iter); defaultModule.TopLevelDecls.Add(iter); break; } - case 71: { + case 72: { TraitDecl(defaultModule, out trait); defaultModule.TopLevelDecls.Add(trait); break; } - case 37: case 38: case 39: case 40: case 41: case 72: case 73: case 74: case 77: case 83: case 84: case 85: case 86: { + case 38: case 39: case 40: case 41: case 42: case 73: case 74: case 75: case 78: case 84: case 85: case 86: case 87: { ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals, false); break; } @@ -621,20 +641,20 @@ bool IsType(ref IToken pt) { bool isExclusively = false; bool opened = false; - if (la.kind == 60 || la.kind == 61) { - if (la.kind == 60) { + if (la.kind == 61 || la.kind == 62) { + if (la.kind == 61) { Get(); isAbstract = true; } - Expect(61); - while (la.kind == 45) { + Expect(62); + while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 62 || la.kind == 63) { - if (la.kind == 62) { + if (la.kind == 63 || la.kind == 64) { + if (la.kind == 63) { Get(); - Expect(63); + Expect(64); QualifiedModuleName(out idRefined); isExclusively = true; } else { @@ -644,79 +664,79 @@ bool IsType(ref IToken pt) { } } module = new ModuleDefinition(id, id.val, isAbstract, false, isExclusively, idRefined == null ? null : idRefined, parent, attrs, false, this); - Expect(45); + Expect(46); module.BodyStartTok = t; while (StartOf(1)) { switch (la.kind) { - case 60: case 61: case 64: { + case 61: case 62: case 65: { SubModuleDecl(module, out sm); module.TopLevelDecls.Add(sm); break; } - case 69: { + case 70: { ClassDecl(module, out c); module.TopLevelDecls.Add(c); break; } - case 71: { + case 72: { TraitDecl(module, out trait); module.TopLevelDecls.Add(trait); break; } - case 75: case 76: { + case 76: case 77: { DatatypeDecl(module, out dt); module.TopLevelDecls.Add(dt); break; } - case 78: { + case 79: { NewtypeDecl(module, out td); module.TopLevelDecls.Add(td); break; } - case 79: { + case 80: { OtherTypeDecl(module, out td); module.TopLevelDecls.Add(td); break; } - case 80: { + case 81: { IteratorDecl(module, out iter); module.TopLevelDecls.Add(iter); break; } - case 37: case 38: case 39: case 40: case 41: case 72: case 73: case 74: case 77: case 83: case 84: case 85: case 86: { + case 38: case 39: case 40: case 41: case 42: case 73: case 74: case 75: case 78: case 84: case 85: case 86: case 87: { ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals, DafnyOptions.O.IronDafny && isAbstract); break; } } } - Expect(46); + Expect(47); module.BodyEndTok = t; module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); submodule = new LiteralModuleDecl(module, parent); - } else if (la.kind == 64) { + } else if (la.kind == 65) { Get(); - if (la.kind == 65) { + if (la.kind == 66) { Get(); opened = true; } NoUSIdent(out id); - if (la.kind == 66 || la.kind == 67) { - if (la.kind == 66) { + if (la.kind == 67 || la.kind == 68) { + if (la.kind == 67) { Get(); QualifiedModuleName(out idPath); submodule = new AliasModuleDecl(idPath, id, parent, opened); } else { Get(); QualifiedModuleName(out idPath); - if (la.kind == 68) { + if (la.kind == 69) { Get(); QualifiedModuleName(out idAssignment); } submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); } } - if (la.kind == 27) { - while (!(la.kind == 0 || la.kind == 27)) {SynErr(139); Get();} + if (la.kind == 28) { + while (!(la.kind == 0 || la.kind == 28)) {SynErr(139); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -740,16 +760,16 @@ bool IsType(ref IToken pt) { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 69)) {SynErr(141); Get();} - Expect(69); - while (la.kind == 45) { + while (!(la.kind == 0 || la.kind == 70)) {SynErr(141); Get();} + Expect(70); + while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 51) { + if (la.kind == 52) { GenericParameters(typeArgs); } - if (la.kind == 70) { + if (la.kind == 71) { Get(); Type(out trait); traits.Add(trait); @@ -759,12 +779,12 @@ bool IsType(ref IToken pt) { traits.Add(trait); } } - Expect(45); + Expect(46); bodyStart = t; while (StartOf(2)) { ClassMemberDecl(members, true, false, false); } - Expect(46); + Expect(47); c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits); c.BodyStartTok = bodyStart; c.BodyEndTok = t; @@ -781,29 +801,29 @@ bool IsType(ref IToken pt) { IToken bodyStart = Token.NoToken; // dummy assignment bool co = false; - while (!(la.kind == 0 || la.kind == 75 || la.kind == 76)) {SynErr(142); Get();} - if (la.kind == 75) { + while (!(la.kind == 0 || la.kind == 76 || la.kind == 77)) {SynErr(142); Get();} + if (la.kind == 76) { Get(); - } else if (la.kind == 76) { + } else if (la.kind == 77) { Get(); co = true; } else SynErr(143); - while (la.kind == 45) { + while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 51) { + if (la.kind == 52) { GenericParameters(typeArgs); } - Expect(66); + Expect(67); bodyStart = t; DatatypeMemberDecl(ctors); while (la.kind == 23) { Get(); DatatypeMemberDecl(ctors); } - if (la.kind == 27) { - while (!(la.kind == 0 || la.kind == 27)) {SynErr(144); Get();} + if (la.kind == 28) { + while (!(la.kind == 0 || la.kind == 28)) {SynErr(144); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate a (co)datatype declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -824,12 +844,12 @@ bool IsType(ref IToken pt) { Type baseType = null; Expression wh; - Expect(78); - while (la.kind == 45) { + Expect(79); + while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - Expect(66); + Expect(67); if (IsIdentColonOrBar()) { NoUSIdent(out bvId); if (la.kind == 21) { @@ -854,24 +874,24 @@ bool IsType(ref IToken pt) { td = null; Type ty; - Expect(79); - while (la.kind == 45) { + Expect(80); + while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 49) { + if (la.kind == 50) { Get(); - Expect(53); - Expect(50); + Expect(54); + Expect(51); eqSupport = TypeParameter.EqualitySupportValue.Required; - if (la.kind == 51) { + if (la.kind == 52) { GenericParameters(typeArgs); } } else if (StartOf(4)) { - if (la.kind == 51) { + if (la.kind == 52) { GenericParameters(typeArgs); } - if (la.kind == 66) { + if (la.kind == 67) { Get(); Type(out ty); td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); @@ -881,8 +901,8 @@ bool IsType(ref IToken pt) { td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs); } - if (la.kind == 27) { - while (!(la.kind == 0 || la.kind == 27)) {SynErr(147); Get();} + if (la.kind == 28) { + while (!(la.kind == 0 || la.kind == 28)) {SynErr(147); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -911,19 +931,19 @@ bool IsType(ref IToken pt) { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(la.kind == 0 || la.kind == 80)) {SynErr(148); Get();} - Expect(80); - while (la.kind == 45) { + while (!(la.kind == 0 || la.kind == 81)) {SynErr(148); Get();} + Expect(81); + while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 49 || la.kind == 51) { - if (la.kind == 51) { + if (la.kind == 50 || la.kind == 52) { + if (la.kind == 52) { GenericParameters(typeArgs); } Formals(true, true, ins); - if (la.kind == 81 || la.kind == 82) { - if (la.kind == 81) { + if (la.kind == 82 || la.kind == 83) { + if (la.kind == 82) { Get(); } else { Get(); @@ -931,14 +951,14 @@ bool IsType(ref IToken pt) { } Formals(false, true, outs); } - } else if (la.kind == 58) { + } else if (la.kind == 59) { Get(); signatureEllipsis = t; } else SynErr(149); while (StartOf(5)) { IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs); } - if (la.kind == 45) { + if (la.kind == 46) { BlockStmt(out body, out bodyStart, out bodyEnd); } iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs, @@ -961,21 +981,21 @@ bool IsType(ref IToken pt) { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 71)) {SynErr(150); Get();} - Expect(71); - while (la.kind == 45) { + while (!(la.kind == 0 || la.kind == 72)) {SynErr(150); Get();} + Expect(72); + while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 51) { + if (la.kind == 52) { GenericParameters(typeArgs); } - Expect(45); + Expect(46); bodyStart = t; while (StartOf(2)) { ClassMemberDecl(members, true, false, false); } - Expect(46); + Expect(47); trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs); trait.BodyStartTok = bodyStart; trait.BodyEndTok = t; @@ -989,11 +1009,11 @@ bool IsType(ref IToken pt) { MemberModifiers mmod = new MemberModifiers(); IToken staticToken = null, protectedToken = null; - while (la.kind == 72 || la.kind == 73 || la.kind == 74) { - if (la.kind == 72) { + while (la.kind == 73 || la.kind == 74 || la.kind == 75) { + if (la.kind == 73) { Get(); mmod.IsGhost = true; - } else if (la.kind == 73) { + } else if (la.kind == 74) { Get(); mmod.IsStatic = true; staticToken = t; } else { @@ -1001,7 +1021,7 @@ bool IsType(ref IToken pt) { mmod.IsProtected = true; protectedToken = t; } } - if (la.kind == 77) { + if (la.kind == 78) { if (moduleLevelDecl) { SemErr(la, "fields are not allowed to be declared at the module level; instead, wrap the field in a 'class' declaration"); mmod.IsStatic = false; @@ -1036,14 +1056,14 @@ bool IsType(ref IToken pt) { IToken x; string name; var args = new List(); - Expect(45); + Expect(46); Expect(21); NoUSIdent(out x); name = x.val; if (StartOf(7)) { Expressions(args); } - Expect(46); + Expect(47); attrs = new Attributes(name, args, attrs); } @@ -1061,7 +1081,7 @@ bool IsType(ref IToken pt) { IToken id; ids = new List(); Ident(out id); ids.Add(id); - while (la.kind == 26) { + while (la.kind == 27) { Get(); Ident(out id); ids.Add(id); @@ -1079,13 +1099,13 @@ bool IsType(ref IToken pt) { IToken/*!*/ id; TypeParameter.EqualitySupportValue eqSupport; - Expect(51); + Expect(52); NoUSIdent(out id); eqSupport = TypeParameter.EqualitySupportValue.Unspecified; - if (la.kind == 49) { + if (la.kind == 50) { Get(); - Expect(53); - Expect(50); + Expect(54); + Expect(51); eqSupport = TypeParameter.EqualitySupportValue.Required; } typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); @@ -1093,15 +1113,15 @@ bool IsType(ref IToken pt) { Get(); NoUSIdent(out id); eqSupport = TypeParameter.EqualitySupportValue.Unspecified; - if (la.kind == 49) { + if (la.kind == 50) { Get(); - Expect(53); - Expect(50); + Expect(54); + Expect(51); eqSupport = TypeParameter.EqualitySupportValue.Required; } typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); } - Expect(52); + Expect(53); } void Type(out Type ty) { @@ -1114,11 +1134,11 @@ bool IsType(ref IToken pt) { Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; - while (!(la.kind == 0 || la.kind == 77)) {SynErr(152); Get();} - Expect(77); + while (!(la.kind == 0 || la.kind == 78)) {SynErr(152); Get();} + Expect(78); if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } - while (la.kind == 45) { + while (la.kind == 46) { Attribute(ref attrs); } FIdentType(out id, out ty); @@ -1150,48 +1170,48 @@ bool IsType(ref IToken pt) { IToken signatureEllipsis = null; bool missingOpenParen; - if (la.kind == 37) { + if (la.kind == 38) { Get(); - if (la.kind == 83) { + if (la.kind == 84) { Get(); isFunctionMethod = true; } if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); } - while (la.kind == 45) { + while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 49 || la.kind == 51) { - if (la.kind == 51) { + if (la.kind == 50 || la.kind == 52) { + if (la.kind == 52) { GenericParameters(typeArgs); } Formals(true, isFunctionMethod, formals); Expect(21); Type(out returnType); - } else if (la.kind == 58) { + } else if (la.kind == 59) { Get(); signatureEllipsis = t; } else SynErr(153); - } else if (la.kind == 38) { + } else if (la.kind == 39) { Get(); isPredicate = true; - if (la.kind == 83) { + if (la.kind == 84) { Get(); isFunctionMethod = true; } if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); } - while (la.kind == 45) { + while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); if (StartOf(8)) { - if (la.kind == 51) { + if (la.kind == 52) { GenericParameters(typeArgs); } missingOpenParen = true; - if (la.kind == 49) { + if (la.kind == 50) { Formals(true, isFunctionMethod, formals); missingOpenParen = false; } @@ -1200,22 +1220,22 @@ bool IsType(ref IToken pt) { Get(); SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); } - } else if (la.kind == 58) { + } else if (la.kind == 59) { Get(); signatureEllipsis = t; } else SynErr(154); - } else if (la.kind == 39) { + } else if (la.kind == 40) { Get(); - Expect(38); + Expect(39); isIndPredicate = true; if (mmod.IsGhost) { SemErr(t, "inductive predicates cannot be declared 'ghost' (they are ghost by default)"); } - while (la.kind == 45) { + while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 49 || la.kind == 51) { - if (la.kind == 51) { + if (la.kind == 50 || la.kind == 52) { + if (la.kind == 52) { GenericParameters(typeArgs); } Formals(true, isFunctionMethod, formals); @@ -1223,21 +1243,21 @@ bool IsType(ref IToken pt) { Get(); SemErr(t, "inductive predicates do not have an explicitly declared return type; it is always bool"); } - } else if (la.kind == 58) { + } else if (la.kind == 59) { Get(); signatureEllipsis = t; } else SynErr(155); - } else if (la.kind == 41) { + } else if (la.kind == 42) { Get(); isCoPredicate = true; if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); } - while (la.kind == 45) { + while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 49 || la.kind == 51) { - if (la.kind == 51) { + if (la.kind == 50 || la.kind == 52) { + if (la.kind == 52) { GenericParameters(typeArgs); } Formals(true, isFunctionMethod, formals); @@ -1245,7 +1265,7 @@ bool IsType(ref IToken pt) { Get(); SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); } - } else if (la.kind == 58) { + } else if (la.kind == 59) { Get(); signatureEllipsis = t; } else SynErr(156); @@ -1254,7 +1274,7 @@ bool IsType(ref IToken pt) { while (StartOf(9)) { FunctionSpec(reqs, reads, ens, decreases); } - if (la.kind == 45) { + if (la.kind == 46) { FunctionBody(out body, out bodyStart, out bodyEnd); } if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported")) { @@ -1310,34 +1330,34 @@ bool IsType(ref IToken pt) { while (!(StartOf(10))) {SynErr(158); Get();} switch (la.kind) { - case 83: { + case 84: { Get(); break; } - case 40: { + case 41: { Get(); isLemma = true; break; } - case 84: { + case 85: { Get(); isCoLemma = true; break; } - case 85: { + case 86: { Get(); isCoLemma = true; errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'"); break; } - case 39: { + case 40: { Get(); - Expect(40); + Expect(41); isIndLemma = true; break; } - case 86: { + case 87: { Get(); if (allowConstructor) { isConstructor = true; @@ -1371,7 +1391,7 @@ bool IsType(ref IToken pt) { } } - while (la.kind == 45) { + while (la.kind == 46) { Attribute(ref attrs); } if (la.kind == 1) { @@ -1385,24 +1405,24 @@ bool IsType(ref IToken pt) { } } - if (la.kind == 49 || la.kind == 51) { - if (la.kind == 51) { + if (la.kind == 50 || la.kind == 52) { + if (la.kind == 52) { GenericParameters(typeArgs); } Formals(true, !mmod.IsGhost, ins); - if (la.kind == 82) { + if (la.kind == 83) { Get(); if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } Formals(false, !mmod.IsGhost, outs); } - } else if (la.kind == 58) { + } else if (la.kind == 59) { Get(); signatureEllipsis = t; } else SynErr(160); while (StartOf(11)) { MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs); } - if (la.kind == 45) { + if (la.kind == 46) { BlockStmt(out body, out bodyStart, out bodyEnd); } if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { @@ -1437,11 +1457,11 @@ bool IsType(ref IToken pt) { IToken/*!*/ id; List formals = new List(); - while (la.kind == 45) { + while (la.kind == 46) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 49) { + if (la.kind == 50) { FormalsOptionalIds(formals); } ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); @@ -1449,7 +1469,7 @@ bool IsType(ref IToken pt) { void FormalsOptionalIds(List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; - Expect(49); + Expect(50); if (StartOf(12)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); @@ -1459,7 +1479,7 @@ bool IsType(ref IToken pt) { formals.Add(new Formal(id, name, ty, true, isGhost)); } } - Expect(50); + Expect(51); } void FIdentType(out IToken/*!*/ id, out Type/*!*/ ty) { @@ -1477,8 +1497,8 @@ bool IsType(ref IToken pt) { } void OldSemi() { - if (la.kind == 27) { - while (!(la.kind == 0 || la.kind == 27)) {SynErr(162); Get();} + if (la.kind == 28) { + while (!(la.kind == 0 || la.kind == 28)) {SynErr(162); Get();} Get(); } } @@ -1487,7 +1507,7 @@ bool IsType(ref IToken pt) { Expression e0; IToken endTok; EquivExpression(out e, allowSemi, allowLambda); if (SemiFollowsCall(allowSemi, e)) { - Expect(27); + Expect(28); endTok = t; Expression(out e0, allowSemi, allowLambda); e = new StmtExpr(e.tok, @@ -1501,7 +1521,7 @@ bool IsType(ref IToken pt) { Contract.Ensures(Contract.ValueAtReturn(out id)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty)!=null); isGhost = false; - if (la.kind == 72) { + if (la.kind == 73) { Get(); if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } } @@ -1553,7 +1573,7 @@ bool IsType(ref IToken pt) { Contract.Ensures(Contract.ValueAtReturn(out ty)!=null); Contract.Ensures(Contract.ValueAtReturn(out identName)!=null); string name = null; id = Token.NoToken; ty = new BoolType()/*dummy*/; isGhost = false; - if (la.kind == 72) { + if (la.kind == 73) { Get(); isGhost = true; } @@ -1623,7 +1643,7 @@ bool IsType(ref IToken pt) { case 13: { Get(); tok = t; gt = new List(); - if (la.kind == 51) { + if (la.kind == 52) { GenericInstantiation(gt); } if (gt.Count > 1) { @@ -1636,7 +1656,7 @@ bool IsType(ref IToken pt) { case 14: { Get(); tok = t; gt = new List(); - if (la.kind == 51) { + if (la.kind == 52) { GenericInstantiation(gt); } if (gt.Count > 1) { @@ -1649,7 +1669,7 @@ bool IsType(ref IToken pt) { case 15: { Get(); tok = t; gt = new List(); - if (la.kind == 51) { + if (la.kind == 52) { GenericInstantiation(gt); } if (gt.Count > 1) { @@ -1662,7 +1682,7 @@ bool IsType(ref IToken pt) { case 16: { Get(); tok = t; gt = new List(); - if (la.kind == 51) { + if (la.kind == 52) { GenericInstantiation(gt); } if (gt.Count > 1) { @@ -1680,7 +1700,7 @@ bool IsType(ref IToken pt) { case 17: { Get(); tok = t; gt = new List(); - if (la.kind == 51) { + if (la.kind == 52) { GenericInstantiation(gt); } if (gt.Count == 0) { @@ -1697,7 +1717,7 @@ bool IsType(ref IToken pt) { case 18: { Get(); tok = t; gt = new List(); - if (la.kind == 51) { + if (la.kind == 52) { GenericInstantiation(gt); } if (gt.Count == 0) { @@ -1714,7 +1734,7 @@ bool IsType(ref IToken pt) { case 5: { Get(); tok = t; gt = null; - if (la.kind == 51) { + if (la.kind == 52) { gt = new List(); GenericInstantiation(gt); } @@ -1723,7 +1743,7 @@ bool IsType(ref IToken pt) { break; } - case 49: { + case 50: { Get(); tok = t; tupleArgTypes = new List(); if (StartOf(3)) { @@ -1735,7 +1755,7 @@ bool IsType(ref IToken pt) { tupleArgTypes.Add(ty); } } - Expect(50); + Expect(51); if (tupleArgTypes.Count == 1) { // just return the type 'ty' } else { @@ -1750,11 +1770,11 @@ bool IsType(ref IToken pt) { Expression e; tok = t; NameSegmentForTypeName(out e); tok = t; - while (la.kind == 26) { + while (la.kind == 27) { Get(); Expect(1); tok = t; List typeArgs = null; - if (la.kind == 51) { + if (la.kind == 52) { typeArgs = new List(); GenericInstantiation(typeArgs); } @@ -1765,7 +1785,7 @@ bool IsType(ref IToken pt) { } default: SynErr(164); break; } - if (la.kind == 29) { + if (la.kind == 30) { Type t2; Get(); tok = t; @@ -1783,8 +1803,8 @@ bool IsType(ref IToken pt) { void Formals(bool incoming, bool allowGhostKeyword, List formals) { Contract.Requires(cce.NonNullElements(formals)); IToken id; Type ty; bool isGhost; - Expect(49); - if (la.kind == 1 || la.kind == 72) { + Expect(50); + if (la.kind == 1 || la.kind == 73) { GIdentType(allowGhostKeyword, out id, out ty, out isGhost); formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); while (la.kind == 22) { @@ -1793,7 +1813,7 @@ bool IsType(ref IToken pt) { formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); } } - Expect(50); + Expect(51); } void IteratorSpec(List/*!*/ reads, List/*!*/ mod, List decreases, @@ -1803,7 +1823,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null; while (!(StartOf(13))) {SynErr(165); Get();} - if (la.kind == 43) { + if (la.kind == 44) { Get(); while (IsAttribute()) { Attribute(ref readsAttrs); @@ -1816,7 +1836,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { reads.Add(fe); } OldSemi(); - } else if (la.kind == 42) { + } else if (la.kind == 43) { Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -1830,17 +1850,17 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { } OldSemi(); } else if (StartOf(14)) { - if (la.kind == 87) { + if (la.kind == 88) { Get(); isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated"); } - if (la.kind == 89) { + if (la.kind == 90) { Get(); isYield = true; } - if (la.kind == 44) { + if (la.kind == 45) { Get(); Expression(out e, false, false); OldSemi(); @@ -1850,7 +1870,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { req.Add(new MaybeFreeExpression(e, isFree)); } - } else if (la.kind == 88) { + } else if (la.kind == 89) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); @@ -1864,7 +1884,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { } } else SynErr(166); - } else if (la.kind == 35) { + } else if (la.kind == 36) { Get(); while (IsAttribute()) { Attribute(ref decrAttrs); @@ -1878,12 +1898,12 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Contract.Ensures(Contract.ValueAtReturn(out block) != null); List body = new List(); - Expect(45); + Expect(46); bodyStart = t; while (StartOf(15)) { Stmt(body); } - Expect(46); + Expect(47); bodyEnd = t; block = new BlockStmt(bodyStart, bodyEnd, body); } @@ -1894,7 +1914,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null; while (!(StartOf(16))) {SynErr(168); Get();} - if (la.kind == 42) { + if (la.kind == 43) { Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -1907,19 +1927,19 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } OldSemi(); - } else if (la.kind == 44 || la.kind == 87 || la.kind == 88) { - if (la.kind == 87) { + } else if (la.kind == 45 || la.kind == 88 || la.kind == 89) { + if (la.kind == 88) { Get(); isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated"); } - if (la.kind == 44) { + if (la.kind == 45) { Get(); Expression(out e, false, false); OldSemi(); req.Add(new MaybeFreeExpression(e, isFree)); - } else if (la.kind == 88) { + } else if (la.kind == 89) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); @@ -1928,7 +1948,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo OldSemi(); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } else SynErr(169); - } else if (la.kind == 35) { + } else if (la.kind == 36) { Get(); while (IsAttribute()) { Attribute(ref decAttrs); @@ -1948,13 +1968,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(7)) { Expression(out e, allowSemi, allowLambda); feTok = e.tok; - if (la.kind == 90) { + if (la.kind == 91) { Get(); Ident(out id); fieldName = id.val; feTok = id; } fe = new FrameExpression(feTok, e, fieldName); - } else if (la.kind == 90) { + } else if (la.kind == 91) { Get(); Ident(out id); fieldName = id.val; @@ -1985,7 +2005,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void GenericInstantiation(List/*!*/ gt) { Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; - Expect(51); + Expect(52); Type(out ty); gt.Add(ty); while (la.kind == 22) { @@ -1993,7 +2013,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Type(out ty); gt.Add(ty); } - Expect(52); + Expect(53); } void NameSegmentForTypeName(out Expression e) { @@ -2001,7 +2021,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List typeArgs = null; Ident(out id); - if (la.kind == 51) { + if (la.kind == 52) { typeArgs = new List(); GenericInstantiation(typeArgs); } @@ -2015,12 +2035,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(decreases == null || cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; while (!(StartOf(17))) {SynErr(172); Get();} - if (la.kind == 44) { + if (la.kind == 45) { Get(); Expression(out e, false, false); OldSemi(); reqs.Add(e); - } else if (la.kind == 43) { + } else if (la.kind == 44) { Get(); PossiblyWildFrameExpression(out fe, false); reads.Add(fe); @@ -2030,12 +2050,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe); } OldSemi(); - } else if (la.kind == 88) { + } else if (la.kind == 89) { Get(); Expression(out e, false, false); OldSemi(); ens.Add(e); - } else if (la.kind == 35) { + } else if (la.kind == 36) { Get(); if (decreases == null) { SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed"); @@ -2049,16 +2069,16 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; - Expect(45); + Expect(46); bodyStart = t; Expression(out e, true, true); - Expect(46); + Expect(47); bodyEnd = t; } void PossiblyWildFrameExpression(out FrameExpression fe, bool allowSemi) { Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; - if (la.kind == 56) { + if (la.kind == 57) { Get(); fe = new FrameExpression(t, new WildcardExpr(t), null); } else if (StartOf(18)) { @@ -2069,7 +2089,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildExpression(out Expression e, bool allowLambda) { Contract.Ensures(Contract.ValueAtReturn(out e)!=null); e = dummyExpr; - if (la.kind == 56) { + if (la.kind == 57) { Get(); e = new WildcardExpr(t); } else if (StartOf(7)) { @@ -2093,7 +2113,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (!(StartOf(19))) {SynErr(176); Get();} switch (la.kind) { - case 45: { + case 46: { BlockStmt(out bs, out bodyStart, out bodyEnd); s = bs; break; @@ -2102,7 +2122,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssertStmt(out s); break; } - case 30: { + case 31: { AssumeStmt(out s); break; } @@ -2110,11 +2130,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo PrintStmt(out s); break; } - case 1: case 2: case 3: case 4: case 8: case 10: case 19: case 20: case 23: case 49: case 131: case 132: case 133: case 134: case 135: case 136: { + case 1: case 2: case 3: case 4: case 8: case 10: case 19: case 20: case 23: case 50: case 131: case 132: case 133: case 134: case 135: case 136: { UpdateStmt(out s); break; } - case 72: case 77: { + case 73: case 78: { VarDeclStatement(out s); break; } @@ -2134,7 +2154,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ForallStmt(out s); break; } - case 31: { + case 32: { CalcStmt(out s); break; } @@ -2142,7 +2162,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ModifyStmt(out s); break; } - case 91: { + case 92: { Get(); x = t; NoUSIdent(out id); @@ -2151,28 +2171,28 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList