From e5ab3ec7a78f288f966a2a7767052ef5eff56276 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 10 May 2013 19:55:27 -0700 Subject: Made the semi-colon after "type" and "module" declarations optional. --- Source/Dafny/Dafny.atg | 37 ++++++++--- Source/Dafny/Parser.cs | 167 +++++++++++++++++++++++++----------------------- Source/Dafny/Printer.cs | 8 +-- Source/Dafny/Scanner.cs | 6 +- 4 files changed, 122 insertions(+), 96 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index f3d0449a..ba3a17fb 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -213,16 +213,27 @@ SubModuleDecl "}" (. module.BodyEndTok = t; module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); submodule = new LiteralModuleDecl(module, parent); .) - | + | "import" ["opened" (.opened = true;.)] - ( NoUSIdent ( "=" QualifiedName ";" - (. submodule = new AliasModuleDecl(idPath, id, parent, opened); .) - | ";" - (. idPath = new List(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent, opened); .) - | "as" QualifiedName ["default" QualifiedName ] ";" - (.submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); .) - ) - ) + NoUSIdent + [ "=" QualifiedName + (. submodule = new AliasModuleDecl(idPath, id, parent, opened); .) + | "as" QualifiedName ["default" QualifiedName ] + (. submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); .) + ] + [ SYNC ";" + // This semi-colon used to be required, but it seems silly to have it. + // To stage the transition toward not having it at all, let's make it optional for now. Then, + // in a next big version of Dafny, including the following warning message: + // (. errors.Warning(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .) + // And in a version after that, don't allow the semi-colon at all. + ] + (. if (submodule == null) { + idPath = new List(); + idPath.Add(id); + submodule = new AliasModuleDecl(idPath, id, parent, opened); + } + .) ) . @@ -342,7 +353,13 @@ ArbitraryTypeDecl NoUSIdent [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .) ] (. at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); .) - SYNC ";" + [ SYNC ";" + // This semi-colon used to be required, but it seems silly to have it. + // To stage the transition toward not having it at all, let's make it optional for now. Then, + // in a next big version of Dafny, including the following warning message: + // (. errors.Warning(t, "the semi-colon that used to terminate an arbitrary-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .) + // And in a version after that, don't allow the semi-colon at all. + ] . GIdentType /* isGhost always returns as false if allowGhostKeyword is false */ diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index aecb4ab1..a44680ac 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -332,24 +332,31 @@ bool IsLoopSpecOrAlternative() { opened = true; } NoUSIdent(out id); - if (la.kind == 14) { - Get(); - QualifiedName(out idPath); - Expect(15); - submodule = new AliasModuleDecl(idPath, id, parent, opened); - } else if (la.kind == 15) { - Get(); - idPath = new List(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent, opened); - } else if (la.kind == 16) { - Get(); - QualifiedName(out idPath); - if (la.kind == 17) { + if (la.kind == 14 || la.kind == 15) { + if (la.kind == 14) { Get(); - QualifiedName(out idAssignment); + QualifiedName(out idPath); + submodule = new AliasModuleDecl(idPath, id, parent, opened); + } else { + Get(); + QualifiedName(out idPath); + if (la.kind == 16) { + Get(); + QualifiedName(out idAssignment); + } + submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); } - Expect(15); - submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); - } else SynErr(120); + } + if (la.kind == 17) { + while (!(la.kind == 0 || la.kind == 17)) {SynErr(120); Get();} + Get(); + } + if (submodule == null) { + idPath = new List(); + idPath.Add(id); + submodule = new AliasModuleDecl(idPath, id, parent, opened); + } + } else SynErr(121); } @@ -414,8 +421,8 @@ bool IsLoopSpecOrAlternative() { Get(); DatatypeMemberDecl(ctors); } - if (la.kind == 15) { - while (!(la.kind == 0 || la.kind == 15)) {SynErr(125); Get();} + if (la.kind == 17) { + while (!(la.kind == 0 || la.kind == 17)) {SynErr(125); Get();} Get(); } if (co) { @@ -445,8 +452,10 @@ bool IsLoopSpecOrAlternative() { eqSupport = TypeParameter.EqualitySupportValue.Required; } at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(126); Get();} - Expect(15); + if (la.kind == 17) { + while (!(la.kind == 0 || la.kind == 17)) {SynErr(126); Get();} + Get(); + } } void IteratorDecl(ModuleDefinition module, out IteratorDecl/*!*/ iter) { @@ -622,8 +631,8 @@ bool IsLoopSpecOrAlternative() { IdentType(out id, out ty, false); mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); } - while (!(la.kind == 0 || la.kind == 15)) {SynErr(131); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(131); Get();} + Expect(17); } void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) { @@ -1076,8 +1085,8 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { reads.Add(fe); } } - while (!(la.kind == 0 || la.kind == 15)) {SynErr(141); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(141); Get();} + Expect(17); } else if (la.kind == 40) { Get(); while (IsAttribute()) { @@ -1092,8 +1101,8 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 15)) {SynErr(142); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(142); Get();} + Expect(17); } else if (StartOf(11)) { if (la.kind == 41) { Get(); @@ -1106,8 +1115,8 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { if (la.kind == 42) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(143); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(143); Get();} + Expect(17); if (isYield) { yieldReq.Add(new MaybeFreeExpression(e, isFree)); } else { @@ -1120,8 +1129,8 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Attribute(ref ensAttrs); } Expression(out e); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(144); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(144); Get();} + Expect(17); if (isYield) { yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } else { @@ -1135,8 +1144,8 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Attribute(ref decrAttrs); } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(146); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(146); Get();} + Expect(17); } else SynErr(147); } @@ -1174,8 +1183,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 15)) {SynErr(149); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(149); Get();} + Expect(17); } else if (la.kind == 41 || la.kind == 42 || la.kind == 43) { if (la.kind == 41) { Get(); @@ -1184,8 +1193,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 42) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(150); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(150); Get();} + Expect(17); req.Add(new MaybeFreeExpression(e, isFree)); } else if (la.kind == 43) { Get(); @@ -1193,8 +1202,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Attribute(ref ensAttrs); } Expression(out e); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(151); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(151); Get();} + Expect(17); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } else SynErr(152); } else if (la.kind == 44) { @@ -1203,8 +1212,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Attribute(ref decAttrs); } DecreasesList(decreases, true); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(153); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(153); Get();} + Expect(17); } else SynErr(154); } @@ -1317,8 +1326,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (!(la.kind == 0 || la.kind == 42)) {SynErr(157); Get();} Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(158); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(158); Get();} + Expect(17); reqs.Add(e); } else if (la.kind == 45) { Get(); @@ -1331,13 +1340,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe); } } - while (!(la.kind == 0 || la.kind == 15)) {SynErr(159); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(159); Get();} + Expect(17); } else if (la.kind == 43) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(160); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(160); Get();} + Expect(17); ens.Add(e); } else if (la.kind == 44) { Get(); @@ -1347,8 +1356,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(161); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(161); Get();} + Expect(17); } else SynErr(162); } @@ -1458,14 +1467,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) { NoUSIdent(out id); label = id.val; - } else if (la.kind == 15 || la.kind == 61) { + } else if (la.kind == 17 || la.kind == 61) { while (la.kind == 61) { Get(); breakCount++; } } else SynErr(166); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(167); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(167); Get();} + Expect(17); s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); break; } @@ -1475,7 +1484,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } case 34: { SkeletonStmt(out s); - Expect(15); + Expect(17); break; } default: SynErr(168); break; @@ -1496,7 +1505,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 34) { Get(); } else SynErr(169); - Expect(15); + Expect(17); if (e == null) { s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false); } else { @@ -1525,7 +1534,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s = new AssumeStmt(x, e, attrs); } - Expect(15); + Expect(17); } void PrintStmt(out Statement/*!*/ s) { @@ -1541,7 +1550,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AttributeArg(out arg); args.Add(arg); } - Expect(15); + Expect(17); s = new PrintStmt(x, args); } @@ -1557,11 +1566,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Lhs(out e); x = e.tok; - if (la.kind == 6 || la.kind == 15) { + if (la.kind == 6 || la.kind == 17) { while (la.kind == 6) { Attribute(ref attrs); } - Expect(15); + Expect(17); rhss.Add(new ExprRhs(e, attrs)); } else if (la.kind == 26 || la.kind == 63 || la.kind == 65) { lhss.Add(e); lhs0 = e; @@ -1589,7 +1598,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expression(out suchThat); } else SynErr(171); - Expect(15); + Expect(17); } else if (la.kind == 5) { Get(); SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); @@ -1652,7 +1661,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out suchThat); } } - Expect(15); + Expect(17); ConcreteUpdateStatement update; if (suchThat != null) { var ies = new List(); @@ -1833,7 +1842,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(43); Expression(out e); - Expect(15); + Expect(17); ens.Add(new MaybeFreeExpression(e, isFree)); } BlockStmt(out block, out bodyStart, out bodyEnd); @@ -1868,7 +1877,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(14)) { Expression(out e); lines.Add(e); stepOp = calcOp; - Expect(15); + Expect(17); while (StartOf(20)) { if (StartOf(19)) { CalcOp(out opTok, out op); @@ -1886,7 +1895,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo hints.Add(h); Expression(out e); lines.Add(e); stepOp = calcOp; - Expect(15); + Expect(17); } } Expect(7); @@ -1915,7 +1924,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo rhss.Add(r); } } - Expect(15); + Expect(17); if (isYield) { s = new YieldStmt(returnTok, rhss); } else { @@ -2085,8 +2094,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (StartOf(23)) { if (la.kind == 41 || la.kind == 75) { Invariant(out invariant); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(183); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(183); Get();} + Expect(17); invariants.Add(invariant); } else if (la.kind == 44) { while (!(la.kind == 0 || la.kind == 44)) {SynErr(184); Get();} @@ -2095,8 +2104,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Attribute(ref decAttrs); } DecreasesList(decreases, true); - while (!(la.kind == 0 || la.kind == 15)) {SynErr(185); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(185); Get();} + Expect(17); } else { while (!(la.kind == 0 || la.kind == 40)) {SynErr(186); Get();} Get(); @@ -2113,8 +2122,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 15)) {SynErr(187); Get();} - Expect(15); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(187); Get();} + Expect(17); } } } @@ -2777,7 +2786,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); x = t; Expression(out e0); - Expect(15); + Expect(17); Expression(out e1); e = new AssertExpr(x, e0, e1); break; @@ -2786,7 +2795,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); x = t; Expression(out e0); - Expect(15); + Expect(17); Expression(out e1); e = new AssumeExpr(x, e0, e1); break; @@ -3217,7 +3226,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e); letRHSs.Add(e); } - Expect(15); + Expect(17); Expression(out e); e = new LetExpr(x, letVars, letRHSs, e, exact); } @@ -3310,7 +3319,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } static readonly bool[,]/*!*/ set = { - {T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,T,T, T,T,x,x, T,x,x,T, x,x,T,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,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,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, T,x,T,T, T,T,x,x, T,x,x,T, x,x,T,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,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,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,T,T,x, T,x,x,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,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,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, 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}, @@ -3337,8 +3346,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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, T,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,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,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,x,x,x, x,T,x,T, T,T,x,T, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, T,T,x,x, x,T,T,x, x}, - {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,x,x,x, T,T,x,T, T,T,x,T, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, T,T,x,x, x,T,T,x, x}, + {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,x,x,x, x,T,x,T, T,T,x,T, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, T,T,x,x, x,T,T,x, x}, + {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,x,x,x, T,T,x,T, T,T,x,T, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, T,T,x,x, x,T,T,x, x}, {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,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,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,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} }; @@ -3379,9 +3388,9 @@ public class Errors { case 12: s = "\"import\" expected"; break; case 13: s = "\"opened\" expected"; break; case 14: s = "\"=\" expected"; break; - case 15: s = "\";\" expected"; break; - case 16: s = "\"as\" expected"; break; - case 17: s = "\"default\" expected"; break; + case 15: s = "\"as\" expected"; break; + case 16: s = "\"default\" expected"; break; + case 17: s = "\";\" expected"; break; case 18: s = "\".\" expected"; break; case 19: s = "\"class\" expected"; break; case 20: s = "\"ghost\" expected"; break; @@ -3484,7 +3493,7 @@ public class Errors { case 117: s = "\"::\" expected"; break; case 118: s = "\"\\u2022\" expected"; break; case 119: s = "??? expected"; break; - case 120: s = "invalid SubModuleDecl"; break; + case 120: s = "this symbol not expected in SubModuleDecl"; break; case 121: s = "invalid SubModuleDecl"; break; case 122: s = "this symbol not expected in ClassDecl"; break; case 123: s = "this symbol not expected in DatatypeDecl"; break; diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 2578f0eb..776cf601 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -50,7 +50,7 @@ namespace Microsoft.Dafny { if (at.EqualitySupport == TypeParameter.EqualitySupportValue.Required) { wr.Write("(==)"); } - wr.WriteLine(";"); + wr.WriteLine(); } else if (d is DatatypeDecl) { if (i++ != 0) { wr.WriteLine(); } PrintDatatype((DatatypeDecl)d, indent); @@ -142,11 +142,11 @@ namespace Microsoft.Dafny { } else if (d is AliasModuleDecl) { wr.Write("import"); if (((AliasModuleDecl)d).Opened) wr.Write(" opened"); wr.Write(" {0} ", ((AliasModuleDecl)d).Name); - wr.WriteLine("= {0};", Util.Comma(".", ((AliasModuleDecl)d).Path, id => id.val)); + wr.WriteLine("= {0}", Util.Comma(".", ((AliasModuleDecl)d).Path, id => id.val)); } else if (d is ModuleFacadeDecl) { wr.Write("import"); if (((ModuleFacadeDecl)d).Opened) wr.Write(" opened"); wr.Write(" {0} ", ((ModuleFacadeDecl)d).Name); - wr.WriteLine("as {0};", Util.Comma(".", ((ModuleFacadeDecl)d).Path, id => id.val)); + wr.WriteLine("as {0}", Util.Comma(".", ((ModuleFacadeDecl)d).Path, id => id.val)); } } else { Contract.Assert(false); // unexpected TopLevelDecl @@ -240,7 +240,7 @@ namespace Microsoft.Dafny { } sep = " |"; } - wr.WriteLine(";"); + wr.WriteLine(); } /// diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 84f3f9eb..9526d9fe 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -495,8 +495,8 @@ public class Scanner { case "refines": t.kind = 11; break; case "import": t.kind = 12; break; case "opened": t.kind = 13; break; - case "as": t.kind = 16; break; - case "default": t.kind = 17; break; + case "as": t.kind = 15; break; + case "default": t.kind = 16; break; case "class": t.kind = 19; break; case "ghost": t.kind = 20; break; case "static": t.kind = 21; break; @@ -671,7 +671,7 @@ public class Scanner { else if (ch >= '0' && ch <= '9') {AddCh(); goto case 21;} else {t.kind = 3; break;} case 22: - {t.kind = 15; break;} + {t.kind = 17; break;} case 23: {t.kind = 26; break;} case 24: -- cgit v1.2.3