From cb2fc85d19ef3775d6e05376f59ba2fd4442fffa Mon Sep 17 00:00:00 2001 From: leino Date: Tue, 11 Nov 2014 01:19:46 -0800 Subject: Took a pass through the whole grammar to clean up allowSemi/allowLambda parameters --- Source/Dafny/Dafny.atg | 220 +++++++++++----------- Source/Dafny/Parser.cs | 482 +++++++++++++++++++++++------------------------- Source/Dafny/Scanner.cs | 52 +++--- 3 files changed, 373 insertions(+), 381 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index b994f4f2..1f503e78 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -153,9 +153,11 @@ bool IsAddOp() { bool IsMulOp() { return la.kind == _star || la.val == "/" || la.val == "%"; } +bool IsQSep() { + return la.kind == _doublecolon || la.kind == _bullet; +} -bool IsColonExpr() { - // more precisely, "is colon, but is not colon + rbracket" +bool IsNonFinalColon() { return la.kind == _colon && scanner.Peek().kind != _rbracket; } @@ -821,20 +823,20 @@ MethodSpec<.List/*!*/ req, List/ .) SYNC ( "modifies" { IF(IsAttribute()) Attribute } - FrameExpression (. mod.Add(fe); .) - { "," FrameExpression (. mod.Add(fe); .) + FrameExpression (. mod.Add(fe); .) + { "," FrameExpression (. mod.Add(fe); .) } OldSemi | [ "free" (. isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated"); .) ] - ( "requires" Expression OldSemi (. req.Add(new MaybeFreeExpression(e, isFree)); .) + ( "requires" Expression OldSemi (. req.Add(new MaybeFreeExpression(e, isFree)); .) | "ensures" { IF(IsAttribute()) Attribute } - Expression OldSemi (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .) + Expression OldSemi (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .) ) - | "decreases" { IF(IsAttribute()) Attribute } DecreasesList OldSemi + | "decreases" { IF(IsAttribute()) Attribute } DecreasesList OldSemi ) . IteratorSpec<.List/*!*/ reads, List/*!*/ mod, List decreases, @@ -845,13 +847,13 @@ IteratorSpec<.List/*!*/ reads, List/ .) SYNC ( "reads" { IF(IsAttribute()) Attribute } - FrameExpression (. reads.Add(fe); .) - { "," FrameExpression (. reads.Add(fe); .) + FrameExpression (. reads.Add(fe); .) + { "," FrameExpression (. reads.Add(fe); .) } OldSemi | "modifies" { IF(IsAttribute()) Attribute } - FrameExpression (. mod.Add(fe); .) - { "," FrameExpression (. mod.Add(fe); .) + FrameExpression (. mod.Add(fe); .) + { "," FrameExpression (. mod.Add(fe); .) } OldSemi | [ "free" (. isFree = true; @@ -860,21 +862,21 @@ IteratorSpec<.List/*!*/ reads, List/ ] [ "yield" (. isYield = true; .) ] - ( "requires" Expression OldSemi (. if (isYield) { + ( "requires" Expression OldSemi (. if (isYield) { yieldReq.Add(new MaybeFreeExpression(e, isFree)); } else { req.Add(new MaybeFreeExpression(e, isFree)); } .) | "ensures" { IF(IsAttribute()) Attribute } - Expression OldSemi (. if (isYield) { + Expression OldSemi (. if (isYield) { yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } else { ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } .) ) - | "decreases" { IF(IsAttribute()) Attribute } DecreasesList OldSemi + | "decreases" { IF(IsAttribute()) Attribute } DecreasesList OldSemi ) . Formals<.bool incoming, bool allowGhostKeyword, List formals.> @@ -1101,47 +1103,48 @@ FunctionSpec<.List/*!*/ reqs, List/*!*/ r Expression/*!*/ e; FrameExpression/*!*/ fe; .) ( SYNC - "requires" Expression OldSemi (. reqs.Add(e); .) - | "reads" PossiblyWildFrameExpression (. reads.Add(fe); .) - { "," PossiblyWildFrameExpression (. reads.Add(fe); .) - } - OldSemi - | "ensures" Expression OldSemi (. ens.Add(e); .) + "requires" Expression OldSemi (. reqs.Add(e); .) + | "reads" + PossiblyWildFrameExpression (. reads.Add(fe); .) + { "," PossiblyWildFrameExpression (. reads.Add(fe); .) + } + OldSemi + | "ensures" Expression OldSemi (. ens.Add(e); .) | "decreases" (. if (decreases == null) { SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed"); decreases = new List(); } .) - DecreasesList OldSemi + DecreasesList OldSemi ) . LambdaSpec<.out Expression req, List reads.> = (. Contract.Requires(reads != null); Expression e; req = null; FrameExpression fe; .) - { ( "requires" Expression + { ( "requires" Expression (. if (req == null) { req = e; } else { req = new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, e); } .) - | "reads" PossiblyWildFrameExpression (. reads.Add(fe); .) + | "reads" PossiblyWildFrameExpression (. reads.Add(fe); .) ) } . -PossiblyWildExpression +PossiblyWildExpression = (. Contract.Ensures(Contract.ValueAtReturn(out e)!=null); e = dummyExpr; .) /* A decreases clause on a loop asks that no termination check be performed. * Use of this feature is sound only with respect to partial correctness. */ ( "*" (. e = new WildcardExpr(t); .) - | Expression + | Expression ) . -PossiblyWildFrameExpression +PossiblyWildFrameExpression = (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; .) /* A reads clause can list a wildcard, which allows the enclosing function to * read anything. In many cases, and in particular in all cases where @@ -1150,25 +1153,23 @@ PossiblyWildFrameExpression * language allows it (and it is sound). */ ( "*" (. fe = new FrameExpression(t, new WildcardExpr(t), null); .) - | FrameExpression + | FrameExpression ) . -FrameExpression +FrameExpression = (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; IToken feTok = null; fe = null; .) - (( Expression (. feTok = e.tok; .) - [ "`" Ident (. fieldName = id.val; feTok = id; .) - ] - (. fe = new FrameExpression(feTok, e, fieldName); .) - ) + ( Expression (. feTok = e.tok; .) + [ "`" Ident (. fieldName = id.val; feTok = id; .) + ] (. fe = new FrameExpression(feTok, e, fieldName); .) | - ( "`" Ident (. fieldName = id.val; .) - (. fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); .) - )) + "`" Ident (. fieldName = id.val; .) + (. fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); .) + ) . FunctionBody = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .) @@ -1260,10 +1261,9 @@ ReturnStmt ( "return" (. returnTok = t; .) | "yield" (. returnTok = t; isYield = true; .) ) - [ - Rhs (. rhss = new List(); rhss.Add(r); .) - { "," Rhs (. rhss.Add(r); .) - } + [ Rhs (. rhss = new List(); rhss.Add(r); .) + { "," Rhs (. rhss.Add(r); .) + } ] ";" (. if (isYield) { s = new YieldStmt(returnTok, t, rhss); @@ -1343,7 +1343,7 @@ Rhs } .) | "*" (. r = new HavocRhs(t); .) - | Expression (. r = new ExprRhs(e); .) + | Expression (. r = new ExprRhs(e); .) ) { Attribute } (. r.Attributes = attrs; .) . @@ -1511,11 +1511,11 @@ LoopSpec<.out List invariants, out List OldSemi (. invariants.Add(invariant); .) | SYNC "decreases" { IF(IsAttribute()) Attribute } - DecreasesList OldSemi + DecreasesList OldSemi | SYNC "modifies" { IF(IsAttribute()) Attribute } (. mod = mod ?? new List(); .) - [ FrameExpression (. mod.Add(fe); .) - { "," FrameExpression (. mod.Add(fe); .) + [ FrameExpression (. mod.Add(fe); .) + { "," FrameExpression (. mod.Add(fe); .) } ] OldSemi } @@ -1530,20 +1530,21 @@ Invariant "invariant" { IF(IsAttribute()) Attribute } Expression (. invariant = new MaybeFreeExpression(e, isFree, attrs); .) . -DecreasesList<.List decreases, bool allowWildcard.> +DecreasesList<.List decreases, bool allowWildcard, bool allowLambda.> = (. Expression/*!*/ e; .) - PossiblyWildExpression (. if (!allowWildcard && e is WildcardExpr) { - SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods"); - } else { - decreases.Add(e); - } - .) - { "," PossiblyWildExpression (. if (!allowWildcard && e is WildcardExpr) { - SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods"); - } else { - decreases.Add(e); - } - .) + PossiblyWildExpression (. if (!allowWildcard && e is WildcardExpr) { + SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods"); + } else { + decreases.Add(e); + } + .) + { "," PossiblyWildExpression + (. if (!allowWildcard && e is WildcardExpr) { + SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods"); + } else { + decreases.Add(e); + } + .) } . Guard /* null represents demonic-choice */ @@ -1562,7 +1563,9 @@ MatchStmt "match" (. x = t; .) Expression ( IF(la.kind == _lbrace) /* always favor brace-enclosed match body to a case-less match */ - "{" { CaseStatement (. cases.Add(c); .) } "}" (. usesOptionalBrace = true; .) + "{" (. usesOptionalBrace = true; .) + { CaseStatement (. cases.Add(c); .) } + "}" | { IF(la.kind == _case) /* let each "case" bind to the closest preceding "match" */ CaseStatement (. cases.Add(c); .) } @@ -1626,13 +1629,14 @@ AssumeStmt } .) . -PrintStmt -= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression arg; - List args = new List(); +PrintStmt += (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); + IToken x; Expression e; + var args = new List(); .) "print" (. x = t; .) - AttributeArg (. args.Add(arg); .) - { "," AttributeArg (. args.Add(arg); .) + Expression (. args.Add(e); .) + { "," Expression (. args.Add(e); .) } ";" (. s = new PrintStmt(x, t, args); .) . @@ -1701,10 +1705,10 @@ ModifyStmt * may also look like a BlockStmt. We're happy to parse the former, because if the user intended * the latter, then an explicit FrameExpression of {} could be given. */ - ( FrameExpression (. mod.Add(fe); .) - { "," FrameExpression (. mod.Add(fe); .) + ( FrameExpression (. mod.Add(fe); .) + { "," FrameExpression (. mod.Add(fe); .) } - | "..." (. ellipsisToken = t; .) + | "..." (. ellipsisToken = t; .) ) ( BlockStmt | SYNC ";" (. endTok = t; .) @@ -1815,8 +1819,8 @@ Hint . /*------------------------------------------------------------------------*/ /* Note. In order to avoid LL(1) warnings for expressions that "parse as far as possible", it is - * necessary to use Coco/R's IF construct. That means there are two ways to check for these - * operators, both in Is...() methods (defined above) and as grammar non-terminals (defined + * necessary to use Coco/R's IF construct. That means there are two ways to check for some of + * these operators, both in Is...() methods (defined above) and as grammar non-terminals (defined * here). These pairs of definitions must be changed together. */ EquivOp = "<==>" | '\u21d4'. @@ -1825,18 +1829,29 @@ ExpliesOp = "<==" | '\u21d0'. AndOp = "&&" | '\u2227'. OrOp = "||" | '\u2228'. -/* The "allowSemi" argument says whether or not the top-level expression +NegOp = "!" | '\u00ac'. +Forall = "forall" | '\u2200'. +Exists = "exists" | '\u2203'. +QSep = "::" | '\u2022'. + +/* The "allowSemi" argument says whether or not the expression * to be parsed is allowed to have the form S;E where S is a call to a lemma. * "allowSemi" should be passed in as "false" whenever the expression to * be parsed sits in a context that itself is terminated by a semi-colon. * - * The "allowLambda" is there to be able to parse "case x => e". - * Directly after the case keyword, you cannot do identifier-sequence-lambdas. + * The "allowLambda" says whether or not the expression to be parsed is + * allowed to be a lambda expression. More precisely, an identifier or + * parenthesized-enclosed comma-delimited list of identifiers is allowed to + * continue as a lambda expression (that is, continue with a "reads", "requires", + * or "=>") only if "allowLambda" is true. This affects function/method/iterator + * specifications, if/while statements with guarded alternatives, and expressions + * in the specification of a lambda expression itself. */ Expression = (. Expression e0; IToken endTok; .) EquivExpression [ IF(SemiFollowsCall(allowSemi, e)) + /* here we parse the ";E" that is part of a "LemmaCall;E" expression (other "S;E" expressions are parsed elsewhere) */ ";" (. endTok = t; .) Expression (. e = new StmtExpr(e.tok, @@ -1859,6 +1874,9 @@ ImpliesExpliesExpression = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .) LogicalExpression [ IF(IsImpliesOp() || IsExpliesOp()) /* read an ImpliesExpliesExpression as far as possible */ + /* Note, the asymmetry in the parsing of implies and explies expressions stems from the fact that + * implies is right associative whereas reverse implication is left associative + */ ( ImpliesOp (. x = t; .) ImpliesExpression (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .) | ExpliesOp (. x = t; .) @@ -2082,7 +2100,8 @@ UnaryExpression | "map" (. x = t; .) ( MapDisplayExpr { Suffix } - | MapComprehensionExpr + | MapComprehensionExpr + /* Note, a MapComprehensionExpr cannot be followed by suffixes */ ) | ConstAtomExpression { Suffix } @@ -2098,7 +2117,7 @@ Lhs { Suffix } ) . -NegOp = "!" | '\u00ac'. + /* A ConstAtomExpression is never an l-value. Also, a ConstAtomExpression is never followed by * an open paren (but could very well have a suffix that starts with a period or a square bracket). * (The "Also..." part may change if expressions in Dafny could yield functions.) @@ -2150,10 +2169,10 @@ ParensExpression Type tt; bool isLambda = false; .) - "(" (. x = t; .) + "(" (. x = t; .) [ - OptTypedExpr (. args.Add(ee); types.Add(tt); .) - { "," OptTypedExpr (. args.Add(ee); types.Add(tt); .) + OptTypedExpr (. args.Add(ee); types.Add(tt); .) + { "," OptTypedExpr (. args.Add(ee); types.Add(tt); .) } ] ")" @@ -2217,9 +2236,9 @@ ParensExpression } ] . -OptTypedExpr +OptTypedExpr = (. tt = null; .) - Expression + Expression [ ":" Type ] . DisplayExpr @@ -2265,7 +2284,7 @@ MapLiteralExpressions<.out List elements.> { "," Expression ":=" Expression (. elements.Add(new ExpressionPair(d,r)); .) } . -MapComprehensionExpr +MapComprehensionExpr = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); BoundVar bv; List bvars = new List(); @@ -2275,7 +2294,7 @@ MapComprehensionExpr IdentTypeOptional (. bvars.Add(bv); .) [ "|" Expression ] QSep - Expression + Expression (. e = new MapComprehension(mapToken, bvars, range ?? new LiteralExpr(mapToken, true), body); .) . @@ -2360,11 +2379,13 @@ MatchExpression bool usesOptionalBrace = false; .) "match" (. x = t; .) - Expression + Expression ( IF(la.kind == _lbrace) /* always favor brace-enclosed match body to a case-less match */ - "{" { CaseExpression (. cases.Add(c); .) } "}" (. usesOptionalBrace = true; .) + "{" (. usesOptionalBrace = true; .) + { CaseExpression (. cases.Add(c); .) } + "}" | { IF(la.kind == _case) /* let each "case" bind to the closest preceding "match" */ - CaseExpression (. cases.Add(c); .) + CaseExpression (. cases.Add(c); .) } ) (. e = new MatchExpr(x, e, cases, usesOptionalBrace); .) @@ -2444,7 +2465,7 @@ DottedIdentifiersAndFunction .) LambdaSpec LambdaArrow - Expression + Expression (. if (idents.Count != 1) { SemErr(id, "Invalid variable binding in lambda."); @@ -2500,7 +2521,7 @@ Suffix takeRest = true; .) [ Expression (. multipleLengths.Add(ee); takeRest = false; .) - { IF(IsColonExpr()) + { IF(IsNonFinalColon()) ":" Expression (. multipleLengths.Add(ee); .) } @@ -2583,10 +2604,6 @@ QuantifierGuts .) . -Forall = "forall" | '\u2200'. -Exists = "exists" | '\u2203'. -QSep = "::" | '\u2022'. - QuantifierDomain<.out List bvars, out Attributes attrs, out Expression range.> = (. bvars = new List(); @@ -2619,7 +2636,7 @@ SetComprehensionExpr IdentTypeOptional (. bvars.Add(bv); .) } "|" Expression - [ IF(la.kind == _doublecolon || la.kind == _bullet) /* let any given body bind to the closest enclosing set comprehension */ + [ IF(IsQSep()) /* let any given body bind to the closest enclosing set comprehension */ QSep Expression ] @@ -2635,24 +2652,13 @@ Expressions<.List/*!*/ args.> . /*------------------------------------------------------------------------*/ Attribute -= "{" - AttributeBody - "}" - . -AttributeBody -= (. string aName; - List aArgs = new List(); - Expression aArg; += (. string name; + var args = new List(); .) - ":" ident (. aName = t.val; .) - [ AttributeArg (. aArgs.Add(aArg); .) - { "," AttributeArg (. aArgs.Add(aArg); .) - } - ] (. attrs = new Attributes(aName, aArgs, attrs); .) - . -AttributeArg -= (. Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyExpr; .) - Expression (. arg = e; .) + "{" ":" ident (. name = t.val; .) + [ Expressions ] + "}" + (. attrs = new Attributes(name, args, attrs); .) . /*------------------------------------------------------------------------*/ Ident diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 4268db25..c8058ac9 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -197,9 +197,11 @@ bool IsAddOp() { bool IsMulOp() { return la.kind == _star || la.val == "/" || la.val == "%"; } +bool IsQSep() { + return la.kind == _doublecolon || la.kind == _bullet; +} -bool IsColonExpr() { - // more precisely, "is colon, but is not colon + rbracket" +bool IsNonFinalColon() { return la.kind == _colon && scanner.Peek().kind != _rbracket; } @@ -784,9 +786,18 @@ bool IsNotEndOfCase() { } void Attribute(ref Attributes attrs) { + string name; + var args = new List(); + Expect(23); - AttributeBody(ref attrs); + Expect(8); + Expect(1); + name = t.val; + if (StartOf(7)) { + Expressions(args); + } Expect(24); + attrs = new Attributes(name, args, attrs); } void NoUSIdent(out IToken/*!*/ x) { @@ -971,7 +982,7 @@ bool IsNotEndOfCase() { Attribute(ref attrs); } NoUSIdent(out id); - if (StartOf(7)) { + if (StartOf(8)) { if (la.kind == 56) { GenericParameters(typeArgs); } @@ -998,7 +1009,7 @@ bool IsNotEndOfCase() { Attribute(ref attrs); } NoUSIdent(out id); - if (StartOf(7)) { + if (StartOf(8)) { if (la.kind == 56) { GenericParameters(typeArgs); } @@ -1018,7 +1029,7 @@ bool IsNotEndOfCase() { } else SynErr(151); } else SynErr(152); decreases = isCoPredicate ? null : new List(); - while (StartOf(8)) { + while (StartOf(9)) { FunctionSpec(reqs, reads, ens, decreases); } if (la.kind == 23) { @@ -1071,7 +1082,7 @@ bool IsNotEndOfCase() { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(StartOf(9))) {SynErr(153); Get();} + while (!(StartOf(10))) {SynErr(153); Get();} if (la.kind == 58) { Get(); } else if (la.kind == 59) { @@ -1140,7 +1151,7 @@ bool IsNotEndOfCase() { Get(); signatureEllipsis = t; } else SynErr(155); - while (StartOf(10)) { + while (StartOf(11)) { MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs); } if (la.kind == 23) { @@ -1188,7 +1199,7 @@ bool IsNotEndOfCase() { void FormalsOptionalIds(List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; Expect(27); - if (StartOf(11)) { + if (StartOf(12)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); while (la.kind == 49) { @@ -1479,17 +1490,17 @@ List/*!*/ yieldReq, List/*!* ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null; - while (!(StartOf(12))) {SynErr(160); Get();} + while (!(StartOf(13))) {SynErr(160); Get();} if (la.kind == 21) { Get(); while (IsAttribute()) { Attribute(ref readsAttrs); } - FrameExpression(out fe); + FrameExpression(out fe, false, false); reads.Add(fe); while (la.kind == 49) { Get(); - FrameExpression(out fe); + FrameExpression(out fe, false, false); reads.Add(fe); } OldSemi(); @@ -1498,15 +1509,15 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { while (IsAttribute()) { Attribute(ref modAttrs); } - FrameExpression(out fe); + FrameExpression(out fe, false, false); mod.Add(fe); while (la.kind == 49) { Get(); - FrameExpression(out fe); + FrameExpression(out fe, false, false); mod.Add(fe); } OldSemi(); - } else if (StartOf(13)) { + } else if (StartOf(14)) { if (la.kind == 63) { Get(); isFree = true; @@ -1519,7 +1530,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { } if (la.kind == 22) { Get(); - Expression(out e, false, true); + Expression(out e, false, false); OldSemi(); if (isYield) { yieldReq.Add(new MaybeFreeExpression(e, isFree)); @@ -1532,7 +1543,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { while (IsAttribute()) { Attribute(ref ensAttrs); } - Expression(out e, false, true); + Expression(out e, false, false); OldSemi(); if (isYield) { yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); @@ -1546,7 +1557,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { while (IsAttribute()) { Attribute(ref decrAttrs); } - DecreasesList(decreases, false); + DecreasesList(decreases, false, false); OldSemi(); } else SynErr(162); } @@ -1557,7 +1568,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Expect(23); bodyStart = t; - while (StartOf(14)) { + while (StartOf(15)) { Stmt(body); } Expect(24); @@ -1570,17 +1581,17 @@ 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(15))) {SynErr(163); Get();} + while (!(StartOf(16))) {SynErr(163); Get();} if (la.kind == 20) { Get(); while (IsAttribute()) { Attribute(ref modAttrs); } - FrameExpression(out fe); + FrameExpression(out fe, false, false); mod.Add(fe); while (la.kind == 49) { Get(); - FrameExpression(out fe); + FrameExpression(out fe, false, false); mod.Add(fe); } OldSemi(); @@ -1593,7 +1604,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } if (la.kind == 22) { Get(); - Expression(out e, false, true); + Expression(out e, false, false); OldSemi(); req.Add(new MaybeFreeExpression(e, isFree)); } else if (la.kind == 64) { @@ -1601,7 +1612,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsAttribute()) { Attribute(ref ensAttrs); } - Expression(out e, false, true); + Expression(out e, false, false); OldSemi(); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } else SynErr(164); @@ -1610,20 +1621,20 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsAttribute()) { Attribute(ref decAttrs); } - DecreasesList(decreases, true); + DecreasesList(decreases, true, false); OldSemi(); } else SynErr(165); } - void FrameExpression(out FrameExpression/*!*/ fe) { + void FrameExpression(out FrameExpression fe, bool allowSemi, bool allowLambda) { Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; IToken feTok = null; fe = null; - if (StartOf(16)) { - Expression(out e, false, false); + if (StartOf(7)) { + Expression(out e, allowSemi, allowLambda); feTok = e.tok; if (la.kind == 81) { Get(); @@ -1639,9 +1650,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else SynErr(166); } - void DecreasesList(List decreases, bool allowWildcard) { + void DecreasesList(List decreases, bool allowWildcard, bool allowLambda) { Expression/*!*/ e; - PossiblyWildExpression(out e); + PossiblyWildExpression(out e, allowLambda); if (!allowWildcard && e is WildcardExpr) { SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods"); } else { @@ -1650,7 +1661,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 49) { Get(); - PossiblyWildExpression(out e); + PossiblyWildExpression(out e, allowLambda); if (!allowWildcard && e is WildcardExpr) { SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods"); } else { @@ -1715,22 +1726,22 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 22) { while (!(la.kind == 0 || la.kind == 22)) {SynErr(168); Get();} Get(); - Expression(out e, false, true); + Expression(out e, false, false); OldSemi(); reqs.Add(e); } else if (la.kind == 21) { Get(); - PossiblyWildFrameExpression(out fe); + PossiblyWildFrameExpression(out fe, false); reads.Add(fe); while (la.kind == 49) { Get(); - PossiblyWildFrameExpression(out fe); + PossiblyWildFrameExpression(out fe, false); reads.Add(fe); } OldSemi(); } else if (la.kind == 64) { Get(); - Expression(out e, false, true); + Expression(out e, false, false); OldSemi(); ens.Add(e); } else if (la.kind == 18) { @@ -1740,7 +1751,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo decreases = new List(); } - DecreasesList(decreases, false); + DecreasesList(decreases, false, false); OldSemi(); } else SynErr(169); } @@ -1754,13 +1765,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo bodyEnd = t; } - void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) { + void PossiblyWildFrameExpression(out FrameExpression fe, bool allowSemi) { Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; if (la.kind == 29) { Get(); fe = new FrameExpression(t, new WildcardExpr(t), null); } else if (StartOf(17)) { - FrameExpression(out fe); + FrameExpression(out fe, allowSemi, false); } else SynErr(170); } @@ -1770,7 +1781,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 21 || la.kind == 22) { if (la.kind == 22) { Get(); - Expression(out e, false, false); + Expression(out e, true, false); if (req == null) { req = e; } else { @@ -1779,20 +1790,20 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else { Get(); - PossiblyWildFrameExpression(out fe); + PossiblyWildFrameExpression(out fe, true); reads.Add(fe); } } } - void PossiblyWildExpression(out Expression/*!*/ e) { + void PossiblyWildExpression(out Expression e, bool allowLambda) { Contract.Ensures(Contract.ValueAtReturn(out e)!=null); e = dummyExpr; if (la.kind == 29) { Get(); e = new WildcardExpr(t); - } else if (StartOf(16)) { - Expression(out e, false, false); + } else if (StartOf(7)) { + Expression(out e, false, allowLambda); } else SynErr(171); } @@ -1829,7 +1840,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo PrintStmt(out s); break; } - case 1: case 2: case 3: case 4: case 6: case 7: case 9: case 27: case 69: case 70: case 122: case 123: case 124: case 125: case 126: case 127: { + case 1: case 2: case 3: case 4: case 6: case 7: case 9: case 27: case 69: case 70: case 125: case 126: case 127: case 128: case 129: case 130: { UpdateStmt(out s); break; } @@ -1909,7 +1920,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsAttribute()) { Attribute(ref attrs); } - if (StartOf(16)) { + if (StartOf(7)) { Expression(out e, false, true); } else if (la.kind == 31) { Get(); @@ -1934,7 +1945,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsAttribute()) { Attribute(ref attrs); } - if (StartOf(16)) { + if (StartOf(7)) { Expression(out e, false, true); } else if (la.kind == 31) { Get(); @@ -1949,18 +1960,19 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } - void PrintStmt(out Statement/*!*/ s) { - Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression arg; - List args = new List(); + void PrintStmt(out Statement s) { + Contract.Ensures(Contract.ValueAtReturn(out s) != null); + IToken x; Expression e; + var args = new List(); Expect(94); x = t; - AttributeArg(out arg, false); - args.Add(arg); + Expression(out e, false, true); + args.Add(e); while (la.kind == 49) { Get(); - AttributeArg(out arg, false); - args.Add(arg); + Expression(out e, false, true); + args.Add(e); } Expect(12); s = new PrintStmt(x, t, args); @@ -2215,12 +2227,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, true, true); if (la.kind == _lbrace) { Expect(23); + usesOptionalBrace = true; while (la.kind == 17) { CaseStatement(out c); cases.Add(c); } Expect(24); - usesOptionalBrace = true; } else if (StartOf(21)) { while (la.kind == _case) { CaseStatement(out c); @@ -2320,7 +2332,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(23); - while (StartOf(16)) { + while (StartOf(7)) { Expression(out e, false, true); lines.Add(e); stepOp = calcOp; danglingOperator = null; Expect(12); @@ -2367,11 +2379,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Attribute(ref attrs); } if (StartOf(17)) { - FrameExpression(out fe); + FrameExpression(out fe, false, true); mod.Add(fe); while (la.kind == 49) { Get(); - FrameExpression(out fe); + FrameExpression(out fe, false, true); mod.Add(fe); } } else if (la.kind == 31) { @@ -2486,7 +2498,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out x); } Expect(27); - if (StartOf(16)) { + if (StartOf(7)) { Expressions(args); } Expect(28); @@ -2503,7 +2515,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 29) { Get(); r = new HavocRhs(t); - } else if (StartOf(16)) { + } else if (StartOf(7)) { Expression(out e, false, true); r = new ExprRhs(e); } else SynErr(191); @@ -2554,7 +2566,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, true, false); Expect(13); body = new List(); - while (StartOf(14)) { + while (StartOf(15)) { Stmt(body); } alternatives.Add(new GuardedAlternative(x, e, body)); @@ -2573,7 +2585,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(29); Expect(28); e = null; - } else if (StartOf(16)) { + } else if (StartOf(7)) { Expression(out ee, true, true); e = ee; } else SynErr(193); @@ -2597,7 +2609,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsAttribute()) { Attribute(ref decAttrs); } - DecreasesList(decreases, true); + DecreasesList(decreases, true, true); OldSemi(); } else { while (!(la.kind == 0 || la.kind == 20)) {SynErr(195); Get();} @@ -2607,11 +2619,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } mod = mod ?? new List(); if (StartOf(17)) { - FrameExpression(out fe); + FrameExpression(out fe, false, true); mod.Add(fe); while (la.kind == 49) { Get(); - FrameExpression(out fe); + FrameExpression(out fe, false, true); mod.Add(fe); } } @@ -2665,12 +2677,6 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo c = new MatchCaseStmt(x, id.val, arguments, body); } - void AttributeArg(out Expression arg, bool allowSemi) { - Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyExpr; - Expression(out e, allowSemi, true); - arg = e; - } - void QuantifierDomain(out List bvars, out Attributes attrs, out Expression range) { bvars = new List(); BoundVar/*!*/ bv; @@ -2837,6 +2843,38 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else SynErr(203); } + void NegOp() { + if (la.kind == 115) { + Get(); + } else if (la.kind == 116) { + Get(); + } else SynErr(204); + } + + void Forall() { + if (la.kind == 95) { + Get(); + } else if (la.kind == 117) { + Get(); + } else SynErr(205); + } + + void Exists() { + if (la.kind == 118) { + Get(); + } else if (la.kind == 119) { + Get(); + } else SynErr(206); + } + + void QSep() { + if (la.kind == 10) { + Get(); + } else if (la.kind == 11) { + Get(); + } else SynErr(207); + } + void EquivExpression(out Expression e0, bool allowSemi, bool allowLambda) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; ImpliesExpliesExpression(out e0, allowSemi, allowLambda); @@ -2868,7 +2906,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LogicalExpression(out e1, allowSemi, allowLambda); e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); } - } else SynErr(204); + } else SynErr(208); } } @@ -2898,7 +2936,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo RelationalExpression(out e1, allowSemi, allowLambda); e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); } - } else SynErr(205); + } else SynErr(209); } } @@ -3073,7 +3111,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } break; } - case 115: { + case 120: { Get(); x = t; op = BinaryExpr.Opcode.In; break; @@ -3083,11 +3121,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.NotIn; break; } - case 116: { + case 115: { Get(); x = t; y = Token.NoToken; if (la.val == "!") { - Expect(116); + Expect(115); y = t; } if (y == Token.NoToken) { @@ -3116,7 +3154,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(206); break; + default: SynErr(210); break; } } @@ -3132,33 +3170,33 @@ 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 == 117) { + if (la.kind == 121) { Get(); x = t; op = BinaryExpr.Opcode.Add; - } else if (la.kind == 118) { + } else if (la.kind == 122) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(207); + } else SynErr(211); } void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; switch (la.kind) { - case 118: { + case 122: { Get(); x = t; UnaryExpression(out e, allowSemi, allowLambda); e = new NegationExpression(x, e); break; } - case 116: case 121: { + case 115: case 116: { NegOp(); x = t; UnaryExpression(out e, allowSemi, allowLambda); e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Not, e); break; } - case 15: case 16: case 44: case 48: case 71: case 82: case 89: case 92: case 93: case 95: case 130: case 131: case 132: { + case 15: case 16: case 44: case 48: case 71: case 82: case 89: case 92: case 93: case 95: case 117: case 118: case 119: { EndlessExpression(out e, allowSemi, allowLambda); break; } @@ -3192,18 +3230,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Suffix(ref e); } } else if (la.kind == 1) { - MapComprehensionExpr(x, out e, allowSemi); - } else SynErr(208); + MapComprehensionExpr(x, out e, allowSemi, allowLambda); + } else SynErr(212); break; } - case 2: case 3: case 4: case 6: case 7: case 9: case 27: case 69: case 70: case 122: case 123: case 124: case 125: case 126: case 127: { + case 2: case 3: case 4: case 6: case 7: case 9: case 27: case 69: case 70: case 125: case 126: case 127: case 128: case 129: case 130: { ConstAtomExpression(out e, allowSemi, allowLambda); while (la.kind == 25 || la.kind == 27 || la.kind == 77) { Suffix(ref e); } break; } - default: SynErr(209); break; + default: SynErr(213); break; } } @@ -3212,21 +3250,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 29) { Get(); x = t; op = BinaryExpr.Opcode.Mul; - } else if (la.kind == 119) { + } else if (la.kind == 123) { Get(); x = t; op = BinaryExpr.Opcode.Div; - } else if (la.kind == 120) { + } else if (la.kind == 124) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(210); - } - - void NegOp() { - if (la.kind == 116) { - Get(); - } else if (la.kind == 121) { - Get(); - } else SynErr(211); + } else SynErr(214); } void EndlessExpression(out Expression e, bool allowSemi, bool allowLambda) { @@ -3240,7 +3270,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); x = t; Expression(out e, true, true); - Expect(128); + Expect(131); Expression(out e0, true, true); Expect(90); Expression(out e1, allowSemi, allowLambda); @@ -3251,7 +3281,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo MatchExpression(out e, allowSemi, allowLambda); break; } - case 95: case 130: case 131: case 132: { + case 95: case 117: case 118: case 119: { QuantifierGuts(out e, allowSemi, allowLambda); break; } @@ -3273,7 +3303,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo NamedExpr(out e, allowSemi, allowLambda); break; } - default: SynErr(212); break; + default: SynErr(215); break; } } @@ -3304,7 +3334,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(27); openParen = t; - if (StartOf(16)) { + if (StartOf(7)) { Expressions(args); } Expect(28); @@ -3317,7 +3347,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LambdaSpec(out req, reads); LambdaArrow(out oneShot); - Expression(out body, allowSemi, true); + Expression(out body, allowSemi, allowLambda); if (idents.Count != 1) { SemErr(id, "Invalid variable binding in lambda."); } @@ -3366,7 +3396,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(27); IToken openParen = t; - if (StartOf(16)) { + if (StartOf(7)) { Expressions(args); } Expect(28); @@ -3376,13 +3406,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 25) { Get(); x = t; - if (StartOf(16)) { + if (StartOf(7)) { Expression(out ee, true, true); e0 = ee; - if (la.kind == 129) { + if (la.kind == 132) { Get(); anyDots = true; - if (StartOf(16)) { + if (StartOf(7)) { Expression(out ee, true, true); e1 = ee; } @@ -3396,10 +3426,10 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleLengths.Add(e0); // account for the Expression read before the colon takeRest = true; - if (StartOf(16)) { + if (StartOf(7)) { Expression(out ee, true, true); multipleLengths.Add(ee); takeRest = false; - while (IsColonExpr()) { + while (IsNonFinalColon()) { Expect(8); Expression(out ee, true, true); multipleLengths.Add(ee); @@ -3420,15 +3450,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee); } - } else SynErr(213); - } else if (la.kind == 129) { + } else SynErr(216); + } else if (la.kind == 132) { Get(); anyDots = true; - if (StartOf(16)) { + if (StartOf(7)) { Expression(out ee, true, true); e1 = ee; } - } else SynErr(214); + } else SynErr(217); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -3467,12 +3497,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 27) { Get(); IToken openParen = t; args = new List(); - if (StartOf(16)) { + if (StartOf(7)) { Expressions(args); } Expect(28); e = new ApplyExpr(e.tok, openParen, e, args); - } else SynErr(215); + } else SynErr(218); } void DisplayExpr(out Expression e) { @@ -3483,7 +3513,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 23) { Get(); x = t; elements = new List(); - if (StartOf(16)) { + if (StartOf(7)) { Expressions(elements); } e = new SetDisplayExpr(x, elements); @@ -3491,12 +3521,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 25) { Get(); x = t; elements = new List(); - if (StartOf(16)) { + if (StartOf(7)) { Expressions(elements); } e = new SeqDisplayExpr(x, elements); Expect(26); - } else SynErr(216); + } else SynErr(219); } void MultiSetExpr(out Expression e) { @@ -3509,7 +3539,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 23) { Get(); elements = new List(); - if (StartOf(16)) { + if (StartOf(7)) { Expressions(elements); } e = new MultiSetDisplayExpr(x, elements); @@ -3520,7 +3550,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, true, true); e = new MultiSetFormingExpr(x, e); Expect(28); - } else SynErr(217); + } else SynErr(220); } void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) { @@ -3529,14 +3559,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr; Expect(25); - if (StartOf(16)) { + if (StartOf(7)) { MapLiteralExpressions(out elements); } e = new MapDisplayExpr(mapToken, elements); Expect(26); } - void MapComprehensionExpr(IToken mapToken, out Expression e, bool allowSemi) { + void MapComprehensionExpr(IToken mapToken, out Expression e, bool allowSemi, bool allowLambda) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); BoundVar bv; List bvars = new List(); @@ -3550,7 +3580,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out range, true, true); } QSep(); - Expression(out body, allowSemi, true); + Expression(out body, allowSemi, allowLambda); e = new MapComprehension(mapToken, bvars, range ?? new LiteralExpr(mapToken, true), body); } @@ -3561,17 +3591,17 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr; Type toType = null; switch (la.kind) { - case 122: { + case 125: { Get(); e = new LiteralExpr(t, false); break; } - case 123: { + case 126: { Get(); e = new LiteralExpr(t, true); break; } - case 124: { + case 127: { Get(); e = new LiteralExpr(t); break; @@ -3599,12 +3629,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break; } - case 125: { + case 128: { Get(); e = new ThisExpr(t); break; } - case 126: { + case 129: { Get(); x = t; Expect(27); @@ -3613,7 +3643,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Fresh, e); break; } - case 127: { + case 130: { Get(); x = t; Expect(27); @@ -3648,7 +3678,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ParensExpression(out e, allowSemi, allowLambda); break; } - default: SynErr(218); break; + default: SynErr(221); break; } } @@ -3677,7 +3707,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo n = BigInteger.Zero; } - } else SynErr(219); + } else SynErr(222); } void Dec(out Basetypes.BigDec d) { @@ -3704,12 +3734,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(27); x = t; - if (StartOf(16)) { - OptTypedExpr(out ee, out tt, true); + if (StartOf(7)) { + OptTypedExpr(out ee, out tt); args.Add(ee); types.Add(tt); while (la.kind == 49) { Get(); - OptTypedExpr(out ee, out tt, true); + OptTypedExpr(out ee, out tt); args.Add(ee); types.Add(tt); } } @@ -3770,7 +3800,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 27) { Get(); openParen = t; args = new List(); - if (StartOf(16)) { + if (StartOf(7)) { Expressions(args); } Expect(28); @@ -3787,12 +3817,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 14) { Get(); oneShot = true; - } else SynErr(220); + } else SynErr(223); } - void OptTypedExpr(out Expression e, out Type tt, bool allowSemi) { + void OptTypedExpr(out Expression e, out Type tt) { tt = null; - Expression(out e, allowSemi, true); + Expression(out e, true, true); if (la.kind == 8) { Get(); Type(out tt); @@ -3815,14 +3845,6 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } - void QSep() { - if (la.kind == 10) { - Get(); - } else if (la.kind == 11) { - Get(); - } else SynErr(221); - } - void MatchExpression(out Expression e, bool allowSemi, bool allowLambda) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c; List cases = new List(); @@ -3830,21 +3852,21 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(92); x = t; - Expression(out e, allowSemi, true); + Expression(out e, allowSemi, allowLambda); if (la.kind == _lbrace) { Expect(23); + usesOptionalBrace = true; while (la.kind == 17) { - CaseExpression(out c, allowSemi, usesOptionalBrace || allowLambda); + CaseExpression(out c, true, true); cases.Add(c); } Expect(24); - usesOptionalBrace = true; } else if (StartOf(27)) { while (la.kind == _case) { - CaseExpression(out c, allowSemi, usesOptionalBrace || allowLambda); + CaseExpression(out c, allowSemi, allowLambda); cases.Add(c); } - } else SynErr(222); + } else SynErr(224); e = new MatchExpr(x, e, cases, usesOptionalBrace); } @@ -3856,13 +3878,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression range; Expression/*!*/ body; - if (la.kind == 95 || la.kind == 130) { + if (la.kind == 95 || la.kind == 117) { Forall(); x = t; univ = true; - } else if (la.kind == 131 || la.kind == 132) { + } else if (la.kind == 118 || la.kind == 119) { Exists(); x = t; - } else SynErr(223); + } else SynErr(225); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body, allowSemi, allowLambda); @@ -3893,7 +3915,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(9); Expression(out range, allowSemi, allowLambda); - if (la.kind == _doublecolon || la.kind == _bullet) { + if (IsQSep()) { QSep(); Expression(out body, allowSemi, allowLambda); } @@ -3910,7 +3932,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s); } else if (la.kind == 16) { CalcStmt(out s); - } else SynErr(224); + } else SynErr(226); } void LetExpr(out Expression e, bool allowSemi, bool allowLambda) { @@ -3950,7 +3972,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } - } else SynErr(225); + } else SynErr(227); Expression(out e, false, true); letRHSs.Add(e); while (la.kind == 49) { @@ -4001,7 +4023,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv); pat = new CasePattern(bv.tok, bv); - } else SynErr(226); + } else SynErr(228); if (pat == null) { pat = new CasePattern(t, "_ParseError", new List()); } @@ -4033,42 +4055,6 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo c = new MatchCaseExpr(x, id.val, arguments, body); } - void Forall() { - if (la.kind == 95) { - Get(); - } else if (la.kind == 130) { - Get(); - } else SynErr(227); - } - - void Exists() { - if (la.kind == 131) { - Get(); - } else if (la.kind == 132) { - Get(); - } else SynErr(228); - } - - void AttributeBody(ref Attributes attrs) { - string aName; - List aArgs = new List(); - Expression aArg; - - Expect(8); - Expect(1); - aName = t.val; - if (StartOf(16)) { - AttributeArg(out aArg, true); - aArgs.Add(aArg); - while (la.kind == 49) { - Get(); - AttributeArg(out aArg, true); - aArgs.Add(aArg); - } - } - attrs = new Attributes(aName, aArgs, attrs); - } - public void Parse() { @@ -4082,13 +4068,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } static readonly bool[,]/*!*/ set = { - {T,T,T,T, T,x,T,T, x,T,x,x, T,x,x,T, T,x,T,T, T,T,T,T, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,T, T,x,T,T, T,x,x,x, x,T,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x}, + {T,T,T,T, T,x,T,T, x,T,x,x, T,x,x,T, T,x,T,T, T,T,T,T, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,T, T,x,T,T, T,x,x,x, x,T,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,T,x,T, T,T,T,T, T,x,T,T, x,T,x,x, x,x,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,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,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,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,T,x, T,x,T,x, x,T,x,T, T,T,T,T, T,x,T,T, x,T,x,x, T,x,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,T,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,T,T,T, T,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, T,T,x,T, 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,T,x, x,T,T,T, T,T,T,x, x,x,x}, {T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,x,x,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,x,T, T,T,T,T, T,x,T,T, x,T,x,x, T,x,T,T, T,T,T,x, T,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,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, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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}, @@ -4096,20 +4083,19 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,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,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,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,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,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, 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,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x}, + {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, 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,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x}, {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,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,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, - {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,T,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,T,T,T, T,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, T,T,x,T, 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,T,T,T, T,T,T,T, x,x,T,T, T,x,x}, - {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,T,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,T,T,T, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,T,x,x, T,T,x,T, 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,T,T,T, T,T,T,T, x,x,T,T, T,x,x}, - {T,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, 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,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x}, - {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,T,x,T, x,T,x,T, 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,T,T,T, T,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, T,T,x,T, 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,T,T,T, T,T,T,T, x,x,T,T, T,x,x}, - {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,T,x,T, x,T,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,T,T,T, T,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, T,T,x,T, 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,T,T,T, T,T,T,T, x,x,T,T, T,x,x}, - {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,T,x,x, x,x,x,T, T,x,x,T, x,x,x,T, 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,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x}, - {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,T,x,x, x,x,x,T, T,x,x,T, x,x,x,T, 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,T, T,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x}, + {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,T,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,T,T,T, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,T,x,x, T,T,x,T, 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,T,x, x,T,T,T, T,T,T,x, x,x,x}, + {T,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, 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,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x}, + {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,T,x,T, x,T,x,T, 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,T,T,T, T,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, T,T,x,T, 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,T,x, x,T,T,T, T,T,T,x, x,x,x}, + {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,T,x,T, x,T,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,T,T,T, T,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, T,T,x,T, 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,T,x, x,T,T,T, T,T,T,x, x,x,x}, + {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,T,x,x, x,x,x,T, T,x,x,T, x,x,x,T, 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,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x}, + {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,T,x,x, x,x,x,T, T,x,x,T, x,x,x,T, 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,T, T,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, - {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,T,x,T, x,T,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,T,T,T, T,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,T,x,x, T,T,x,T, 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,T,T,T, T,T,T,T, x,x,T,T, T,x,x}, - {x,x,T,T, T,x,T,T, x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x}, + {x,T,T,T, T,x,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,T, x,T,x,T, x,T,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,T,T,T, T,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,T,x,x, T,T,x,T, 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,T,x, x,T,T,T, T,T,T,x, x,x,x}, + {x,x,T,T, T,x,T,T, x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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}, - {T,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,x, T,x,x,x, x,T,x,T, T,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, x,T,T,x, x,x,x,x, x,T,T,T, T,T,T,T, x,T,T,T, x,T,T,T, T,T,T,T, T,T,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, T,T,x,x, x,x,x} + {T,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,x, T,x,x,x, x,T,x,T, T,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, x,T,T,x, x,x,x,x, x,T,T,T, T,T,T,T, x,T,T,T, x,T,T,T, T,T,T,T, T,T,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x} }; } // end Parser @@ -4249,24 +4235,24 @@ public class Errors { case 112: s = "\"\\u2227\" expected"; break; case 113: s = "\"||\" expected"; break; case 114: s = "\"\\u2228\" expected"; break; - case 115: s = "\"in\" expected"; break; - case 116: s = "\"!\" expected"; break; - case 117: s = "\"+\" expected"; break; - case 118: s = "\"-\" expected"; break; - case 119: s = "\"/\" expected"; break; - case 120: s = "\"%\" expected"; break; - case 121: s = "\"\\u00ac\" expected"; break; - case 122: s = "\"false\" expected"; break; - case 123: s = "\"true\" expected"; break; - case 124: s = "\"null\" expected"; break; - case 125: s = "\"this\" expected"; break; - case 126: s = "\"fresh\" expected"; break; - case 127: s = "\"old\" expected"; break; - case 128: s = "\"then\" expected"; break; - case 129: s = "\"..\" expected"; break; - case 130: s = "\"\\u2200\" expected"; break; - case 131: s = "\"exists\" expected"; break; - case 132: s = "\"\\u2203\" expected"; break; + case 115: s = "\"!\" expected"; break; + case 116: s = "\"\\u00ac\" expected"; break; + case 117: s = "\"\\u2200\" expected"; break; + case 118: s = "\"exists\" expected"; break; + case 119: s = "\"\\u2203\" expected"; break; + case 120: s = "\"in\" expected"; break; + case 121: s = "\"+\" expected"; break; + case 122: s = "\"-\" expected"; break; + case 123: s = "\"/\" expected"; break; + case 124: s = "\"%\" expected"; break; + case 125: s = "\"false\" expected"; break; + case 126: s = "\"true\" expected"; break; + case 127: s = "\"null\" expected"; break; + case 128: s = "\"this\" expected"; break; + case 129: s = "\"fresh\" expected"; break; + case 130: s = "\"old\" expected"; break; + case 131: s = "\"then\" expected"; break; + case 132: s = "\"..\" expected"; break; case 133: s = "??? expected"; break; case 134: s = "this symbol not expected in SubModuleDecl"; break; case 135: s = "invalid SubModuleDecl"; break; @@ -4338,31 +4324,31 @@ public class Errors { case 201: s = "invalid ExpliesOp"; break; case 202: s = "invalid AndOp"; break; case 203: s = "invalid OrOp"; break; - case 204: s = "invalid ImpliesExpliesExpression"; break; - case 205: s = "invalid LogicalExpression"; break; - case 206: s = "invalid RelOp"; break; - case 207: s = "invalid AddOp"; break; - case 208: s = "invalid UnaryExpression"; break; - case 209: s = "invalid UnaryExpression"; break; - case 210: s = "invalid MulOp"; break; - case 211: s = "invalid NegOp"; break; - case 212: s = "invalid EndlessExpression"; break; - case 213: s = "invalid Suffix"; break; - case 214: s = "invalid Suffix"; break; - case 215: s = "invalid Suffix"; break; - case 216: s = "invalid DisplayExpr"; break; - case 217: s = "invalid MultiSetExpr"; break; - case 218: s = "invalid ConstAtomExpression"; break; - case 219: s = "invalid Nat"; break; - case 220: s = "invalid LambdaArrow"; break; - case 221: s = "invalid QSep"; break; - case 222: s = "invalid MatchExpression"; break; - case 223: s = "invalid QuantifierGuts"; break; - case 224: s = "invalid StmtInExpr"; break; - case 225: s = "invalid LetExpr"; break; - case 226: s = "invalid CasePattern"; break; - case 227: s = "invalid Forall"; break; - case 228: s = "invalid Exists"; break; + case 204: s = "invalid NegOp"; break; + case 205: s = "invalid Forall"; break; + case 206: s = "invalid Exists"; break; + case 207: s = "invalid QSep"; break; + case 208: s = "invalid ImpliesExpliesExpression"; break; + case 209: s = "invalid LogicalExpression"; break; + case 210: s = "invalid RelOp"; break; + case 211: s = "invalid AddOp"; break; + case 212: s = "invalid UnaryExpression"; break; + case 213: s = "invalid UnaryExpression"; break; + case 214: s = "invalid MulOp"; break; + case 215: s = "invalid EndlessExpression"; break; + case 216: s = "invalid Suffix"; break; + case 217: s = "invalid Suffix"; break; + case 218: s = "invalid Suffix"; break; + case 219: s = "invalid DisplayExpr"; break; + case 220: s = "invalid MultiSetExpr"; break; + case 221: s = "invalid ConstAtomExpression"; break; + case 222: s = "invalid Nat"; break; + case 223: s = "invalid LambdaArrow"; break; + case 224: s = "invalid MatchExpression"; break; + case 225: s = "invalid QuantifierGuts"; break; + case 226: s = "invalid StmtInExpr"; break; + case 227: s = "invalid LetExpr"; break; + case 228: s = "invalid CasePattern"; break; default: s = "error " + n; break; } diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index dae511ef..7afd3ab7 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -288,12 +288,12 @@ public class Scanner { start[38] = 78; start[8743] = 80; start[8744] = 82; - start[43] = 83; - start[47] = 84; - start[37] = 85; - start[172] = 86; - start[8704] = 87; - start[8707] = 88; + start[172] = 83; + start[8704] = 84; + start[8707] = 85; + start[43] = 86; + start[47] = 87; + start[37] = 88; start[Buffer.EOF] = -1; } @@ -560,15 +560,15 @@ public class Scanner { case "forall": t.kind = 95; break; case "parallel": t.kind = 96; break; case "modify": t.kind = 97; break; - case "in": t.kind = 115; break; - case "false": t.kind = 122; break; - case "true": t.kind = 123; break; - case "null": t.kind = 124; break; - case "this": t.kind = 125; break; - case "fresh": t.kind = 126; break; - case "old": t.kind = 127; break; - case "then": t.kind = 128; break; - case "exists": t.kind = 131; break; + case "exists": t.kind = 118; break; + case "in": t.kind = 120; break; + case "false": t.kind = 125; break; + case "true": t.kind = 126; break; + case "null": t.kind = 127; break; + case "this": t.kind = 128; break; + case "fresh": t.kind = 129; break; + case "old": t.kind = 130; break; + case "then": t.kind = 131; break; default: break; } } @@ -864,17 +864,17 @@ public class Scanner { case 82: {t.kind = 114; break;} case 83: - {t.kind = 117; break;} + {t.kind = 116; break;} case 84: - {t.kind = 119; break;} + {t.kind = 117; break;} case 85: - {t.kind = 120; break;} + {t.kind = 119; break;} case 86: {t.kind = 121; break;} case 87: - {t.kind = 130; break;} + {t.kind = 123; break;} case 88: - {t.kind = 132; break;} + {t.kind = 124; break;} case 89: recEnd = pos; recKind = 8; if (ch == ':') {AddCh(); goto case 29;} @@ -891,14 +891,14 @@ public class Scanner { else if (ch == '=') {AddCh(); goto case 97;} else {t.kind = 38; break;} case 92: - recEnd = pos; recKind = 118; + recEnd = pos; recKind = 122; if (ch == '>') {AddCh(); goto case 33;} - else {t.kind = 118; break;} + else {t.kind = 122; break;} case 93: - recEnd = pos; recKind = 116; + recEnd = pos; recKind = 115; if (ch == 'i') {AddCh(); goto case 41;} else if (ch == '=') {AddCh(); goto case 69;} - else {t.kind = 116; break;} + else {t.kind = 115; break;} case 94: recEnd = pos; recKind = 77; if (ch == '.') {AddCh(); goto case 98;} @@ -916,9 +916,9 @@ public class Scanner { if (ch == '>') {AddCh(); goto case 75;} else {t.kind = 52; break;} case 98: - recEnd = pos; recKind = 129; + recEnd = pos; recKind = 132; if (ch == '.') {AddCh(); goto case 44;} - else {t.kind = 129; break;} + else {t.kind = 132; break;} case 99: recEnd = pos; recKind = 99; if (ch == '=') {AddCh(); goto case 100;} -- cgit v1.2.3