From 6d32fe37e3d343f9e310eeea193efc8da5982600 Mon Sep 17 00:00:00 2001 From: chmaria Date: Tue, 3 Jun 2014 16:55:05 -0700 Subject: Added support for 'dirty' forall statements. One can now write forall statements without bodies (but with ensures clauses) as follows: forall s | s in S ensures s < 0; where S is set. The ensures clauses are assumed but not checked. --- Source/Dafny/Printer.cs | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'Source/Dafny/Printer.cs') diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index bf9214b9..8239fb75 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -48,7 +48,7 @@ namespace Microsoft.Dafny { Contract.Requires(expr != null); using (var wr = new System.IO.StringWriter()) { var pr = new Printer(wr); - pr.PrintExtendedExpr(expr, 0, true, false); + pr.PrintExtendedExpr(expr, 0, true, false); return wr.ToString(); } } @@ -560,7 +560,7 @@ namespace Microsoft.Dafny { } } - internal void PrintSpec(string kind, List ee, int indent) { + internal void PrintSpec(string kind, List ee, int indent, bool newLine = true) { Contract.Requires(kind != null); Contract.Requires(ee != null); foreach (MaybeFreeExpression e in ee) @@ -577,7 +577,11 @@ namespace Microsoft.Dafny { wr.Write(" "); PrintExpression(e.E, true); - wr.WriteLine(";"); + if (newLine) { + wr.WriteLine(";"); + } else { + wr.Write(";"); + } } } @@ -730,10 +734,12 @@ namespace Microsoft.Dafny { wr.Write(" "); } else { wr.WriteLine(); - PrintSpec("ensures", s.Ens, indent + IndentAmount); + PrintSpec("ensures", s.Ens, indent + IndentAmount, s.Body != null); Indent(indent); } - PrintStatement(s.Body, indent); + if (s.Body != null) { + PrintStatement(s.Body, indent); + } } else if (stmt is ModifyStmt) { var s = (ModifyStmt)stmt; -- cgit v1.2.3 From dfb1a7554e63d76c8c74ffe8da52d68144418238 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 24 Jun 2014 15:09:23 -0700 Subject: Make syntax of "match" expressions and "match" statements the same -- curly braces around the cases are now supported for both and are optional for both --- Source/Dafny/Cloner.cs | 4 +- Source/Dafny/Dafny.atg | 35 ++- Source/Dafny/DafnyAst.cs | 10 +- Source/Dafny/Parser.cs | 536 ++++++++++++++++++++----------------- Source/Dafny/Printer.cs | 39 ++- Source/Dafny/Resolver.cs | 2 +- Source/Dafny/Scanner.cs | 108 ++++---- Source/Dafny/Translator.cs | 4 +- Test/dafny0/MatchBraces.dfy | 147 ++++++++++ Test/dafny0/MatchBraces.dfy.expect | 121 +++++++++ 10 files changed, 673 insertions(+), 333 deletions(-) create mode 100644 Test/dafny0/MatchBraces.dfy create mode 100644 Test/dafny0/MatchBraces.dfy.expect (limited to 'Source/Dafny/Printer.cs') 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 /* null represents demonic-choice */ MatchStmt = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c; - List cases = new List(); .) + List cases = new List(); + bool usesOptionalBrace = false; + .) "match" (. x = t; .) Expression - "{" + [ "{" (. usesOptionalBrace = true; .) + ] { CaseStatement (. 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 = (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); @@ -1436,7 +1451,8 @@ ForallStmt (. if (bvars == null) { bvars = new List(); } 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 MatchExpression = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c; List cases = new List(); + bool usesOptionalBrace = false; .) "match" (. x = t; .) Expression + [ "{" (. 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 (. 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 = (. 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 Cases; public readonly List MissingCases = new List(); // filled in during resolution + public readonly bool UsesOptionalBraces; - public MatchStmt(IToken tok, IToken endTok, Expression source, [Captured] List cases) + public MatchStmt(IToken tok, IToken endTok, Expression source, [Captured] List 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 SubStatements { @@ -4340,7 +4342,7 @@ namespace Microsoft.Dafny { /// Create a match expression with a resolved type /// public static Expression CreateMatch(IToken tok, Expression src, List 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 Cases; public readonly List MissingCases = new List(); // 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 cases) + public MatchExpr(IToken tok, Expression source, [Captured] List 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 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 members = new List(); 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/*!*/ reads, List/*!*/ mod, List 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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 cases = new List(); + List cases = new List(); + 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/*!*/ 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/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (bvars == null) { bvars = new List(); } 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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(); rhss.Add(r); - while (la.kind == 30) { + while (la.kind == 31) { Get(); Rhs(out r, null); rhss.Add(r); @@ -2178,7 +2195,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo names = new List(); exprs = new List(); 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/*!*/ 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/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(16)) { Expressions(args); } - Expect(33); + Expect(12); } } if (ee != null) { @@ -2243,13 +2260,13 @@ List/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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 invariants, out List decreases, out List mod, ref Attributes decAttrs, ref Attributes modAttrs) { @@ -2329,23 +2346,23 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo decreases = new List(); 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/*!*/ 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/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Invariant(out MaybeFreeExpression/*!*/ invariant) { bool isFree = false; Expression/*!*/ e; List ids = new List(); invariant = null; Attributes attrs = null; - while (!(la.kind == 0 || la.kind == 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/*!*/ 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/*!*/ 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 bvars, out Attributes attrs, out Expression range) { @@ -2428,7 +2445,7 @@ List/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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(); ops = new List(); @@ -2752,7 +2769,7 @@ List/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; elements = new List(); 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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() { classTok, fnTok }, openParen, new List() { e }); @@ -3362,7 +3379,7 @@ List/*!*/ 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() { classTok, fnTok }, openParen, new List() { e }); @@ -3370,7 +3387,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break; } - default: SynErr(220); break; + default: SynErr(221); break; } } @@ -3395,7 +3412,7 @@ List/*!*/ 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/*!*/ 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/*!*/ 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 cases = new List(); + 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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 479dac39..e64c0da6 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -10993,7 +10993,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; } @@ -11278,7 +11278,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 -- cgit v1.2.3 From 05bbbcc402870c5064df987d7f14c5b83cece22c Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 27 Jun 2014 18:56:15 -0700 Subject: Added tuples and tuple types. Syntax is the expected one, namely parentheses around a comma-delimited list of expressions or types. Unit and the unit type are denoted (). --- Source/Dafny/Cloner.cs | 3 + Source/Dafny/Compiler.cs | 11 +++- Source/Dafny/Dafny.atg | 83 ++++++++++++++++++------- Source/Dafny/DafnyAst.cs | 98 ++++++++++++++++++++++++++--- Source/Dafny/Parser.cs | 107 ++++++++++++++++++++++++-------- Source/Dafny/Printer.cs | 13 +++- Source/Dafny/Resolver.cs | 4 ++ Test/dafny0/ResolutionErrors.dfy | 31 +++++++++ Test/dafny0/ResolutionErrors.dfy.expect | 8 ++- Test/dafny0/Tuples.dfy | 34 ++++++++++ Test/dafny0/Tuples.dfy.expect | 8 +++ 11 files changed, 342 insertions(+), 58 deletions(-) create mode 100644 Test/dafny0/Tuples.dfy create mode 100644 Test/dafny0/Tuples.dfy.expect (limited to 'Source/Dafny/Printer.cs') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 537dae1d..5b8f8cc5 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -30,6 +30,9 @@ namespace Microsoft.Dafny if (d is ArbitraryTypeDecl) { var dd = (ArbitraryTypeDecl)d; return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, CloneAttributes(dd.Attributes)); + } else if (d is TupleTypeDecl) { + var dd = (TupleTypeDecl)d; + return new TupleTypeDecl(dd.Dims, dd.Module); } else if (d is IndDatatypeDecl) { var dd = (IndDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 56c6edc2..fcf8a2ca 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -107,6 +107,10 @@ namespace Microsoft.Dafny { indent += IndentAmount; } foreach (TopLevelDecl d in m.TopLevelDecls) { + bool compileIt = true; + if (Attributes.ContainsBool(d.Attributes, "compile", ref compileIt) && !compileIt) { + continue; + } wr.WriteLine(); if (d is ArbitraryTypeDecl) { var at = (ArbitraryTypeDecl)d; @@ -411,7 +415,12 @@ namespace Microsoft.Dafny { if (dt is IndDatatypeDecl) { Indent(ind); wr.WriteLine("public override string ToString() {"); - string nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName; + string nm; + if (dt is TupleTypeDecl) { + nm = ""; + } else { + nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName; + } Indent(ind + IndentAmount); wr.WriteLine("string s = \"{0}\";", nm); if (ctor.Formals.Count != 0) { Indent(ind + IndentAmount); wr.WriteLine("s += \"(\";"); diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 2ab70c4f..5c1148c6 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -739,8 +739,9 @@ Type TypeAndToken . TypeAndToken -= (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ - List/*!*/ gt; += (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); + tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ + List gt; .) ( "bool" (. tok = t; .) | "nat" (. tok = t; ty = new NatType(); .) @@ -774,6 +775,20 @@ TypeAndToken ty = new MapType(gt[0], gt[1]); } .) + | "(" (. tok = t; gt = new List(); .) + [ Type (. gt.Add(ty); .) + { "," Type (. gt.Add(ty); .) + } + ] + ")" (. if (gt.Count == 1) { + // just return the type 'ty' + } else { + // make sure the nullary tuple type exists + var dims = gt.Count; + var tmp = theBuiltIns.TupleType(tok, dims, true); + ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List()); + } + .) | ReferenceType ) . @@ -1876,25 +1891,51 @@ ConstAtomExpression | "|" (. x = t; .) Expression (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .) "|" - | "(" (. x = t; .) - Expression (. e = new ParensExpression(x, e); .) - ")" - | "real" (. x = t; .) - "(" (. IToken openParen = t; .) - Expression - ")" (. 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() { classTok, fnTok }, openParen, new List() { e }); - e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List() { e }); - .) - | "int" (. x = t; .) - "(" (. IToken openParen = t; .) - Expression - ")" (. 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() { classTok, fnTok }, openParen, new List() { e }); - e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List() { e }); - .) + | ParensExpression + | "real" (. x = t; .) + "(" (. IToken openParen = t; .) + Expression + ")" (. 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() { classTok, fnTok }, openParen, new List() { e }); + e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List() { e }); + .) + | "int" (. x = t; .) + "(" (. IToken openParen = t; .) + Expression + ")" (. 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() { classTok, fnTok }, openParen, new List() { e }); + e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List() { e }); + .) + ) + . +ParensExpression += (. IToken x; + List args = null; + .) + "(" (. x = t; e = null; .) + ( ")" (. // unit + // make sure the nullary tuple type exists + var tmp = theBuiltIns.TupleType(x, 0, true); + e = new DatatypeValue(x, BuiltIns.TupleTypeName(0), BuiltIns.TupleTypeCtorName, new List()); + .) + | Expression + { "," (. if (args == null) { + args = new List(); + args.Add(e); // add the first argument, which was parsed above + } + .) + Expression (. args.Add(e); .) + } + ")" (. if (args == null) { + e = new ParensExpression(x, e); + } else { + // make sure the corresponding tuple type exists + var tmp = theBuiltIns.TupleType(x, args.Count, true); + e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args); + } + .) ) . DisplayExpr diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index ad98a0c0..55dc973f 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -88,15 +88,17 @@ namespace Microsoft.Dafny { { public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, null, true); Dictionary arrayTypeDecls = new Dictionary(); + Dictionary tupleTypeDecls = new Dictionary(); public readonly ClassDecl ObjectDecl; public readonly ClassDecl RealClass; //public readonly Function RealToInt; //public readonly Function IntToReal; public BuiltIns() { // create class 'object' - ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List(), new List(), null); + ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List(), new List(), DontCompile()); SystemModule.TopLevelDecls.Add(ObjectDecl); // add one-dimensional arrays, since they may arise during type checking + // Arrays of other dimensions may be added during parsing as the parser detects the need for these UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true); // add real number functions Function RealToInt = new Function(Token.NoToken, "RealToInt", true, true, new List(), Token.NoToken, @@ -108,12 +110,19 @@ namespace Microsoft.Dafny { new List(), new List(), new Specification(new List(), null), null, null, Token.NoToken); RealClass = new ClassDecl(Token.NoToken, "Real", SystemModule, new List(), - new List() { RealToInt, IntToReal }, null); + new List() { RealToInt, IntToReal }, DontCompile()); RealToInt.EnclosingClass = RealClass; IntToReal.EnclosingClass = RealClass; RealToInt.IsBuiltin = true; IntToReal.IsBuiltin = true; SystemModule.TopLevelDecls.Add(RealClass); + // Note, in addition to these types, the _System module contains tuple types. These tuple types are added to SystemModule + // by the parser as the parser detects the need for these. + } + + private Attributes DontCompile() { + var flse = new Attributes.Argument(Token.NoToken, Expression.CreateBoolLiteral(Token.NoToken, false)); + return new Attributes("compile", new List() { flse }, null); } public UserDefinedType ArrayType(int dims, Type arg) { @@ -129,7 +138,7 @@ namespace Microsoft.Dafny { typeArgs.Add(arg); UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs, null); if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) { - ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule); + ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule, DontCompile()); for (int d = 0; d < dims; d++) { string name = dims == 1 ? "Length" : "Length" + d; string compiledName = dims == 1 ? "Length" : "GetLength(" + d + ")"; @@ -152,6 +161,30 @@ namespace Microsoft.Dafny { return "array" + dims; } } + + public TupleTypeDecl TupleType(IToken tok, int dims, bool allowCreationOfNewType) { + Contract.Requires(tok != null); + Contract.Requires(0 <= dims); + Contract.Ensures(Contract.Result() != null); + + TupleTypeDecl tt; + if (!tupleTypeDecls.TryGetValue(dims, out tt)) { + Contract.Assume(allowCreationOfNewType); // the parser should ensure that all needed tuple types exist by the time of resolution + tt = new TupleTypeDecl(dims, SystemModule); + tupleTypeDecls.Add(dims, tt); + SystemModule.TopLevelDecls.Add(tt); + } + return tt; + } + public static string TupleTypeName(int dims) { + Contract.Requires(0 <= dims); + return "_tuple#" + dims; + } + public static bool IsTupleTypeName(string s) { + Contract.Requires(s != null); + return s.StartsWith("_tuple#"); + } + public const string TupleTypeCtorName = "_#Make"; // the printer wants this name to be uniquely recognizable } public class Attributes { @@ -714,6 +747,9 @@ namespace Microsoft.Dafny { [Pure] public override string TypeName(ModuleDefinition context) { Contract.Ensures(Contract.Result() != null); + if (BuiltIns.IsTupleTypeName(Name)) { + return "(" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ")"; + } string s = ""; foreach (var t in Path) { if (context != null && t == context.tok) { @@ -1355,10 +1391,10 @@ namespace Microsoft.Dafny { public class ArrayClassDecl : ClassDecl { public readonly int Dims; - public ArrayClassDecl(int dims, ModuleDefinition module) + public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs) : base(Token.NoToken, BuiltIns.ArrayClassName(dims), module, new List(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}), - new List(), null) + new List(), attrs) { Contract.Requires(1 <= dims); Contract.Requires(module != null); @@ -1367,7 +1403,8 @@ namespace Microsoft.Dafny { } } - public abstract class DatatypeDecl : TopLevelDecl { + public abstract class DatatypeDecl : TopLevelDecl + { public readonly List Ctors; [ContractInvariantMethod] void ObjectInvariant() { @@ -1413,6 +1450,52 @@ namespace Microsoft.Dafny { } } + public class TupleTypeDecl : IndDatatypeDecl + { + public readonly int Dims; + /// + /// Construct a resolved built-in tuple type with "dim" arguments. "systemModule" is expected to be the _System module. + /// + public TupleTypeDecl(int dims, ModuleDefinition systemModule) + : this(systemModule, CreateTypeParameters(dims)) { + Contract.Requires(0 <= dims); + Contract.Requires(systemModule != null); + } + private TupleTypeDecl(ModuleDefinition systemModule, List typeArgs) + : base(Token.NoToken, BuiltIns.TupleTypeName(typeArgs.Count), systemModule, typeArgs, CreateConstructors(typeArgs), null) { + Contract.Requires(systemModule != null); + Contract.Requires(typeArgs != null); + Dims = typeArgs.Count; + foreach (var ctor in Ctors) { + ctor.EnclosingDatatype = this; // resolve here + DefaultCtor = ctor; + TypeParametersUsedInConstructionByDefaultCtor = new bool[typeArgs.Count]; + for (int i = 0; i < typeArgs.Count; i++) { + TypeParametersUsedInConstructionByDefaultCtor[i] = true; + } + } + } + private static List CreateTypeParameters(int dims) { + Contract.Requires(0 <= dims); + var ts = new List(); + for (int i = 0; i < dims; i++) { + ts.Add(new TypeParameter(Token.NoToken, "T" + i)); + } + return ts; + } + private static List CreateConstructors(List typeArgs) { + Contract.Requires(typeArgs != null); + var formals = new List(); + for (int i = 0; i < typeArgs.Count; i++) { + var tp = typeArgs[i]; + var f = new Formal(Token.NoToken, i.ToString(), new UserDefinedType(Token.NoToken, tp.Name, tp), true, false); + formals.Add(f); + } + var ctor = new DatatypeCtor(Token.NoToken, BuiltIns.TupleTypeCtorName, formals, null); + return new List() { ctor }; + } + } + public class CoDatatypeDecl : DatatypeDecl { public CoDatatypeDecl SscRepr; // filled in during resolution @@ -1918,7 +2001,7 @@ namespace Microsoft.Dafny { } return UniqueName; } - static char[] specialChars = new char[] { '\'', '_', '?', '\\' }; + static char[] specialChars = new char[] { '\'', '_', '?', '\\', '#' }; public static string CompilerizeName(string nm) { if ('0' <= nm[0] && nm[0] <= '9') { // the identifier is one that consists of just digits @@ -1942,6 +2025,7 @@ namespace Microsoft.Dafny { case '_': name += "__"; break; case '?': name += "_q"; break; case '\\': name += "_b"; break; + case '#': name += "_h"; break; default: Contract.Assume(false); // unexpected character break; diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 969774db..a7f058db 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1115,8 +1115,9 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } void TypeAndToken(out IToken/*!*/ tok, out Type/*!*/ ty) { - Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ - List/*!*/ gt; + Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); + tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ + List gt; switch (la.kind) { case 52: { @@ -1195,6 +1196,30 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { break; } + case 11: { + Get(); + tok = t; gt = new List(); + if (StartOf(10)) { + Type(out ty); + gt.Add(ty); + while (la.kind == 31) { + Get(); + Type(out ty); + gt.Add(ty); + } + } + Expect(12); + if (gt.Count == 1) { + // just return the type 'ty' + } else { + // make sure the nullary tuple type exists + var dims = gt.Count; + var tmp = theBuiltIns.TupleType(tok, dims, true); + ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List()); + } + + break; + } case 1: case 5: case 60: { ReferenceType(out tok, out ty); break; @@ -3352,11 +3377,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break; } case 11: { - Get(); - x = t; - Expression(out e, true); - e = new ParensExpression(x, e); - Expect(12); + ParensExpression(out e); break; } case 55: { @@ -3427,6 +3448,41 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } + void ParensExpression(out Expression e) { + IToken x; + List args = null; + + Expect(11); + x = t; e = null; + if (la.kind == 12) { + Get(); + var tmp = theBuiltIns.TupleType(x, 0, true); + e = new DatatypeValue(x, BuiltIns.TupleTypeName(0), BuiltIns.TupleTypeCtorName, new List()); + + } else if (StartOf(16)) { + Expression(out e, true); + while (la.kind == 31) { + Get(); + if (args == null) { + args = new List(); + args.Add(e); // add the first argument, which was parsed above + } + + Expression(out e, true); + args.Add(e); + } + Expect(12); + if (args == null) { + e = new ParensExpression(x, e); + } else { + // make sure the corresponding tuple type exists + var tmp = theBuiltIns.TupleType(x, args.Count, true); + e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args); + } + + } else SynErr(223); + } + void MapLiteralExpressions(out List elements) { Expression/*!*/ d, r; elements = new List(); @@ -3448,7 +3504,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 125) { Get(); - } else SynErr(223); + } else SynErr(224); } void MatchExpression(out Expression e, bool allowSemi) { @@ -3471,7 +3527,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(10); } else if (StartOf(31)) { if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } - } else SynErr(224); + } else SynErr(225); e = new MatchExpr(x, e, cases, usesOptionalBrace); } @@ -3489,7 +3545,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 122 || la.kind == 123) { Exists(); x = t; - } else SynErr(225); + } else SynErr(226); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body, allowSemi); @@ -3537,7 +3593,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s); } else if (la.kind == 88) { CalcStmt(out s); - } else SynErr(226); + } else SynErr(227); } void LetExpr(out Expression e, bool allowSemi) { @@ -3577,7 +3633,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } - } else SynErr(227); + } else SynErr(228); Expression(out e, false); letRHSs.Add(e); while (la.kind == 31) { @@ -3628,7 +3684,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv); pat = new CasePattern(bv.tok, bv); - } else SynErr(228); + } else SynErr(229); } void CaseExpression(out MatchCaseExpr c, bool allowSemi) { @@ -3661,7 +3717,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 121) { Get(); - } else SynErr(229); + } else SynErr(230); } void Exists() { @@ -3669,7 +3725,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 123) { Get(); - } else SynErr(230); + } else SynErr(231); } void AttributeBody(ref Attributes attrs) { @@ -3714,8 +3770,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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, 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}, + {x,T,T,x, x,T,x,x, x,x,x,T, 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,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,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, 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}, @@ -3986,14 +4042,15 @@ public class Errors { 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; + case 223: s = "invalid ParensExpression"; break; + case 224: s = "invalid QSep"; break; + case 225: s = "invalid MatchExpression"; break; + case 226: s = "invalid QuantifierGuts"; break; + case 227: s = "invalid StmtInExpr"; break; + case 228: s = "invalid LetExpr"; break; + case 229: s = "invalid CasePattern"; break; + case 230: s = "invalid Forall"; break; + case 231: s = "invalid Exists"; break; default: s = "error " + n; break; } diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 0a970498..5be5614d 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1191,9 +1191,16 @@ namespace Microsoft.Dafny { wr.Write(((IdentifierExpr)expr).Name); } else if (expr is DatatypeValue) { - DatatypeValue dtv = (DatatypeValue)expr; - wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName); - if (dtv.Arguments.Count != 0) { + var dtv = (DatatypeValue)expr; + bool printParens; + if (dtv.MemberName == BuiltIns.TupleTypeCtorName) { + // we're looking at a tuple, whose printed constructor name is essentially the empty string + printParens = true; + } else { + wr.Write("{0}.{1}", dtv.DatatypeName, dtv.MemberName); + printParens = dtv.Arguments.Count != 0; + } + if (printParens) { wr.Write("("); PrintExpressionList(dtv.Arguments, false); wr.Write(")"); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 8de010fb..73925aef 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -197,6 +197,7 @@ namespace Microsoft.Dafny rewriters.Add(opaqueRewriter); systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false); + prog.CompileModules.Add(prog.BuiltIns.SystemModule); foreach (var decl in sortedDecls) { if (decl is LiteralModuleDecl) { // The declaration is a literal module, so it has members and such that we need @@ -1019,6 +1020,9 @@ namespace Microsoft.Dafny if (d is ArbitraryTypeDecl) { var dd = (ArbitraryTypeDecl)d; return new ArbitraryTypeDecl(dd.tok, dd.Name, m, dd.EqualitySupport, null); + } else if (d is TupleTypeDecl) { + var dd = (TupleTypeDecl)d; + return new TupleTypeDecl(dd.Dims, dd.Module); } else if (d is IndDatatypeDecl) { var dd = (IndDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index f3297ed7..35c17112 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -912,3 +912,34 @@ method DirtyM(S: set) { forall s | s in S ensures s < 0; assert s < 0; // error: s is unresolved } + +// ------------------- tuples ------------------- + +method TupleResolution(x: int, y: int, r: real) +{ + var unit: () := (); + var expr: int := (x); + var pair: (int,int) := (x, x); + var triple: (int,int,int) := (y, x, x); + var badTriple: (int,real,int) := (y, x, r); // error: parameters 1 and 2 have the wrong types + var quadruple: (int,real,int,real) := (y, r, x); // error: trying to use a triple as a quadruple + + assert unit == (); + assert pair.0 == pair.1; + assert triple.2 == x; + + assert triple.2; // error: 2 has type int, not the expected bool + assert triple.3 == pair.x; // error(s): 3 and x are not destructors + + var k0 := (5, (true, 2, 3.14)); + var k1 := (((false, 10, 2.7)), 100, 120); + if k0.1 == k1.0 { + assert false; + } else if k0.1.1 < k1.0.1 { + assert k1.2 == 120; + } + + // int and (int) are the same type (i.e., there are no 1-tuples) + var pp: (int) := x; + var qq: int := pp; +} diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 2c0664d9..22f3274e 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -133,4 +133,10 @@ ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only i ResolutionErrors.dfy(546,18): Error: unresolved identifier: w ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses ResolutionErrors.dfy(913,9): Error: unresolved identifier: s -135 resolution/type errors detected in ResolutionErrors.dfy +ResolutionErrors.dfy(924,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int)) +ResolutionErrors.dfy(925,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real)) +ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, but is int +ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3 +ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2 +ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int)) +141 resolution/type errors detected in ResolutionErrors.dfy diff --git a/Test/dafny0/Tuples.dfy b/Test/dafny0/Tuples.dfy new file mode 100644 index 00000000..81d054dd --- /dev/null +++ b/Test/dafny0/Tuples.dfy @@ -0,0 +1,34 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method M(x: int) +{ + var unit := (); + var expr := (x); + var pair := (x, x); + var triple := (x, x, x); +} + +method N(x: int, y: int) +{ + var unit: () := (); + var expr: int := (x); + var pair: (int,int) := (x, x); + var triple: (int,int,int) := (y, x, x); + + assert unit == (); + assert pair.0 == pair.1; + assert triple.2 == x; + assert triple.0 == triple.1; // error: they may be different + + var k := (24, 100 / y); // error: possible division by zero + assert 2 <= k.0 < 29; + + var k0 := (5, (true, 2, 3.14)); + var k1 := (((false, 10, 2.7)), 100, 120); + if k0.1 == k1.0 { + assert false; + } else if k0.1.1 < k1.0.1 { + assert k1.2 == 120; + } +} diff --git a/Test/dafny0/Tuples.dfy.expect b/Test/dafny0/Tuples.dfy.expect new file mode 100644 index 00000000..13c706d3 --- /dev/null +++ b/Test/dafny0/Tuples.dfy.expect @@ -0,0 +1,8 @@ +Tuples.dfy(22,19): Error: assertion violation +Execution trace: + (0,0): anon0 +Tuples.dfy(24,21): Error: possible division by zero +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 3 verified, 2 errors -- cgit v1.2.3