diff options
| author |  leino <unknown> | 2014-06-24 19:07:42 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-06-24 19:07:42 -0700 |
| commit | 20f71a77b757f446f1e0459f9fcb2899e9c6c4dd (patch) | |
| tree | 5321d40f660d6b95e15f819bd987818a4fbe7dcb | |
| parent | 9587c569b00f969e18920c19a2a023489af93d3e (diff) | |
| parent | 16f17e96c48946f925620e1be86fd82cefce923c (diff) | |
Merge
| -rw-r--r-- | Source/Dafny/Cloner.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 35 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 10 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 536 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 39 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 108 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 4 | ||||
| -rw-r--r-- | Test/dafny0/MatchBraces.dfy | 147 | ||||
| -rw-r--r-- | Test/dafny0/MatchBraces.dfy.expect | 121 |
10 files changed, 673 insertions, 333 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 4bb4f85c..537dae1d 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -349,7 +349,7 @@ namespace Microsoft.Dafny } else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
return new MatchExpr(Tok(e.tok), CloneExpr(e.Source),
- e.Cases.ConvertAll(c => new MatchCaseExpr(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))));
+ e.Cases.ConvertAll(c => new MatchCaseExpr(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))), e.UsesOptionalBraces);
} else if (expr is NegationExpression) {
var e = (NegationExpression)expr;
@@ -472,7 +472,7 @@ namespace Microsoft.Dafny } else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
r = new MatchStmt(Tok(s.Tok), Tok(s.EndTok), CloneExpr(s.Source),
- s.Cases.ConvertAll(c => new MatchCaseStmt(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), c.Body.ConvertAll(CloneStmt))));
+ s.Cases.ConvertAll(c => new MatchCaseStmt(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), c.Body.ConvertAll(CloneStmt))), s.UsesOptionalBraces);
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index dd3ab8fe..2ab70c4f 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -130,6 +130,14 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { (e is FunctionCallExpr ||
(e is IdentifierSequence && ((IdentifierSequence)e).OpenParen != null));
}
+
+bool CloseOptionalParen(bool usesOptionalParen) {
+ return usesOptionalParen && la.kind == _closeparen;
+}
+
+bool CloseOptionalBrace(bool usesOptionalBrace) {
+ return usesOptionalBrace && la.kind == _rbrace;
+}
/*--------------------------------------------------------------------------*/
CHARACTERS
letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
@@ -172,6 +180,7 @@ TOKENS lbrace = '{'.
rbrace = '}'.
openparen = '('.
+ closeparen = ')'.
star = '*'.
notIn = "!in" CONTEXT (nonidchar).
COMMENTS FROM "/*" TO "*/" NESTED
@@ -1332,14 +1341,20 @@ Guard<out Expression e> /* null represents demonic-choice */ MatchStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
- List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>(); .)
+ List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
+ bool usesOptionalBrace = false;
+ .)
"match" (. x = t; .)
Expression<out e, true>
- "{"
+ [ "{" (. usesOptionalBrace = true; .)
+ ]
{ CaseStatement<out c> (. cases.Add(c); .)
}
- "}"
- (. s = new MatchStmt(x, t, e, cases); .)
+ ( IF(CloseOptionalBrace(usesOptionalBrace))
+ "}"
+ | (. if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } .)
+ )
+ (. s = new MatchStmt(x, t, e, cases, usesOptionalBrace); .)
.
CaseStatement<out MatchCaseStmt/*!*/ c>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
@@ -1436,7 +1451,8 @@ ForallStmt<out Statement/*!*/ s> (. if (bvars == null) { bvars = new List<BoundVar>(); }
if (range == null) { range = new LiteralExpr(x, true); }
.)
- ( ")" (. if (!usesOptionalParen) { SemErr(t, "found but didn't expect a close parenthesis"); } .)
+ ( IF(CloseOptionalParen(usesOptionalParen))
+ ")"
| (. if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); } .)
)
{ (. isFree = false; .)
@@ -2017,15 +2033,22 @@ NamedExpr<out Expression e, bool allowSemi> MatchExpression<out Expression e, bool allowSemi>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
+ bool usesOptionalBrace = false;
.)
"match" (. x = t; .)
Expression<out e, allowSemi>
+ [ "{" (. usesOptionalBrace = true; .)
+ ]
/* Note: The following gives rise to a '"case" is start & successor of deletable structure' error,
but it's okay, because we want this closer match expression to bind as much as possible--use
parens around it to limit its scope. */
{ CaseExpression<out c, allowSemi> (. cases.Add(c); .)
}
- (. e = new MatchExpr(x, e, cases); .)
+ ( IF(CloseOptionalBrace(usesOptionalBrace))
+ "}"
+ | (. if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } .)
+ )
+ (. e = new MatchExpr(x, e, cases, usesOptionalBrace); .)
.
CaseExpression<out MatchCaseExpr c, bool allowSemi>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 44f9742b..ad98a0c0 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -3859,8 +3859,9 @@ namespace Microsoft.Dafny { public readonly Expression Source;
public readonly List<MatchCaseStmt> Cases;
public readonly List<DatatypeCtor> MissingCases = new List<DatatypeCtor>(); // filled in during resolution
+ public readonly bool UsesOptionalBraces;
- public MatchStmt(IToken tok, IToken endTok, Expression source, [Captured] List<MatchCaseStmt> cases)
+ public MatchStmt(IToken tok, IToken endTok, Expression source, [Captured] List<MatchCaseStmt> cases, bool usesOptionalBraces)
: base(tok, endTok) {
Contract.Requires(tok != null);
Contract.Requires(endTok != null);
@@ -3868,6 +3869,7 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(cases));
this.Source = source;
this.Cases = cases;
+ this.UsesOptionalBraces = usesOptionalBraces;
}
public override IEnumerable<Statement> SubStatements {
@@ -4340,7 +4342,7 @@ namespace Microsoft.Dafny { /// Create a match expression with a resolved type
/// </summary>
public static Expression CreateMatch(IToken tok, Expression src, List<MatchCaseExpr> cases, Type type) {
- MatchExpr e = new MatchExpr(tok, src, cases);
+ MatchExpr e = new MatchExpr(tok, src, cases, false);
e.Type = type; // resolve here
return e;
@@ -5562,6 +5564,7 @@ namespace Microsoft.Dafny { public readonly Expression Source;
public readonly List<MatchCaseExpr> Cases;
public readonly List<DatatypeCtor> MissingCases = new List<DatatypeCtor>(); // filled in during resolution
+ public readonly bool UsesOptionalBraces;
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -5570,13 +5573,14 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(MissingCases));
}
- public MatchExpr(IToken tok, Expression source, [Captured] List<MatchCaseExpr> cases)
+ public MatchExpr(IToken tok, Expression source, [Captured] List<MatchCaseExpr> cases, bool usesOptionalBraces)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(source != null);
Contract.Requires(cce.NonNullElements(cases));
this.Source = source;
this.Cases = cases;
+ this.UsesOptionalBraces = usesOptionalBraces;
}
public override IEnumerable<Expression> SubExpressions {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index d0a205df..969774db 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -25,8 +25,9 @@ public class Parser { public const int _lbrace = 9;
public const int _rbrace = 10;
public const int _openparen = 11;
- public const int _star = 12;
- public const int _notIn = 13;
+ public const int _closeparen = 12;
+ public const int _star = 13;
+ public const int _notIn = 14;
public const int maxT = 126;
const bool T = true;
@@ -156,6 +157,14 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { (e is FunctionCallExpr ||
(e is IdentifierSequence && ((IdentifierSequence)e).OpenParen != null));
}
+
+bool CloseOptionalParen(bool usesOptionalParen) {
+ return usesOptionalParen && la.kind == _closeparen;
+}
+
+bool CloseOptionalBrace(bool usesOptionalBrace) {
+ return usesOptionalBrace && la.kind == _rbrace;
+}
/*--------------------------------------------------------------------------*/
@@ -236,7 +245,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { // theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl)
Contract.Assert(defaultModule != null);
- while (la.kind == 14) {
+ while (la.kind == 15) {
Get();
Expect(6);
{
@@ -254,22 +263,22 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { }
while (StartOf(1)) {
switch (la.kind) {
- case 15: case 16: case 18: {
+ case 16: case 17: case 19: {
SubModuleDecl(defaultModule, out submodule);
defaultModule.TopLevelDecls.Add(submodule);
break;
}
- case 23: {
+ case 24: {
ClassDecl(defaultModule, out c);
defaultModule.TopLevelDecls.Add(c);
break;
}
- case 26: case 27: {
+ case 27: case 28: {
DatatypeDecl(defaultModule, out dt);
defaultModule.TopLevelDecls.Add(dt);
break;
}
- case 31: {
+ case 32: {
ArbitraryTypeDecl(defaultModule, out at);
defaultModule.TopLevelDecls.Add(at);
break;
@@ -279,7 +288,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { defaultModule.TopLevelDecls.Add(iter);
break;
}
- case 24: case 25: case 29: case 40: case 41: case 42: case 43: case 44: case 62: case 63: case 64: {
+ case 25: case 26: case 30: case 40: case 41: case 42: case 43: case 44: case 62: case 63: case 64: {
ClassMemberDecl(membersDefaultClass, false);
break;
}
@@ -311,17 +320,17 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { bool isAbstract = false;
bool opened = false;
- if (la.kind == 15 || la.kind == 16) {
- if (la.kind == 15) {
+ if (la.kind == 16 || la.kind == 17) {
+ if (la.kind == 16) {
Get();
isAbstract = true;
}
- Expect(16);
+ Expect(17);
while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 17) {
+ if (la.kind == 18) {
Get();
QualifiedName(out idRefined);
}
@@ -330,22 +339,22 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { module.BodyStartTok = t;
while (StartOf(1)) {
switch (la.kind) {
- case 15: case 16: case 18: {
+ case 16: case 17: case 19: {
SubModuleDecl(module, out sm);
module.TopLevelDecls.Add(sm);
break;
}
- case 23: {
+ case 24: {
ClassDecl(module, out c);
module.TopLevelDecls.Add(c);
break;
}
- case 26: case 27: {
+ case 27: case 28: {
DatatypeDecl(module, out dt);
module.TopLevelDecls.Add(dt);
break;
}
- case 31: {
+ case 32: {
ArbitraryTypeDecl(module, out at);
module.TopLevelDecls.Add(at);
break;
@@ -355,7 +364,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { module.TopLevelDecls.Add(iter);
break;
}
- case 24: case 25: case 29: case 40: case 41: case 42: case 43: case 44: case 62: case 63: case 64: {
+ case 25: case 26: case 30: case 40: case 41: case 42: case 43: case 44: case 62: case 63: case 64: {
ClassMemberDecl(namedModuleDefaultClassMembers, false);
break;
}
@@ -365,22 +374,22 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { module.BodyEndTok = t;
module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
submodule = new LiteralModuleDecl(module, parent);
- } else if (la.kind == 18) {
+ } else if (la.kind == 19) {
Get();
- if (la.kind == 19) {
+ if (la.kind == 20) {
Get();
opened = true;
}
NoUSIdent(out id);
- if (la.kind == 20 || la.kind == 21) {
- if (la.kind == 20) {
+ if (la.kind == 21 || la.kind == 22) {
+ if (la.kind == 21) {
Get();
QualifiedName(out idPath);
submodule = new AliasModuleDecl(idPath, id, parent, opened);
} else {
Get();
QualifiedName(out idPath);
- if (la.kind == 22) {
+ if (la.kind == 23) {
Get();
QualifiedName(out idAssignment);
}
@@ -409,8 +418,8 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 23)) {SynErr(129); Get();}
- Expect(23);
+ while (!(la.kind == 0 || la.kind == 24)) {SynErr(129); Get();}
+ Expect(24);
while (la.kind == 9) {
Attribute(ref attrs);
}
@@ -440,10 +449,10 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { IToken bodyStart = Token.NoToken; // dummy assignment
bool co = false;
- while (!(la.kind == 0 || la.kind == 26 || la.kind == 27)) {SynErr(130); Get();}
- if (la.kind == 26) {
+ while (!(la.kind == 0 || la.kind == 27 || la.kind == 28)) {SynErr(130); Get();}
+ if (la.kind == 27) {
Get();
- } else if (la.kind == 27) {
+ } else if (la.kind == 28) {
Get();
co = true;
} else SynErr(131);
@@ -454,10 +463,10 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { if (la.kind == 38) {
GenericParameters(typeArgs);
}
- Expect(20);
+ Expect(21);
bodyStart = t;
DatatypeMemberDecl(ctors);
- while (la.kind == 28) {
+ while (la.kind == 29) {
Get();
DatatypeMemberDecl(ctors);
}
@@ -480,15 +489,15 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { Attributes attrs = null;
var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
- Expect(31);
+ Expect(32);
while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (la.kind == 11) {
Get();
- Expect(32);
Expect(33);
+ Expect(12);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);
@@ -569,8 +578,8 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { Function/*!*/ f;
MemberModifiers mmod = new MemberModifiers();
- while (la.kind == 24 || la.kind == 25) {
- if (la.kind == 24) {
+ while (la.kind == 25 || la.kind == 26) {
+ if (la.kind == 25) {
Get();
mmod.IsGhost = true;
} else {
@@ -578,7 +587,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { mmod.IsStatic = true;
}
}
- if (la.kind == 29) {
+ if (la.kind == 30) {
FieldDecl(mmod, mm);
} else if (la.kind == 62 || la.kind == 63 || la.kind == 64) {
FunctionDecl(mmod, out f);
@@ -669,19 +678,19 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
if (la.kind == 11) {
Get();
- Expect(32);
Expect(33);
+ Expect(12);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
NoUSIdent(out id);
eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
if (la.kind == 11) {
Get();
- Expect(32);
Expect(33);
+ Expect(12);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
@@ -694,8 +703,8 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- while (!(la.kind == 0 || la.kind == 29)) {SynErr(138); Get();}
- Expect(29);
+ while (!(la.kind == 0 || la.kind == 30)) {SynErr(138); Get();}
+ Expect(30);
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
while (la.kind == 9) {
@@ -703,7 +712,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { }
FIdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
FIdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
@@ -984,13 +993,13 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { if (StartOf(9)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
}
}
- Expect(33);
+ Expect(12);
}
void FIdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
@@ -1011,7 +1020,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
isGhost = false;
- if (la.kind == 24) {
+ if (la.kind == 25) {
Get();
if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
}
@@ -1074,7 +1083,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { 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 == 24) {
+ if (la.kind == 25) {
Get();
isGhost = true;
}
@@ -1198,16 +1207,16 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
Expect(11);
openParen = t;
- if (la.kind == 1 || la.kind == 24) {
+ if (la.kind == 1 || la.kind == 25) {
GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
}
}
- Expect(33);
+ Expect(12);
}
void IteratorSpec(List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/*!*/ mod, List<Expression/*!*/> decreases,
@@ -1225,7 +1234,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { if (StartOf(12)) {
FrameExpression(out fe);
reads.Add(fe);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
FrameExpression(out fe);
reads.Add(fe);
@@ -1241,7 +1250,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { if (StartOf(12)) {
FrameExpression(out fe);
mod.Add(fe);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
FrameExpression(out fe);
mod.Add(fe);
@@ -1323,7 +1332,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(12)) {
FrameExpression(out fe);
mod.Add(fe);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
FrameExpression(out fe);
mod.Add(fe);
@@ -1410,7 +1419,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo decreases.Add(e);
}
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
PossiblyWildExpression(out e);
if (!allowWildcard && e is WildcardExpr) {
@@ -1427,7 +1436,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(38);
Type(out ty);
gt.Add(ty);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
Type(out ty);
gt.Add(ty);
@@ -1490,7 +1499,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(17)) {
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
@@ -1528,7 +1537,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
- if (la.kind == 12) {
+ if (la.kind == 13) {
Get();
fe = new FrameExpression(t, new WildcardExpr(t), null);
} else if (StartOf(12)) {
@@ -1539,7 +1548,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 12) {
+ if (la.kind == 13) {
Get();
e = new WildcardExpr(t);
} else if (StartOf(16)) {
@@ -1580,11 +1589,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo PrintStmt(out s);
break;
}
- case 1: case 2: case 3: case 4: case 11: case 28: case 54: case 55: case 113: case 114: case 115: case 116: case 117: case 118: {
+ case 1: case 2: case 3: case 4: case 11: case 29: case 54: case 55: case 113: case 114: case 115: case 116: case 117: case 118: {
UpdateStmt(out s);
break;
}
- case 24: case 29: {
+ case 25: case 30: {
VarDeclStatement(out s);
break;
}
@@ -1708,7 +1717,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
AttributeArg(out arg, false);
args.Add(arg);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
AttributeArg(out arg, false);
args.Add(arg);
@@ -1735,9 +1744,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(8);
endTok = t; rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 30 || la.kind == 69 || la.kind == 71) {
+ } else if (la.kind == 31 || la.kind == 69 || la.kind == 71) {
lhss.Add(e); lhs0 = e;
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
Lhs(out e);
lhss.Add(e);
@@ -1747,7 +1756,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
Rhs(out r, lhs0);
rhss.Add(r);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
Rhs(out r, lhs0);
rhss.Add(r);
@@ -1790,18 +1799,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Attributes attrs = null;
IToken endTok;
- if (la.kind == 24) {
+ if (la.kind == 25) {
Get();
isGhost = true; x = t;
}
- Expect(29);
+ Expect(30);
if (!isGhost) { x = t; }
while (la.kind == 9) {
Attribute(ref attrs);
}
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d); d.Attributes = attrs; attrs = null;
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
while (la.kind == 9) {
Attribute(ref attrs);
@@ -1817,7 +1826,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0);
rhss.Add(r);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
Rhs(out r, lhs0);
rhss.Add(r);
@@ -1954,17 +1963,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void MatchStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
- List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
+ List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
+ bool usesOptionalBrace = false;
+
Expect(82);
x = t;
Expression(out e, true);
- Expect(9);
+ if (la.kind == 9) {
+ Get();
+ usesOptionalBrace = true;
+ }
while (la.kind == 78) {
CaseStatement(out c);
cases.Add(c);
}
- Expect(10);
- s = new MatchStmt(x, t, e, cases);
+ if (CloseOptionalBrace(usesOptionalBrace)) {
+ Expect(10);
+ } else if (StartOf(21)) {
+ if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); }
+ } else SynErr(187);
+ s = new MatchStmt(x, t, e, cases, usesOptionalBrace);
}
void ForallStmt(out Statement/*!*/ s) {
@@ -1989,7 +2007,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
- } else SynErr(187);
+ } else SynErr(188);
if (la.kind == 11) {
Get();
usesOptionalParen = true;
@@ -2003,12 +2021,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (bvars == null) { bvars = new List<BoundVar>(); }
if (range == null) { range = new LiteralExpr(x, true); }
- if (la.kind == 33) {
- Get();
- if (!usesOptionalParen) { SemErr(t, "found but didn't expect a close parenthesis"); }
- } else if (StartOf(21)) {
+ if (CloseOptionalParen(usesOptionalParen)) {
+ Expect(12);
+ } else if (StartOf(22)) {
if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); }
- } else SynErr(188);
+ } else SynErr(189);
while (la.kind == 46 || la.kind == 48) {
isFree = false;
if (la.kind == 46) {
@@ -2051,7 +2068,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(88);
x = t;
- if (StartOf(22)) {
+ if (StartOf(23)) {
CalcOp(out opTok, out calcOp);
maybeOp = calcOp.ResultOp(calcOp); // guard against non-transitive calcOp (like !=)
if (maybeOp == null) {
@@ -2065,7 +2082,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, false);
lines.Add(e); stepOp = calcOp; danglingOperator = null;
Expect(8);
- if (StartOf(22)) {
+ if (StartOf(23)) {
CalcOp(out opTok, out op);
maybeOp = resOp.ResultOp(op);
if (maybeOp == null) {
@@ -2107,11 +2124,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsAttribute()) {
Attribute(ref attrs);
}
- if (StartOf(23)) {
+ if (StartOf(24)) {
if (StartOf(12)) {
FrameExpression(out fe);
mod.Add(fe);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
FrameExpression(out fe);
mod.Add(fe);
@@ -2124,10 +2141,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 9) {
BlockStmt(out body, out bodyStart, out endTok);
} else if (la.kind == 8) {
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(189); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(190); Get();}
Get();
endTok = t;
- } else SynErr(190);
+ } else SynErr(191);
s = new ModifyStmt(tok, endTok, mod, attrs, body);
if (ellipsisToken != null) {
s = new SkeletonStatement(s, ellipsisToken, null);
@@ -2147,11 +2164,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 51) {
Get();
returnTok = t; isYield = true;
- } else SynErr(191);
- if (StartOf(24)) {
+ } else SynErr(192);
+ if (StartOf(25)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
Rhs(out r, null);
rhss.Add(r);
@@ -2178,7 +2195,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;
Ident(out tok);
names.Add(tok);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
Ident(out tok);
names.Add(tok);
@@ -2186,7 +2203,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(69);
Expression(out e, false);
exprs.Add(e);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
Expression(out e, false);
exprs.Add(e);
@@ -2232,7 +2249,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(16)) {
Expressions(args);
}
- Expect(33);
+ Expect(12);
}
}
if (ee != null) {
@@ -2243,13 +2260,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = new TypeRhs(newToken, ty);
}
- } else if (la.kind == 12) {
+ } else if (la.kind == 13) {
Get();
r = new HavocRhs(t);
} else if (StartOf(16)) {
Expression(out e, false);
r = new ExprRhs(e);
- } else SynErr(192);
+ } else SynErr(193);
while (la.kind == 9) {
Attribute(ref attrs);
}
@@ -2264,20 +2281,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
- } else if (StartOf(25)) {
+ } else if (StartOf(26)) {
ConstAtomExpression(out e);
Suffix(ref e);
while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
- } else SynErr(193);
+ } else SynErr(194);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e;
Expression(out e, true);
args.Add(e);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
Expression(out e, true);
args.Add(e);
@@ -2308,18 +2325,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
- if (la.kind == 12) {
+ if (la.kind == 13) {
Get();
e = null;
} else if (IsParenStar()) {
Expect(11);
+ Expect(13);
Expect(12);
- Expect(33);
e = null;
} else if (StartOf(16)) {
Expression(out ee, true);
e = ee;
- } else SynErr(194);
+ } else SynErr(195);
}
void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs) {
@@ -2329,23 +2346,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo decreases = new List<Expression/*!*/>();
mod = null;
- while (StartOf(26)) {
+ while (StartOf(27)) {
if (la.kind == 46 || la.kind == 81) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(195); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(196); Get();}
Expect(8);
invariants.Add(invariant);
} else if (la.kind == 49) {
- while (!(la.kind == 0 || la.kind == 49)) {SynErr(196); Get();}
+ while (!(la.kind == 0 || la.kind == 49)) {SynErr(197); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(197); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(198); Get();}
Expect(8);
} else {
- while (!(la.kind == 0 || la.kind == 45)) {SynErr(198); Get();}
+ while (!(la.kind == 0 || la.kind == 45)) {SynErr(199); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -2354,13 +2371,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(12)) {
FrameExpression(out fe);
mod.Add(fe);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
FrameExpression(out fe);
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(199); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(200); Get();}
Expect(8);
}
}
@@ -2368,7 +2385,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Invariant(out MaybeFreeExpression/*!*/ invariant) {
bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null;
- while (!(la.kind == 0 || la.kind == 46 || la.kind == 81)) {SynErr(200); Get();}
+ while (!(la.kind == 0 || la.kind == 46 || la.kind == 81)) {SynErr(201); Get();}
if (la.kind == 46) {
Get();
isFree = true;
@@ -2395,12 +2412,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
}
- Expect(33);
+ Expect(12);
}
Expect(79);
while (StartOf(14)) {
@@ -2417,7 +2434,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(16)) {
Expression(out e, allowSemi);
arg = new Attributes.Argument(t, e);
- } else SynErr(201);
+ } else SynErr(202);
}
void QuantifierDomain(out List<BoundVar> bvars, out Attributes attrs, out Expression range) {
@@ -2428,7 +2445,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
bvars.Add(bv);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
IdentTypeOptional(out bv);
bvars.Add(bv);
@@ -2436,7 +2453,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsAttribute()) {
Attribute(ref attrs);
}
- if (la.kind == 28) {
+ if (la.kind == 29) {
Get();
Expression(out range, true);
}
@@ -2448,7 +2465,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = null;
switch (la.kind) {
- case 32: {
+ case 33: {
Get();
x = t; binOp = BinaryExpr.Opcode.Eq;
if (la.kind == 89) {
@@ -2514,7 +2531,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; binOp = BinaryExpr.Opcode.Exp;
break;
}
- default: SynErr(202); break;
+ default: SynErr(203); break;
}
if (k == null) {
op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
@@ -2551,7 +2568,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 97) {
Get();
- } else SynErr(203);
+ } else SynErr(204);
}
void ImpliesOp() {
@@ -2559,7 +2576,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 99) {
Get();
- } else SynErr(204);
+ } else SynErr(205);
}
void ExpliesOp() {
@@ -2567,7 +2584,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 101) {
Get();
- } else SynErr(205);
+ } else SynErr(206);
}
void EquivExpression(out Expression e0, bool allowSemi) {
@@ -2584,7 +2601,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ImpliesExpliesExpression(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0, allowSemi);
- if (StartOf(27)) {
+ if (StartOf(28)) {
if (la.kind == 98 || la.kind == 99) {
ImpliesOp();
x = t;
@@ -2608,7 +2625,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void LogicalExpression(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0, allowSemi);
- if (StartOf(28)) {
+ if (StartOf(29)) {
if (la.kind == 102 || la.kind == 103) {
AndOp();
x = t;
@@ -2662,7 +2679,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Term(out e0, allowSemi);
e = e0;
- if (StartOf(29)) {
+ if (StartOf(30)) {
RelOp(out x, out op, out k);
firstOpTok = x;
Term(out e1, allowSemi);
@@ -2675,7 +2692,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new TernaryExpr(x, op == BinaryExpr.Opcode.Eq ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp, k, e0, e1);
}
- while (StartOf(29)) {
+ while (StartOf(30)) {
if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -2752,7 +2769,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 103) {
Get();
- } else SynErr(206);
+ } else SynErr(207);
}
void OrOp() {
@@ -2760,7 +2777,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 105) {
Get();
- } else SynErr(207);
+ } else SynErr(208);
}
void Term(out Expression e0, bool allowSemi) {
@@ -2780,7 +2797,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo k = null;
switch (la.kind) {
- case 32: {
+ case 33: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
if (la.kind == 89) {
@@ -2827,7 +2844,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 13: {
+ case 14: {
Get();
x = t; op = BinaryExpr.Opcode.NotIn;
break;
@@ -2865,14 +2882,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(208); break;
+ default: SynErr(209); break;
}
}
void Factor(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0, allowSemi);
- while (la.kind == 12 || la.kind == 110 || la.kind == 111) {
+ while (la.kind == 13 || la.kind == 110 || la.kind == 111) {
MulOp(out x, out op);
UnaryExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2887,7 +2904,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 109) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(209);
+ } else SynErr(210);
}
void UnaryExpression(out Expression e, bool allowSemi) {
@@ -2907,7 +2924,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 24: case 29: case 56: case 66: case 72: case 76: case 82: case 83: case 85: case 88: case 121: case 122: case 123: {
+ case 25: case 30: case 56: case 66: case 72: case 76: case 82: case 83: case 85: case 88: case 121: case 122: case 123: {
EndlessExpression(out e, allowSemi);
break;
}
@@ -2942,25 +2959,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
} else if (la.kind == 1) {
MapComprehensionExpr(x, out e, allowSemi);
- } else if (StartOf(30)) {
+ } else if (StartOf(31)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(210);
+ } else SynErr(211);
break;
}
- case 2: case 3: case 4: case 11: case 28: case 54: case 55: case 113: case 114: case 115: case 116: case 117: case 118: {
+ case 2: case 3: case 4: case 11: case 29: case 54: case 55: case 113: case 114: case 115: case 116: case 117: case 118: {
ConstAtomExpression(out e);
while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
break;
}
- default: SynErr(211); break;
+ default: SynErr(212); break;
}
}
void MulOp(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 == 12) {
+ if (la.kind == 13) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
} else if (la.kind == 110) {
@@ -2969,7 +2986,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 111) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(212);
+ } else SynErr(213);
}
void NegOp() {
@@ -2977,7 +2994,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 112) {
Get();
- } else SynErr(213);
+ } else SynErr(214);
}
void EndlessExpression(out Expression e, bool allowSemi) {
@@ -3016,7 +3033,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new StmtExpr(s.Tok, s, e);
break;
}
- case 24: case 29: {
+ case 25: case 30: {
LetExpr(out e, allowSemi);
break;
}
@@ -3024,7 +3041,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo NamedExpr(out e, allowSemi);
break;
}
- default: SynErr(214); break;
+ default: SynErr(215); break;
}
}
@@ -3056,7 +3073,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(16)) {
Expressions(args);
}
- Expect(33);
+ Expect(12);
}
e = new IdentifierSequence(idents, openParen, args);
}
@@ -3090,7 +3107,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(16)) {
Expressions(args);
}
- Expect(33);
+ Expect(12);
e = new FunctionCallExpr(id, id.val, e, openParen, args);
}
if (!func) { e = new ExprDotName(id, e, id.val); }
@@ -3127,8 +3144,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- } else if (la.kind == 30 || la.kind == 75) {
- while (la.kind == 30) {
+ } else if (la.kind == 31 || la.kind == 75) {
+ while (la.kind == 31) {
Get();
Expression(out ee, true);
if (multipleIndices == null) {
@@ -3138,7 +3155,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee);
}
- } else SynErr(215);
+ } else SynErr(216);
} else if (la.kind == 120) {
Get();
anyDots = true;
@@ -3146,7 +3163,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out ee, true);
e1 = ee;
}
- } else SynErr(216);
+ } else SynErr(217);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -3187,7 +3204,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(75);
- } else SynErr(217);
+ } else SynErr(218);
}
void DisplayExpr(out Expression e) {
@@ -3211,7 +3228,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new SeqDisplayExpr(x, elements);
Expect(75);
- } else SynErr(218);
+ } else SynErr(219);
}
void MultiSetExpr(out Expression e) {
@@ -3234,10 +3251,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; elements = new List<Expression/*!*/>();
Expression(out e, true);
e = new MultiSetFormingExpr(x, e);
- Expect(33);
- } else if (StartOf(31)) {
+ Expect(12);
+ } else if (StartOf(32)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(219);
+ } else SynErr(220);
}
void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {
@@ -3262,7 +3279,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
bvars.Add(bv);
- if (la.kind == 28) {
+ if (la.kind == 29) {
Get();
Expression(out range, true);
}
@@ -3313,7 +3330,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
Expect(11);
Expression(out e, true);
- Expect(33);
+ Expect(12);
e = new FreshExpr(x, e);
break;
}
@@ -3322,16 +3339,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
Expect(11);
Expression(out e, true);
- Expect(33);
+ Expect(12);
e = new OldExpr(x, e);
break;
}
- case 28: {
+ case 29: {
Get();
x = t;
Expression(out e, true);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
- Expect(28);
+ Expect(29);
break;
}
case 11: {
@@ -3339,7 +3356,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
Expression(out e, true);
e = new ParensExpression(x, e);
- Expect(33);
+ Expect(12);
break;
}
case 55: {
@@ -3348,7 +3365,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(11);
IToken openParen = t;
Expression(out e, true);
- Expect(33);
+ Expect(12);
IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";
//e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
@@ -3362,7 +3379,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(11);
IToken openParen = t;
Expression(out e, true);
- Expect(33);
+ Expect(12);
IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";
//e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
@@ -3370,7 +3387,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break;
}
- default: SynErr(220); break;
+ default: SynErr(221); break;
}
}
@@ -3395,7 +3412,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo n = BigInteger.Zero;
}
- } else SynErr(221);
+ } else SynErr(222);
}
void Dec(out Basetypes.BigDec d) {
@@ -3417,7 +3434,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(69);
Expression(out r, true);
elements.Add(new ExpressionPair(d,r));
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
Expression(out d, true);
Expect(69);
@@ -3431,21 +3448,31 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 125) {
Get();
- } else SynErr(222);
+ } else SynErr(223);
}
void MatchExpression(out Expression e, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
+ bool usesOptionalBrace = false;
Expect(82);
x = t;
Expression(out e, allowSemi);
+ if (la.kind == 9) {
+ Get();
+ usesOptionalBrace = true;
+ }
while (la.kind == 78) {
CaseExpression(out c, allowSemi);
cases.Add(c);
}
- e = new MatchExpr(x, e, cases);
+ if (CloseOptionalBrace(usesOptionalBrace)) {
+ Expect(10);
+ } else if (StartOf(31)) {
+ if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); }
+ } else SynErr(224);
+ e = new MatchExpr(x, e, cases, usesOptionalBrace);
}
void QuantifierGuts(out Expression q, bool allowSemi) {
@@ -3462,7 +3489,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 122 || la.kind == 123) {
Exists();
x = t;
- } else SynErr(223);
+ } else SynErr(225);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body, allowSemi);
@@ -3486,12 +3513,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
IdentTypeOptional(out bv);
bvars.Add(bv);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
IdentTypeOptional(out bv);
bvars.Add(bv);
}
- Expect(28);
+ Expect(29);
Expression(out range, allowSemi);
if (la.kind == 124 || la.kind == 125) {
QSep();
@@ -3510,7 +3537,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s);
} else if (la.kind == 88) {
CalcStmt(out s);
- } else SynErr(224);
+ } else SynErr(226);
}
void LetExpr(out Expression e, bool allowSemi) {
@@ -3522,17 +3549,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo bool exact = true;
e = dummyExpr;
- if (la.kind == 24) {
+ if (la.kind == 25) {
Get();
isGhost = true; x = t;
}
- Expect(29);
+ Expect(30);
if (!isGhost) { x = t; }
CasePattern(out pat);
if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); }
letLHSs.Add(pat);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
CasePattern(out pat);
if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); }
@@ -3550,10 +3577,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- } else SynErr(225);
+ } else SynErr(227);
Expression(out e, false);
letRHSs.Add(e);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
Expression(out e, false);
letRHSs.Add(e);
@@ -3589,19 +3616,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) {
CasePattern(out pat);
arguments.Add(pat);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
CasePattern(out pat);
arguments.Add(pat);
}
}
- Expect(33);
+ Expect(12);
pat = new CasePattern(id, id.val, arguments);
} else if (la.kind == 1) {
IdentTypeOptional(out bv);
pat = new CasePattern(bv.tok, bv);
- } else SynErr(226);
+ } else SynErr(228);
}
void CaseExpression(out MatchCaseExpr c, bool allowSemi) {
@@ -3617,12 +3644,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
}
- Expect(33);
+ Expect(12);
}
Expect(79);
Expression(out body, allowSemi);
@@ -3634,7 +3661,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 121) {
Get();
- } else SynErr(227);
+ } else SynErr(229);
}
void Exists() {
@@ -3642,7 +3669,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 123) {
Get();
- } else SynErr(228);
+ } else SynErr(230);
}
void AttributeBody(ref Attributes attrs) {
@@ -3653,10 +3680,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(7);
Expect(1);
aName = t.val;
- if (StartOf(32)) {
+ if (StartOf(33)) {
AttributeArg(out aArg, true);
aArgs.Add(aArg);
- while (la.kind == 30) {
+ while (la.kind == 31) {
Get();
AttributeArg(out aArg, true);
aArgs.Add(aArg);
@@ -3678,39 +3705,40 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
static readonly bool[,]/*!*/ set = {
- {T,T,T,T, T,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,T, T,T,x,x, x,x,T,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,T,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {T,T,T,T, T,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, T,T,T,x, x,x,T,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,T,T,T, T,x,T,x, T,x,T,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, 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, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,T, T,x,T,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, T,T,x,T, x,x,x,x, T,T,T,T, T,x,T,x, T,x,T,x, x,x,T,x, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,T,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, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, 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,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, 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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {T,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,T,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
- {x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, 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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {T,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,T,T, 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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,T,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,T,T, 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,T,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,T,x, T,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,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,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, 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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,T, x,T,T,x, T,x,x,T, T,T,T,T, 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, T,T,x,x},
- {x,T,T,T, T,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,T, x,x,T,T, x,x,x,x, x,T,x,x, x,T,T,T, x,T,T,x, T,x,T,T, T,T,T,T, 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, T,T,x,x},
- {x,T,T,T, T,x,T,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x}
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,T, T,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,T, x,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,T, x,T,T,x, T,x,x,T, T,T,T,T, 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, T,T,x,x},
+ {x,T,T,T, T,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,T, x,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,T, x,x,T,T, x,x,x,x, x,T,x,x, x,T,T,T, x,T,T,x, T,x,T,T, T,T,T,T, 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, T,T,x,x},
+ {x,T,T,T, T,x,T,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x}
};
} // end Parser
@@ -3747,28 +3775,28 @@ public class Errors { case 9: s = "lbrace expected"; break;
case 10: s = "rbrace expected"; break;
case 11: s = "openparen expected"; break;
- case 12: s = "star expected"; break;
- case 13: s = "notIn expected"; break;
- case 14: s = "\"include\" expected"; break;
- case 15: s = "\"abstract\" expected"; break;
- case 16: s = "\"module\" expected"; break;
- case 17: s = "\"refines\" expected"; break;
- case 18: s = "\"import\" expected"; break;
- case 19: s = "\"opened\" expected"; break;
- case 20: s = "\"=\" expected"; break;
- case 21: s = "\"as\" expected"; break;
- case 22: s = "\"default\" expected"; break;
- case 23: s = "\"class\" expected"; break;
- case 24: s = "\"ghost\" expected"; break;
- case 25: s = "\"static\" expected"; break;
- case 26: s = "\"datatype\" expected"; break;
- case 27: s = "\"codatatype\" expected"; break;
- case 28: s = "\"|\" expected"; break;
- case 29: s = "\"var\" expected"; break;
- case 30: s = "\",\" expected"; break;
- case 31: s = "\"type\" expected"; break;
- case 32: s = "\"==\" expected"; break;
- case 33: s = "\")\" expected"; break;
+ case 12: s = "closeparen expected"; break;
+ case 13: s = "star expected"; break;
+ case 14: s = "notIn expected"; break;
+ case 15: s = "\"include\" expected"; break;
+ case 16: s = "\"abstract\" expected"; break;
+ case 17: s = "\"module\" expected"; break;
+ case 18: s = "\"refines\" expected"; break;
+ case 19: s = "\"import\" expected"; break;
+ case 20: s = "\"opened\" expected"; break;
+ case 21: s = "\"=\" expected"; break;
+ case 22: s = "\"as\" expected"; break;
+ case 23: s = "\"default\" expected"; break;
+ case 24: s = "\"class\" expected"; break;
+ case 25: s = "\"ghost\" expected"; break;
+ case 26: s = "\"static\" expected"; break;
+ case 27: s = "\"datatype\" expected"; break;
+ case 28: s = "\"codatatype\" expected"; break;
+ case 29: s = "\"|\" expected"; break;
+ case 30: s = "\"var\" expected"; break;
+ case 31: s = "\",\" expected"; break;
+ case 32: s = "\"type\" expected"; break;
+ case 33: s = "\"==\" expected"; break;
case 34: s = "\"iterator\" expected"; break;
case 35: s = "\"yields\" expected"; break;
case 36: s = "\"returns\" expected"; break;
@@ -3922,48 +3950,50 @@ public class Errors { case 184: s = "invalid IfStmt"; break;
case 185: s = "invalid WhileStmt"; break;
case 186: s = "invalid WhileStmt"; break;
- case 187: s = "invalid ForallStmt"; break;
+ case 187: s = "invalid MatchStmt"; break;
case 188: s = "invalid ForallStmt"; break;
- case 189: s = "this symbol not expected in ModifyStmt"; break;
- case 190: s = "invalid ModifyStmt"; break;
- case 191: s = "invalid ReturnStmt"; break;
- case 192: s = "invalid Rhs"; break;
- case 193: s = "invalid Lhs"; break;
- case 194: s = "invalid Guard"; break;
- case 195: s = "this symbol not expected in LoopSpec"; break;
+ case 189: s = "invalid ForallStmt"; break;
+ case 190: s = "this symbol not expected in ModifyStmt"; break;
+ case 191: s = "invalid ModifyStmt"; break;
+ case 192: s = "invalid ReturnStmt"; break;
+ case 193: s = "invalid Rhs"; break;
+ case 194: s = "invalid Lhs"; break;
+ case 195: s = "invalid Guard"; break;
case 196: s = "this symbol not expected in LoopSpec"; break;
case 197: s = "this symbol not expected in LoopSpec"; break;
case 198: s = "this symbol not expected in LoopSpec"; break;
case 199: s = "this symbol not expected in LoopSpec"; break;
- case 200: s = "this symbol not expected in Invariant"; break;
- case 201: s = "invalid AttributeArg"; break;
- case 202: s = "invalid CalcOp"; break;
- case 203: s = "invalid EquivOp"; break;
- case 204: s = "invalid ImpliesOp"; break;
- case 205: s = "invalid ExpliesOp"; break;
- case 206: s = "invalid AndOp"; break;
- case 207: s = "invalid OrOp"; break;
- case 208: s = "invalid RelOp"; break;
- case 209: s = "invalid AddOp"; break;
- case 210: s = "invalid UnaryExpression"; break;
+ case 200: s = "this symbol not expected in LoopSpec"; break;
+ case 201: s = "this symbol not expected in Invariant"; break;
+ case 202: s = "invalid AttributeArg"; break;
+ case 203: s = "invalid CalcOp"; break;
+ case 204: s = "invalid EquivOp"; break;
+ case 205: s = "invalid ImpliesOp"; break;
+ case 206: s = "invalid ExpliesOp"; break;
+ case 207: s = "invalid AndOp"; break;
+ case 208: s = "invalid OrOp"; break;
+ case 209: s = "invalid RelOp"; break;
+ case 210: s = "invalid AddOp"; break;
case 211: s = "invalid UnaryExpression"; break;
- case 212: s = "invalid MulOp"; break;
- case 213: s = "invalid NegOp"; break;
- case 214: s = "invalid EndlessExpression"; break;
- case 215: s = "invalid Suffix"; break;
+ case 212: s = "invalid UnaryExpression"; break;
+ case 213: s = "invalid MulOp"; break;
+ case 214: s = "invalid NegOp"; break;
+ case 215: s = "invalid EndlessExpression"; break;
case 216: s = "invalid Suffix"; break;
case 217: s = "invalid Suffix"; break;
- case 218: s = "invalid DisplayExpr"; break;
- case 219: s = "invalid MultiSetExpr"; break;
- case 220: s = "invalid ConstAtomExpression"; break;
- case 221: s = "invalid Nat"; break;
- case 222: s = "invalid QSep"; 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 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 QSep"; 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;
+ case 229: s = "invalid Forall"; break;
+ case 230: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 8239fb75..0a970498 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -790,9 +790,12 @@ namespace Microsoft.Dafny { MatchStmt s = (MatchStmt)stmt;
wr.Write("match ");
PrintExpression(s.Source, false);
- wr.WriteLine(" {");
- int caseInd = indent + IndentAmount;
+ if (s.UsesOptionalBraces) {
+ wr.Write(" {");
+ }
+ int caseInd = indent + (s.UsesOptionalBraces ? IndentAmount : 0);
foreach (MatchCaseStmt mc in s.Cases) {
+ wr.WriteLine();
Indent(caseInd);
wr.Write("case {0}", mc.Id);
if (mc.Arguments.Count != 0) {
@@ -803,15 +806,18 @@ namespace Microsoft.Dafny { }
wr.Write(")");
}
- wr.WriteLine(" =>");
+ wr.Write(" =>");
foreach (Statement bs in mc.Body) {
+ wr.WriteLine();
Indent(caseInd + IndentAmount);
PrintStatement(bs, caseInd + IndentAmount);
- wr.WriteLine();
}
}
- Indent(indent);
- wr.Write("}");
+ if (s.UsesOptionalBraces) {
+ wr.WriteLine();
+ Indent(indent);
+ wr.Write("}");
+ }
} else if (stmt is ConcreteUpdateStatement) {
var s = (ConcreteUpdateStatement)stmt;
@@ -1083,15 +1089,18 @@ namespace Microsoft.Dafny { } else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
Indent(indent);
- var parensNeeded = !isRightmost;
+ var parensNeeded = !isRightmost && !e.UsesOptionalBraces;
if (parensNeeded) { wr.Write("("); }
wr.Write("match ");
PrintExpression(e.Source, isRightmost && e.Cases.Count == 0, false);
- if (parensNeeded && e.Cases.Count == 0) { wr.WriteLine(")"); } else { wr.WriteLine(); }
+ if (e.UsesOptionalBraces) { wr.WriteLine(" {"); }
+ else if (parensNeeded && e.Cases.Count == 0) { wr.WriteLine(")"); }
+ else { wr.WriteLine(); }
int i = 0;
+ int ind = indent + (e.UsesOptionalBraces ? IndentAmount : 0);
foreach (var mc in e.Cases) {
bool isLastCase = i == e.Cases.Count - 1;
- Indent(indent);
+ Indent(ind);
wr.Write("case {0}", mc.Id);
if (mc.Arguments.Count != 0) {
string sep = "(";
@@ -1102,9 +1111,13 @@ namespace Microsoft.Dafny { wr.Write(")");
}
wr.WriteLine(" =>");
- PrintExtendedExpr(mc.Body, indent + IndentAmount, isLastCase, isLastCase && (parensNeeded || endWithCloseParen));
+ PrintExtendedExpr(mc.Body, ind + IndentAmount, isLastCase, isLastCase && (parensNeeded || endWithCloseParen));
i++;
}
+ if (e.UsesOptionalBraces) {
+ Indent(indent);
+ wr.WriteLine("}");
+ }
} else if (expr is ParensExpression) {
PrintExtendedExpr(((ParensExpression)expr).E, indent, isRightmost, endWithCloseParen);
} else {
@@ -1636,10 +1649,11 @@ namespace Microsoft.Dafny { } else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
- var parensNeeded = !isRightmost;
+ var parensNeeded = !isRightmost && !e.UsesOptionalBraces;
if (parensNeeded) { wr.Write("("); }
wr.Write("match ");
PrintExpression(e.Source, isRightmost && e.Cases.Count == 0, !parensNeeded && isFollowedBySemicolon);
+ if (e.UsesOptionalBraces) { wr.Write(" {"); }
int i = 0;
foreach (var mc in e.Cases) {
bool isLastCase = i == e.Cases.Count - 1;
@@ -1656,7 +1670,8 @@ namespace Microsoft.Dafny { PrintExpression(mc.Body, isRightmost && isLastCase, !parensNeeded && isFollowedBySemicolon);
i++;
}
- if (parensNeeded) { wr.Write(")"); }
+ if (e.UsesOptionalBraces) { wr.Write(" }"); }
+ else if (parensNeeded) { wr.Write(")"); }
} else if (expr is BoxingCastExpr) {
// this is not expected for a parsed program, but we may be called for /trace purposes in the translator
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a194390c..8de010fb 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1331,7 +1331,7 @@ namespace Microsoft.Dafny } else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
return new MatchExpr(e.tok, CloneExpr(e.Source),
- e.Cases.ConvertAll(c => new MatchCaseExpr(c.tok, c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))));
+ e.Cases.ConvertAll(c => new MatchCaseExpr(c.tok, c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))), e.UsesOptionalBraces);
} else if (expr is NegationExpression) {
var e = (NegationExpression)expr;
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 4b473e9d..87dee5aa 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -255,21 +255,21 @@ public class Scanner { for (int i = 92; i <= 92; ++i) start[i] = 1;
for (int i = 95; i <= 95; ++i) start[i] = 1;
for (int i = 98; i <= 122; ++i) start[i] = 1;
- for (int i = 49; i <= 57; ++i) start[i] = 21;
+ for (int i = 49; i <= 57; ++i) start[i] = 22;
for (int i = 34; i <= 34; ++i) start[i] = 11;
- start[97] = 22;
- start[48] = 23;
+ start[97] = 23;
+ start[48] = 24;
start[58] = 64;
start[59] = 13;
start[123] = 14;
start[125] = 15;
start[40] = 16;
- start[42] = 17;
+ start[41] = 17;
+ start[42] = 18;
start[33] = 65;
start[61] = 66;
start[124] = 67;
- start[44] = 30;
- start[41] = 31;
+ start[44] = 31;
start[46] = 68;
start[60] = 69;
start[62] = 70;
@@ -491,21 +491,21 @@ public class Scanner { void CheckLiteral() {
switch (t.val) {
- case "include": t.kind = 14; break;
- case "abstract": t.kind = 15; break;
- case "module": t.kind = 16; break;
- case "refines": t.kind = 17; break;
- case "import": t.kind = 18; break;
- case "opened": t.kind = 19; break;
- case "as": t.kind = 21; break;
- case "default": t.kind = 22; break;
- case "class": t.kind = 23; break;
- case "ghost": t.kind = 24; break;
- case "static": t.kind = 25; break;
- case "datatype": t.kind = 26; break;
- case "codatatype": t.kind = 27; break;
- case "var": t.kind = 29; break;
- case "type": t.kind = 31; break;
+ case "include": t.kind = 15; break;
+ case "abstract": t.kind = 16; break;
+ case "module": t.kind = 17; break;
+ case "refines": t.kind = 18; break;
+ case "import": t.kind = 19; break;
+ case "opened": t.kind = 20; break;
+ case "as": t.kind = 22; break;
+ case "default": t.kind = 23; break;
+ case "class": t.kind = 24; break;
+ case "ghost": t.kind = 25; break;
+ case "static": t.kind = 26; break;
+ case "datatype": t.kind = 27; break;
+ case "codatatype": t.kind = 28; break;
+ case "var": t.kind = 30; break;
+ case "type": t.kind = 32; break;
case "iterator": t.kind = 34; break;
case "yields": t.kind = 35; break;
case "returns": t.kind = 36; break;
@@ -648,65 +648,65 @@ public class Scanner { case 17:
{t.kind = 12; break;}
case 18:
- if (ch == 'n') {AddCh(); goto case 19;}
- else {goto case 0;}
+ {t.kind = 13; break;}
case 19:
- if (ch <= '&' || ch >= '(' && ch <= '/' || ch >= ':' && ch <= '>' || ch == '@' || ch == '[' || ch >= ']' && ch <= '^' || ch == '`' || ch >= '{' && ch <= 65535) {apx++; AddCh(); goto case 20;}
+ if (ch == 'n') {AddCh(); goto case 20;}
else {goto case 0;}
case 20:
+ if (ch <= '&' || ch >= '(' && ch <= '/' || ch >= ':' && ch <= '>' || ch == '@' || ch == '[' || ch >= ']' && ch <= '^' || ch == '`' || ch >= '{' && ch <= 65535) {apx++; AddCh(); goto case 21;}
+ else {goto case 0;}
+ case 21:
{
tlen -= apx;
SetScannerBehindT();
- t.kind = 13; break;}
- case 21:
+ t.kind = 14; break;}
+ case 22:
recEnd = pos; recKind = 2;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 21;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 22;}
else if (ch == '.') {AddCh(); goto case 9;}
else {t.kind = 2; break;}
- case 22:
+ case 23:
recEnd = pos; recKind = 1;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'q' || ch >= 's' && ch <= 'z') {AddCh(); goto case 2;}
- else if (ch == 'r') {AddCh(); goto case 25;}
+ else if (ch == 'r') {AddCh(); goto case 26;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 23:
+ case 24:
recEnd = pos; recKind = 2;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 21;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 22;}
else if (ch == 'x') {AddCh(); goto case 7;}
else if (ch == '.') {AddCh(); goto case 9;}
else {t.kind = 2; break;}
- case 24:
+ case 25:
recEnd = pos; recKind = 1;
- if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 24;}
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 25;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 25:
+ case 26:
recEnd = pos; recKind = 1;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'q' || ch >= 's' && ch <= 'z') {AddCh(); goto case 3;}
- else if (ch == 'r') {AddCh(); goto case 26;}
+ else if (ch == 'r') {AddCh(); goto case 27;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 26:
+ case 27:
recEnd = pos; recKind = 1;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'b' && ch <= 'z') {AddCh(); goto case 4;}
- else if (ch == 'a') {AddCh(); goto case 27;}
+ else if (ch == 'a') {AddCh(); goto case 28;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 27:
+ case 28:
recEnd = pos; recKind = 1;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'x' || ch == 'z') {AddCh(); goto case 5;}
- else if (ch == 'y') {AddCh(); goto case 28;}
+ else if (ch == 'y') {AddCh(); goto case 29;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 28:
+ case 29:
recEnd = pos; recKind = 5;
if (ch == 39 || ch == '0' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 6;}
- else if (ch >= '1' && ch <= '9') {AddCh(); goto case 29;}
+ else if (ch >= '1' && ch <= '9') {AddCh(); goto case 30;}
else {t.kind = 5; break;}
- case 29:
+ case 30:
recEnd = pos; recKind = 5;
- if (ch == 39 || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 24;}
- else if (ch >= '0' && ch <= '9') {AddCh(); goto case 29;}
+ if (ch == 39 || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 25;}
+ else if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;}
else {t.kind = 5; break;}
- case 30:
- {t.kind = 30; break;}
case 31:
- {t.kind = 33; break;}
+ {t.kind = 31; break;}
case 32:
{t.kind = 37; break;}
case 33:
@@ -780,18 +780,18 @@ public class Scanner { else {t.kind = 7; break;}
case 65:
recEnd = pos; recKind = 107;
- if (ch == 'i') {AddCh(); goto case 18;}
+ if (ch == 'i') {AddCh(); goto case 19;}
else if (ch == '=') {AddCh(); goto case 41;}
else {t.kind = 107; break;}
case 66:
- recEnd = pos; recKind = 20;
+ recEnd = pos; recKind = 21;
if (ch == '=') {AddCh(); goto case 71;}
else if (ch == '>') {AddCh(); goto case 38;}
- else {t.kind = 20; break;}
+ else {t.kind = 21; break;}
case 67:
- recEnd = pos; recKind = 28;
+ recEnd = pos; recKind = 29;
if (ch == '|') {AddCh(); goto case 53;}
- else {t.kind = 28; break;}
+ else {t.kind = 29; break;}
case 68:
recEnd = pos; recKind = 61;
if (ch == '.') {AddCh(); goto case 72;}
@@ -805,9 +805,9 @@ public class Scanner { if (ch == '=') {AddCh(); goto case 40;}
else {t.kind = 39; break;}
case 71:
- recEnd = pos; recKind = 32;
+ recEnd = pos; recKind = 33;
if (ch == '>') {AddCh(); goto case 47;}
- else {t.kind = 32; break;}
+ else {t.kind = 33; break;}
case 72:
recEnd = pos; recKind = 120;
if (ch == '.') {AddCh(); goto case 32;}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 81e603c7..e2e7155d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -11002,7 +11002,7 @@ namespace Microsoft.Dafny { cases.Add(newCaseExpr);
}
if (anythingChanged) {
- var newME = new MatchExpr(expr.tok, src, cases);
+ var newME = new MatchExpr(expr.tok, src, cases, e.UsesOptionalBraces);
newME.MissingCases.AddRange(e.MissingCases);
newExpr = newME;
}
@@ -11287,7 +11287,7 @@ namespace Microsoft.Dafny { r = rr;
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
- var rr = new MatchStmt(s.Tok, s.EndTok, Substitute(s.Source), s.Cases.ConvertAll(SubstMatchCaseStmt));
+ var rr = new MatchStmt(s.Tok, s.EndTok, Substitute(s.Source), s.Cases.ConvertAll(SubstMatchCaseStmt), s.UsesOptionalBraces);
rr.MissingCases.AddRange(s.MissingCases);
r = rr;
} else if (stmt is AssignSuchThatStmt) {
diff --git a/Test/dafny0/MatchBraces.dfy b/Test/dafny0/MatchBraces.dfy new file mode 100644 index 00000000..7da3647d --- /dev/null +++ b/Test/dafny0/MatchBraces.dfy @@ -0,0 +1,147 @@ +// RUN: %dafny /print:"%t.print" /env:0 /dprint:- "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Color = Red | Green | Blue
+
+// ----- match expressions in general positions
+
+method M(c: Color, d: Color) {
+ var x := match c
+ case Red => 5
+ case Green => 7
+ case Blue => 11;
+ var y := match c
+ case Red => 0.3
+ case Green => (match d case Red => 0.18 case Green => 0.21 case Blue => 0.98)
+ case Blue => 98.0;
+ var z := match c
+ case Red => Green
+ case Green => match d {
+ case Red => Red
+ case Green => Blue
+ case Blue => Red
+ }
+ case Blue => Green;
+ var w := match c { case Red => 2 case Green => 3 case Blue => 4 } + 10;
+ var t := match c
+ case Red => 0
+ case Green => (match d {
+ case Red => 2
+ case Green => 2
+ case Blue => 1
+ } + (((match d case Red => 10 case Green => 8 case Blue => 5))))
+ case Blue => (match d {
+ case Red => 20
+ case Green => 20
+ case Blue => 10
+ } + (((match d case Red => 110 case Green => 108 case Blue => 105))));
+}
+
+// ----- match expressions in top-level positions
+
+function Heat(c: Color): int
+{
+ match c
+ case Red => 10
+ case Green => 12
+ case Blue => 14
+}
+
+function IceCream(c: Color): int
+{
+ match c {
+ case Red => 0
+ case Green => 4
+ case Blue => 1
+ }
+}
+
+function Flowers(c: Color, d: Color): int
+{
+ match c {
+ case Red =>
+ match d {
+ case Red => 0
+ case Green => 1
+ case Blue => 2
+ }
+ case Green =>
+ match d {
+ case Red => 3
+ case Green => 3
+ case Blue => 2
+ } + 20
+ case Blue =>
+ match d {
+ case Red => 9
+ case Green => 8
+ case Blue => 7
+ } +
+ ((match d case Red => 23 case Green => 29 case Blue => 31))
+ }
+}
+
+// ----- match statements
+
+method P(c: Color, d: Color) {
+ var x: int;
+ match c {
+ case Red =>
+ x := 20;
+ case Green =>
+ case Blue =>
+ }
+ match c
+ case Red =>
+ match d {
+ case Red =>
+ case Green =>
+ case Blue =>
+ }
+ case Green =>
+ var y := 25;
+ var z := y + 3;
+ case Blue =>
+ {
+ var y := 25;
+ var z := y + 3;
+ }
+ match d // note: this 'match' is part of the previous case
+ case Red =>
+ case Green =>
+ x := x + 1;
+ case Blue =>
+}
+
+lemma HeatIsEven(c: Color)
+ ensures Heat(c) % 2 == 0;
+{
+ match c
+ case Red =>
+ assert 10 % 2 == 0;
+ case Green =>
+ assert 12 % 2 == 0;
+ case Blue => // all looks nice, huh? :)
+ // obvious
+}
+
+method DegenerateExamples(c: Color)
+ requires Heat(c) == 10; // this implies c == Red
+{
+ match c
+ case Red =>
+ case Green =>
+ match c { }
+ case Blue =>
+ match c
+}
+
+method MoreDegenerateExamples(c: Color)
+ requires Heat(c) == 10; // this implies c == Red
+{
+ if c == Green {
+ var x: int := match c;
+ var y: int := match c {};
+ var z := match c case Blue => 4;
+ }
+}
diff --git a/Test/dafny0/MatchBraces.dfy.expect b/Test/dafny0/MatchBraces.dfy.expect new file mode 100644 index 00000000..dfe1215f --- /dev/null +++ b/Test/dafny0/MatchBraces.dfy.expect @@ -0,0 +1,121 @@ +// MatchBraces.dfy
+
+datatype Color = Red | Green | Blue
+
+method M(c: Color, d: Color)
+{
+ var x := match c case Red => 5 case Green => 7 case Blue => 11;
+ var y := match c case Red => 0.3 case Green => (match d case Red => 0.18 case Green => 0.21 case Blue => 0.98) case Blue => 98.0;
+ var z := match c case Red => Green case Green => match d { case Red => Red case Green => Blue case Blue => Red } case Blue => Green;
+ var w := match c { case Red => 2 case Green => 3 case Blue => 4 } + 10;
+ var t := match c case Red => 0 case Green => match d { case Red => 2 case Green => 2 case Blue => 1 } + (match d case Red => 10 case Green => 8 case Blue => 5) case Blue => match d { case Red => 20 case Green => 20 case Blue => 10 } + match d case Red => 110 case Green => 108 case Blue => 105;
+}
+
+function Heat(c: Color): int
+{
+ match c
+ case Red =>
+ 10
+ case Green =>
+ 12
+ case Blue =>
+ 14
+}
+
+function IceCream(c: Color): int
+{
+ match c {
+ case Red =>
+ 0
+ case Green =>
+ 4
+ case Blue =>
+ 1
+ }
+}
+
+function Flowers(c: Color, d: Color): int
+{
+ match c {
+ case Red =>
+ match d {
+ case Red =>
+ 0
+ case Green =>
+ 1
+ case Blue =>
+ 2
+ }
+ case Green =>
+ match d { case Red => 3 case Green => 3 case Blue => 2 } + 20
+ case Blue =>
+ match d { case Red => 9 case Green => 8 case Blue => 7 } + match d case Red => 23 case Green => 29 case Blue => 31
+ }
+}
+
+method P(c: Color, d: Color)
+{
+ var x: int;
+ match c {
+ case Red =>
+ x := 20;
+ case Green =>
+ case Blue =>
+ }
+ match c
+ case Red =>
+ match d {
+ case Red =>
+ case Green =>
+ case Blue =>
+ }
+ case Green =>
+ var y := 25;
+ var z := y + 3;
+ case Blue =>
+ {
+ var y := 25;
+ var z := y + 3;
+ }
+ match d
+ case Red =>
+ case Green =>
+ x := x + 1;
+ case Blue =>
+}
+
+lemma HeatIsEven(c: Color)
+ ensures Heat(c) % 2 == 0;
+{
+ match c
+ case Red =>
+ assert 10 % 2 == 0;
+ case Green =>
+ assert 12 % 2 == 0;
+ case Blue =>
+}
+
+method DegenerateExamples(c: Color)
+ requires Heat(c) == 10;
+{
+ match c
+ case Red =>
+ case Green =>
+ match c {
+ }
+ case Blue =>
+ match c
+}
+
+method MoreDegenerateExamples(c: Color)
+ requires Heat(c) == 10;
+{
+ if c == Green {
+ var x: int := match c;
+ var y: int := match c { };
+ var z := match c case Blue => 4;
+ }
+}
+
+Dafny program verifier finished with 13 verified, 0 errors
+Compiled assembly into MatchBraces.dll
|