From 66a3f49f71dff8091919967b8dc49468435fdb00 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 5 Jan 2012 14:12:52 -0800 Subject: Dafny: firmed up the module system --- Source/Dafny/Dafny.atg | 6 +- Source/Dafny/DafnyAst.cs | 24 +- Source/Dafny/Parser.cs | 1017 +++++++++++++++++++++++----------------------- Source/Dafny/Printer.cs | 7 +- Source/Dafny/Resolver.cs | 186 +++++++-- Source/Dafny/Scanner.cs | 207 +++++----- 6 files changed, 785 insertions(+), 662 deletions(-) (limited to 'Source/Dafny') diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index ddb8d15e..f072747c 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -156,11 +156,13 @@ Dafny defaultModuleCreatedHere = true; defaultModule = new DefaultModuleDecl(); } + IToken idRefined = null; .) { "module" (. attrs = null; theImports = new List(); .) { Attribute } - Ident - [ "imports" Idents ] (. module = new ModuleDecl(id, id.val, theImports, attrs); .) + Ident (. defaultModule.ImportNames.Add(id.val); .) + [ "refines" Ident ] + [ "imports" Idents ] (. module = new ModuleDecl(id, id.val, idRefined == null ? null : idRefined.val, theImports, attrs); .) "{" (. module.BodyStartTok = t; .) { ClassDecl (. module.TopLevelDecls.Add(c); .) | DatatypeDecl (. module.TopLevelDecls.Add(dt); .) diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 86342409..7884b40c 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -32,7 +32,7 @@ namespace Microsoft.Dafny { public class BuiltIns { - public readonly ModuleDecl SystemModule = new ModuleDecl(Token.NoToken, "_System", new List(), null); + public readonly ModuleDecl SystemModule = new ModuleDecl(Token.NoToken, "_System", null, new List(), null); Dictionary arrayTypeDecls = new Dictionary(); public BuiltIns() { @@ -604,26 +604,34 @@ namespace Microsoft.Dafny { } public class ModuleDecl : Declaration { - public readonly List/*!*/ Imports; + public readonly string RefinementBaseName; // null if no refinement base + public ModuleDecl RefinementBase; // filled in during resolution (null if no refinement base) + public readonly List/*!*/ ImportNames; // contains no duplicates + public readonly List/*!*/ Imports = new List(); // filled in during resolution, contains no duplicates public readonly List TopLevelDecls = new List(); // filled in by the parser; readonly after that public readonly Graph CallGraph = new Graph(); // filled in during resolution public int Height; // height in the topological sorting of modules; filled in during resolution [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(Imports)); + Contract.Invariant(cce.NonNullElements(ImportNames)); Contract.Invariant(cce.NonNullElements(TopLevelDecls)); Contract.Invariant(CallGraph != null); } - - public ModuleDecl(IToken tok, string name, [Captured] List/*!*/ imports, Attributes attributes) + public ModuleDecl(IToken tok, string name, string refinementBase, [Captured] List/*!*/ imports, Attributes attributes) : base(tok, name, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(imports)); - Imports = imports; - + RefinementBaseName = refinementBase; + // set "ImportNames" to "imports" minus any duplicates + ImportNames = new List(); + foreach (var nm in imports) { + if (!ImportNames.Contains(nm)) { + ImportNames.Add(nm); + } + } } public virtual bool IsDefaultModule { get { @@ -633,7 +641,7 @@ namespace Microsoft.Dafny { } public class DefaultModuleDecl : ModuleDecl { - public DefaultModuleDecl() : base(Token.NoToken, "_default", new List(), null) { + public DefaultModuleDecl() : base(Token.NoToken, "_default", null, new List(), null) { } public override bool IsDefaultModule { get { diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index f344aa76..cc87bdab 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/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 = 102; + public const int maxT = 103; const bool T = true; const bool x = false; @@ -206,6 +206,7 @@ bool IsAttribute() { defaultModuleCreatedHere = true; defaultModule = new DefaultModuleDecl(); } + IToken idRefined = null; while (StartOf(1)) { if (la.kind == 8) { @@ -215,18 +216,23 @@ bool IsAttribute() { Attribute(ref attrs); } Ident(out id); + defaultModule.ImportNames.Add(id.val); if (la.kind == 9) { + Get(); + Ident(out idRefined); + } + if (la.kind == 10) { Get(); Idents(theImports); } - module = new ModuleDecl(id, id.val, theImports, attrs); + module = new ModuleDecl(id, id.val, idRefined == null ? null : idRefined.val, theImports, attrs); Expect(6); module.BodyStartTok = t; - while (la.kind == 10 || la.kind == 14 || la.kind == 20) { - if (la.kind == 10) { + while (la.kind == 11 || la.kind == 15 || la.kind == 21) { + if (la.kind == 11) { ClassDecl(module, out c); module.TopLevelDecls.Add(c); - } else if (la.kind == 14) { + } else if (la.kind == 15) { DatatypeDecl(module, out dt); module.TopLevelDecls.Add(dt); } else { @@ -237,13 +243,13 @@ bool IsAttribute() { Expect(7); module.BodyEndTok = t; theModules.Add(module); - } else if (la.kind == 10) { + } else if (la.kind == 11) { ClassDecl(defaultModule, out c); defaultModule.TopLevelDecls.Add(c); - } else if (la.kind == 14) { + } else if (la.kind == 15) { DatatypeDecl(defaultModule, out dt); defaultModule.TopLevelDecls.Add(dt); - } else if (la.kind == 20) { + } else if (la.kind == 21) { ArbitraryTypeDecl(defaultModule, out at); defaultModule.TopLevelDecls.Add(at); } else { @@ -283,7 +289,7 @@ bool IsAttribute() { IToken/*!*/ id; Ident(out id); ids.Add(id.val); - while (la.kind == 19) { + while (la.kind == 20) { Get(); Ident(out id); ids.Add(id.val); @@ -299,13 +305,13 @@ bool IsAttribute() { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 10)) {SynErr(103); Get();} - Expect(10); + while (!(la.kind == 0 || la.kind == 11)) {SynErr(104); Get();} + Expect(11); while (la.kind == 6) { Attribute(ref attrs); } Ident(out id); - if (la.kind == 21) { + if (la.kind == 22) { GenericParameters(typeArgs); } Expect(6); @@ -329,24 +335,24 @@ bool IsAttribute() { List ctors = new List(); IToken bodyStart = Token.NoToken; // dummy assignment - while (!(la.kind == 0 || la.kind == 14)) {SynErr(104); Get();} - Expect(14); + while (!(la.kind == 0 || la.kind == 15)) {SynErr(105); Get();} + Expect(15); while (la.kind == 6) { Attribute(ref attrs); } Ident(out id); - if (la.kind == 21) { + if (la.kind == 22) { GenericParameters(typeArgs); } - Expect(15); + Expect(16); bodyStart = t; DatatypeMemberDecl(ctors); - while (la.kind == 16) { + while (la.kind == 17) { Get(); DatatypeMemberDecl(ctors); } - while (!(la.kind == 0 || la.kind == 17)) {SynErr(105); Get();} - Expect(17); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(106); Get();} + Expect(18); dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); dt.BodyStartTok = bodyStart; dt.BodyEndTok = t; @@ -357,14 +363,14 @@ bool IsAttribute() { IToken/*!*/ id; Attributes attrs = null; - Expect(20); + Expect(21); while (la.kind == 6) { Attribute(ref attrs); } Ident(out id); at = new ArbitraryTypeDecl(id, id.val, module, attrs); - while (!(la.kind == 0 || la.kind == 17)) {SynErr(106); Get();} - Expect(17); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(107); Get();} + Expect(18); } void ClassMemberDecl(List/*!*/ mm, bool allowConstructors) { @@ -373,11 +379,11 @@ bool IsAttribute() { Function/*!*/ f; MemberModifiers mmod = new MemberModifiers(); - while (la.kind == 11 || la.kind == 12 || la.kind == 13) { - if (la.kind == 11) { + while (la.kind == 12 || la.kind == 13 || la.kind == 14) { + if (la.kind == 12) { Get(); mmod.IsGhost = true; - } else if (la.kind == 12) { + } else if (la.kind == 13) { Get(); mmod.IsStatic = true; } else { @@ -385,29 +391,29 @@ bool IsAttribute() { mmod.IsUnlimited = true; } } - if (la.kind == 18) { + if (la.kind == 19) { FieldDecl(mmod, mm); - } else if (la.kind == 40) { + } else if (la.kind == 41) { FunctionDecl(mmod, out f); mm.Add(f); - } else if (la.kind == 23 || la.kind == 24) { + } else if (la.kind == 24 || la.kind == 25) { MethodDecl(mmod, allowConstructors, out m); mm.Add(m); - } else SynErr(107); + } else SynErr(108); } void GenericParameters(List/*!*/ typeArgs) { Contract.Requires(cce.NonNullElements(typeArgs)); IToken/*!*/ id; - Expect(21); + Expect(22); Ident(out id); typeArgs.Add(new TypeParameter(id, id.val)); - while (la.kind == 19) { + while (la.kind == 20) { Get(); Ident(out id); typeArgs.Add(new TypeParameter(id, id.val)); } - Expect(22); + Expect(23); } void FieldDecl(MemberModifiers mmod, List/*!*/ mm) { @@ -415,8 +421,8 @@ bool IsAttribute() { Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; - while (!(la.kind == 0 || la.kind == 18)) {SynErr(108); Get();} - Expect(18); + while (!(la.kind == 0 || la.kind == 19)) {SynErr(109); Get();} + Expect(19); if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); } if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } @@ -425,13 +431,13 @@ bool IsAttribute() { } IdentType(out id, out ty); mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); - while (la.kind == 19) { + while (la.kind == 20) { Get(); IdentType(out id, out ty); mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); } - while (!(la.kind == 0 || la.kind == 17)) {SynErr(109); Get();} - Expect(17); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(110); Get();} + Expect(18); } void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) { @@ -450,8 +456,8 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - Expect(40); - if (la.kind == 23) { + Expect(41); + if (la.kind == 24) { Get(); isFunctionMethod = true; } @@ -461,7 +467,7 @@ bool IsAttribute() { Attribute(ref attrs); } Ident(out id); - if (la.kind == 21) { + if (la.kind == 22) { GenericParameters(typeArgs); } Formals(true, isFunctionMethod, formals); @@ -498,10 +504,10 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(la.kind == 0 || la.kind == 23 || la.kind == 24)) {SynErr(110); Get();} - if (la.kind == 23) { + while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(111); Get();} + if (la.kind == 24) { Get(); - } else if (la.kind == 24) { + } else if (la.kind == 25) { Get(); if (allowConstructor) { isConstructor = true; @@ -509,7 +515,7 @@ bool IsAttribute() { SemErr(t, "constructors are only allowed in classes"); } - } else SynErr(111); + } else SynErr(112); if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); } if (isConstructor) { if (mmod.IsGhost) { @@ -524,11 +530,11 @@ bool IsAttribute() { Attribute(ref attrs); } Ident(out id); - if (la.kind == 21) { + if (la.kind == 22) { GenericParameters(typeArgs); } Formals(true, !mmod.IsGhost, ins); - if (la.kind == 25) { + if (la.kind == 26) { Get(); if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } Formals(false, !mmod.IsGhost, outs); @@ -559,7 +565,7 @@ bool IsAttribute() { Attribute(ref attrs); } Ident(out id); - if (la.kind == 31) { + if (la.kind == 32) { FormalsOptionalIds(formals); } ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); @@ -567,17 +573,17 @@ bool IsAttribute() { void FormalsOptionalIds(List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; - Expect(31); + Expect(32); if (StartOf(5)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); - while (la.kind == 19) { + while (la.kind == 20) { Get(); TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); } } - Expect(32); + Expect(33); } void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) { @@ -591,7 +597,7 @@ bool IsAttribute() { Contract.Ensures(Contract.ValueAtReturn(out id)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty)!=null); isGhost = false; - if (la.kind == 11) { + if (la.kind == 12) { Get(); if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } } @@ -632,7 +638,7 @@ bool IsAttribute() { Contract.Ensures(Contract.ValueAtReturn(out ty)!=null); Contract.Ensures(Contract.ValueAtReturn(out identName)!=null); string name = null; isGhost = false; - if (la.kind == 11) { + if (la.kind == 12) { Get(); isGhost = true; } @@ -661,22 +667,22 @@ bool IsAttribute() { List/*!*/ gt; switch (la.kind) { - case 33: { + case 34: { Get(); tok = t; break; } - case 34: { + case 35: { Get(); tok = t; ty = new NatType(); break; } - case 35: { + case 36: { Get(); tok = t; ty = new IntType(); break; } - case 36: { + case 37: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -687,7 +693,7 @@ bool IsAttribute() { break; } - case 37: { + case 38: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -698,7 +704,7 @@ bool IsAttribute() { break; } - case 38: { + case 39: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -709,27 +715,27 @@ bool IsAttribute() { break; } - case 1: case 3: case 39: { + case 1: case 3: case 40: { ReferenceType(out tok, out ty); break; } - default: SynErr(112); break; + default: SynErr(113); break; } } void Formals(bool incoming, bool allowGhostKeyword, List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; - Expect(31); - if (la.kind == 1 || la.kind == 11) { + Expect(32); + if (la.kind == 1 || la.kind == 12) { GIdentType(allowGhostKeyword, out id, out ty, out isGhost); formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); - while (la.kind == 19) { + while (la.kind == 20) { Get(); GIdentType(allowGhostKeyword, out id, out ty, out isGhost); formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); } } - Expect(32); + Expect(33); } void MethodSpec(List/*!*/ req, List/*!*/ mod, List/*!*/ ens, @@ -737,8 +743,8 @@ 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(6))) {SynErr(113); Get();} - if (la.kind == 26) { + while (!(StartOf(6))) {SynErr(114); Get();} + if (la.kind == 27) { Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -746,44 +752,44 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(7)) { FrameExpression(out fe); mod.Add(fe); - while (la.kind == 19) { + while (la.kind == 20) { Get(); FrameExpression(out fe); mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 17)) {SynErr(114); Get();} - Expect(17); - } else if (la.kind == 27 || la.kind == 28 || la.kind == 29) { - if (la.kind == 27) { + while (!(la.kind == 0 || la.kind == 18)) {SynErr(115); Get();} + Expect(18); + } else if (la.kind == 28 || la.kind == 29 || la.kind == 30) { + if (la.kind == 28) { Get(); isFree = true; } - if (la.kind == 28) { + if (la.kind == 29) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 17)) {SynErr(115); Get();} - Expect(17); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(116); Get();} + Expect(18); req.Add(new MaybeFreeExpression(e, isFree)); - } else if (la.kind == 29) { + } else if (la.kind == 30) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); } Expression(out e); - while (!(la.kind == 0 || la.kind == 17)) {SynErr(116); Get();} - Expect(17); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(117); Get();} + Expect(18); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); - } else SynErr(117); - } else if (la.kind == 30) { + } else SynErr(118); + } else if (la.kind == 31) { Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 17)) {SynErr(118); Get();} - Expect(17); - } else SynErr(119); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(119); Get();} + Expect(18); + } else SynErr(120); } void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -803,7 +809,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void FrameExpression(out FrameExpression/*!*/ fe) { Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; Expression(out e); - if (la.kind == 43) { + if (la.kind == 44) { Get(); Ident(out id); fieldName = id.val; @@ -824,7 +830,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo decreases.Add(e); } - while (la.kind == 19) { + while (la.kind == 20) { Get(); PossiblyWildExpression(out e); if (!allowWildcard && e is WildcardExpr) { @@ -838,15 +844,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void GenericInstantiation(List/*!*/ gt) { Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; - Expect(21); + Expect(22); Type(out ty); gt.Add(ty); - while (la.kind == 19) { + while (la.kind == 20) { Get(); Type(out ty); gt.Add(ty); } - Expect(22); + Expect(23); } void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) { @@ -854,7 +860,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ List/*!*/ gt; - if (la.kind == 39) { + if (la.kind == 40) { Get(); tok = t; ty = new ObjectType(); } else if (la.kind == 3) { @@ -873,48 +879,48 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 1) { Ident(out tok); gt = new List(); - if (la.kind == 21) { + if (la.kind == 22) { GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt); - } else SynErr(120); + } else SynErr(121); } 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 == 28) { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(121); Get();} + if (la.kind == 29) { + while (!(la.kind == 0 || la.kind == 29)) {SynErr(122); Get();} Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 17)) {SynErr(122); Get();} - Expect(17); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(123); Get();} + Expect(18); reqs.Add(e); - } else if (la.kind == 41) { + } else if (la.kind == 42) { Get(); if (StartOf(9)) { PossiblyWildFrameExpression(out fe); reads.Add(fe); - while (la.kind == 19) { + while (la.kind == 20) { Get(); PossiblyWildFrameExpression(out fe); reads.Add(fe); } } - while (!(la.kind == 0 || la.kind == 17)) {SynErr(123); Get();} - Expect(17); - } else if (la.kind == 29) { + while (!(la.kind == 0 || la.kind == 18)) {SynErr(124); Get();} + Expect(18); + } else if (la.kind == 30) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 17)) {SynErr(124); Get();} - Expect(17); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(125); Get();} + Expect(18); ens.Add(e); - } else if (la.kind == 30) { + } else if (la.kind == 31) { Get(); DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 17)) {SynErr(125); Get();} - Expect(17); - } else SynErr(126); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(126); Get();} + Expect(18); + } else SynErr(127); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -928,23 +934,23 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) { Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; - if (la.kind == 42) { + if (la.kind == 43) { Get(); fe = new FrameExpression(new WildcardExpr(t), null); } else if (StartOf(7)) { FrameExpression(out fe); - } else SynErr(127); + } else SynErr(128); } void PossiblyWildExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e)!=null); e = dummyExpr; - if (la.kind == 42) { + if (la.kind == 43) { Get(); e = new WildcardExpr(t); } else if (StartOf(7)) { Expression(out e); - } else SynErr(128); + } else SynErr(129); } void Stmt(List/*!*/ ss) { @@ -960,49 +966,49 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd; int breakCount; - while (!(StartOf(10))) {SynErr(129); Get();} + while (!(StartOf(10))) {SynErr(130); Get();} switch (la.kind) { case 6: { BlockStmt(out s, out bodyStart, out bodyEnd); break; } - case 60: { + case 61: { AssertStmt(out s); break; } - case 61: { + case 62: { AssumeStmt(out s); break; } - case 62: { + case 63: { PrintStmt(out s); break; } - case 1: case 2: case 16: case 31: case 87: case 88: case 89: case 90: case 91: case 92: case 93: { + case 1: case 2: case 17: case 32: case 88: case 89: case 90: case 91: case 92: case 93: case 94: { UpdateStmt(out s); break; } - case 11: case 18: { + case 12: case 19: { VarDeclStatement(out s); break; } - case 53: { + case 54: { IfStmt(out s); break; } - case 57: { + case 58: { WhileStmt(out s); break; } - case 59: { + case 60: { MatchStmt(out s); break; } - case 63: { + case 64: { ParallelStmt(out s); break; } - case 44: { + case 45: { Get(); x = t; Ident(out id); @@ -1011,49 +1017,49 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LabelNode(x, id.val, s.Labels); break; } - case 45: { + case 46: { Get(); x = t; breakCount = 1; label = null; if (la.kind == 1) { Ident(out id); label = id.val; - } else if (la.kind == 17 || la.kind == 45) { - while (la.kind == 45) { + } else if (la.kind == 18 || la.kind == 46) { + while (la.kind == 46) { Get(); breakCount++; } - } else SynErr(130); - while (!(la.kind == 0 || la.kind == 17)) {SynErr(131); Get();} - Expect(17); + } else SynErr(131); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(132); Get();} + Expect(18); s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); break; } - case 46: { + case 47: { ReturnStmt(out s); break; } - default: SynErr(132); break; + default: SynErr(133); break; } } void AssertStmt(out Statement/*!*/ s) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; Attributes attrs = null; - Expect(60); + Expect(61); x = t; s = null; while (IsAttribute()) { Attribute(ref attrs); } Expression(out e); s = new AssertStmt(x, e, attrs); - Expect(17); + Expect(18); } void AssumeStmt(out Statement/*!*/ s) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; - Expect(61); + Expect(62); x = t; Expression(out e); - Expect(17); + Expect(18); s = new AssumeStmt(x, e); } @@ -1061,16 +1067,16 @@ 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(62); + Expect(63); x = t; AttributeArg(out arg); args.Add(arg); - while (la.kind == 19) { + while (la.kind == 20) { Get(); AttributeArg(out arg); args.Add(arg); } - Expect(17); + Expect(18); s = new PrintStmt(x, args); } @@ -1084,33 +1090,33 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Lhs(out e); x = e.tok; - if (la.kind == 6 || la.kind == 17) { + if (la.kind == 6 || la.kind == 18) { while (IsAttribute()) { Attribute(ref attrs); } - Expect(17); + Expect(18); rhss.Add(new ExprRhs(e, attrs)); - } else if (la.kind == 19 || la.kind == 47) { + } else if (la.kind == 20 || la.kind == 48) { lhss.Add(e); lhs0 = e; - while (la.kind == 19) { + while (la.kind == 20) { Get(); Lhs(out e); lhss.Add(e); } - Expect(47); + Expect(48); x = t; Rhs(out r, lhs0); rhss.Add(r); - while (la.kind == 19) { + while (la.kind == 20) { Get(); Rhs(out r, lhs0); rhss.Add(r); } - Expect(17); + Expect(18); } else if (la.kind == 5) { Get(); SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); - } else SynErr(133); + } else SynErr(134); s = new UpdateStmt(x, lhss, rhss); } @@ -1121,20 +1127,20 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List lhss = new List(); List rhss = new List(); - if (la.kind == 11) { + if (la.kind == 12) { Get(); isGhost = true; x = t; } - Expect(18); + Expect(19); if (!isGhost) { x = t; } LocalIdentTypeOptional(out d, isGhost); lhss.Add(d); - while (la.kind == 19) { + while (la.kind == 20) { Get(); LocalIdentTypeOptional(out d, isGhost); lhss.Add(d); } - if (la.kind == 47) { + if (la.kind == 48) { Get(); assignTok = t; lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); @@ -1142,13 +1148,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0); rhss.Add(r); - while (la.kind == 19) { + while (la.kind == 20) { Get(); Rhs(out r, lhs0); rhss.Add(r); } } - Expect(17); + Expect(18); UpdateStmt update; if (rhss.Count == 0) { update = null; @@ -1173,26 +1179,26 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List alternatives; ifStmt = dummyStmt; // to please the compiler - Expect(53); + Expect(54); x = t; - if (la.kind == 31) { + if (la.kind == 32) { Guard(out guard); BlockStmt(out thn, out bodyStart, out bodyEnd); - if (la.kind == 54) { + if (la.kind == 55) { Get(); - if (la.kind == 53) { + if (la.kind == 54) { IfStmt(out s); els = s; } else if (la.kind == 6) { BlockStmt(out s, out bodyStart, out bodyEnd); els = s; - } else SynErr(134); + } else SynErr(135); } ifStmt = new IfStmt(x, guard, thn, els); } else if (la.kind == 6) { AlternativeBlock(out alternatives); ifStmt = new AlternativeStmt(x, alternatives); - } else SynErr(135); + } else SynErr(136); } void WhileStmt(out Statement/*!*/ stmt) { @@ -1208,9 +1214,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List alternatives; stmt = dummyStmt; // to please the compiler - Expect(57); + Expect(58); x = t; - if (la.kind == 31) { + if (la.kind == 32) { Guard(out guard); Contract.Assume(guard == null || cce.Owner.None(guard)); LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs); @@ -1220,18 +1226,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(136); + } else SynErr(137); } void MatchStmt(out Statement/*!*/ s) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c; List cases = new List(); - Expect(59); + Expect(60); x = t; Expression(out e); Expect(6); - while (la.kind == 55) { + while (la.kind == 56) { CaseStatement(out c); cases.Add(c); } @@ -1251,21 +1257,21 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Statement/*!*/ block; IToken bodyStart, bodyEnd; - Expect(63); + Expect(64); x = t; - Expect(31); + Expect(32); QuantifierDomain(out bvars, out attrs, out range); if (range == null) { range = new LiteralExpr(x, true); } - Expect(32); - while (la.kind == 27 || la.kind == 29) { + Expect(33); + while (la.kind == 28 || la.kind == 30) { isFree = false; - if (la.kind == 27) { + if (la.kind == 28) { Get(); isFree = true; } - Expect(29); + Expect(30); Expression(out e); - Expect(17); + Expect(18); ens.Add(new MaybeFreeExpression(e, isFree)); } BlockStmt(out block, out bodyStart, out bodyEnd); @@ -1277,18 +1283,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List rhss = null; AssignmentRhs r; - Expect(46); + Expect(47); returnTok = t; if (StartOf(12)) { Rhs(out r, null); rhss = new List(); rhss.Add(r); - while (la.kind == 19) { + while (la.kind == 20) { Get(); Rhs(out r, null); rhss.Add(r); } } - Expect(17); + Expect(18); s = new ReturnStmt(returnTok, rhss); } @@ -1301,27 +1307,27 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = null; // to please compiler Attributes attrs = null; - if (la.kind == 48) { + if (la.kind == 49) { Get(); newToken = t; TypeAndToken(out x, out ty); - if (la.kind == 49 || la.kind == 51) { - if (la.kind == 49) { + if (la.kind == 50 || la.kind == 52) { + if (la.kind == 50) { Get(); ee = new List(); Expressions(ee); - Expect(50); + Expect(51); UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true); } else { Get(); Ident(out x); - Expect(31); + Expect(32); args = new List(); if (StartOf(7)) { Expressions(args); } - Expect(32); + Expect(33); initCall = new CallStmt(x, new List(), receiverForInitCall, x.val, args); } @@ -1332,18 +1338,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = new TypeRhs(newToken, ty, initCall); } - } else if (la.kind == 52) { + } else if (la.kind == 53) { Get(); x = t; Expression(out e); r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); - } else if (la.kind == 42) { + } else if (la.kind == 43) { Get(); r = new HavocRhs(t); } else if (StartOf(7)) { Expression(out e); r = new ExprRhs(e); - } else SynErr(137); + } else SynErr(138); while (IsAttribute()) { Attribute(ref attrs); } @@ -1355,23 +1361,23 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) { DottedIdentifiersAndFunction(out e); - while (la.kind == 49 || la.kind == 51) { + while (la.kind == 50 || la.kind == 52) { Suffix(ref e); } } else if (StartOf(13)) { ConstAtomExpression(out e); Suffix(ref e); - while (la.kind == 49 || la.kind == 51) { + while (la.kind == 50 || la.kind == 52) { Suffix(ref e); } - } else SynErr(138); + } else SynErr(139); } void Expressions(List/*!*/ args) { Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; Expression(out e); args.Add(e); - while (la.kind == 19) { + while (la.kind == 20) { Get(); Expression(out e); args.Add(e); @@ -1380,15 +1386,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Guard(out Expression e) { Expression/*!*/ ee; e = null; - Expect(31); - if (la.kind == 42) { + Expect(32); + if (la.kind == 43) { Get(); e = null; } else if (StartOf(7)) { Expression(out ee); e = ee; - } else SynErr(139); - Expect(32); + } else SynErr(140); + Expect(33); } void AlternativeBlock(out List alternatives) { @@ -1398,11 +1404,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List body; Expect(6); - while (la.kind == 55) { + while (la.kind == 56) { Get(); x = t; Expression(out e); - Expect(56); + Expect(57); body = new List(); while (StartOf(8)) { Stmt(body); @@ -1420,22 +1426,22 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod = null; while (StartOf(14)) { - if (la.kind == 27 || la.kind == 58) { + if (la.kind == 28 || la.kind == 59) { Invariant(out invariant); - while (!(la.kind == 0 || la.kind == 17)) {SynErr(140); Get();} - Expect(17); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(141); Get();} + Expect(18); invariants.Add(invariant); - } else if (la.kind == 30) { - while (!(la.kind == 0 || la.kind == 30)) {SynErr(141); Get();} + } else if (la.kind == 31) { + while (!(la.kind == 0 || la.kind == 31)) {SynErr(142); Get();} Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, true); - while (!(la.kind == 0 || la.kind == 17)) {SynErr(142); Get();} - Expect(17); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(143); Get();} + Expect(18); } else { - while (!(la.kind == 0 || la.kind == 26)) {SynErr(143); Get();} + while (!(la.kind == 0 || la.kind == 27)) {SynErr(144); Get();} Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -1444,26 +1450,26 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(7)) { FrameExpression(out fe); mod.Add(fe); - while (la.kind == 19) { + while (la.kind == 20) { Get(); FrameExpression(out fe); mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 17)) {SynErr(144); Get();} - Expect(17); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(145); Get();} + Expect(18); } } } 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 == 27 || la.kind == 58)) {SynErr(145); Get();} - if (la.kind == 27) { + while (!(la.kind == 0 || la.kind == 28 || la.kind == 59)) {SynErr(146); Get();} + if (la.kind == 28) { Get(); isFree = true; } - Expect(58); + Expect(59); while (IsAttribute()) { Attribute(ref attrs); } @@ -1478,21 +1484,21 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv; List body = new List(); - Expect(55); + Expect(56); x = t; Ident(out id); - if (la.kind == 31) { + if (la.kind == 32) { Get(); IdentTypeOptional(out bv); arguments.Add(bv); - while (la.kind == 19) { + while (la.kind == 20) { Get(); IdentTypeOptional(out bv); arguments.Add(bv); } - Expect(32); + Expect(33); } - Expect(56); + Expect(57); while (StartOf(8)) { Stmt(body); } @@ -1507,7 +1513,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(7)) { Expression(out e); arg = new Attributes.Argument(t, e); - } else SynErr(146); + } else SynErr(147); } void QuantifierDomain(out List bvars, out Attributes attrs, out Expression range) { @@ -1518,7 +1524,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv); bvars.Add(bv); - while (la.kind == 19) { + while (la.kind == 20) { Get(); IdentTypeOptional(out bv); bvars.Add(bv); @@ -1526,7 +1532,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 6) { Attribute(ref attrs); } - if (la.kind == 16) { + if (la.kind == 17) { Get(); Expression(out range); } @@ -1535,7 +1541,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 == 64 || la.kind == 65) { + while (la.kind == 65 || la.kind == 66) { EquivOp(); x = t; ImpliesExpression(out e1); @@ -1546,7 +1552,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 == 66 || la.kind == 67) { + if (la.kind == 67 || la.kind == 68) { ImpliesOp(); x = t; ImpliesExpression(out e1); @@ -1555,23 +1561,23 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } void EquivOp() { - if (la.kind == 64) { + if (la.kind == 65) { Get(); - } else if (la.kind == 65) { + } else if (la.kind == 66) { Get(); - } else SynErr(147); + } else SynErr(148); } void LogicalExpression(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; RelationalExpression(out e0); if (StartOf(15)) { - if (la.kind == 68 || la.kind == 69) { + if (la.kind == 69 || la.kind == 70) { AndOp(); x = t; RelationalExpression(out e1); e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); - while (la.kind == 68 || la.kind == 69) { + while (la.kind == 69 || la.kind == 70) { AndOp(); x = t; RelationalExpression(out e1); @@ -1582,7 +1588,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 == 70 || la.kind == 71) { + while (la.kind == 71 || la.kind == 72) { OrOp(); x = t; RelationalExpression(out e1); @@ -1593,11 +1599,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } void ImpliesOp() { - if (la.kind == 66) { + if (la.kind == 67) { Get(); - } else if (la.kind == 67) { + } else if (la.kind == 68) { Get(); - } else SynErr(148); + } else SynErr(149); } void RelationalExpression(out Expression/*!*/ e) { @@ -1691,25 +1697,25 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } void AndOp() { - if (la.kind == 68) { + if (la.kind == 69) { Get(); - } else if (la.kind == 69) { + } else if (la.kind == 70) { Get(); - } else SynErr(149); + } else SynErr(150); } void OrOp() { - if (la.kind == 70) { + if (la.kind == 71) { Get(); - } else if (la.kind == 71) { + } else if (la.kind == 72) { Get(); - } else SynErr(150); + } else SynErr(151); } 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 == 82 || la.kind == 83) { + while (la.kind == 83 || la.kind == 84) { AddOp(out x, out op); Factor(out e1); e0 = new BinaryExpr(x, op, e0, e1); @@ -1722,50 +1728,50 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken y; switch (la.kind) { - case 72: { + case 73: { Get(); x = t; op = BinaryExpr.Opcode.Eq; break; } - case 21: { + case 22: { Get(); x = t; op = BinaryExpr.Opcode.Lt; break; } - case 22: { + case 23: { Get(); x = t; op = BinaryExpr.Opcode.Gt; break; } - case 73: { + case 74: { Get(); x = t; op = BinaryExpr.Opcode.Le; break; } - case 74: { + case 75: { Get(); x = t; op = BinaryExpr.Opcode.Ge; break; } - case 75: { + case 76: { Get(); x = t; op = BinaryExpr.Opcode.Neq; break; } - case 76: { + case 77: { Get(); x = t; op = BinaryExpr.Opcode.Disjoint; break; } - case 77: { + case 78: { Get(); x = t; op = BinaryExpr.Opcode.In; break; } - case 78: { + case 79: { Get(); x = t; y = Token.NoToken; - if (la.kind == 77) { + if (la.kind == 78) { Get(); y = t; } @@ -1780,29 +1786,29 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break; } - case 79: { + case 80: { Get(); x = t; op = BinaryExpr.Opcode.Neq; break; } - case 80: { + case 81: { Get(); x = t; op = BinaryExpr.Opcode.Le; break; } - case 81: { + case 82: { Get(); x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(151); break; + default: SynErr(152); 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 == 42 || la.kind == 84 || la.kind == 85) { + while (la.kind == 43 || la.kind == 85 || la.kind == 86) { MulOp(out x, out op); UnaryExpression(out e1); e0 = new BinaryExpr(x, op, e0, e1); @@ -1811,82 +1817,82 @@ 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 == 82) { + if (la.kind == 83) { Get(); x = t; op = BinaryExpr.Opcode.Add; - } else if (la.kind == 83) { + } else if (la.kind == 84) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(152); + } else SynErr(153); } void UnaryExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; switch (la.kind) { - case 83: { + case 84: { Get(); x = t; UnaryExpression(out e); e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); break; } - case 78: case 86: { + case 79: case 87: { NegOp(); x = t; UnaryExpression(out e); e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); break; } - case 18: case 36: case 53: case 59: case 60: case 61: case 96: case 97: case 98: case 99: { + case 19: case 37: case 54: case 60: case 61: case 62: case 97: case 98: case 99: case 100: { EndlessExpression(out e); break; } case 1: { DottedIdentifiersAndFunction(out e); - while (la.kind == 49 || la.kind == 51) { + while (la.kind == 50 || la.kind == 52) { Suffix(ref e); } break; } - case 6: case 49: { + case 6: case 50: { DisplayExpr(out e); break; } - case 37: { + case 38: { MultiSetExpr(out e); break; } - case 2: case 16: case 31: case 87: case 88: case 89: case 90: case 91: case 92: case 93: { + case 2: case 17: case 32: case 88: case 89: case 90: case 91: case 92: case 93: case 94: { ConstAtomExpression(out e); - while (la.kind == 49 || la.kind == 51) { + while (la.kind == 50 || la.kind == 52) { Suffix(ref e); } break; } - default: SynErr(153); break; + default: SynErr(154); break; } } void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; - if (la.kind == 42) { + if (la.kind == 43) { Get(); x = t; op = BinaryExpr.Opcode.Mul; - } else if (la.kind == 84) { + } else if (la.kind == 85) { Get(); x = t; op = BinaryExpr.Opcode.Div; - } else if (la.kind == 85) { + } else if (la.kind == 86) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(154); + } else SynErr(155); } void NegOp() { - if (la.kind == 78) { + if (la.kind == 79) { Get(); - } else if (la.kind == 86) { + } else if (la.kind == 87) { Get(); - } else SynErr(155); + } else SynErr(156); } void EndlessExpression(out Expression e) { @@ -1897,73 +1903,73 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List letVars; List letRHSs; switch (la.kind) { - case 53: { + case 54: { Get(); x = t; Expression(out e); - Expect(94); + Expect(95); Expression(out e0); - Expect(54); + Expect(55); Expression(out e1); e = new ITEExpr(x, e, e0, e1); break; } - case 59: { + case 60: { MatchExpression(out e); break; } - case 96: case 97: case 98: case 99: { + case 97: case 98: case 99: case 100: { QuantifierGuts(out e); break; } - case 36: { + case 37: { ComprehensionExpr(out e); break; } - case 60: { + case 61: { Get(); x = t; Expression(out e0); - Expect(17); + Expect(18); Expression(out e1); e = new AssertExpr(x, e0, e1); break; } - case 61: { + case 62: { Get(); x = t; Expression(out e0); - Expect(17); + Expect(18); Expression(out e1); e = new AssumeExpr(x, e0, e1); break; } - case 18: { + case 19: { Get(); x = t; letVars = new List(); letRHSs = new List(); IdentTypeOptional(out d); letVars.Add(d); - while (la.kind == 19) { + while (la.kind == 20) { Get(); IdentTypeOptional(out d); letVars.Add(d); } - Expect(47); + Expect(48); Expression(out e); letRHSs.Add(e); - while (la.kind == 19) { + while (la.kind == 20) { Get(); Expression(out e); letRHSs.Add(e); } - Expect(17); + Expect(18); Expression(out e); e = new LetExpr(x, letVars, letRHSs, e); break; } - default: SynErr(156); break; + default: SynErr(157); break; } } @@ -1974,18 +1980,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out id); idents.Add(id); - while (la.kind == 51) { + while (la.kind == 52) { Get(); Ident(out id); idents.Add(id); } - if (la.kind == 31) { + if (la.kind == 32) { Get(); openParen = t; args = new List(); if (StartOf(7)) { Expressions(args); } - Expect(32); + Expect(33); } e = new IdentifierSequence(idents, openParen, args); } @@ -1996,38 +2002,38 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List multipleIndices = null; bool func = false; - if (la.kind == 51) { + if (la.kind == 52) { Get(); Ident(out id); - if (la.kind == 31) { + if (la.kind == 32) { Get(); args = new List(); func = true; if (StartOf(7)) { Expressions(args); } - Expect(32); + Expect(33); e = new FunctionCallExpr(id, id.val, e, args); } if (!func) { e = new FieldSelectExpr(id, e, id.val); } - } else if (la.kind == 49) { + } else if (la.kind == 50) { Get(); x = t; if (StartOf(7)) { Expression(out ee); e0 = ee; - if (la.kind == 95) { + if (la.kind == 96) { Get(); anyDots = true; if (StartOf(7)) { Expression(out ee); e1 = ee; } - } else if (la.kind == 47) { + } else if (la.kind == 48) { Get(); Expression(out ee); e1 = ee; - } else if (la.kind == 19 || la.kind == 50) { - while (la.kind == 19) { + } else if (la.kind == 20 || la.kind == 51) { + while (la.kind == 20) { Get(); Expression(out ee); if (multipleIndices == null) { @@ -2037,15 +2043,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee); } - } else SynErr(157); - } else if (la.kind == 95) { + } else SynErr(158); + } else if (la.kind == 96) { Get(); anyDots = true; if (StartOf(7)) { Expression(out ee); e1 = ee; } - } else SynErr(158); + } else SynErr(159); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -2068,8 +2074,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } - Expect(50); - } else SynErr(159); + Expect(51); + } else SynErr(160); } void DisplayExpr(out Expression e) { @@ -2085,15 +2091,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } e = new SetDisplayExpr(x, elements); Expect(7); - } else if (la.kind == 49) { + } else if (la.kind == 50) { Get(); x = t; elements = new List(); if (StartOf(7)) { Expressions(elements); } e = new SeqDisplayExpr(x, elements); - Expect(50); - } else SynErr(160); + Expect(51); + } else SynErr(161); } void MultiSetExpr(out Expression e) { @@ -2101,7 +2107,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken/*!*/ x = null; List/*!*/ elements; e = dummyExpr; - Expect(37); + Expect(38); x = t; if (la.kind == 6) { Get(); @@ -2111,15 +2117,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } e = new MultiSetDisplayExpr(x, elements); Expect(7); - } else if (la.kind == 31) { + } else if (la.kind == 32) { Get(); x = t; elements = new List(); Expression(out e); e = new MultiSetFormingExpr(x, e); - Expect(32); + Expect(33); } else if (StartOf(17)) { SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); - } else SynErr(161); + } else SynErr(162); } void ConstAtomExpression(out Expression/*!*/ e) { @@ -2128,17 +2134,17 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr; switch (la.kind) { - case 87: { + case 88: { Get(); e = new LiteralExpr(t, false); break; } - case 88: { + case 89: { Get(); e = new LiteralExpr(t, true); break; } - case 89: { + case 90: { Get(); e = new LiteralExpr(t); break; @@ -2148,55 +2154,55 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LiteralExpr(t, n); break; } - case 90: { + case 91: { Get(); e = new ThisExpr(t); break; } - case 91: { + case 92: { Get(); x = t; - Expect(31); - Expression(out e); Expect(32); + Expression(out e); + Expect(33); e = new FreshExpr(x, e); break; } - case 92: { + case 93: { Get(); x = t; - Expect(31); - Expression(out e); Expect(32); + Expression(out e); + Expect(33); e = new AllocatedExpr(x, e); break; } - case 93: { + case 94: { Get(); x = t; - Expect(31); - Expression(out e); Expect(32); + Expression(out e); + Expect(33); e = new OldExpr(x, e); break; } - case 16: { + case 17: { Get(); x = t; Expression(out e); e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); - Expect(16); + Expect(17); break; } - case 31: { + case 32: { Get(); x = t; Expression(out e); e = new ParensExpression(x, e); - Expect(32); + Expect(33); break; } - default: SynErr(162); break; + default: SynErr(163); break; } } @@ -2215,10 +2221,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(59); + Expect(60); x = t; Expression(out e); - while (la.kind == 55) { + while (la.kind == 56) { CaseExpression(out c); cases.Add(c); } @@ -2233,13 +2239,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression range; Expression/*!*/ body; - if (la.kind == 96 || la.kind == 97) { + if (la.kind == 97 || la.kind == 98) { Forall(); x = t; univ = true; - } else if (la.kind == 98 || la.kind == 99) { + } else if (la.kind == 99 || la.kind == 100) { Exists(); x = t; - } else SynErr(163); + } else SynErr(164); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body); @@ -2259,18 +2265,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ range; Expression body = null; - Expect(36); + Expect(37); x = t; IdentTypeOptional(out bv); bvars.Add(bv); - while (la.kind == 19) { + while (la.kind == 20) { Get(); IdentTypeOptional(out bv); bvars.Add(bv); } - Expect(16); + Expect(17); Expression(out range); - if (la.kind == 100 || la.kind == 101) { + if (la.kind == 101 || la.kind == 102) { QSep(); Expression(out body); } @@ -2285,47 +2291,47 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv; Expression/*!*/ body; - Expect(55); + Expect(56); x = t; Ident(out id); - if (la.kind == 31) { + if (la.kind == 32) { Get(); IdentTypeOptional(out bv); arguments.Add(bv); - while (la.kind == 19) { + while (la.kind == 20) { Get(); IdentTypeOptional(out bv); arguments.Add(bv); } - Expect(32); + Expect(33); } - Expect(56); + Expect(57); Expression(out body); c = new MatchCaseExpr(x, id.val, arguments, body); } void Forall() { - if (la.kind == 96) { + if (la.kind == 97) { Get(); - } else if (la.kind == 97) { + } else if (la.kind == 98) { Get(); - } else SynErr(164); + } else SynErr(165); } void Exists() { - if (la.kind == 98) { + if (la.kind == 99) { Get(); - } else if (la.kind == 99) { + } else if (la.kind == 100) { Get(); - } else SynErr(165); + } else SynErr(166); } void QSep() { - if (la.kind == 100) { + if (la.kind == 101) { Get(); - } else if (la.kind == 101) { + } else if (la.kind == 102) { Get(); - } else SynErr(166); + } else SynErr(167); } void AttributeBody(ref Attributes attrs) { @@ -2339,7 +2345,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(18)) { AttributeArg(out aArg); aArgs.Add(aArg); - while (la.kind == 19) { + while (la.kind == 20) { Get(); AttributeArg(out aArg); aArgs.Add(aArg); @@ -2360,25 +2366,25 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } static readonly bool[,]/*!*/ set = { - {T,T,T,x, x,x,T,x, x,x,T,T, x,x,T,x, T,T,T,x, x,x,x,T, T,x,T,T, T,T,T,T, 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,x,T,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, 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,T, 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, 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,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,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,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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}, - {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,T,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,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, x,x,x,T, x,x,x,x, T,x,T,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, 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, T,x,T,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,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, x,x,x,T, x,x,x,x, T,x,T,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, 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,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,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, T,x,T,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,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, 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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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,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, 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,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, 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, T,T,x,T, x,T,T,x, x,x,x,x, x,x,x,x, T,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, T,x,T,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,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, x,x,x,T, T,x,x,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,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,x,x,T, 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,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,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,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,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,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,T,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,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, T,x,x,x, x,T,T,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, x,x,x,x, T,x,x,x, x,T,x,T, 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,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, T,x,x,x, x,T,T,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, x,x,x,x, T,x,x,x, x,T,x,T, 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,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,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,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, T,x,x,x, x,T,T,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,T,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, T,x,x,x, x,T,T,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 @@ -2410,164 +2416,165 @@ public class Errors { case 6: s = "lbrace expected"; break; case 7: s = "rbrace expected"; break; case 8: s = "\"module\" expected"; break; - case 9: s = "\"imports\" expected"; break; - case 10: s = "\"class\" expected"; break; - case 11: s = "\"ghost\" expected"; break; - case 12: s = "\"static\" expected"; break; - case 13: s = "\"unlimited\" expected"; break; - case 14: s = "\"datatype\" expected"; break; - case 15: s = "\"=\" expected"; break; - case 16: s = "\"|\" expected"; break; - case 17: s = "\";\" expected"; break; - case 18: s = "\"var\" expected"; break; - case 19: s = "\",\" expected"; break; - case 20: s = "\"type\" expected"; break; - case 21: s = "\"<\" expected"; break; - case 22: s = "\">\" expected"; break; - case 23: s = "\"method\" expected"; break; - case 24: s = "\"constructor\" expected"; break; - case 25: s = "\"returns\" expected"; break; - case 26: s = "\"modifies\" expected"; break; - case 27: s = "\"free\" expected"; break; - case 28: s = "\"requires\" expected"; break; - case 29: s = "\"ensures\" expected"; break; - case 30: s = "\"decreases\" expected"; break; - case 31: s = "\"(\" expected"; break; - case 32: s = "\")\" expected"; break; - case 33: s = "\"bool\" expected"; break; - case 34: s = "\"nat\" expected"; break; - case 35: s = "\"int\" expected"; break; - case 36: s = "\"set\" expected"; break; - case 37: s = "\"multiset\" expected"; break; - case 38: s = "\"seq\" expected"; break; - case 39: s = "\"object\" expected"; break; - case 40: s = "\"function\" expected"; break; - case 41: s = "\"reads\" expected"; break; - case 42: s = "\"*\" expected"; break; - case 43: s = "\"`\" expected"; break; - case 44: s = "\"label\" expected"; break; - case 45: s = "\"break\" expected"; break; - case 46: s = "\"return\" expected"; break; - case 47: s = "\":=\" expected"; break; - case 48: s = "\"new\" expected"; break; - case 49: s = "\"[\" expected"; break; - case 50: s = "\"]\" expected"; break; - case 51: s = "\".\" expected"; break; - case 52: s = "\"choose\" expected"; break; - case 53: s = "\"if\" expected"; break; - case 54: s = "\"else\" expected"; break; - case 55: s = "\"case\" expected"; break; - case 56: s = "\"=>\" expected"; break; - case 57: s = "\"while\" expected"; break; - case 58: s = "\"invariant\" expected"; break; - case 59: s = "\"match\" expected"; break; - case 60: s = "\"assert\" expected"; break; - case 61: s = "\"assume\" expected"; break; - case 62: s = "\"print\" expected"; break; - case 63: s = "\"parallel\" expected"; break; - case 64: s = "\"<==>\" expected"; break; - case 65: s = "\"\\u21d4\" expected"; break; - case 66: s = "\"==>\" expected"; break; - case 67: s = "\"\\u21d2\" expected"; break; - case 68: s = "\"&&\" expected"; break; - case 69: s = "\"\\u2227\" expected"; break; - case 70: s = "\"||\" expected"; break; - case 71: s = "\"\\u2228\" expected"; break; - case 72: s = "\"==\" expected"; break; - case 73: s = "\"<=\" expected"; break; - case 74: s = "\">=\" expected"; break; - case 75: s = "\"!=\" expected"; break; - case 76: s = "\"!!\" expected"; break; - case 77: s = "\"in\" expected"; break; - case 78: s = "\"!\" expected"; break; - case 79: s = "\"\\u2260\" expected"; break; - case 80: s = "\"\\u2264\" expected"; break; - case 81: s = "\"\\u2265\" expected"; break; - case 82: s = "\"+\" expected"; break; - case 83: s = "\"-\" expected"; break; - case 84: s = "\"/\" expected"; break; - case 85: s = "\"%\" expected"; break; - case 86: s = "\"\\u00ac\" expected"; break; - case 87: s = "\"false\" expected"; break; - case 88: s = "\"true\" expected"; break; - case 89: s = "\"null\" expected"; break; - case 90: s = "\"this\" expected"; break; - case 91: s = "\"fresh\" expected"; break; - case 92: s = "\"allocated\" expected"; break; - case 93: s = "\"old\" expected"; break; - case 94: s = "\"then\" expected"; break; - case 95: s = "\"..\" expected"; break; - case 96: s = "\"forall\" expected"; break; - case 97: s = "\"\\u2200\" expected"; break; - case 98: s = "\"exists\" expected"; break; - case 99: s = "\"\\u2203\" expected"; break; - case 100: s = "\"::\" expected"; break; - case 101: s = "\"\\u2022\" expected"; break; - case 102: s = "??? expected"; break; - case 103: s = "this symbol not expected in ClassDecl"; break; - case 104: s = "this symbol not expected in DatatypeDecl"; break; + case 9: s = "\"refines\" expected"; break; + case 10: s = "\"imports\" expected"; break; + case 11: s = "\"class\" expected"; break; + case 12: s = "\"ghost\" expected"; break; + case 13: s = "\"static\" expected"; break; + case 14: s = "\"unlimited\" expected"; break; + case 15: s = "\"datatype\" expected"; break; + case 16: s = "\"=\" expected"; break; + case 17: s = "\"|\" expected"; break; + case 18: s = "\";\" expected"; break; + case 19: s = "\"var\" expected"; break; + case 20: s = "\",\" expected"; break; + case 21: s = "\"type\" expected"; break; + case 22: s = "\"<\" expected"; break; + case 23: s = "\">\" expected"; break; + case 24: s = "\"method\" expected"; break; + case 25: s = "\"constructor\" expected"; break; + case 26: s = "\"returns\" expected"; break; + case 27: s = "\"modifies\" expected"; break; + case 28: s = "\"free\" expected"; break; + case 29: s = "\"requires\" expected"; break; + case 30: s = "\"ensures\" expected"; break; + case 31: s = "\"decreases\" expected"; break; + case 32: s = "\"(\" expected"; break; + case 33: s = "\")\" expected"; break; + case 34: s = "\"bool\" expected"; break; + case 35: s = "\"nat\" expected"; break; + case 36: s = "\"int\" expected"; break; + case 37: s = "\"set\" expected"; break; + case 38: s = "\"multiset\" expected"; break; + case 39: s = "\"seq\" expected"; break; + case 40: s = "\"object\" expected"; break; + case 41: s = "\"function\" expected"; break; + case 42: s = "\"reads\" expected"; break; + case 43: s = "\"*\" expected"; break; + case 44: s = "\"`\" expected"; break; + case 45: s = "\"label\" expected"; break; + case 46: s = "\"break\" expected"; break; + case 47: s = "\"return\" expected"; break; + case 48: s = "\":=\" expected"; break; + case 49: s = "\"new\" expected"; break; + case 50: s = "\"[\" expected"; break; + case 51: s = "\"]\" expected"; break; + case 52: s = "\".\" expected"; break; + case 53: s = "\"choose\" expected"; break; + case 54: s = "\"if\" expected"; break; + case 55: s = "\"else\" expected"; break; + case 56: s = "\"case\" expected"; break; + case 57: s = "\"=>\" expected"; break; + case 58: s = "\"while\" expected"; break; + case 59: s = "\"invariant\" expected"; break; + case 60: s = "\"match\" expected"; break; + case 61: s = "\"assert\" expected"; break; + case 62: s = "\"assume\" expected"; break; + case 63: s = "\"print\" expected"; break; + case 64: s = "\"parallel\" expected"; break; + case 65: s = "\"<==>\" expected"; break; + case 66: s = "\"\\u21d4\" expected"; break; + case 67: s = "\"==>\" expected"; break; + case 68: s = "\"\\u21d2\" expected"; break; + case 69: s = "\"&&\" expected"; break; + case 70: s = "\"\\u2227\" expected"; break; + case 71: s = "\"||\" expected"; break; + case 72: s = "\"\\u2228\" expected"; break; + case 73: s = "\"==\" expected"; break; + case 74: s = "\"<=\" expected"; break; + case 75: s = "\">=\" expected"; break; + case 76: s = "\"!=\" expected"; break; + case 77: s = "\"!!\" expected"; break; + case 78: s = "\"in\" expected"; break; + case 79: s = "\"!\" expected"; break; + case 80: s = "\"\\u2260\" expected"; break; + case 81: s = "\"\\u2264\" expected"; break; + case 82: s = "\"\\u2265\" expected"; break; + case 83: s = "\"+\" expected"; break; + case 84: s = "\"-\" expected"; break; + case 85: s = "\"/\" expected"; break; + case 86: s = "\"%\" expected"; break; + case 87: s = "\"\\u00ac\" expected"; break; + case 88: s = "\"false\" expected"; break; + case 89: s = "\"true\" expected"; break; + case 90: s = "\"null\" expected"; break; + case 91: s = "\"this\" expected"; break; + case 92: s = "\"fresh\" expected"; break; + case 93: s = "\"allocated\" expected"; break; + case 94: s = "\"old\" expected"; break; + case 95: s = "\"then\" expected"; break; + case 96: s = "\"..\" expected"; break; + case 97: s = "\"forall\" expected"; break; + case 98: s = "\"\\u2200\" expected"; break; + case 99: s = "\"exists\" expected"; break; + case 100: s = "\"\\u2203\" expected"; break; + case 101: s = "\"::\" expected"; break; + case 102: s = "\"\\u2022\" expected"; break; + case 103: s = "??? expected"; break; + case 104: s = "this symbol not expected in ClassDecl"; break; case 105: s = "this symbol not expected in DatatypeDecl"; break; - case 106: s = "this symbol not expected in ArbitraryTypeDecl"; break; - case 107: s = "invalid ClassMemberDecl"; break; - case 108: s = "this symbol not expected in FieldDecl"; break; + case 106: s = "this symbol not expected in DatatypeDecl"; break; + case 107: s = "this symbol not expected in ArbitraryTypeDecl"; break; + case 108: s = "invalid ClassMemberDecl"; break; case 109: s = "this symbol not expected in FieldDecl"; break; - case 110: s = "this symbol not expected in MethodDecl"; break; - case 111: s = "invalid MethodDecl"; break; - case 112: s = "invalid TypeAndToken"; break; - case 113: s = "this symbol not expected in MethodSpec"; break; + case 110: s = "this symbol not expected in FieldDecl"; break; + case 111: s = "this symbol not expected in MethodDecl"; break; + case 112: s = "invalid MethodDecl"; break; + case 113: s = "invalid TypeAndToken"; break; case 114: s = "this symbol not expected in MethodSpec"; break; case 115: s = "this symbol not expected in MethodSpec"; break; case 116: s = "this symbol not expected in MethodSpec"; break; - case 117: s = "invalid MethodSpec"; break; - case 118: s = "this symbol not expected in MethodSpec"; break; - case 119: s = "invalid MethodSpec"; break; - case 120: s = "invalid ReferenceType"; break; - case 121: s = "this symbol not expected in FunctionSpec"; break; + case 117: s = "this symbol not expected in MethodSpec"; break; + case 118: s = "invalid MethodSpec"; break; + case 119: s = "this symbol not expected in MethodSpec"; break; + case 120: s = "invalid MethodSpec"; break; + case 121: s = "invalid ReferenceType"; break; case 122: s = "this symbol not expected in FunctionSpec"; break; case 123: s = "this symbol not expected in FunctionSpec"; break; case 124: s = "this symbol not expected in FunctionSpec"; break; case 125: s = "this symbol not expected in FunctionSpec"; break; - case 126: s = "invalid FunctionSpec"; break; - case 127: s = "invalid PossiblyWildFrameExpression"; break; - case 128: s = "invalid PossiblyWildExpression"; break; - case 129: s = "this symbol not expected in OneStmt"; break; - case 130: s = "invalid OneStmt"; break; - case 131: s = "this symbol not expected in OneStmt"; break; - case 132: s = "invalid OneStmt"; break; - case 133: s = "invalid UpdateStmt"; break; - case 134: s = "invalid IfStmt"; break; + case 126: s = "this symbol not expected in FunctionSpec"; break; + case 127: s = "invalid FunctionSpec"; break; + case 128: s = "invalid PossiblyWildFrameExpression"; break; + case 129: s = "invalid PossiblyWildExpression"; break; + case 130: s = "this symbol not expected in OneStmt"; break; + case 131: s = "invalid OneStmt"; break; + case 132: s = "this symbol not expected in OneStmt"; break; + case 133: s = "invalid OneStmt"; break; + case 134: s = "invalid UpdateStmt"; break; case 135: s = "invalid IfStmt"; break; - case 136: s = "invalid WhileStmt"; break; - case 137: s = "invalid Rhs"; break; - case 138: s = "invalid Lhs"; break; - case 139: s = "invalid Guard"; break; - case 140: s = "this symbol not expected in LoopSpec"; break; + case 136: s = "invalid IfStmt"; break; + case 137: s = "invalid WhileStmt"; break; + case 138: s = "invalid Rhs"; break; + case 139: s = "invalid Lhs"; break; + case 140: s = "invalid Guard"; break; case 141: s = "this symbol not expected in LoopSpec"; break; case 142: s = "this symbol not expected in LoopSpec"; break; case 143: s = "this symbol not expected in LoopSpec"; break; case 144: s = "this symbol not expected in LoopSpec"; break; - case 145: s = "this symbol not expected in Invariant"; break; - case 146: s = "invalid AttributeArg"; break; - case 147: s = "invalid EquivOp"; break; - case 148: s = "invalid ImpliesOp"; break; - case 149: s = "invalid AndOp"; break; - case 150: s = "invalid OrOp"; break; - case 151: s = "invalid RelOp"; break; - case 152: s = "invalid AddOp"; break; - case 153: s = "invalid UnaryExpression"; break; - case 154: s = "invalid MulOp"; break; - case 155: s = "invalid NegOp"; break; - case 156: s = "invalid EndlessExpression"; break; - case 157: s = "invalid Suffix"; break; + case 145: s = "this symbol not expected in LoopSpec"; break; + case 146: s = "this symbol not expected in Invariant"; break; + case 147: s = "invalid AttributeArg"; break; + case 148: s = "invalid EquivOp"; break; + case 149: s = "invalid ImpliesOp"; break; + case 150: s = "invalid AndOp"; break; + case 151: s = "invalid OrOp"; break; + case 152: s = "invalid RelOp"; break; + case 153: s = "invalid AddOp"; break; + case 154: s = "invalid UnaryExpression"; break; + case 155: s = "invalid MulOp"; break; + case 156: s = "invalid NegOp"; break; + case 157: s = "invalid EndlessExpression"; break; case 158: s = "invalid Suffix"; break; case 159: s = "invalid Suffix"; break; - case 160: s = "invalid DisplayExpr"; break; - case 161: s = "invalid MultiSetExpr"; break; - case 162: s = "invalid ConstAtomExpression"; break; - case 163: s = "invalid QuantifierGuts"; break; - case 164: s = "invalid Forall"; break; - case 165: s = "invalid Exists"; break; - case 166: s = "invalid QSep"; break; + case 160: s = "invalid Suffix"; break; + case 161: s = "invalid DisplayExpr"; break; + case 162: s = "invalid MultiSetExpr"; break; + case 163: s = "invalid ConstAtomExpression"; break; + case 164: s = "invalid QuantifierGuts"; break; + case 165: s = "invalid Forall"; break; + case 166: s = "invalid Exists"; break; + case 167: s = "invalid QSep"; break; default: s = "error " + n; break; } diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 0912c58d..fcedb829 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -40,9 +40,12 @@ namespace Microsoft.Dafny { wr.Write("module"); PrintAttributes(module.Attributes); wr.Write(" {0} ", module.Name); - if (module.Imports.Count != 0) { + if (module.RefinementBaseName != null) { + wr.Write("refines {0} ", module.RefinementBaseName); + } + if (module.ImportNames.Count != 0) { string sep = "imports "; - foreach (string imp in module.Imports) { + foreach (string imp in module.ImportNames) { wr.Write("{0}{1}", sep, imp); sep = ", "; } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 4f62745d..d5b0bba6 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -59,11 +59,37 @@ namespace Microsoft.Dafny { } readonly BuiltIns builtIns; - readonly Dictionary/*!*/ classes = new Dictionary(); - readonly Dictionary/*!*/>/*!*/ classMembers = new Dictionary/*!*/>(); + + Dictionary/*!*/ classes; // can map to AmbiguousTopLevelDecl + class AmbiguousTopLevelDecl : TopLevelDecl // only used with "classes" + { + readonly TopLevelDecl A; + readonly TopLevelDecl B; + public AmbiguousTopLevelDecl(ModuleDecl m, TopLevelDecl a, TopLevelDecl b) + : base(a.tok, a.Name + "/" + b.Name, m, new List(), null) { + A = a; + B = b; + } + public string ModuleNames() { + string nm; + if (A is AmbiguousTopLevelDecl) { + nm = ((AmbiguousTopLevelDecl)A).ModuleNames(); + } else { + nm = A.Module.Name; + } + if (B is AmbiguousTopLevelDecl) { + nm += ", " + ((AmbiguousTopLevelDecl)B).ModuleNames(); + } else { + nm += ", " + B.Module.Name; + } + return nm; + } + } + Dictionary> allDatatypeCtors; + + readonly Dictionary/*!*/>/*!*/ classMembers = new Dictionary/*!*/>(); readonly Dictionary/*!*/>/*!*/ datatypeMembers = new Dictionary/*!*/>(); readonly Dictionary/*!*/>/*!*/ datatypeCtors = new Dictionary/*!*/>(); - readonly Dictionary> allDatatypeCtors = new Dictionary>(); readonly Graph/*!*/ importGraph = new Graph(); public Resolver(Program prog) { @@ -83,19 +109,30 @@ namespace Microsoft.Dafny { public void ResolveProgram(Program prog) { Contract.Requires(prog != null); // register modules - Dictionary modules = new Dictionary(); - foreach (ModuleDecl m in prog.Modules) { + var modules = new Dictionary(); + foreach (var m in prog.Modules) { if (modules.ContainsKey(m.Name)) { Error(m, "Duplicate module name: {0}", m.Name); } else { modules.Add(m.Name, m); } } - // resolve imports and register top-level declarations - RegisterTopLevelDecls(prog.BuiltIns.SystemModule.TopLevelDecls); - foreach (ModuleDecl m in prog.Modules) { + // resolve refines and imports + foreach (var m in prog.Modules) { importGraph.AddVertex(m); - foreach (string imp in m.Imports) { + if (m.RefinementBaseName != null) { + ModuleDecl other; + if (!modules.TryGetValue(m.RefinementBaseName, out other)) { + Error(m, "module {0} named as refinement base does not exist", m.RefinementBaseName); + } else if (other == m) { + Error(m, "module cannot refine itself: {0}", m.RefinementBaseName); + } else { + Contract.Assert(other != null); // follows from postcondition of TryGetValue + importGraph.AddEdge(m, other); + m.RefinementBase = other; + } + } + foreach (string imp in m.ImportNames) { ModuleDecl other; if (!modules.TryGetValue(imp, out other)) { Error(m, "module {0} named among imports does not exist", imp); @@ -104,9 +141,9 @@ namespace Microsoft.Dafny { } else { Contract.Assert(other != null); // follows from postcondition of TryGetValue importGraph.AddEdge(m, other); + m.Imports.Add(other); } } - RegisterTopLevelDecls(m.TopLevelDecls); } // check for cycles in the import graph List cycle = importGraph.TryFindCycle(); @@ -118,27 +155,41 @@ namespace Microsoft.Dafny { sep = " -> "; } Error(cycle[0], "import graph contains a cycle: {0}", cy); - } else { - // fill in module heights - List mm = importGraph.TopologicallySortedComponents(); - Contract.Assert(mm.Count == prog.Modules.Count); // follows from the fact that there are no cycles - int h = 0; - foreach (ModuleDecl m in mm) { - m.Height = h; - h++; - } + return; // give up on trying to resolve anything else + } + + // fill in module heights + List mm = importGraph.TopologicallySortedComponents(); + Contract.Assert(mm.Count == prog.Modules.Count); // follows from the fact that there are no cycles + int h = 0; + foreach (ModuleDecl m in mm) { + m.Height = h; + h++; + } + + // register top-level declarations + var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule.TopLevelDecls); + var moduleNameInfo = new ModuleNameInformation[h]; + foreach (var m in mm) { + moduleNameInfo[m.Height] = RegisterTopLevelDecls(m.TopLevelDecls); } // resolve top-level declarations Graph datatypeDependencies = new Graph(); - foreach (ModuleDecl m in prog.Modules) { + foreach (ModuleDecl m in mm) { + // set up environment + ModuleNameInformation info = ModuleNameInformation.Merge(m, systemNameInfo, moduleNameInfo); + classes = info.Classes; + allDatatypeCtors = info.Ctors; + // resolve ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies); - } - foreach (ModuleDecl m in prog.Modules) { ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies); + // tear down + classes = null; + allDatatypeCtors = null; } // compute IsRecursive bit for mutually recursive functions - foreach (ModuleDecl m in prog.Modules) { + foreach (ModuleDecl m in mm) { foreach (TopLevelDecl decl in m.TopLevelDecls) { ClassDecl cl = decl as ClassDecl; if (cl != null) { @@ -157,15 +208,67 @@ namespace Microsoft.Dafny { } } - public void RegisterTopLevelDecls(List declarations) { + class ModuleNameInformation + { + public readonly Dictionary Classes = new Dictionary(); + public readonly Dictionary> Ctors = new Dictionary>(); + + public static ModuleNameInformation Merge(ModuleDecl m, ModuleNameInformation system, ModuleNameInformation[] modules) { + var info = new ModuleNameInformation(); + // add the system-declared information, among which we know there are no duplicates + foreach (var kv in system.Classes) { + info.Classes.Add(kv.Key, kv.Value); + } + foreach (var kv in system.Ctors) { + info.Ctors.Add(kv.Key, kv.Value); + } + // for each imported module, add its information, noting any duplicates + foreach (var im in m.Imports) { + Contract.Assume(0 <= im.Height && im.Height < m.Height); + var import = modules[im.Height]; + // classes: + foreach (var kv in import.Classes) { + TopLevelDecl d; + if (info.Classes.TryGetValue(kv.Key, out d)) { + info.Classes[kv.Key] = new AmbiguousTopLevelDecl(m, d, kv.Value); + } else { + info.Classes.Add(kv.Key, kv.Value); + } + } + // constructors: + foreach (var kv in import.Ctors) { + Tuple pair; + if (info.Ctors.TryGetValue(kv.Key, out pair)) { + // mark it as a duplicate + info.Ctors[kv.Key] = new Tuple(pair.Item1, true); + } else { + // add new + info.Ctors.Add(kv.Key, kv.Value); + } + } + } + // finally, for the module itself, let its information override whatever is imported + foreach (var kv in modules[m.Height].Classes) { + info.Classes[kv.Key] = kv.Value; + } + foreach (var kv in modules[m.Height].Ctors) { + info.Ctors[kv.Key] = kv.Value; + } + return info; + } + } + + ModuleNameInformation RegisterTopLevelDecls(List declarations) { Contract.Requires(declarations != null); + var info = new ModuleNameInformation(); + foreach (TopLevelDecl d in declarations) { Contract.Assert(d != null); // register the class/datatype name - if (classes.ContainsKey(d.Name)) { + if (info.Classes.ContainsKey(d.Name)) { Error(d, "Duplicate name of top-level declaration: {0}", d.Name); } else { - classes.Add(d.Name, d); + info.Classes.Add(d.Name, d); } if (d is ArbitraryTypeDecl) { @@ -218,12 +321,12 @@ namespace Microsoft.Dafny { // also register the constructor name globally Tuple pair; - if (allDatatypeCtors.TryGetValue(ctor.Name, out pair)) { + if (info.Ctors.TryGetValue(ctor.Name, out pair)) { // mark it as a duplicate - allDatatypeCtors[ctor.Name] = new Tuple(pair.Item1, true); + info.Ctors[ctor.Name] = new Tuple(pair.Item1, true); } else { // add new - allDatatypeCtors.Add(ctor.Name, new Tuple(ctor, false)); + info.Ctors.Add(ctor.Name, new Tuple(ctor, false)); } } } @@ -245,6 +348,7 @@ namespace Microsoft.Dafny { } } } + return info; } public void ResolveTopLevelDecls_Signatures(List/*!*/ declarations, Graph/*!*/ datatypeDependencies) { @@ -759,7 +863,9 @@ namespace Microsoft.Dafny { } else if (t.ResolvedClass == null) { // this test is because 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string') TopLevelDecl d; if (!classes.TryGetValue(t.Name, out d)) { - Error(t.tok, "Undeclared top-level type or type parameter: {0}", t.Name); + Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget a module import?)", t.Name); + } else if (d is AmbiguousTopLevelDecl) { + Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames()); } else if (d.TypeArgs.Count != t.TypeArgs.Count) { Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name); } else if (d is ArbitraryTypeDecl) { @@ -1906,12 +2012,8 @@ namespace Microsoft.Dafny { if (callerModule == calleeModule) { // intra-module call; this is allowed; add edge in module's call graph callerModule.CallGraph.AddEdge(method, callee); - } else if (calleeModule.IsDefaultModule) { - // all is fine: everything implicitly imports the default module - } else if (importGraph.Reaches(callerModule, calleeModule)) { - // all is fine: the callee is downstream of the caller } else { - Error(s, "inter-module calls must follow the module import relation (so module {0} must transitively import {1})", callerModule.Name, calleeModule.Name); + Contract.Assert(importGraph.Reaches(callerModule, calleeModule)); } } } @@ -2322,6 +2424,8 @@ namespace Microsoft.Dafny { TopLevelDecl d; if (!classes.TryGetValue(dtv.DatatypeName, out d)) { Error(expr.tok, "Undeclared datatype: {0}", dtv.DatatypeName); + } else if (d is AmbiguousTopLevelDecl) { + Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", dtv.DatatypeName, ((AmbiguousTopLevelDecl)d).ModuleNames()); } else if (!(d is DatatypeDecl)) { Error(expr.tok, "Expected datatype, found class: {0}", dtv.DatatypeName); } else { @@ -3067,12 +3171,8 @@ namespace Microsoft.Dafny { if (currentFunction == function) { currentFunction.IsRecursive = true; // self recursion (mutual recursion is determined elsewhere) } - } else if (calleeModule.IsDefaultModule) { - // all is fine: everything implicitly imports the default module - } else if (importGraph.Reaches(callerModule, calleeModule)) { - // all is fine: the callee is downstream of the caller } else { - Error(e, "inter-module calls must follow the module import relation (so module {0} must transitively import {1})", callerModule.Name, calleeModule.Name); + Contract.Assert(importGraph.Reaches(callerModule, calleeModule)); } } } @@ -3086,7 +3186,7 @@ namespace Microsoft.Dafny { CallRhs ResolveIdentifierSequence(IdentifierSequence e, bool twoState, bool allowMethodCall) { // Look up "id" as follows: // - local variable, parameter, or bound variable (if this clashes with something of interest, one can always rename the local variable locally) - // - type name (class or datatype) + // - unamibugous type name (class or datatype or arbitrary-type) (if two imported types have the same name, an error message is produced here) // - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here) // - field name (with implicit receiver) (if the field is ocluded by anything above, one can use an explicit "this.") // Note, at present, modules do not give rise to new namespaces, which is something that should @@ -3106,7 +3206,9 @@ namespace Microsoft.Dafny { r = ResolveSuffix(r, e, 1, twoState, allowMethodCall, out call); } else if (classes.TryGetValue(id.val, out decl)) { - if (e.Tokens.Count == 1 && e.Arguments == null) { + if (decl is AmbiguousTopLevelDecl) { + Error(id, "The name {0} ambiguously refers to a type in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames()); + } else if (e.Tokens.Count == 1 && e.Arguments == null) { Error(id, "name of type ('{0}') is used as a variable", id.val); } else if (e.Tokens.Count == 1 && e.Arguments != null) { Error(id, "name of type ('{0}') is used as a function", id.val); diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index e4d769d9..0f2dfe39 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -209,8 +209,8 @@ public class UTF8Buffer: Buffer { public class Scanner { const char EOL = '\n'; const int eofSym = 0; /* pdt */ - const int maxT = 102; - const int noSym = 102; + const int maxT = 103; + const int noSym = 103; [ContractInvariantMethod] @@ -487,57 +487,58 @@ void objectInvariant(){ void CheckLiteral() { switch (t.val) { case "module": t.kind = 8; break; - case "imports": t.kind = 9; break; - case "class": t.kind = 10; break; - case "ghost": t.kind = 11; break; - case "static": t.kind = 12; break; - case "unlimited": t.kind = 13; break; - case "datatype": t.kind = 14; break; - case "var": t.kind = 18; break; - case "type": t.kind = 20; break; - case "method": t.kind = 23; break; - case "constructor": t.kind = 24; break; - case "returns": t.kind = 25; break; - case "modifies": t.kind = 26; break; - case "free": t.kind = 27; break; - case "requires": t.kind = 28; break; - case "ensures": t.kind = 29; break; - case "decreases": t.kind = 30; break; - case "bool": t.kind = 33; break; - case "nat": t.kind = 34; break; - case "int": t.kind = 35; break; - case "set": t.kind = 36; break; - case "multiset": t.kind = 37; break; - case "seq": t.kind = 38; break; - case "object": t.kind = 39; break; - case "function": t.kind = 40; break; - case "reads": t.kind = 41; break; - case "label": t.kind = 44; break; - case "break": t.kind = 45; break; - case "return": t.kind = 46; break; - case "new": t.kind = 48; break; - case "choose": t.kind = 52; break; - case "if": t.kind = 53; break; - case "else": t.kind = 54; break; - case "case": t.kind = 55; break; - case "while": t.kind = 57; break; - case "invariant": t.kind = 58; break; - case "match": t.kind = 59; break; - case "assert": t.kind = 60; break; - case "assume": t.kind = 61; break; - case "print": t.kind = 62; break; - case "parallel": t.kind = 63; break; - case "in": t.kind = 77; break; - case "false": t.kind = 87; break; - case "true": t.kind = 88; break; - case "null": t.kind = 89; break; - case "this": t.kind = 90; break; - case "fresh": t.kind = 91; break; - case "allocated": t.kind = 92; break; - case "old": t.kind = 93; break; - case "then": t.kind = 94; break; - case "forall": t.kind = 96; break; - case "exists": t.kind = 98; break; + case "refines": t.kind = 9; break; + case "imports": t.kind = 10; break; + case "class": t.kind = 11; break; + case "ghost": t.kind = 12; break; + case "static": t.kind = 13; break; + case "unlimited": t.kind = 14; break; + case "datatype": t.kind = 15; break; + case "var": t.kind = 19; break; + case "type": t.kind = 21; break; + case "method": t.kind = 24; break; + case "constructor": t.kind = 25; break; + case "returns": t.kind = 26; break; + case "modifies": t.kind = 27; break; + case "free": t.kind = 28; break; + case "requires": t.kind = 29; break; + case "ensures": t.kind = 30; break; + case "decreases": t.kind = 31; break; + case "bool": t.kind = 34; break; + case "nat": t.kind = 35; break; + case "int": t.kind = 36; break; + case "set": t.kind = 37; break; + case "multiset": t.kind = 38; break; + case "seq": t.kind = 39; break; + case "object": t.kind = 40; break; + case "function": t.kind = 41; break; + case "reads": t.kind = 42; break; + case "label": t.kind = 45; break; + case "break": t.kind = 46; break; + case "return": t.kind = 47; break; + case "new": t.kind = 49; break; + case "choose": t.kind = 53; break; + case "if": t.kind = 54; break; + case "else": t.kind = 55; break; + case "case": t.kind = 56; break; + case "while": t.kind = 58; break; + case "invariant": t.kind = 59; break; + case "match": t.kind = 60; break; + case "assert": t.kind = 61; break; + case "assume": t.kind = 62; break; + case "print": t.kind = 63; break; + case "parallel": t.kind = 64; break; + case "in": t.kind = 78; break; + case "false": t.kind = 88; break; + case "true": t.kind = 89; break; + case "null": t.kind = 90; break; + case "this": t.kind = 91; break; + case "fresh": t.kind = 92; break; + case "allocated": t.kind = 93; break; + case "old": t.kind = 94; break; + case "then": t.kind = 95; break; + case "forall": t.kind = 97; break; + case "exists": t.kind = 99; break; default: break; } } @@ -640,118 +641,118 @@ void objectInvariant(){ else if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;} else {t.kind = 3; break;} case 19: - {t.kind = 17; break;} + {t.kind = 18; break;} case 20: - {t.kind = 19; break;} + {t.kind = 20; break;} case 21: - {t.kind = 31; break;} - case 22: {t.kind = 32; break;} + case 22: + {t.kind = 33; break;} case 23: - {t.kind = 42; break;} - case 24: {t.kind = 43; break;} + case 24: + {t.kind = 44; break;} case 25: - {t.kind = 47; break;} + {t.kind = 48; break;} case 26: - {t.kind = 49; break;} - case 27: {t.kind = 50; break;} + case 27: + {t.kind = 51; break;} case 28: - {t.kind = 56; break;} + {t.kind = 57; break;} case 29: if (ch == '>') {AddCh(); goto case 30;} else {goto case 0;} case 30: - {t.kind = 64; break;} - case 31: {t.kind = 65; break;} - case 32: + case 31: {t.kind = 66; break;} - case 33: + case 32: {t.kind = 67; break;} + case 33: + {t.kind = 68; break;} case 34: if (ch == '&') {AddCh(); goto case 35;} else {goto case 0;} case 35: - {t.kind = 68; break;} - case 36: {t.kind = 69; break;} - case 37: + case 36: {t.kind = 70; break;} - case 38: + case 37: {t.kind = 71; break;} + case 38: + {t.kind = 72; break;} case 39: - {t.kind = 74; break;} - case 40: {t.kind = 75; break;} - case 41: + case 40: {t.kind = 76; break;} + case 41: + {t.kind = 77; break;} case 42: - {t.kind = 79; break;} - case 43: {t.kind = 80; break;} - case 44: + case 43: {t.kind = 81; break;} - case 45: + case 44: {t.kind = 82; break;} - case 46: + case 45: {t.kind = 83; break;} - case 47: + case 46: {t.kind = 84; break;} - case 48: + case 47: {t.kind = 85; break;} - case 49: + case 48: {t.kind = 86; break;} + case 49: + {t.kind = 87; break;} case 50: - {t.kind = 95; break;} + {t.kind = 96; break;} case 51: - {t.kind = 97; break;} + {t.kind = 98; break;} case 52: - {t.kind = 99; break;} - case 53: {t.kind = 100; break;} - case 54: + case 53: {t.kind = 101; break;} + case 54: + {t.kind = 102; break;} case 55: recEnd = pos; recKind = 5; if (ch == '=') {AddCh(); goto case 25;} else if (ch == ':') {AddCh(); goto case 53;} else {t.kind = 5; break;} case 56: - recEnd = pos; recKind = 15; + recEnd = pos; recKind = 16; if (ch == '>') {AddCh(); goto case 28;} else if (ch == '=') {AddCh(); goto case 62;} - else {t.kind = 15; break;} + else {t.kind = 16; break;} case 57: - recEnd = pos; recKind = 16; + recEnd = pos; recKind = 17; if (ch == '|') {AddCh(); goto case 37;} - else {t.kind = 16; break;} + else {t.kind = 17; break;} case 58: - recEnd = pos; recKind = 21; + recEnd = pos; recKind = 22; if (ch == '=') {AddCh(); goto case 63;} - else {t.kind = 21; break;} + else {t.kind = 22; break;} case 59: - recEnd = pos; recKind = 22; + recEnd = pos; recKind = 23; if (ch == '=') {AddCh(); goto case 39;} - else {t.kind = 22; break;} + else {t.kind = 23; break;} case 60: - recEnd = pos; recKind = 51; + recEnd = pos; recKind = 52; if (ch == '.') {AddCh(); goto case 50;} - else {t.kind = 51; break;} + else {t.kind = 52; break;} case 61: - recEnd = pos; recKind = 78; + recEnd = pos; recKind = 79; if (ch == '=') {AddCh(); goto case 40;} else if (ch == '!') {AddCh(); goto case 41;} - else {t.kind = 78; break;} + else {t.kind = 79; break;} case 62: - recEnd = pos; recKind = 72; + recEnd = pos; recKind = 73; if (ch == '>') {AddCh(); goto case 32;} - else {t.kind = 72; break;} + else {t.kind = 73; break;} case 63: - recEnd = pos; recKind = 73; + recEnd = pos; recKind = 74; if (ch == '=') {AddCh(); goto case 29;} - else {t.kind = 73; break;} + else {t.kind = 74; break;} } t.val = new String(tval, 0, tlen); -- cgit v1.2.3