From 8bf9d3f838df8e8e42f496d9de5468e2946bd5e4 Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 15 Mar 2012 17:10:20 -0700 Subject: Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr; --- Dafny/Compiler.cs | 39 +-- Dafny/Dafny.atg | 32 +- Dafny/DafnyAst.cs | 38 ++- Dafny/Parser.cs | 683 +++++++++++++++++++++-------------------- Dafny/Printer.cs | 47 +-- Dafny/RefinementTransformer.cs | 6 +- Dafny/Resolver.cs | 170 +++++----- Dafny/Rewriter.cs | 4 +- Dafny/Scanner.cs | 175 +++++------ Dafny/Translator.cs | 19 ++ Test/dafny0/Answer | 123 +++++++- Test/dafny0/SmallTests.dfy | 68 ++++ 12 files changed, 837 insertions(+), 567 deletions(-) diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index d5b15300..454b47be 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -710,40 +710,11 @@ namespace Microsoft.Dafny { Contract.Requires(stmt != null); if (stmt is AssumeStmt) { Error("an assume statement cannot be compiled (line {0})", stmt.Tok.line); - } else if (stmt is BlockStmt) { - foreach (Statement s in ((BlockStmt)stmt).Body) { - CheckHasNoAssumes(s); - } - } else if (stmt is IfStmt) { - IfStmt s = (IfStmt)stmt; - CheckHasNoAssumes(s.Thn); - if (s.Els != null) { - CheckHasNoAssumes(s.Els); - } - } else if (stmt is AlternativeStmt) { - foreach (var alternative in ((AlternativeStmt)stmt).Alternatives) { - foreach (Statement s in alternative.Body) { - CheckHasNoAssumes(s); - } - } - } else if (stmt is WhileStmt) { - WhileStmt s = (WhileStmt)stmt; - CheckHasNoAssumes(s.Body); - } else if (stmt is AlternativeLoopStmt) { - foreach (var alternative in ((AlternativeLoopStmt)stmt).Alternatives) { - foreach (Statement s in alternative.Body) { - CheckHasNoAssumes(s); - } - } - } else if (stmt is ParallelStmt) { - var s = (ParallelStmt)stmt; - CheckHasNoAssumes(s.Body); - } else if (stmt is MatchStmt) { - MatchStmt s = (MatchStmt)stmt; - foreach (MatchCaseStmt mc in s.Cases) { - foreach (Statement bs in mc.Body) { - CheckHasNoAssumes(bs); - } + } else if (stmt is AssignSuchThatStmt) { + Error("an assign-such-that statement cannot be compiled (line {0})", stmt.Tok.line); + } else { + foreach (var ss in stmt.SubStatements) { + CheckHasNoAssumes(ss); } } } diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 740926e5..c6609b4c 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -712,6 +712,7 @@ UpdateStmt Expression lhs0; IToken x; Attributes attrs = null; + Expression suchThat = null; .) Lhs (. x = e.tok; .) ( { Attribute } @@ -719,14 +720,22 @@ UpdateStmt | (. lhss.Add(e); lhs0 = e; .) { "," Lhs (. lhss.Add(e); .) } - ":=" (. x = t; .) - Rhs (. rhss.Add(r); .) - { "," Rhs (. rhss.Add(r); .) - } + ( ":=" (. x = t; .) + Rhs (. rhss.Add(r); .) + { "," Rhs (. rhss.Add(r); .) + } + | ":|" (. x = t; .) + Expression + ) ";" | ":" (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .) ) - (. s = new UpdateStmt(x, lhss, rhss); .) + (. if (suchThat != null) { + s = new AssignSuchThatStmt(x, lhss, suchThat); + } else { + s = new UpdateStmt(x, lhss, rhss); + } + .) . Rhs = (. IToken/*!*/ x, newToken; Expression/*!*/ e; @@ -770,6 +779,7 @@ VarDeclStatement<.out Statement/*!*/ s.> AssignmentRhs r; IdentifierExpr lhs0; List lhss = new List(); List rhss = new List(); + Expression suchThat = null; .) [ "ghost" (. isGhost = true; x = t; .) ] @@ -785,10 +795,18 @@ VarDeclStatement<.out Statement/*!*/ s.> Rhs (. rhss.Add(r); .) { "," Rhs (. rhss.Add(r); .) } + | ":|" (. assignTok = t; .) + Expression ] ";" - (. UpdateStmt update; - if (rhss.Count == 0) { + (. ConcreteUpdateStatement update; + if (suchThat != null) { + var ies = new List(); + foreach (var lhs in lhss) { + ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name)); + } + update = new AssignSuchThatStmt(assignTok, ies, suchThat); + } else if (rhss.Count == 0) { update = null; } else { var ies = new List(); diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 407966bb..f5955d11 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -1562,13 +1562,13 @@ namespace Microsoft.Dafny { public class VarDeclStmt : ConcreteSyntaxStatement { public readonly List Lhss; - public readonly UpdateStmt Update; + public readonly ConcreteUpdateStatement Update; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(Lhss)); } - public VarDeclStmt(IToken tok, List lhss, UpdateStmt update) + public VarDeclStmt(IToken tok, List lhss, ConcreteUpdateStatement update) : base(tok) { Contract.Requires(lhss != null); @@ -1578,9 +1578,35 @@ namespace Microsoft.Dafny { } } - public class UpdateStmt : ConcreteSyntaxStatement + /// + /// Common superclass of UpdateStmt and AssignSuchThatStmt. + /// + public abstract class ConcreteUpdateStatement : ConcreteSyntaxStatement { public readonly List Lhss; + public ConcreteUpdateStatement(IToken tok, List lhss) + : base(tok) { + Contract.Requires(tok != null); + Contract.Requires(cce.NonNullElements(lhss)); + Lhss = lhss; + } + } + + public class AssignSuchThatStmt : ConcreteUpdateStatement + { + public readonly AssumeStmt Assume; + public AssignSuchThatStmt(IToken tok, List lhss, Expression expr) + : base(tok, lhss) { + Contract.Requires(tok != null); + Contract.Requires(cce.NonNullElements(lhss)); + Contract.Requires(lhss.Count != 0); + Contract.Requires(expr != null); + Assume = new AssumeStmt(tok, expr); + } + } + + public class UpdateStmt : ConcreteUpdateStatement + { public readonly List Rhss; public readonly bool CanMutateKnownState; [ContractInvariantMethod] @@ -1589,24 +1615,22 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(Rhss)); } public UpdateStmt(IToken tok, List lhss, List rhss) - : base(tok) + : base(tok, lhss) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(lhss)); Contract.Requires(cce.NonNullElements(rhss)); Contract.Requires(lhss.Count != 0 || rhss.Count == 1); - Lhss = lhss; Rhss = rhss; CanMutateKnownState = false; } public UpdateStmt(IToken tok, List lhss, List rhss, bool mutate) - : base(tok) + : base(tok, lhss) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(lhss)); Contract.Requires(cce.NonNullElements(rhss)); Contract.Requires(lhss.Count != 0 || rhss.Count == 1); - Lhss = lhss; Rhss = rhss; CanMutateKnownState = mutate; } diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index bf7d1fe1..8e0d2e31 100644 --- a/Dafny/Parser.cs +++ b/Dafny/Parser.cs @@ -21,7 +21,7 @@ public class Parser { public const int _colon = 5; public const int _lbrace = 6; public const int _rbrace = 7; - public const int maxT = 105; + public const int maxT = 106; const bool T = true; const bool x = false; @@ -259,7 +259,7 @@ bool IsAttribute() { defaultModule.TopLevelDecls.Add(at); } else if (StartOf(3)) { ClassMemberDecl(membersDefaultClass, isGhost, false); - } else SynErr(106); + } else SynErr(107); } if (defaultModuleCreatedHere) { defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass)); @@ -310,7 +310,7 @@ bool IsAttribute() { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 12)) {SynErr(107); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(108); Get();} Expect(12); while (la.kind == 6) { Attribute(ref attrs); @@ -340,7 +340,7 @@ bool IsAttribute() { List ctors = new List(); IToken bodyStart = Token.NoToken; // dummy assignment - while (!(la.kind == 0 || la.kind == 15)) {SynErr(108); Get();} + while (!(la.kind == 0 || la.kind == 15)) {SynErr(109); Get();} Expect(15); while (la.kind == 6) { Attribute(ref attrs); @@ -356,7 +356,7 @@ bool IsAttribute() { Get(); DatatypeMemberDecl(ctors); } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(109); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(110); Get();} Expect(18); dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); dt.BodyStartTok = bodyStart; @@ -374,7 +374,7 @@ bool IsAttribute() { } Ident(out id); at = new ArbitraryTypeDecl(id, id.val, module, attrs); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(110); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(111); Get();} Expect(18); } @@ -405,7 +405,7 @@ bool IsAttribute() { } else if (la.kind == 24 || la.kind == 25) { MethodDecl(mmod, allowConstructors, out m); mm.Add(m); - } else SynErr(111); + } else SynErr(112); } void GenericParameters(List/*!*/ typeArgs) { @@ -427,7 +427,7 @@ bool IsAttribute() { Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; - while (!(la.kind == 0 || la.kind == 19)) {SynErr(112); Get();} + while (!(la.kind == 0 || la.kind == 19)) {SynErr(113); Get();} Expect(19); if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); } if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } @@ -442,7 +442,7 @@ bool IsAttribute() { IdentType(out id, out ty); mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(113); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(114); Get();} Expect(18); } @@ -488,7 +488,7 @@ bool IsAttribute() { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(114); + } else SynErr(115); } else if (la.kind == 43) { Get(); isPredicate = true; @@ -517,8 +517,8 @@ bool IsAttribute() { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(115); - } else SynErr(116); + } else SynErr(116); + } else SynErr(117); while (StartOf(5)) { FunctionSpec(reqs, reads, ens, decreases); } @@ -557,7 +557,7 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(117); Get();} + while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(118); Get();} if (la.kind == 24) { Get(); } else if (la.kind == 25) { @@ -568,7 +568,7 @@ bool IsAttribute() { SemErr(t, "constructors are only allowed in classes"); } - } else SynErr(118); + } else SynErr(119); if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); } if (isConstructor) { if (mmod.IsGhost) { @@ -596,7 +596,7 @@ bool IsAttribute() { } else if (la.kind == 27) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(119); + } else SynErr(120); while (StartOf(6)) { MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs); } @@ -779,7 +779,7 @@ bool IsAttribute() { ReferenceType(out tok, out ty); break; } - default: SynErr(120); break; + default: SynErr(121); break; } } @@ -804,7 +804,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null; - while (!(StartOf(8))) {SynErr(121); Get();} + while (!(StartOf(8))) {SynErr(122); Get();} if (la.kind == 28) { Get(); while (IsAttribute()) { @@ -819,7 +819,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(122); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(123); Get();} Expect(18); } else if (la.kind == 29 || la.kind == 30 || la.kind == 31) { if (la.kind == 29) { @@ -829,7 +829,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 30) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(123); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(124); Get();} Expect(18); req.Add(new MaybeFreeExpression(e, isFree)); } else if (la.kind == 31) { @@ -838,19 +838,19 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Attribute(ref ensAttrs); } Expression(out e); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(124); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(125); Get();} Expect(18); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); - } else SynErr(125); + } else SynErr(126); } else if (la.kind == 32) { Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(126); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(127); Get();} Expect(18); - } else SynErr(127); + } else SynErr(128); } void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -944,17 +944,17 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt); - } else SynErr(128); + } else SynErr(129); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List/*!*/ decreases) { Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; if (la.kind == 30) { - while (!(la.kind == 0 || la.kind == 30)) {SynErr(129); Get();} + while (!(la.kind == 0 || la.kind == 30)) {SynErr(130); Get();} Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(130); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(131); Get();} Expect(18); reqs.Add(e); } else if (la.kind == 44) { @@ -968,20 +968,20 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe); } } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(131); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(132); Get();} Expect(18); } else if (la.kind == 31) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(132); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(133); Get();} Expect(18); ens.Add(e); } else if (la.kind == 32) { Get(); DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(133); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(134); Get();} Expect(18); - } else SynErr(134); + } else SynErr(135); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -1000,7 +1000,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo fe = new FrameExpression(new WildcardExpr(t), null); } else if (StartOf(9)) { FrameExpression(out fe); - } else SynErr(135); + } else SynErr(136); } void PossiblyWildExpression(out Expression/*!*/ e) { @@ -1011,7 +1011,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new WildcardExpr(t); } else if (StartOf(9)) { Expression(out e); - } else SynErr(136); + } else SynErr(137); } void Stmt(List/*!*/ ss) { @@ -1028,26 +1028,26 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd; int breakCount; - while (!(StartOf(12))) {SynErr(137); Get();} + while (!(StartOf(12))) {SynErr(138); Get();} switch (la.kind) { case 6: { BlockStmt(out bs, out bodyStart, out bodyEnd); s = bs; break; } - case 63: { + case 64: { AssertStmt(out s); break; } - case 64: { + case 65: { AssumeStmt(out s); break; } - case 65: { + case 66: { PrintStmt(out s); break; } - case 1: case 2: case 17: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: { + case 1: case 2: case 17: case 33: case 91: case 92: case 93: case 94: case 95: case 96: case 97: { UpdateStmt(out s); break; } @@ -1055,19 +1055,19 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo VarDeclStatement(out s); break; } - case 56: { + case 57: { IfStmt(out s); break; } - case 60: { + case 61: { WhileStmt(out s); break; } - case 62: { + case 63: { MatchStmt(out s); break; } - case 66: { + case 67: { ParallelStmt(out s); break; } @@ -1091,8 +1091,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); breakCount++; } - } else SynErr(138); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(139); Get();} + } else SynErr(139); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(140); Get();} Expect(18); s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); break; @@ -1107,7 +1107,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(18); break; } - default: SynErr(140); break; + default: SynErr(141); break; } } @@ -1115,7 +1115,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e = null; Attributes attrs = null; - Expect(63); + Expect(64); x = t; s = null; while (IsAttribute()) { Attribute(ref attrs); @@ -1124,7 +1124,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e); } else if (la.kind == 27) { Get(); - } else SynErr(141); + } else SynErr(142); Expect(18); if (e == null) { s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false); @@ -1136,7 +1136,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void AssumeStmt(out Statement/*!*/ s) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; - Expect(64); + Expect(65); x = t; Expression(out e); Expect(18); @@ -1147,7 +1147,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg; List args = new List(); - Expect(65); + Expect(66); x = t; AttributeArg(out arg); args.Add(arg); @@ -1167,6 +1167,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression lhs0; IToken x; Attributes attrs = null; + Expression suchThat = null; Lhs(out e); x = e.tok; @@ -1176,28 +1177,39 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(18); rhss.Add(new ExprRhs(e, attrs)); - } else if (la.kind == 20 || la.kind == 50) { + } else if (la.kind == 20 || la.kind == 50 || la.kind == 51) { lhss.Add(e); lhs0 = e; while (la.kind == 20) { Get(); Lhs(out e); lhss.Add(e); } - Expect(50); - x = t; - Rhs(out r, lhs0); - rhss.Add(r); - while (la.kind == 20) { + if (la.kind == 50) { Get(); + x = t; Rhs(out r, lhs0); rhss.Add(r); - } + while (la.kind == 20) { + Get(); + Rhs(out r, lhs0); + rhss.Add(r); + } + } else if (la.kind == 51) { + Get(); + x = t; + Expression(out suchThat); + } else SynErr(143); Expect(18); } else if (la.kind == 5) { Get(); SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); - } else SynErr(142); - s = new UpdateStmt(x, lhss, rhss); + } else SynErr(144); + if (suchThat != null) { + s = new AssignSuchThatStmt(x, lhss, suchThat); + } else { + s = new UpdateStmt(x, lhss, rhss); + } + } void VarDeclStatement(out Statement/*!*/ s) { @@ -1206,6 +1218,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssignmentRhs r; IdentifierExpr lhs0; List lhss = new List(); List rhss = new List(); + Expression suchThat = null; if (la.kind == 8) { Get(); @@ -1220,23 +1233,35 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LocalIdentTypeOptional(out d, isGhost); lhss.Add(d); } - if (la.kind == 50) { - Get(); - assignTok = t; - lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); - lhs0.Var = lhss[0]; lhs0.Type = lhss[0].OptionalType; // resolve here - - Rhs(out r, lhs0); - rhss.Add(r); - while (la.kind == 20) { + if (la.kind == 50 || la.kind == 51) { + if (la.kind == 50) { Get(); + assignTok = t; + lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); + lhs0.Var = lhss[0]; lhs0.Type = lhss[0].OptionalType; // resolve here + Rhs(out r, lhs0); rhss.Add(r); + while (la.kind == 20) { + Get(); + Rhs(out r, lhs0); + rhss.Add(r); + } + } else { + Get(); + assignTok = t; + Expression(out suchThat); } } Expect(18); - UpdateStmt update; - if (rhss.Count == 0) { + ConcreteUpdateStatement update; + if (suchThat != null) { + var ies = new List(); + foreach (var lhs in lhss) { + ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name)); + } + update = new AssignSuchThatStmt(assignTok, ies, suchThat); + } else if (rhss.Count == 0) { update = null; } else { var ies = new List(); @@ -1260,7 +1285,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List alternatives; ifStmt = dummyStmt; // to please the compiler - Expect(56); + Expect(57); x = t; if (la.kind == 27 || la.kind == 33) { if (la.kind == 33) { @@ -1270,15 +1295,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo guardOmitted = true; } BlockStmt(out thn, out bodyStart, out bodyEnd); - if (la.kind == 57) { + if (la.kind == 58) { Get(); - if (la.kind == 56) { + if (la.kind == 57) { IfStmt(out s); els = s; } else if (la.kind == 6) { BlockStmt(out bs, out bodyStart, out bodyEnd); els = bs; - } else SynErr(143); + } else SynErr(145); } if (guardOmitted) { ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false); @@ -1289,7 +1314,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 6) { AlternativeBlock(out alternatives); ifStmt = new AlternativeStmt(x, alternatives); - } else SynErr(144); + } else SynErr(146); } void WhileStmt(out Statement/*!*/ stmt) { @@ -1305,7 +1330,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List alternatives; stmt = dummyStmt; // to please the compiler - Expect(60); + Expect(61); x = t; if (la.kind == 27 || la.kind == 33) { if (la.kind == 33) { @@ -1321,7 +1346,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 27) { Get(); bodyOmitted = true; - } else SynErr(145); + } else SynErr(147); if (guardOmitted || bodyOmitted) { if (decreases.Count != 0) { SemErr(decreases[0].tok, "'decreases' clauses are not allowed on refining loops"); @@ -1342,18 +1367,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs); AlternativeBlock(out alternatives); stmt = new AlternativeLoopStmt(x, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), alternatives); - } else SynErr(146); + } else SynErr(148); } void MatchStmt(out Statement/*!*/ s) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c; List cases = new List(); - Expect(62); + Expect(63); x = t; Expression(out e); Expect(6); - while (la.kind == 58) { + while (la.kind == 59) { CaseStatement(out c); cases.Add(c); } @@ -1373,7 +1398,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BlockStmt/*!*/ block; IToken bodyStart, bodyEnd; - Expect(66); + Expect(67); x = t; Expect(33); if (la.kind == 1) { @@ -1430,16 +1455,16 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = null; // to please compiler Attributes attrs = null; - if (la.kind == 51) { + if (la.kind == 52) { Get(); newToken = t; TypeAndToken(out x, out ty); - if (la.kind == 52 || la.kind == 54) { - if (la.kind == 52) { + if (la.kind == 53 || la.kind == 55) { + if (la.kind == 53) { Get(); ee = new List(); Expressions(ee); - Expect(53); + Expect(54); UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true); } else { @@ -1461,7 +1486,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = new TypeRhs(newToken, ty, initCall); } - } else if (la.kind == 55) { + } else if (la.kind == 56) { Get(); x = t; Expression(out e); @@ -1472,7 +1497,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(9)) { Expression(out e); r = new ExprRhs(e); - } else SynErr(147); + } else SynErr(149); while (la.kind == 6) { Attribute(ref attrs); } @@ -1484,16 +1509,16 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) { DottedIdentifiersAndFunction(out e); - while (la.kind == 52 || la.kind == 54) { + while (la.kind == 53 || la.kind == 55) { Suffix(ref e); } } else if (StartOf(15)) { ConstAtomExpression(out e); Suffix(ref e); - while (la.kind == 52 || la.kind == 54) { + while (la.kind == 53 || la.kind == 55) { Suffix(ref e); } - } else SynErr(148); + } else SynErr(150); } void Expressions(List/*!*/ args) { @@ -1516,7 +1541,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(9)) { Expression(out ee); e = ee; - } else SynErr(149); + } else SynErr(151); Expect(34); } @@ -1527,11 +1552,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List body; Expect(6); - while (la.kind == 58) { + while (la.kind == 59) { Get(); x = t; Expression(out e); - Expect(59); + Expect(60); body = new List(); while (StartOf(10)) { Stmt(body); @@ -1549,22 +1574,22 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod = null; while (StartOf(16)) { - if (la.kind == 29 || la.kind == 61) { + if (la.kind == 29 || la.kind == 62) { Invariant(out invariant); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(150); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(152); Get();} Expect(18); invariants.Add(invariant); } else if (la.kind == 32) { - while (!(la.kind == 0 || la.kind == 32)) {SynErr(151); Get();} + while (!(la.kind == 0 || la.kind == 32)) {SynErr(153); Get();} Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, true); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(152); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(154); Get();} Expect(18); } else { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(153); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(155); Get();} Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -1579,7 +1604,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(154); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(156); Get();} Expect(18); } } @@ -1587,12 +1612,12 @@ 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 == 29 || la.kind == 61)) {SynErr(155); Get();} + while (!(la.kind == 0 || la.kind == 29 || la.kind == 62)) {SynErr(157); Get();} if (la.kind == 29) { Get(); isFree = true; } - Expect(61); + Expect(62); while (IsAttribute()) { Attribute(ref attrs); } @@ -1607,7 +1632,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv; List body = new List(); - Expect(58); + Expect(59); x = t; Ident(out id); if (la.kind == 33) { @@ -1621,7 +1646,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(34); } - Expect(59); + Expect(60); while (StartOf(10)) { Stmt(body); } @@ -1636,7 +1661,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(9)) { Expression(out e); arg = new Attributes.Argument(t, e); - } else SynErr(156); + } else SynErr(158); } void QuantifierDomain(out List bvars, out Attributes attrs, out Expression range) { @@ -1664,7 +1689,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void EquivExpression(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; ImpliesExpression(out e0); - while (la.kind == 67 || la.kind == 68) { + while (la.kind == 68 || la.kind == 69) { EquivOp(); x = t; ImpliesExpression(out e1); @@ -1675,7 +1700,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ImpliesExpression(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; LogicalExpression(out e0); - if (la.kind == 69 || la.kind == 70) { + if (la.kind == 70 || la.kind == 71) { ImpliesOp(); x = t; ImpliesExpression(out e1); @@ -1684,23 +1709,23 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } void EquivOp() { - if (la.kind == 67) { + if (la.kind == 68) { Get(); - } else if (la.kind == 68) { + } else if (la.kind == 69) { Get(); - } else SynErr(157); + } else SynErr(159); } void LogicalExpression(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; RelationalExpression(out e0); if (StartOf(17)) { - if (la.kind == 71 || la.kind == 72) { + if (la.kind == 72 || la.kind == 73) { AndOp(); x = t; RelationalExpression(out e1); e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); - while (la.kind == 71 || la.kind == 72) { + while (la.kind == 72 || la.kind == 73) { AndOp(); x = t; RelationalExpression(out e1); @@ -1711,7 +1736,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; RelationalExpression(out e1); e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); - while (la.kind == 73 || la.kind == 74) { + while (la.kind == 74 || la.kind == 75) { OrOp(); x = t; RelationalExpression(out e1); @@ -1722,11 +1747,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } void ImpliesOp() { - if (la.kind == 69) { + if (la.kind == 70) { Get(); - } else if (la.kind == 70) { + } else if (la.kind == 71) { Get(); - } else SynErr(158); + } else SynErr(160); } void RelationalExpression(out Expression/*!*/ e) { @@ -1820,25 +1845,25 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } void AndOp() { - if (la.kind == 71) { + if (la.kind == 72) { Get(); - } else if (la.kind == 72) { + } else if (la.kind == 73) { Get(); - } else SynErr(159); + } else SynErr(161); } void OrOp() { - if (la.kind == 73) { + if (la.kind == 74) { Get(); - } else if (la.kind == 74) { + } else if (la.kind == 75) { Get(); - } else SynErr(160); + } else SynErr(162); } void Term(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; Factor(out e0); - while (la.kind == 85 || la.kind == 86) { + while (la.kind == 86 || la.kind == 87) { AddOp(out x, out op); Factor(out e1); e0 = new BinaryExpr(x, op, e0, e1); @@ -1851,7 +1876,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken y; switch (la.kind) { - case 75: { + case 76: { Get(); x = t; op = BinaryExpr.Opcode.Eq; break; @@ -1866,35 +1891,35 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Gt; break; } - case 76: { + case 77: { Get(); x = t; op = BinaryExpr.Opcode.Le; break; } - case 77: { + case 78: { Get(); x = t; op = BinaryExpr.Opcode.Ge; break; } - case 78: { + case 79: { Get(); x = t; op = BinaryExpr.Opcode.Neq; break; } - case 79: { + case 80: { Get(); x = t; op = BinaryExpr.Opcode.Disjoint; break; } - case 80: { + case 81: { Get(); x = t; op = BinaryExpr.Opcode.In; break; } - case 81: { + case 82: { Get(); x = t; y = Token.NoToken; - if (la.kind == 80) { + if (la.kind == 81) { Get(); y = t; } @@ -1909,29 +1934,29 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break; } - case 82: { + case 83: { Get(); x = t; op = BinaryExpr.Opcode.Neq; break; } - case 83: { + case 84: { Get(); x = t; op = BinaryExpr.Opcode.Le; break; } - case 84: { + case 85: { Get(); x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(161); break; + default: SynErr(163); break; } } void Factor(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; UnaryExpression(out e0); - while (la.kind == 45 || la.kind == 87 || la.kind == 88) { + while (la.kind == 45 || la.kind == 88 || la.kind == 89) { MulOp(out x, out op); UnaryExpression(out e1); e0 = new BinaryExpr(x, op, e0, e1); @@ -1940,44 +1965,44 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/; - if (la.kind == 85) { + if (la.kind == 86) { Get(); x = t; op = BinaryExpr.Opcode.Add; - } else if (la.kind == 86) { + } else if (la.kind == 87) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(162); + } else SynErr(164); } void UnaryExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; switch (la.kind) { - case 86: { + case 87: { Get(); x = t; UnaryExpression(out e); e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); break; } - case 81: case 89: { + case 82: case 90: { NegOp(); x = t; UnaryExpression(out e); e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); break; } - case 19: case 38: case 56: case 62: case 63: case 64: case 99: case 100: case 101: case 102: { + case 19: case 38: case 57: case 63: case 64: case 65: case 100: case 101: case 102: case 103: { EndlessExpression(out e); break; } case 1: { DottedIdentifiersAndFunction(out e); - while (la.kind == 52 || la.kind == 54) { + while (la.kind == 53 || la.kind == 55) { Suffix(ref e); } break; } - case 6: case 52: { + case 6: case 53: { DisplayExpr(out e); break; } @@ -1985,14 +2010,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo MultiSetExpr(out e); break; } - case 2: case 17: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: { + case 2: case 17: case 33: case 91: case 92: case 93: case 94: case 95: case 96: case 97: { ConstAtomExpression(out e); - while (la.kind == 52 || la.kind == 54) { + while (la.kind == 53 || la.kind == 55) { Suffix(ref e); } break; } - default: SynErr(163); break; + default: SynErr(165); break; } } @@ -2001,21 +2026,21 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 45) { Get(); x = t; op = BinaryExpr.Opcode.Mul; - } else if (la.kind == 87) { + } else if (la.kind == 88) { Get(); x = t; op = BinaryExpr.Opcode.Div; - } else if (la.kind == 88) { + } else if (la.kind == 89) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(164); + } else SynErr(166); } void NegOp() { - if (la.kind == 81) { + if (la.kind == 82) { Get(); - } else if (la.kind == 89) { + } else if (la.kind == 90) { Get(); - } else SynErr(165); + } else SynErr(167); } void EndlessExpression(out Expression e) { @@ -2026,22 +2051,22 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List letVars; List letRHSs; switch (la.kind) { - case 56: { + case 57: { Get(); x = t; Expression(out e); - Expect(97); + Expect(98); Expression(out e0); - Expect(57); + Expect(58); Expression(out e1); e = new ITEExpr(x, e, e0, e1); break; } - case 62: { + case 63: { MatchExpression(out e); break; } - case 99: case 100: case 101: case 102: { + case 100: case 101: case 102: case 103: { QuantifierGuts(out e); break; } @@ -2049,7 +2074,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ComprehensionExpr(out e); break; } - case 63: { + case 64: { Get(); x = t; Expression(out e0); @@ -2058,7 +2083,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new AssertExpr(x, e0, e1); break; } - case 64: { + case 65: { Get(); x = t; Expression(out e0); @@ -2092,7 +2117,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LetExpr(x, letVars, letRHSs, e); break; } - default: SynErr(166); break; + default: SynErr(168); break; } } @@ -2103,7 +2128,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out id); idents.Add(id); - while (la.kind == 54) { + while (la.kind == 55) { Get(); Ident(out id); idents.Add(id); @@ -2125,7 +2150,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List multipleIndices = null; bool func = false; - if (la.kind == 54) { + if (la.kind == 55) { Get(); Ident(out id); if (la.kind == 33) { @@ -2138,13 +2163,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new FunctionCallExpr(id, id.val, e, openParen, args); } if (!func) { e = new ExprDotName(id, e, id.val); } - } else if (la.kind == 52) { + } else if (la.kind == 53) { Get(); x = t; if (StartOf(9)) { Expression(out ee); e0 = ee; - if (la.kind == 98) { + if (la.kind == 99) { Get(); anyDots = true; if (StartOf(9)) { @@ -2155,7 +2180,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); Expression(out ee); e1 = ee; - } else if (la.kind == 20 || la.kind == 53) { + } else if (la.kind == 20 || la.kind == 54) { while (la.kind == 20) { Get(); Expression(out ee); @@ -2166,15 +2191,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee); } - } else SynErr(167); - } else if (la.kind == 98) { + } else SynErr(169); + } else if (la.kind == 99) { Get(); anyDots = true; if (StartOf(9)) { Expression(out ee); e1 = ee; } - } else SynErr(168); + } else SynErr(170); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -2197,8 +2222,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } - Expect(53); - } else SynErr(169); + Expect(54); + } else SynErr(171); } void DisplayExpr(out Expression e) { @@ -2214,15 +2239,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } e = new SetDisplayExpr(x, elements); Expect(7); - } else if (la.kind == 52) { + } else if (la.kind == 53) { Get(); x = t; elements = new List(); if (StartOf(9)) { Expressions(elements); } e = new SeqDisplayExpr(x, elements); - Expect(53); - } else SynErr(170); + Expect(54); + } else SynErr(172); } void MultiSetExpr(out Expression e) { @@ -2248,7 +2273,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(34); } else if (StartOf(19)) { SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); - } else SynErr(171); + } else SynErr(173); } void ConstAtomExpression(out Expression/*!*/ e) { @@ -2257,17 +2282,17 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr; switch (la.kind) { - case 90: { + case 91: { Get(); e = new LiteralExpr(t, false); break; } - case 91: { + case 92: { Get(); e = new LiteralExpr(t, true); break; } - case 92: { + case 93: { Get(); e = new LiteralExpr(t); break; @@ -2277,12 +2302,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LiteralExpr(t, n); break; } - case 93: { + case 94: { Get(); e = new ThisExpr(t); break; } - case 94: { + case 95: { Get(); x = t; Expect(33); @@ -2291,7 +2316,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new FreshExpr(x, e); break; } - case 95: { + case 96: { Get(); x = t; Expect(33); @@ -2300,7 +2325,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new AllocatedExpr(x, e); break; } - case 96: { + case 97: { Get(); x = t; Expect(33); @@ -2325,7 +2350,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(34); break; } - default: SynErr(172); break; + default: SynErr(174); break; } } @@ -2344,10 +2369,10 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c; List cases = new List(); - Expect(62); + Expect(63); x = t; Expression(out e); - while (la.kind == 58) { + while (la.kind == 59) { CaseExpression(out c); cases.Add(c); } @@ -2362,13 +2387,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression range; Expression/*!*/ body; - if (la.kind == 99 || la.kind == 100) { + if (la.kind == 100 || la.kind == 101) { Forall(); x = t; univ = true; - } else if (la.kind == 101 || la.kind == 102) { + } else if (la.kind == 102 || la.kind == 103) { Exists(); x = t; - } else SynErr(173); + } else SynErr(175); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body); @@ -2399,7 +2424,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(17); Expression(out range); - if (la.kind == 103 || la.kind == 104) { + if (la.kind == 104 || la.kind == 105) { QSep(); Expression(out body); } @@ -2414,7 +2439,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv; Expression/*!*/ body; - Expect(58); + Expect(59); x = t; Ident(out id); if (la.kind == 33) { @@ -2428,33 +2453,33 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(34); } - Expect(59); + Expect(60); Expression(out body); c = new MatchCaseExpr(x, id.val, arguments, body); } void Forall() { - if (la.kind == 99) { + if (la.kind == 100) { Get(); - } else if (la.kind == 100) { + } else if (la.kind == 101) { Get(); - } else SynErr(174); + } else SynErr(176); } void Exists() { - if (la.kind == 101) { + if (la.kind == 102) { Get(); - } else if (la.kind == 102) { + } else if (la.kind == 103) { Get(); - } else SynErr(175); + } else SynErr(177); } void QSep() { - if (la.kind == 103) { + if (la.kind == 104) { Get(); - } else if (la.kind == 104) { + } else if (la.kind == 105) { Get(); - } else SynErr(176); + } else SynErr(178); } void AttributeBody(ref Attributes attrs) { @@ -2490,27 +2515,27 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } static readonly bool[,]/*!*/ set = { - {T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,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, 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,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, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, - {x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, - {x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,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,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,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, T,T,x,x, x,x,T,T, T,T,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,T,T, T,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, 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,T,x,T, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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, 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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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, 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, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}, - {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,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, T,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,T,T, T,T,T,T, T,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,x,T, 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,T,x,x, x,x,x,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, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}, - {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,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, T,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,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x}, - {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,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,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,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,T,x,x, x,x,x,T, T,x,x,T, T,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}, - {x,x,T,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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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, 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,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,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,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,T,x, x,T,x,x, x,T,T,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, x,T,T,x, x,x,x,T, T,x,x}, - {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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, 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, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x} + {T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,T,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,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, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,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,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}, + {T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, T,T,x,x, x,x,T,T, T,T,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,T,T, T,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, 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,T,x,T, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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, 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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,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,x,T,x, x,x,x,T, x,x,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x}, + {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,T,x,x, x,T,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,T, T,T,T,T, T,T,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,x,T, 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,T,x,x, x,x,x,x, 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,x,T,x, x,x,x,T, x,x,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x}, + {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,T,x,x, x,T,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,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x}, + {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,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,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,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,T,x,x, x,x,x,x, T,T,x,x, T,T,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, x,x,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x}, + {x,x,T,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,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,T,x,x, x,x,x,x, x,x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,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,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, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x, x,x,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,T,T,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,T,x, x,x,T,x, x,x,T,T, 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,x,T,T, x,x,x,x, T,T,x,x}, + {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, 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,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,x,T,x, x,x,x,T, x,x,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x} }; } // end Parser @@ -2586,132 +2611,134 @@ public class Errors { case 48: s = "\"break\" expected"; break; case 49: s = "\"return\" expected"; break; case 50: s = "\":=\" expected"; break; - case 51: s = "\"new\" expected"; break; - case 52: s = "\"[\" expected"; break; - case 53: s = "\"]\" expected"; break; - case 54: s = "\".\" expected"; break; - case 55: s = "\"choose\" expected"; break; - case 56: s = "\"if\" expected"; break; - case 57: s = "\"else\" expected"; break; - case 58: s = "\"case\" expected"; break; - case 59: s = "\"=>\" expected"; break; - case 60: s = "\"while\" expected"; break; - case 61: s = "\"invariant\" expected"; break; - case 62: s = "\"match\" expected"; break; - case 63: s = "\"assert\" expected"; break; - case 64: s = "\"assume\" expected"; break; - case 65: s = "\"print\" expected"; break; - case 66: s = "\"parallel\" expected"; break; - case 67: s = "\"<==>\" expected"; break; - case 68: s = "\"\\u21d4\" expected"; break; - case 69: s = "\"==>\" expected"; break; - case 70: s = "\"\\u21d2\" expected"; break; - case 71: s = "\"&&\" expected"; break; - case 72: s = "\"\\u2227\" expected"; break; - case 73: s = "\"||\" expected"; break; - case 74: s = "\"\\u2228\" expected"; break; - case 75: s = "\"==\" expected"; break; - case 76: s = "\"<=\" expected"; break; - case 77: s = "\">=\" expected"; break; - case 78: s = "\"!=\" expected"; break; - case 79: s = "\"!!\" expected"; break; - case 80: s = "\"in\" expected"; break; - case 81: s = "\"!\" expected"; break; - case 82: s = "\"\\u2260\" expected"; break; - case 83: s = "\"\\u2264\" expected"; break; - case 84: s = "\"\\u2265\" expected"; break; - case 85: s = "\"+\" expected"; break; - case 86: s = "\"-\" expected"; break; - case 87: s = "\"/\" expected"; break; - case 88: s = "\"%\" expected"; break; - case 89: s = "\"\\u00ac\" expected"; break; - case 90: s = "\"false\" expected"; break; - case 91: s = "\"true\" expected"; break; - case 92: s = "\"null\" expected"; break; - case 93: s = "\"this\" expected"; break; - case 94: s = "\"fresh\" expected"; break; - case 95: s = "\"allocated\" expected"; break; - case 96: s = "\"old\" expected"; break; - case 97: s = "\"then\" expected"; break; - case 98: s = "\"..\" expected"; break; - case 99: s = "\"forall\" expected"; break; - case 100: s = "\"\\u2200\" expected"; break; - case 101: s = "\"exists\" expected"; break; - case 102: s = "\"\\u2203\" expected"; break; - case 103: s = "\"::\" expected"; break; - case 104: s = "\"\\u2022\" expected"; break; - case 105: s = "??? expected"; break; - case 106: s = "invalid Dafny"; break; - case 107: s = "this symbol not expected in ClassDecl"; break; - case 108: s = "this symbol not expected in DatatypeDecl"; break; + case 51: s = "\":|\" expected"; break; + case 52: s = "\"new\" expected"; break; + case 53: s = "\"[\" expected"; break; + case 54: s = "\"]\" expected"; break; + case 55: s = "\".\" expected"; break; + case 56: s = "\"choose\" expected"; break; + case 57: s = "\"if\" expected"; break; + case 58: s = "\"else\" expected"; break; + case 59: s = "\"case\" expected"; break; + case 60: s = "\"=>\" expected"; break; + case 61: s = "\"while\" expected"; break; + case 62: s = "\"invariant\" expected"; break; + case 63: s = "\"match\" expected"; break; + case 64: s = "\"assert\" expected"; break; + case 65: s = "\"assume\" expected"; break; + case 66: s = "\"print\" expected"; break; + case 67: s = "\"parallel\" expected"; break; + case 68: s = "\"<==>\" expected"; break; + case 69: s = "\"\\u21d4\" expected"; break; + case 70: s = "\"==>\" expected"; break; + case 71: s = "\"\\u21d2\" expected"; break; + case 72: s = "\"&&\" expected"; break; + case 73: s = "\"\\u2227\" expected"; break; + case 74: s = "\"||\" expected"; break; + case 75: s = "\"\\u2228\" expected"; break; + case 76: s = "\"==\" expected"; break; + case 77: s = "\"<=\" expected"; break; + case 78: s = "\">=\" expected"; break; + case 79: s = "\"!=\" expected"; break; + case 80: s = "\"!!\" expected"; break; + case 81: s = "\"in\" expected"; break; + case 82: s = "\"!\" expected"; break; + case 83: s = "\"\\u2260\" expected"; break; + case 84: s = "\"\\u2264\" expected"; break; + case 85: s = "\"\\u2265\" expected"; break; + case 86: s = "\"+\" expected"; break; + case 87: s = "\"-\" expected"; break; + case 88: s = "\"/\" expected"; break; + case 89: s = "\"%\" expected"; break; + case 90: s = "\"\\u00ac\" expected"; break; + case 91: s = "\"false\" expected"; break; + case 92: s = "\"true\" expected"; break; + case 93: s = "\"null\" expected"; break; + case 94: s = "\"this\" expected"; break; + case 95: s = "\"fresh\" expected"; break; + case 96: s = "\"allocated\" expected"; break; + case 97: s = "\"old\" expected"; break; + case 98: s = "\"then\" expected"; break; + case 99: s = "\"..\" expected"; break; + case 100: s = "\"forall\" expected"; break; + case 101: s = "\"\\u2200\" expected"; break; + case 102: s = "\"exists\" expected"; break; + case 103: s = "\"\\u2203\" expected"; break; + case 104: s = "\"::\" expected"; break; + case 105: s = "\"\\u2022\" expected"; break; + case 106: s = "??? expected"; break; + case 107: s = "invalid Dafny"; break; + case 108: s = "this symbol not expected in ClassDecl"; break; case 109: s = "this symbol not expected in DatatypeDecl"; break; - case 110: s = "this symbol not expected in ArbitraryTypeDecl"; break; - case 111: s = "invalid ClassMemberDecl"; break; - case 112: s = "this symbol not expected in FieldDecl"; break; + case 110: s = "this symbol not expected in DatatypeDecl"; break; + case 111: s = "this symbol not expected in ArbitraryTypeDecl"; break; + case 112: s = "invalid ClassMemberDecl"; break; case 113: s = "this symbol not expected in FieldDecl"; break; - case 114: s = "invalid FunctionDecl"; break; + case 114: s = "this symbol not expected in FieldDecl"; break; case 115: s = "invalid FunctionDecl"; break; case 116: s = "invalid FunctionDecl"; break; - case 117: s = "this symbol not expected in MethodDecl"; break; - case 118: s = "invalid MethodDecl"; break; + case 117: s = "invalid FunctionDecl"; break; + case 118: s = "this symbol not expected in MethodDecl"; break; case 119: s = "invalid MethodDecl"; break; - case 120: s = "invalid TypeAndToken"; break; - case 121: s = "this symbol not expected in MethodSpec"; break; + case 120: s = "invalid MethodDecl"; break; + case 121: s = "invalid TypeAndToken"; break; case 122: s = "this symbol not expected in MethodSpec"; break; case 123: s = "this symbol not expected in MethodSpec"; break; case 124: s = "this symbol not expected in MethodSpec"; break; - case 125: s = "invalid MethodSpec"; break; - case 126: s = "this symbol not expected in MethodSpec"; break; - case 127: s = "invalid MethodSpec"; break; - case 128: s = "invalid ReferenceType"; break; - case 129: s = "this symbol not expected in FunctionSpec"; break; + case 125: s = "this symbol not expected in MethodSpec"; break; + case 126: s = "invalid MethodSpec"; break; + case 127: s = "this symbol not expected in MethodSpec"; break; + case 128: s = "invalid MethodSpec"; break; + case 129: s = "invalid ReferenceType"; break; case 130: s = "this symbol not expected in FunctionSpec"; break; case 131: s = "this symbol not expected in FunctionSpec"; break; case 132: s = "this symbol not expected in FunctionSpec"; break; case 133: s = "this symbol not expected in FunctionSpec"; break; - case 134: s = "invalid FunctionSpec"; break; - case 135: s = "invalid PossiblyWildFrameExpression"; break; - case 136: s = "invalid PossiblyWildExpression"; break; - case 137: s = "this symbol not expected in OneStmt"; break; - case 138: s = "invalid OneStmt"; break; - case 139: s = "this symbol not expected in OneStmt"; break; - case 140: s = "invalid OneStmt"; break; - case 141: s = "invalid AssertStmt"; break; - case 142: s = "invalid UpdateStmt"; break; - case 143: s = "invalid IfStmt"; break; - case 144: s = "invalid IfStmt"; break; - case 145: s = "invalid WhileStmt"; break; - case 146: s = "invalid WhileStmt"; break; - case 147: s = "invalid Rhs"; break; - case 148: s = "invalid Lhs"; break; - case 149: s = "invalid Guard"; break; - case 150: s = "this symbol not expected in LoopSpec"; break; - case 151: s = "this symbol not expected in LoopSpec"; break; + case 134: s = "this symbol not expected in FunctionSpec"; break; + case 135: s = "invalid FunctionSpec"; break; + case 136: s = "invalid PossiblyWildFrameExpression"; break; + case 137: s = "invalid PossiblyWildExpression"; break; + case 138: s = "this symbol not expected in OneStmt"; break; + case 139: s = "invalid OneStmt"; break; + case 140: s = "this symbol not expected in OneStmt"; break; + case 141: s = "invalid OneStmt"; break; + case 142: s = "invalid AssertStmt"; break; + case 143: s = "invalid UpdateStmt"; break; + case 144: s = "invalid UpdateStmt"; break; + case 145: s = "invalid IfStmt"; break; + case 146: s = "invalid IfStmt"; break; + case 147: s = "invalid WhileStmt"; break; + case 148: s = "invalid WhileStmt"; break; + case 149: s = "invalid Rhs"; break; + case 150: s = "invalid Lhs"; break; + case 151: s = "invalid Guard"; break; case 152: s = "this symbol not expected in LoopSpec"; break; case 153: s = "this symbol not expected in LoopSpec"; break; case 154: s = "this symbol not expected in LoopSpec"; break; - case 155: s = "this symbol not expected in Invariant"; break; - case 156: s = "invalid AttributeArg"; break; - case 157: s = "invalid EquivOp"; break; - case 158: s = "invalid ImpliesOp"; break; - case 159: s = "invalid AndOp"; break; - case 160: s = "invalid OrOp"; break; - case 161: s = "invalid RelOp"; break; - case 162: s = "invalid AddOp"; break; - case 163: s = "invalid UnaryExpression"; break; - case 164: s = "invalid MulOp"; break; - case 165: s = "invalid NegOp"; break; - case 166: s = "invalid EndlessExpression"; break; - case 167: s = "invalid Suffix"; break; - case 168: s = "invalid Suffix"; break; + case 155: s = "this symbol not expected in LoopSpec"; break; + case 156: s = "this symbol not expected in LoopSpec"; break; + case 157: s = "this symbol not expected in Invariant"; break; + case 158: s = "invalid AttributeArg"; break; + case 159: s = "invalid EquivOp"; break; + case 160: s = "invalid ImpliesOp"; break; + case 161: s = "invalid AndOp"; break; + case 162: s = "invalid OrOp"; break; + case 163: s = "invalid RelOp"; break; + case 164: s = "invalid AddOp"; break; + case 165: s = "invalid UnaryExpression"; break; + case 166: s = "invalid MulOp"; break; + case 167: s = "invalid NegOp"; break; + case 168: s = "invalid EndlessExpression"; break; case 169: s = "invalid Suffix"; break; - case 170: s = "invalid DisplayExpr"; break; - case 171: s = "invalid MultiSetExpr"; break; - case 172: s = "invalid ConstAtomExpression"; break; - case 173: s = "invalid QuantifierGuts"; break; - case 174: s = "invalid Forall"; break; - case 175: s = "invalid Exists"; break; - case 176: s = "invalid QSep"; break; + case 170: s = "invalid Suffix"; break; + case 171: s = "invalid Suffix"; break; + case 172: s = "invalid DisplayExpr"; break; + case 173: s = "invalid MultiSetExpr"; break; + case 174: s = "invalid ConstAtomExpression"; break; + case 175: s = "invalid QuantifierGuts"; break; + case 176: s = "invalid Forall"; break; + case 177: s = "invalid Exists"; break; + case 178: s = "invalid QSep"; break; default: s = "error " + n; break; } diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs index 28ce83f4..015bd490 100644 --- a/Dafny/Printer.cs +++ b/Dafny/Printer.cs @@ -595,23 +595,15 @@ namespace Microsoft.Dafny { Indent(indent); wr.Write("}"); - } else if (stmt is UpdateStmt) { - var s = (UpdateStmt)stmt; + } else if (stmt is ConcreteUpdateStatement) { + var s = (ConcreteUpdateStatement)stmt; string sep = ""; foreach (var lhs in s.Lhss) { wr.Write(sep); PrintExpression(lhs); sep = ", "; } - if (s.Lhss.Count != 0) { - sep = " := "; - } - foreach (var rhs in s.Rhss) { - wr.Write(sep); - PrintRhs(rhs); - sep = ", "; - } - + PrintUpdateRHS(s); wr.Write(";"); } else if (stmt is VarDeclStmt) { @@ -627,13 +619,7 @@ namespace Microsoft.Dafny { sep = ", "; } if (s.Update != null) { - wr.Write(" := "); - sep = ""; - foreach (var rhs in s.Update.Rhss) { - wr.Write(sep); - PrintRhs(rhs); - sep = ", "; - } + PrintUpdateRHS(s.Update); } wr.Write(";"); @@ -657,6 +643,31 @@ namespace Microsoft.Dafny { } } + /// + /// Does not print LHS + /// + void PrintUpdateRHS(ConcreteUpdateStatement s) { + Contract.Requires(s != null); + if (s is UpdateStmt) { + var update = (UpdateStmt)s; + if (update.Lhss.Count != 0) { + wr.Write(" := "); + } + var sep = ""; + foreach (var rhs in update.Rhss) { + wr.Write(sep); + PrintRhs(rhs); + sep = ", "; + } + } else if (s is AssignSuchThatStmt) { + var update = (AssignSuchThatStmt)s; + wr.Write(" :| "); + PrintExpression(update.Assume.Expr); + } else { + Contract.Assert(s == null); // otherwise, unknown type + } + } + void PrintIfStatement(int indent, IfStmt s, bool omitGuard) { while (true) { if (omitGuard) { diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs index 36ae8f22..f3e54b01 100644 --- a/Dafny/RefinementTransformer.cs +++ b/Dafny/RefinementTransformer.cs @@ -473,13 +473,17 @@ namespace Microsoft.Dafny { r = new MatchStmt(Tok(s.Tok), CloneExpr(s.Source), s.Cases.ConvertAll(c => new MatchCaseStmt(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), c.Body.ConvertAll(CloneStmt)))); + } else if (stmt is AssignSuchThatStmt) { + var s = (AssignSuchThatStmt)stmt; + r = new AssignSuchThatStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Assume.Expr)); + } else if (stmt is UpdateStmt) { var s = (UpdateStmt)stmt; r = new UpdateStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), s.Rhss.ConvertAll(CloneRHS), s.CanMutateKnownState); } else if (stmt is VarDeclStmt) { var s = (VarDeclStmt)stmt; - r = new VarDeclStmt(Tok(s.Tok), s.Lhss.ConvertAll(c => (VarDecl)CloneStmt(c)), (UpdateStmt)CloneStmt(s.Update)); + r = new VarDeclStmt(Tok(s.Tok), s.Lhss.ConvertAll(c => (VarDecl)CloneStmt(c)), (ConcreteUpdateStatement)CloneStmt(s.Update)); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index b259e426..93ed3b4a 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -1308,8 +1308,8 @@ namespace Microsoft.Dafny { else {// this is a regular return statement. s.hiddenUpdate = null; } - } else if (stmt is UpdateStmt) { - ResolveUpdateStmt((UpdateStmt)stmt, specContextOnly, method); + } else if (stmt is ConcreteUpdateStatement) { + ResolveUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, method); } else if (stmt is VarDeclStmt) { var s = (VarDeclStmt)stmt; foreach (var vd in s.Lhss) { @@ -1725,7 +1725,7 @@ namespace Microsoft.Dafny { } } - private void ResolveUpdateStmt(UpdateStmt s, bool specContextOnly, Method method) + private void ResolveUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, Method method) { int prevErrorCount = ErrorCount; // First, resolve all LHS's and expression-looking RHS's. @@ -1743,32 +1743,38 @@ namespace Microsoft.Dafny { } IToken firstEffectfulRhs = null; CallRhs callRhs = null; + var update = s as UpdateStmt; // Resolve RHSs - foreach (var rhs in s.Rhss) { - bool isEffectful; - if (rhs is TypeRhs) { - var tr = (TypeRhs)rhs; - ResolveTypeRhs(tr, s, specContextOnly, method); - isEffectful = tr.InitCall != null; - } else if (rhs is HavocRhs) { - isEffectful = false; - } else { - var er = (ExprRhs)rhs; - if (er.Expr is IdentifierSequence) { - var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, true); - isEffectful = cRhs != null; - callRhs = callRhs ?? cRhs; - } else if (er.Expr is FunctionCallExpr) { - var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, true); - isEffectful = cRhs != null; - callRhs = callRhs ?? cRhs; - } else { - ResolveExpression(er.Expr, true); + if (update == null) { + var suchThat = (AssignSuchThatStmt)s; // this is the other possible subclass + s.ResolvedStatements.Add(suchThat.Assume); + } else { + foreach (var rhs in update.Rhss) { + bool isEffectful; + if (rhs is TypeRhs) { + var tr = (TypeRhs)rhs; + ResolveTypeRhs(tr, s, specContextOnly, method); + isEffectful = tr.InitCall != null; + } else if (rhs is HavocRhs) { isEffectful = false; + } else { + var er = (ExprRhs)rhs; + if (er.Expr is IdentifierSequence) { + var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, true); + isEffectful = cRhs != null; + callRhs = callRhs ?? cRhs; + } else if (er.Expr is FunctionCallExpr) { + var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, true); + isEffectful = cRhs != null; + callRhs = callRhs ?? cRhs; + } else { + ResolveExpression(er.Expr, true); + isEffectful = false; + } + } + if (isEffectful && firstEffectfulRhs == null) { + firstEffectfulRhs = rhs.Tok; } - } - if (isEffectful && firstEffectfulRhs == null) { - firstEffectfulRhs = rhs.Tok; } } // check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification) @@ -1784,67 +1790,69 @@ namespace Microsoft.Dafny { } } - // figure out what kind of UpdateStmt this is - if (firstEffectfulRhs == null) { - if (s.Lhss.Count == 0) { - Contract.Assert(s.Rhss.Count == 1); // guaranteed by the parser - Error(s, "expected method call, found expression"); - } else if (s.Lhss.Count != s.Rhss.Count) { - Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count); - } else if (arrayRangeLhs != null && s.Lhss.Count != 1) { - Error(arrayRangeLhs, "array-range may not be used as LHS of multi-assignment; use separate assignment statements for each array-range assignment"); - } else if (ErrorCount == prevErrorCount) { - // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment) - for (int i = 0; i < s.Lhss.Count; i++) { - var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, s.Rhss[i]); - s.ResolvedStatements.Add(a); - } - } - - } else if (s.CanMutateKnownState) { - if (1 < s.Rhss.Count) { - Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement."); - } else { // it might be ok, if it is a TypeRhs - Contract.Assert(s.Rhss.Count == 1); - if (callRhs != null) { - Error(callRhs.Tok, "cannot have method call in return statement."); - } else { - // we have a TypeRhs - Contract.Assert(s.Rhss[0] is TypeRhs); - var tr = (TypeRhs)s.Rhss[0]; - Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call. - if (tr.CanAffectPreviouslyKnownExpressions) { - Error(tr.Tok, "can only have initialization methods which modify at most 'this'."); + if (update != null) { + // figure out what kind of UpdateStmt this is + if (firstEffectfulRhs == null) { + if (s.Lhss.Count == 0) { + Contract.Assert(update.Rhss.Count == 1); // guaranteed by the parser + Error(s, "expected method call, found expression"); + } else if (s.Lhss.Count != update.Rhss.Count) { + Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, update.Rhss.Count); + } else if (arrayRangeLhs != null && s.Lhss.Count != 1) { + Error(arrayRangeLhs, "array-range may not be used as LHS of multi-assignment; use separate assignment statements for each array-range assignment"); + } else if (ErrorCount == prevErrorCount) { + // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment) + for (int i = 0; i < s.Lhss.Count; i++) { + var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, update.Rhss[i]); + s.ResolvedStatements.Add(a); } - var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, tr); - s.ResolvedStatements.Add(a); } - } - } else { - // if there was an effectful RHS, that must be the only RHS - if (s.Rhss.Count != 1) { - Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS"); - } else if (arrayRangeLhs != null) { - Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable"); - } else if (callRhs == null) { - // must be a single TypeRhs - if (s.Lhss.Count != 1) { - Contract.Assert(2 <= s.Lhss.Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs) - Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count); - } else if (ErrorCount == prevErrorCount) { - var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, s.Rhss[0]); - s.ResolvedStatements.Add(a); + } else if (update.CanMutateKnownState) { + if (1 < update.Rhss.Count) { + Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement."); + } else { // it might be ok, if it is a TypeRhs + Contract.Assert(update.Rhss.Count == 1); + if (callRhs != null) { + Error(callRhs.Tok, "cannot have method call in return statement."); + } else { + // we have a TypeRhs + Contract.Assert(update.Rhss[0] is TypeRhs); + var tr = (TypeRhs)update.Rhss[0]; + Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call. + if (tr.CanAffectPreviouslyKnownExpressions) { + Error(tr.Tok, "can only have initialization methods which modify at most 'this'."); + } + var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, tr); + s.ResolvedStatements.Add(a); + } } + } else { - // a call statement - if (ErrorCount == prevErrorCount) { - var resolvedLhss = new List(); - foreach (var ll in s.Lhss) { - resolvedLhss.Add(ll.Resolved); + // if there was an effectful RHS, that must be the only RHS + if (update.Rhss.Count != 1) { + Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS"); + } else if (arrayRangeLhs != null) { + Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable"); + } else if (callRhs == null) { + // must be a single TypeRhs + if (s.Lhss.Count != 1) { + Contract.Assert(2 <= s.Lhss.Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs) + Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, update.Rhss.Count); + } else if (ErrorCount == prevErrorCount) { + var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, update.Rhss[0]); + s.ResolvedStatements.Add(a); + } + } else { + // a call statement + if (ErrorCount == prevErrorCount) { + var resolvedLhss = new List(); + foreach (var ll in s.Lhss) { + resolvedLhss.Add(ll.Resolved); + } + var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args); + s.ResolvedStatements.Add(a); } - var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args); - s.ResolvedStatements.Add(a); } } } diff --git a/Dafny/Rewriter.cs b/Dafny/Rewriter.cs index addcce0a..26ec496e 100644 --- a/Dafny/Rewriter.cs +++ b/Dafny/Rewriter.cs @@ -296,8 +296,8 @@ namespace Microsoft.Dafny if (s is AssignStmt) { var ss = (AssignStmt)s; return ss.Lhs.Resolved is IdentifierExpr; - } else if (s is UpdateStmt) { - var ss = (UpdateStmt)s; + } else if (s is ConcreteUpdateStatement) { + var ss = (ConcreteUpdateStatement)s; return ss.Lhss.TrueForAll(e => e.Resolved is IdentifierExpr); } else if (s is CallStmt) { return false; diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs index 3e021fa5..ca2ae13c 100644 --- a/Dafny/Scanner.cs +++ b/Dafny/Scanner.cs @@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer { public class Scanner { const char EOL = '\n'; const int eofSym = 0; /* pdt */ - const int maxT = 105; - const int noSym = 105; + const int maxT = 106; + const int noSym = 106; [ContractInvariantMethod] @@ -258,39 +258,39 @@ public class Scanner { for (int i = 48; i <= 57; ++i) start[i] = 7; for (int i = 34; i <= 34; ++i) start[i] = 8; start[97] = 12; - start[58] = 55; + start[58] = 56; start[123] = 10; start[125] = 11; - start[61] = 56; - start[124] = 57; + start[61] = 57; + start[124] = 58; start[59] = 19; start[44] = 20; - start[60] = 58; - start[62] = 59; - start[46] = 60; + start[60] = 59; + start[62] = 60; + start[46] = 61; start[40] = 22; start[41] = 23; start[42] = 24; start[96] = 25; - start[91] = 27; - start[93] = 28; - start[8660] = 32; - start[8658] = 34; - start[38] = 35; - start[8743] = 37; - start[8744] = 39; - start[33] = 61; - start[8800] = 43; - start[8804] = 44; - start[8805] = 45; - start[43] = 46; - start[45] = 47; - start[47] = 48; - start[37] = 49; - start[172] = 50; - start[8704] = 51; - start[8707] = 52; - start[8226] = 54; + start[91] = 28; + start[93] = 29; + start[8660] = 33; + start[8658] = 35; + start[38] = 36; + start[8743] = 38; + start[8744] = 40; + start[33] = 62; + start[8800] = 44; + start[8804] = 45; + start[8805] = 46; + start[43] = 47; + start[45] = 48; + start[47] = 49; + start[37] = 50; + start[172] = 51; + start[8704] = 52; + start[8707] = 53; + start[8226] = 55; start[Buffer.EOF] = -1; } @@ -519,29 +519,29 @@ public class Scanner { case "label": t.kind = 47; break; case "break": t.kind = 48; break; case "return": t.kind = 49; break; - case "new": t.kind = 51; break; - case "choose": t.kind = 55; break; - case "if": t.kind = 56; break; - case "else": t.kind = 57; break; - case "case": t.kind = 58; break; - case "while": t.kind = 60; break; - case "invariant": t.kind = 61; break; - case "match": t.kind = 62; break; - case "assert": t.kind = 63; break; - case "assume": t.kind = 64; break; - case "print": t.kind = 65; break; - case "parallel": t.kind = 66; break; - case "in": t.kind = 80; break; - case "false": t.kind = 90; break; - case "true": t.kind = 91; break; - case "null": t.kind = 92; break; - case "this": t.kind = 93; break; - case "fresh": t.kind = 94; break; - case "allocated": t.kind = 95; break; - case "old": t.kind = 96; break; - case "then": t.kind = 97; break; - case "forall": t.kind = 99; break; - case "exists": t.kind = 101; break; + case "new": t.kind = 52; break; + case "choose": t.kind = 56; break; + case "if": t.kind = 57; break; + case "else": t.kind = 58; break; + case "case": t.kind = 59; break; + case "while": t.kind = 61; break; + case "invariant": t.kind = 62; break; + case "match": t.kind = 63; break; + case "assert": t.kind = 64; break; + case "assume": t.kind = 65; break; + case "print": t.kind = 66; break; + case "parallel": t.kind = 67; break; + case "in": t.kind = 81; break; + case "false": t.kind = 91; break; + case "true": t.kind = 92; break; + case "null": t.kind = 93; break; + case "this": t.kind = 94; break; + case "fresh": t.kind = 95; break; + case "allocated": t.kind = 96; break; + case "old": t.kind = 97; break; + case "then": t.kind = 98; break; + case "forall": t.kind = 100; break; + case "exists": t.kind = 102; break; default: break; } } @@ -663,16 +663,16 @@ public class Scanner { case 26: {t.kind = 50; break;} case 27: - {t.kind = 52; break;} + {t.kind = 51; break;} case 28: {t.kind = 53; break;} case 29: - {t.kind = 59; break;} + {t.kind = 54; break;} case 30: - if (ch == '>') {AddCh(); goto case 31;} - else {goto case 0;} + {t.kind = 60; break;} case 31: - {t.kind = 67; break;} + if (ch == '>') {AddCh(); goto case 32;} + else {goto case 0;} case 32: {t.kind = 68; break;} case 33: @@ -680,10 +680,10 @@ public class Scanner { case 34: {t.kind = 70; break;} case 35: - if (ch == '&') {AddCh(); goto case 36;} - else {goto case 0;} - case 36: {t.kind = 71; break;} + case 36: + if (ch == '&') {AddCh(); goto case 37;} + else {goto case 0;} case 37: {t.kind = 72; break;} case 38: @@ -691,13 +691,13 @@ public class Scanner { case 39: {t.kind = 74; break;} case 40: - {t.kind = 77; break;} + {t.kind = 75; break;} case 41: {t.kind = 78; break;} case 42: {t.kind = 79; break;} case 43: - {t.kind = 82; break;} + {t.kind = 80; break;} case 44: {t.kind = 83; break;} case 45: @@ -713,56 +713,59 @@ public class Scanner { case 50: {t.kind = 89; break;} case 51: - {t.kind = 100; break;} + {t.kind = 90; break;} case 52: - {t.kind = 102; break;} + {t.kind = 101; break;} case 53: {t.kind = 103; break;} case 54: {t.kind = 104; break;} case 55: + {t.kind = 105; break;} + case 56: recEnd = pos; recKind = 5; if (ch == '=') {AddCh(); goto case 26;} - else if (ch == ':') {AddCh(); goto case 53;} + else if (ch == '|') {AddCh(); goto case 27;} + else if (ch == ':') {AddCh(); goto case 54;} else {t.kind = 5; break;} - case 56: + case 57: recEnd = pos; recKind = 16; - if (ch == '>') {AddCh(); goto case 29;} - else if (ch == '=') {AddCh(); goto case 62;} + if (ch == '>') {AddCh(); goto case 30;} + else if (ch == '=') {AddCh(); goto case 63;} else {t.kind = 16; break;} - case 57: + case 58: recEnd = pos; recKind = 17; - if (ch == '|') {AddCh(); goto case 38;} + if (ch == '|') {AddCh(); goto case 39;} else {t.kind = 17; break;} - case 58: + case 59: recEnd = pos; recKind = 22; - if (ch == '=') {AddCh(); goto case 63;} + if (ch == '=') {AddCh(); goto case 64;} else {t.kind = 22; break;} - case 59: + case 60: recEnd = pos; recKind = 23; - if (ch == '=') {AddCh(); goto case 40;} + if (ch == '=') {AddCh(); goto case 41;} else {t.kind = 23; break;} - case 60: - recEnd = pos; recKind = 54; - if (ch == '.') {AddCh(); goto case 64;} - else {t.kind = 54; break;} case 61: - recEnd = pos; recKind = 81; - if (ch == '=') {AddCh(); goto case 41;} - else if (ch == '!') {AddCh(); goto case 42;} - else {t.kind = 81; break;} + recEnd = pos; recKind = 55; + if (ch == '.') {AddCh(); goto case 65;} + else {t.kind = 55; break;} case 62: - recEnd = pos; recKind = 75; - if (ch == '>') {AddCh(); goto case 33;} - else {t.kind = 75; break;} + recEnd = pos; recKind = 82; + if (ch == '=') {AddCh(); goto case 42;} + else if (ch == '!') {AddCh(); goto case 43;} + else {t.kind = 82; break;} case 63: recEnd = pos; recKind = 76; - if (ch == '=') {AddCh(); goto case 30;} + if (ch == '>') {AddCh(); goto case 34;} else {t.kind = 76; break;} case 64: - recEnd = pos; recKind = 98; + recEnd = pos; recKind = 77; + if (ch == '=') {AddCh(); goto case 31;} + else {t.kind = 77; break;} + case 65: + recEnd = pos; recKind = 99; if (ch == '.') {AddCh(); goto case 21;} - else {t.kind = 98; break;} + else {t.kind = 99; break;} } t.val = new String(tval, 0, tlen); diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index a285a577..29632ea4 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -3331,6 +3331,25 @@ namespace Microsoft.Dafny { TrStmt(s.hiddenUpdate, builder, locals, etran); } builder.Add(new Bpl.ReturnCmd(stmt.Tok)); + } else if (stmt is AssignSuchThatStmt) { + var s = (AssignSuchThatStmt)stmt; + AddComment(builder, s, "assign-such-that statement"); + // treat like a parallel havoc, followed by an assume + // Here comes the havoc part + var lhss = new List(); + var havocRhss = new List(); + foreach (var lhs in s.Lhss) { + lhss.Add(lhs.Resolved); + havocRhss.Add(new HavocRhs(lhs.tok)); // note, a HavocRhs is constructed as already resolved + } + List lhsBuilder; + List bLhss; + ProcessLhss(lhss, false, builder, locals, etran, out lhsBuilder, out bLhss); + ProcessRhss(lhsBuilder, bLhss, lhss, havocRhss, builder, locals, etran); + // End by doing the assume + TrStmt(s.Assume, builder, locals, etran); + builder.Add(CaptureState(s.Tok)); // just do one capture state--here, at the very end (that is, don't do one before the assume) + } else if (stmt is UpdateStmt) { var s = (UpdateStmt)stmt; // This UpdateStmt can be single-target assignment, a multi-assignment, a call statement, or diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 9995c817..22c24816 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -247,8 +247,47 @@ SmallTests.dfy(408,10): Error BP5003: A postcondition might not hold on this ret SmallTests.dfy(411,41): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon6_Else +SmallTests.dfy(561,12): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon3_Then + (0,0): anon2 +SmallTests.dfy(575,20): Error: left-hand sides 0 and 1 may refer to the same location +Execution trace: + (0,0): anon0 + (0,0): anon27_Then + (0,0): anon28_Then + (0,0): anon4 + (0,0): anon29_Then + (0,0): anon30_Then + (0,0): anon9 + (0,0): anon31_Then + (0,0): anon32_Then + (0,0): anon12 +SmallTests.dfy(577,15): Error: left-hand sides 1 and 2 may refer to the same location +Execution trace: + (0,0): anon0 + (0,0): anon27_Then + SmallTests.dfy(570,18): anon28_Else + (0,0): anon4 + (0,0): anon29_Else + (0,0): anon7 + (0,0): anon30_Then + (0,0): anon9 + (0,0): anon31_Else + (0,0): anon35_Then + (0,0): anon36_Then + (0,0): anon37_Then + (0,0): anon22 + (0,0): anon38_Then +SmallTests.dfy(584,18): Error: target object may be null +Execution trace: + (0,0): anon0 +SmallTests.dfy(597,10): Error: assertion violation +Execution trace: + (0,0): anon0 -Dafny program verifier finished with 58 verified, 21 errors +Dafny program verifier finished with 68 verified, 26 errors -------------------- Definedness.dfy -------------------- Definedness.dfy(8,7): Error: possible division by zero @@ -1598,8 +1637,47 @@ SmallTests.dfy(408,10): Error BP5003: A postcondition might not hold on this ret SmallTests.dfy(411,41): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon6_Else +SmallTests.dfy(561,12): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon3_Then + (0,0): anon2 +SmallTests.dfy(575,20): Error: left-hand sides 0 and 1 may refer to the same location +Execution trace: + (0,0): anon0 + (0,0): anon27_Then + (0,0): anon28_Then + (0,0): anon4 + (0,0): anon29_Then + (0,0): anon30_Then + (0,0): anon9 + (0,0): anon31_Then + (0,0): anon32_Then + (0,0): anon12 +SmallTests.dfy(577,15): Error: left-hand sides 1 and 2 may refer to the same location +Execution trace: + (0,0): anon0 + (0,0): anon27_Then + SmallTests.dfy(570,18): anon28_Else + (0,0): anon4 + (0,0): anon29_Else + (0,0): anon7 + (0,0): anon30_Then + (0,0): anon9 + (0,0): anon31_Else + (0,0): anon35_Then + (0,0): anon36_Then + (0,0): anon37_Then + (0,0): anon22 + (0,0): anon38_Then +SmallTests.dfy(584,18): Error: target object may be null +Execution trace: + (0,0): anon0 +SmallTests.dfy(597,10): Error: assertion violation +Execution trace: + (0,0): anon0 -Dafny program verifier finished with 58 verified, 21 errors +Dafny program verifier finished with 68 verified, 26 errors out.tmp.dfy(33,11): Error: index out of range Execution trace: (0,0): anon0 @@ -1707,8 +1785,47 @@ out.tmp.dfy(469,10): Error BP5003: A postcondition might not hold on this return out.tmp.dfy(470,41): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon6_Else +out.tmp.dfy(507,12): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon3_Then + (0,0): anon2 +out.tmp.dfy(521,20): Error: left-hand sides 0 and 1 may refer to the same location +Execution trace: + (0,0): anon0 + (0,0): anon27_Then + (0,0): anon28_Then + (0,0): anon4 + (0,0): anon29_Then + (0,0): anon30_Then + (0,0): anon9 + (0,0): anon31_Then + (0,0): anon32_Then + (0,0): anon12 +out.tmp.dfy(523,15): Error: left-hand sides 1 and 2 may refer to the same location +Execution trace: + (0,0): anon0 + (0,0): anon27_Then + out.tmp.dfy(516,18): anon28_Else + (0,0): anon4 + (0,0): anon29_Else + (0,0): anon7 + (0,0): anon30_Then + (0,0): anon9 + (0,0): anon31_Else + (0,0): anon35_Then + (0,0): anon36_Then + (0,0): anon37_Then + (0,0): anon22 + (0,0): anon38_Then +out.tmp.dfy(530,18): Error: target object may be null +Execution trace: + (0,0): anon0 +out.tmp.dfy(543,10): Error: assertion violation +Execution trace: + (0,0): anon0 -Dafny program verifier finished with 58 verified, 21 errors +Dafny program verifier finished with 68 verified, 26 errors -------------------- LetExpr.dfy -------------------- LetExpr.dfy(5,12): Error: assertion violation diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 914e228e..4d219cd3 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -535,3 +535,71 @@ static method TestNotNot() assert true == !(!true); } + +// ----------------------- Assign-such-that statements ------- + +method AssignSuchThat0(a: int, b: int) returns (x: int, y: int) + ensures x == a && y == b; +{ + if (*) { + x, y :| a <= x < a + 1 && b + a <= y + a && y <= b; + } else { + var xx, yy :| a <= xx < a + 1 && b + a <= yy + a && yy <= b; + x, y := xx, yy; + } +} + +method AssignSuchThat1(a: int, b: int) returns (x: int, y: int) +{ + var k :| 0 <= k < a - b; // this acts like an 'assume 0 < a - b;' + assert b < a; + k :| k == old(2*k); // note, the 'old' has no effect on local variables like k + assert k == 0; + var S := {2, 4, 7}; + var T :| T <= S; + assert 3 !in T; + assert T == {}; // error: T may be larger +} + +method AssignSuchThat2(i: int, j: int, ghost S: set) + modifies S; +{ + var n := new Node; + var a := new int[25]; + var t; + if (0 <= i < j < 25) { + a[i], t, a[j], n.next, n :| true; + } + if (n != null && n.next != null) { + assume n in S && n.next in S; + n.next.next, n.next :| n != null && n.next != null && n.next.next == n.next; // error: n.next may equal n (thus aliasing n.next.next and n.next) + } else if (0 <= i < 25 && 0 <= j < 25) { + t, a[i], a[j] :| t < a[i] < a[j]; // error: i may equal j (thus aliasing a[i] and a[j]) + } +} + +method AssignSuchThat3() +{ + var n := new Node; + n, n.next :| n.next == n; // error: RHS is not well defined (RHS is evaluated after the havocking of the LHS) +} + +method AssignSuchThat4() +{ + var n := new Node; + n, n.next :| n != null && n.next == n; // that's the ticket +} + +method AssignSuchThat5() +{ + var n := new Node; + n :| fresh(n); // fine + assert false; // error +} + +method AssignSuchThat6() +{ + var n: Node; + n :| n != null && fresh(n); // there is no non-null fresh object, so this amounts to 'assume false;' + assert false; // no problemo +} -- cgit v1.2.3