From 2d7df8e142639e3dbd85460c83b16f6af7ae9622 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Tue, 19 Jun 2012 14:06:31 -0700 Subject: Dafny: Added nested modules --- Source/Dafny/Dafny.atg | 124 ++++++----- Source/Dafny/DafnyAst.cs | 37 +++- Source/Dafny/DafnyMain.cs | 6 +- Source/Dafny/Parser.cs | 538 +++++++++++++++++++++++---------------------- Source/Dafny/Resolver.cs | 234 +++++++++++++++----- Source/Dafny/Translator.cs | 42 ++-- 6 files changed, 571 insertions(+), 410 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 13f6c245..7ffdcbbc 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -14,7 +14,7 @@ using System.IO; using System.Text; COMPILER Dafny /*--------------------------------------------------------------------------*/ -static List theModules; +static ModuleDecl theModule; static BuiltIns theBuiltIns; static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken); static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null); @@ -28,51 +28,51 @@ struct MemberModifiers { // helper routine for parsing call statements /// /// Parses top-level things (modules, classes, datatypes, class members) from "filename" -/// and appends them in appropriate form to "modules". +/// and appends them in appropriate form to "module". /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner. /// -public static int Parse (string/*!*/ filename, List/*!*/ modules, BuiltIns builtIns) /* throws System.IO.IOException */ { +public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns) /* throws System.IO.IOException */ { Contract.Requires(filename != null); - Contract.Requires(cce.NonNullElements(modules)); + Contract.Requires(module != null); string s; if (filename == "stdin.dfy") { s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List()); - return Parse(s, filename, modules, builtIns); + return Parse(s, filename, module, builtIns); } else { using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) { s = Microsoft.Boogie.ParserHelper.Fill(reader, new List()); - return Parse(s, filename, modules, builtIns); + return Parse(s, filename, module, builtIns); } } } /// /// Parses top-level things (modules, classes, datatypes, class members) -/// and appends them in appropriate form to "modules". +/// and appends them in appropriate form to "module". /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner. /// -public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ modules, BuiltIns builtIns) { +public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns) { Contract.Requires(s != null); Contract.Requires(filename != null); - Contract.Requires(cce.NonNullElements(modules)); + Contract.Requires(module != null); Errors errors = new Errors(); - return Parse(s, filename, modules, builtIns, errors); + return Parse(s, filename, module, builtIns, errors); } /// /// Parses top-level things (modules, classes, datatypes, class members) -/// and appends them in appropriate form to "modules". +/// and appends them in appropriate form to "module". /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner with the given Errors sink. /// -public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ modules, BuiltIns builtIns, +public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors) { Contract.Requires(s != null); Contract.Requires(filename != null); - Contract.Requires(cce.NonNullElements(modules)); + Contract.Requires(module != null); Contract.Requires(errors != null); - List oldModules = theModules; - theModules = modules; + ModuleDecl oldModule = theModule; + theModule = module; BuiltIns oldBuiltIns = builtIns; theBuiltIns = builtIns; byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s)); @@ -80,7 +80,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List theImports; List membersDefaultClass = new List(); - List namedModuleDefaultClassMembers; - ModuleDecl module; - // to support multiple files, create a default module only if theModules doesn't already contain one - DefaultModuleDecl defaultModule = null; - foreach (ModuleDecl mdecl in theModules) { - defaultModule = mdecl as DefaultModuleDecl; - if (defaultModule != null) { break; } - } - bool defaultModuleCreatedHere = false; - if (defaultModule == null) { - defaultModuleCreatedHere = true; - defaultModule = new DefaultModuleDecl(); - } - IToken idRefined; + SubModuleDecl submodule; + // to support multiple files, create a default module only if theModule is null + DefaultModuleDecl defaultModule = theModule as DefaultModuleDecl; + // theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl) + Contract.Assert(defaultModule != null); bool isGhost; .) { (. isGhost = false; .) [ "ghost" (. isGhost = true; .) ] - ( "module" (. attrs = null; idRefined = null; theImports = new List(); - namedModuleDefaultClassMembers = new List(); - .) - { Attribute } - Ident (. defaultModule.ImportNames.Add(id.val); .) - [ "refines" Ident ] - [ "imports" Idents ] (. module = new ModuleDecl(id, id.val, isGhost, idRefined == null ? null : idRefined.val, theImports, attrs); .) - "{" (. module.BodyStartTok = t; .) - { ClassDecl (. module.TopLevelDecls.Add(c); .) - | DatatypeDecl (. module.TopLevelDecls.Add(dt); .) - | ArbitraryTypeDecl(. module.TopLevelDecls.Add(at); .) - | ClassMemberDecl - } - "}" (. module.BodyEndTok = t; - module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); - theModules.Add(module); .) + ( SubModuleDecl + (. defaultModule.TopLevelDecls.Add(submodule); .) | (. if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } .) ClassDecl (. defaultModule.TopLevelDecls.Add(c); .) | (. if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } .) @@ -177,22 +153,50 @@ Dafny | ClassMemberDecl ) } - (. if (defaultModuleCreatedHere) { - defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass)); - theModules.Add(defaultModule); - } else { - // find the default class in the default module, then append membersDefaultClass to its member list - foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) { - DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl; - if (defaultClass != null) { - defaultClass.Members.AddRange(membersDefaultClass); - break; - } + (. // find the default class in the default module, then append membersDefaultClass to its member list + foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) { + DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl; + if (defaultClass != null) { + defaultClass.Members.AddRange(membersDefaultClass); + break; } - } - .) + } .) EOF . +SubModuleDecl += (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; + Attributes attrs = null; IToken/*!*/ id; + List namedModuleDefaultClassMembers = new List();; + IToken idRefined = null; + List theImports = new List(); + bool isGhost = false; + ModuleDecl module; + SubModuleDecl sm; + .) + "module" + { Attribute } + Ident (. .) + [ "refines" Ident ] + [ "imports" Idents ] (. module = new ModuleDecl(id, id.val, isOverallModuleGhost, idRefined == null ? null : idRefined.val, theImports, attrs); + parent.Dependencies.Add(module); .) + "{" (. module.BodyStartTok = t; .) + { (. isGhost = false; .) + [ "ghost" (. isGhost = true; .) ] + ( SubModuleDecl (. module.TopLevelDecls.Add(sm); .) + | (. if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } .) + ClassDecl (. module.TopLevelDecls.Add(c); .) + | (. if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } .) + DatatypeDecl (. module.TopLevelDecls.Add(dt); .) + | (. if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } .) + ArbitraryTypeDecl (. module.TopLevelDecls.Add(at); .) + | ClassMemberDecl + ) + } + "}" (. module.BodyEndTok = t; + module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); + submodule = new SubModuleDecl(module, parent); .) +. + ClassDecl = (. Contract.Requires(module != null); Contract.Ensures(Contract.ValueAtReturn(out c) != null); diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index a57ef79d..dc012b32 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -15,18 +15,22 @@ namespace Microsoft.Dafny { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Name != null); - Contract.Invariant(cce.NonNullElements(Modules)); + Contract.Invariant(DefaultModule != null); } public readonly string Name; - public readonly List/*!*/ Modules; + public List/*!*/ Modules; // filled in during resolution. + // Resolution essentially flattens the module heirarchy, for + // purposes of translation and compilation. + public readonly ModuleDecl DefaultModule; public readonly BuiltIns BuiltIns; - public Program(string name, [Captured] List/*!*/ modules, [Captured] BuiltIns builtIns) { + public Program(string name, [Captured] ModuleDecl module, [Captured] BuiltIns builtIns) { Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(modules)); + Contract.Requires(module != null); Name = name; - Modules = modules; + DefaultModule = module; BuiltIns = builtIns; + Modules = new List(); } } @@ -730,10 +734,18 @@ namespace Microsoft.Dafny { } } + public class SubModuleDecl : TopLevelDecl { + public readonly ModuleDecl SubModule; + public SubModuleDecl(ModuleDecl submodule, ModuleDecl parent) + : base(submodule.tok, submodule.Name, parent, new List(), submodule.Attributes) { + SubModule = submodule; + } + } public class ModuleDecl : Declaration { 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/*!*/ Dependencies; // filled in during parsing. contains submodules dependencies. 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 @@ -755,6 +767,7 @@ namespace Microsoft.Dafny { RefinementBaseName = refinementBase; // set "ImportNames" to "imports" minus any duplicates ImportNames = new List(); + Dependencies = new List(); foreach (var nm in imports) { if (!ImportNames.Contains(nm)) { ImportNames.Add(nm); @@ -767,6 +780,20 @@ namespace Microsoft.Dafny { return false; } } + string compileName; + new public string CompileName { + get { + if (compileName == null) { + compileName = NonglobalVariable.CompilerizeName(Name) + "_" + Height.ToString(); + } + return compileName; + } + } + public string UniqueName { + get { + return Name + "_" + Height.ToString(); + } + } } public class DefaultModuleDecl : ModuleDecl { diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs index 62facb31..90c2de44 100644 --- a/Source/Dafny/DafnyMain.cs +++ b/Source/Dafny/DafnyMain.cs @@ -20,7 +20,7 @@ namespace Microsoft.Dafny { Contract.Requires(programName != null); Contract.Requires(fileNames != null); program = null; - List modules = new List(); + ModuleDecl module = new DefaultModuleDecl(); BuiltIns builtIns = new BuiltIns(); foreach (string dafnyFileName in fileNames){ Contract.Assert(dafnyFileName != null); @@ -35,7 +35,7 @@ namespace Microsoft.Dafny { int errorCount; try { - errorCount = Dafny.Parser.Parse(dafnyFileName, modules, builtIns); + errorCount = Dafny.Parser.Parse(dafnyFileName, module, builtIns); if (errorCount != 0) { return string.Format("{0} parse errors detected in {1}", errorCount, dafnyFileName); @@ -47,7 +47,7 @@ namespace Microsoft.Dafny { } } - program = new Program(programName, modules, builtIns); + program = new Program(programName, module, builtIns); if (DafnyOptions.O.DafnyPrintFile != null) { string filename = DafnyOptions.O.DafnyPrintFile; diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 9a439914..142d963e 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -34,7 +34,7 @@ public class Parser { public Token/*!*/ la; // lookahead token int errDist = minErrDist; -static List theModules; +static ModuleDecl theModule; static BuiltIns theBuiltIns; static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken); static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null); @@ -48,51 +48,51 @@ struct MemberModifiers { // helper routine for parsing call statements /// /// Parses top-level things (modules, classes, datatypes, class members) from "filename" -/// and appends them in appropriate form to "modules". +/// and appends them in appropriate form to "module". /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner. /// -public static int Parse (string/*!*/ filename, List/*!*/ modules, BuiltIns builtIns) /* throws System.IO.IOException */ { +public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns) /* throws System.IO.IOException */ { Contract.Requires(filename != null); - Contract.Requires(cce.NonNullElements(modules)); + Contract.Requires(module != null); string s; if (filename == "stdin.dfy") { s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List()); - return Parse(s, filename, modules, builtIns); + return Parse(s, filename, module, builtIns); } else { using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) { s = Microsoft.Boogie.ParserHelper.Fill(reader, new List()); - return Parse(s, filename, modules, builtIns); + return Parse(s, filename, module, builtIns); } } } /// /// Parses top-level things (modules, classes, datatypes, class members) -/// and appends them in appropriate form to "modules". +/// and appends them in appropriate form to "module". /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner. /// -public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ modules, BuiltIns builtIns) { +public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns) { Contract.Requires(s != null); Contract.Requires(filename != null); - Contract.Requires(cce.NonNullElements(modules)); + Contract.Requires(module != null); Errors errors = new Errors(); - return Parse(s, filename, modules, builtIns, errors); + return Parse(s, filename, module, builtIns, errors); } /// /// Parses top-level things (modules, classes, datatypes, class members) -/// and appends them in appropriate form to "modules". +/// and appends them in appropriate form to "module". /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner with the given Errors sink. /// -public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ modules, BuiltIns builtIns, +public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors) { Contract.Requires(s != null); Contract.Requires(filename != null); - Contract.Requires(cce.NonNullElements(modules)); + Contract.Requires(module != null); Contract.Requires(errors != null); - List oldModules = theModules; - theModules = modules; + ModuleDecl oldModule = theModule; + theModule = module; BuiltIns oldBuiltIns = builtIns; theBuiltIns = builtIns; byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s)); @@ -100,7 +100,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List theImports; List membersDefaultClass = new List(); - List namedModuleDefaultClassMembers; - ModuleDecl module; - // to support multiple files, create a default module only if theModules doesn't already contain one - DefaultModuleDecl defaultModule = null; - foreach (ModuleDecl mdecl in theModules) { - defaultModule = mdecl as DefaultModuleDecl; - if (defaultModule != null) { break; } - } - bool defaultModuleCreatedHere = false; - if (defaultModule == null) { - defaultModuleCreatedHere = true; - defaultModule = new DefaultModuleDecl(); - } - IToken idRefined; + SubModuleDecl submodule; + // to support multiple files, create a default module only if theModule is null + DefaultModuleDecl defaultModule = theModule as DefaultModuleDecl; + // theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl) + Contract.Assert(defaultModule != null); bool isGhost; while (StartOf(1)) { @@ -206,44 +196,8 @@ bool IsAttribute() { isGhost = true; } if (la.kind == 9) { - Get(); - attrs = null; idRefined = null; theImports = new List(); - namedModuleDefaultClassMembers = new List(); - - while (la.kind == 6) { - Attribute(ref attrs); - } - Ident(out id); - defaultModule.ImportNames.Add(id.val); - if (la.kind == 10) { - Get(); - Ident(out idRefined); - } - if (la.kind == 11) { - Get(); - Idents(theImports); - } - module = new ModuleDecl(id, id.val, isGhost, idRefined == null ? null : idRefined.val, theImports, attrs); - Expect(6); - module.BodyStartTok = t; - while (StartOf(2)) { - if (la.kind == 12) { - ClassDecl(module, out c); - module.TopLevelDecls.Add(c); - } else if (la.kind == 14 || la.kind == 15) { - DatatypeDecl(module, out dt); - module.TopLevelDecls.Add(dt); - } else if (la.kind == 21) { - ArbitraryTypeDecl(module, out at); - module.TopLevelDecls.Add(at); - } else { - ClassMemberDecl(namedModuleDefaultClassMembers, false, false); - } - } - Expect(7); - module.BodyEndTok = t; - module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); - theModules.Add(module); + SubModuleDecl(defaultModule, isGhost, out submodule); + defaultModule.TopLevelDecls.Add(submodule); } else if (la.kind == 12) { if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } ClassDecl(defaultModule, out c); @@ -256,48 +210,77 @@ bool IsAttribute() { if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } ArbitraryTypeDecl(defaultModule, out at); defaultModule.TopLevelDecls.Add(at); - } else if (StartOf(3)) { + } else if (StartOf(2)) { ClassMemberDecl(membersDefaultClass, isGhost, false); } else SynErr(108); } - if (defaultModuleCreatedHere) { - defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass)); - theModules.Add(defaultModule); - } else { - // find the default class in the default module, then append membersDefaultClass to its member list - foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) { - DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl; - if (defaultClass != null) { - defaultClass.Members.AddRange(membersDefaultClass); - break; - } + foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) { + DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl; + if (defaultClass != null) { + defaultClass.Members.AddRange(membersDefaultClass); + break; } - } - + } Expect(0); } - void Attribute(ref Attributes attrs) { - Expect(6); - AttributeBody(ref attrs); - Expect(7); - } - - void Ident(out IToken/*!*/ x) { - Contract.Ensures(Contract.ValueAtReturn(out x) != null); - Expect(1); - x = t; - } - - void Idents(List/*!*/ ids) { - IToken/*!*/ id; + void SubModuleDecl(ModuleDecl parent, bool isOverallModuleGhost, out SubModuleDecl submodule) { + ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; + Attributes attrs = null; IToken/*!*/ id; + List namedModuleDefaultClassMembers = new List();; + IToken idRefined = null; + List theImports = new List(); + bool isGhost = false; + ModuleDecl module; + SubModuleDecl sm; + + Expect(9); + while (la.kind == 6) { + Attribute(ref attrs); + } Ident(out id); - ids.Add(id.val); - while (la.kind == 20) { + + if (la.kind == 10) { Get(); - Ident(out id); - ids.Add(id.val); + Ident(out idRefined); + } + if (la.kind == 11) { + Get(); + Idents(theImports); } + module = new ModuleDecl(id, id.val, isOverallModuleGhost, idRefined == null ? null : idRefined.val, theImports, attrs); + parent.Dependencies.Add(module); + Expect(6); + module.BodyStartTok = t; + while (StartOf(1)) { + isGhost = false; + if (la.kind == 8) { + Get(); + isGhost = true; + } + if (la.kind == 9) { + SubModuleDecl(module, isGhost, out sm); + module.TopLevelDecls.Add(sm); + } else if (la.kind == 12) { + if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } + ClassDecl(module, out c); + module.TopLevelDecls.Add(c); + } else if (la.kind == 14 || la.kind == 15) { + if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } + DatatypeDecl(module, out dt); + module.TopLevelDecls.Add(dt); + } else if (la.kind == 21) { + if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } + ArbitraryTypeDecl(module, out at); + module.TopLevelDecls.Add(at); + } else if (StartOf(2)) { + ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false); + } else SynErr(109); + } + Expect(7); + module.BodyEndTok = t; + module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); + submodule = new SubModuleDecl(module, parent); } void ClassDecl(ModuleDecl/*!*/ module, out ClassDecl/*!*/ c) { @@ -309,7 +292,7 @@ bool IsAttribute() { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 12)) {SynErr(109); Get();} + while (!(la.kind == 0 || la.kind == 12)) {SynErr(110); Get();} Expect(12); while (la.kind == 6) { Attribute(ref attrs); @@ -320,7 +303,7 @@ bool IsAttribute() { } Expect(6); bodyStart = t; - while (StartOf(3)) { + while (StartOf(2)) { ClassMemberDecl(members, false, true); } Expect(7); @@ -340,13 +323,13 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; // dummy assignment bool co = false; - while (!(la.kind == 0 || la.kind == 14 || la.kind == 15)) {SynErr(110); Get();} + while (!(la.kind == 0 || la.kind == 14 || la.kind == 15)) {SynErr(111); Get();} if (la.kind == 14) { Get(); } else if (la.kind == 15) { Get(); co = true; - } else SynErr(111); + } else SynErr(112); while (la.kind == 6) { Attribute(ref attrs); } @@ -361,7 +344,7 @@ bool IsAttribute() { Get(); DatatypeMemberDecl(ctors); } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(112); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(113); Get();} Expect(18); if (co) { dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); @@ -383,7 +366,7 @@ bool IsAttribute() { } Ident(out id); at = new ArbitraryTypeDecl(id, id.val, module, attrs); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(113); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(114); Get();} Expect(18); } @@ -411,7 +394,30 @@ bool IsAttribute() { } else if (la.kind == 24 || la.kind == 25) { MethodDecl(mmod, allowConstructors, out m); mm.Add(m); - } else SynErr(114); + } else SynErr(115); + } + + void Attribute(ref Attributes attrs) { + Expect(6); + AttributeBody(ref attrs); + Expect(7); + } + + void Ident(out IToken/*!*/ x) { + Contract.Ensures(Contract.ValueAtReturn(out x) != null); + Expect(1); + x = t; + } + + void Idents(List/*!*/ ids) { + IToken/*!*/ id; + Ident(out id); + ids.Add(id.val); + while (la.kind == 20) { + Get(); + Ident(out id); + ids.Add(id.val); + } } void GenericParameters(List/*!*/ typeArgs) { @@ -433,7 +439,7 @@ bool IsAttribute() { Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; - while (!(la.kind == 0 || la.kind == 19)) {SynErr(115); Get();} + while (!(la.kind == 0 || la.kind == 19)) {SynErr(116); Get();} Expect(19); if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } @@ -447,7 +453,7 @@ bool IsAttribute() { IdentType(out id, out ty); mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(116); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(117); Get();} Expect(18); } @@ -493,7 +499,7 @@ bool IsAttribute() { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(117); + } else SynErr(118); } else if (la.kind == 45) { Get(); isPredicate = true; @@ -507,7 +513,7 @@ bool IsAttribute() { Attribute(ref attrs); } Ident(out id); - if (StartOf(4)) { + if (StartOf(3)) { if (la.kind == 22) { GenericParameters(typeArgs); } @@ -522,9 +528,9 @@ bool IsAttribute() { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(118); - } else SynErr(119); - while (StartOf(5)) { + } else SynErr(119); + } else SynErr(120); + while (StartOf(4)) { FunctionSpec(reqs, reads, ens, decreases); } if (la.kind == 6) { @@ -562,7 +568,7 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(120); Get();} + while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(121); Get();} if (la.kind == 24) { Get(); } else if (la.kind == 25) { @@ -573,7 +579,7 @@ bool IsAttribute() { SemErr(t, "constructors are only allowed in classes"); } - } else SynErr(121); + } else SynErr(122); if (isConstructor) { if (mmod.IsGhost) { SemErr(t, "constructors cannot be declared 'ghost'"); @@ -600,8 +606,8 @@ bool IsAttribute() { } else if (la.kind == 27) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(122); - while (StartOf(6)) { + } else SynErr(123); + while (StartOf(5)) { MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs); } if (la.kind == 6) { @@ -638,7 +644,7 @@ bool IsAttribute() { void FormalsOptionalIds(List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; Expect(33); - if (StartOf(7)) { + if (StartOf(6)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); while (la.kind == 20) { @@ -794,7 +800,7 @@ bool IsAttribute() { ReferenceType(out tok, out ty); break; } - default: SynErr(123); break; + default: SynErr(124); break; } } @@ -819,13 +825,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null; - while (!(StartOf(8))) {SynErr(124); Get();} + while (!(StartOf(7))) {SynErr(125); Get();} if (la.kind == 28) { Get(); while (IsAttribute()) { Attribute(ref modAttrs); } - if (StartOf(9)) { + if (StartOf(8)) { FrameExpression(out fe); mod.Add(fe); while (la.kind == 20) { @@ -834,7 +840,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(125); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(126); Get();} Expect(18); } else if (la.kind == 29 || la.kind == 30 || la.kind == 31) { if (la.kind == 29) { @@ -844,7 +850,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 30) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(126); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(127); Get();} Expect(18); req.Add(new MaybeFreeExpression(e, isFree)); } else if (la.kind == 31) { @@ -853,19 +859,19 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Attribute(ref ensAttrs); } Expression(out e); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(127); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(128); Get();} Expect(18); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); - } else SynErr(128); + } else SynErr(129); } else if (la.kind == 32) { Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(129); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(130); Get();} Expect(18); - } else SynErr(130); + } else SynErr(131); } void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -874,7 +880,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(6); bodyStart = t; - while (StartOf(10)) { + while (StartOf(9)) { Stmt(body); } Expect(7); @@ -965,22 +971,22 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt, moduleName); - } else SynErr(131); + } else SynErr(132); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List/*!*/ decreases) { Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; if (la.kind == 30) { - while (!(la.kind == 0 || la.kind == 30)) {SynErr(132); Get();} + while (!(la.kind == 0 || la.kind == 30)) {SynErr(133); Get();} Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(133); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(134); Get();} Expect(18); reqs.Add(e); } else if (la.kind == 46) { Get(); - if (StartOf(11)) { + if (StartOf(10)) { PossiblyWildFrameExpression(out fe); reads.Add(fe); while (la.kind == 20) { @@ -989,20 +995,20 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe); } } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(134); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(135); Get();} Expect(18); } else if (la.kind == 31) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(135); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(136); Get();} Expect(18); ens.Add(e); } else if (la.kind == 32) { Get(); DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(136); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(137); Get();} Expect(18); - } else SynErr(137); + } else SynErr(138); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -1019,9 +1025,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 47) { Get(); fe = new FrameExpression(new WildcardExpr(t), null); - } else if (StartOf(9)) { + } else if (StartOf(8)) { FrameExpression(out fe); - } else SynErr(138); + } else SynErr(139); } void PossiblyWildExpression(out Expression/*!*/ e) { @@ -1030,9 +1036,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 47) { Get(); e = new WildcardExpr(t); - } else if (StartOf(9)) { + } else if (StartOf(8)) { Expression(out e); - } else SynErr(139); + } else SynErr(140); } void Stmt(List/*!*/ ss) { @@ -1049,7 +1055,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd; int breakCount; - while (!(StartOf(12))) {SynErr(140); Get();} + while (!(StartOf(11))) {SynErr(141); Get();} switch (la.kind) { case 6: { BlockStmt(out bs, out bodyStart, out bodyEnd); @@ -1112,8 +1118,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); breakCount++; } - } else SynErr(141); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(142); Get();} + } else SynErr(142); + while (!(la.kind == 0 || la.kind == 18)) {SynErr(143); Get();} Expect(18); s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); break; @@ -1128,7 +1134,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(18); break; } - default: SynErr(143); break; + default: SynErr(144); break; } } @@ -1141,11 +1147,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsAttribute()) { Attribute(ref attrs); } - if (StartOf(9)) { + if (StartOf(8)) { Expression(out e); } else if (la.kind == 27) { Get(); - } else SynErr(144); + } else SynErr(145); Expect(18); if (e == null) { s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false); @@ -1224,12 +1230,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo suchThatAssume = t; } Expression(out suchThat); - } else SynErr(145); + } else SynErr(146); Expect(18); } else if (la.kind == 5) { Get(); SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); - } else SynErr(146); + } else SynErr(147); if (suchThat != null) { s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume); } else { @@ -1334,7 +1340,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 6) { BlockStmt(out bs, out bodyStart, out bodyEnd); els = bs; - } else SynErr(147); + } else SynErr(148); } if (guardOmitted) { ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false); @@ -1345,7 +1351,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 6) { AlternativeBlock(out alternatives); ifStmt = new AlternativeStmt(x, alternatives); - } else SynErr(148); + } else SynErr(149); } void WhileStmt(out Statement/*!*/ stmt) { @@ -1377,7 +1383,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 27) { Get(); bodyOmitted = true; - } else SynErr(149); + } else SynErr(150); if (guardOmitted || bodyOmitted) { if (decreases.Count != 0) { SemErr(decreases[0].tok, "'decreases' clauses are not allowed on refining loops"); @@ -1394,11 +1400,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo stmt = new WhileStmt(x, guard, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body); } - } else if (StartOf(13)) { + } else if (StartOf(12)) { 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(150); + } else SynErr(151); } void MatchStmt(out Statement/*!*/ s) { @@ -1464,7 +1470,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(51); returnTok = t; - if (StartOf(14)) { + if (StartOf(13)) { Rhs(out r, null); rhss = new List(); rhss.Add(r); while (la.kind == 20) { @@ -1503,7 +1509,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out x); Expect(33); args = new List(); - if (StartOf(9)) { + if (StartOf(8)) { Expressions(args); } Expect(34); @@ -1521,7 +1527,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = null; } args = new List(); - if (StartOf(9)) { + if (StartOf(8)) { Expressions(args); } Expect(34); @@ -1545,10 +1551,10 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 47) { Get(); r = new HavocRhs(t); - } else if (StartOf(9)) { + } else if (StartOf(8)) { Expression(out e); r = new ExprRhs(e); - } else SynErr(151); + } else SynErr(152); while (la.kind == 6) { Attribute(ref attrs); } @@ -1563,13 +1569,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 43 || la.kind == 56) { Suffix(ref e); } - } else if (StartOf(15)) { + } else if (StartOf(14)) { ConstAtomExpression(out e); Suffix(ref e); while (la.kind == 43 || la.kind == 56) { Suffix(ref e); } - } else SynErr(152); + } else SynErr(153); } void Expressions(List/*!*/ args) { @@ -1589,10 +1595,10 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 47) { Get(); e = null; - } else if (StartOf(9)) { + } else if (StartOf(8)) { Expression(out ee); e = ee; - } else SynErr(153); + } else SynErr(154); Expect(34); } @@ -1609,7 +1615,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e); Expect(62); body = new List(); - while (StartOf(10)) { + while (StartOf(9)) { Stmt(body); } alternatives.Add(new GuardedAlternative(x, e, body)); @@ -1624,29 +1630,29 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo decreases = new List(); mod = null; - while (StartOf(16)) { + while (StartOf(15)) { if (la.kind == 29 || la.kind == 64) { Invariant(out invariant); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(154); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(155); Get();} Expect(18); invariants.Add(invariant); } else if (la.kind == 32) { - while (!(la.kind == 0 || la.kind == 32)) {SynErr(155); Get();} + while (!(la.kind == 0 || la.kind == 32)) {SynErr(156); Get();} Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, true); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(156); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(157); Get();} Expect(18); } else { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(157); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(158); Get();} Get(); while (IsAttribute()) { Attribute(ref modAttrs); } mod = mod ?? new List(); - if (StartOf(9)) { + if (StartOf(8)) { FrameExpression(out fe); mod.Add(fe); while (la.kind == 20) { @@ -1655,7 +1661,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(158); Get();} + while (!(la.kind == 0 || la.kind == 18)) {SynErr(159); Get();} Expect(18); } } @@ -1663,7 +1669,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Invariant(out MaybeFreeExpression/*!*/ invariant) { bool isFree = false; Expression/*!*/ e; List ids = new List(); invariant = null; Attributes attrs = null; - while (!(la.kind == 0 || la.kind == 29 || la.kind == 64)) {SynErr(159); Get();} + while (!(la.kind == 0 || la.kind == 29 || la.kind == 64)) {SynErr(160); Get();} if (la.kind == 29) { Get(); isFree = true; @@ -1698,7 +1704,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(34); } Expect(62); - while (StartOf(10)) { + while (StartOf(9)) { Stmt(body); } c = new MatchCaseStmt(x, id.val, arguments, body); @@ -1709,10 +1715,10 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 4) { Get(); arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2)); - } else if (StartOf(9)) { + } else if (StartOf(8)) { Expression(out e); arg = new Attributes.Argument(t, e); - } else SynErr(160); + } else SynErr(161); } void QuantifierDomain(out List bvars, out Attributes attrs, out Expression range) { @@ -1764,13 +1770,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 70) { Get(); - } else SynErr(161); + } else SynErr(162); } void LogicalExpression(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; RelationalExpression(out e0); - if (StartOf(17)) { + if (StartOf(16)) { if (la.kind == 73 || la.kind == 74) { AndOp(); x = t; @@ -1802,7 +1808,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 72) { Get(); - } else SynErr(162); + } else SynErr(163); } void RelationalExpression(out Expression/*!*/ e) { @@ -1819,7 +1825,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Term(out e0); e = e0; - if (StartOf(18)) { + if (StartOf(17)) { RelOp(out x, out op); firstOpTok = x; Term(out e1); @@ -1827,7 +1833,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (op == BinaryExpr.Opcode.Disjoint) acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands. - while (StartOf(18)) { + while (StartOf(17)) { if (chain == null) { chain = new List(); ops = new List(); @@ -1900,7 +1906,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 74) { Get(); - } else SynErr(163); + } else SynErr(164); } void OrOp() { @@ -1908,7 +1914,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 76) { Get(); - } else SynErr(164); + } else SynErr(165); } void Term(out Expression/*!*/ e0) { @@ -2000,7 +2006,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(165); break; + default: SynErr(166); break; } } @@ -2022,7 +2028,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 88) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(166); + } else SynErr(167); } void UnaryExpression(out Expression/*!*/ e) { @@ -2072,7 +2078,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } break; } - default: SynErr(167); break; + default: SynErr(168); break; } } @@ -2087,7 +2093,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 90) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(168); + } else SynErr(169); } void NegOp() { @@ -2095,7 +2101,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 91) { Get(); - } else SynErr(169); + } else SynErr(170); } void EndlessExpression(out Expression e) { @@ -2172,7 +2178,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LetExpr(x, letVars, letRHSs, e); break; } - default: SynErr(170); break; + default: SynErr(171); break; } } @@ -2191,7 +2197,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 33) { Get(); openParen = t; args = new List(); - if (StartOf(9)) { + if (StartOf(8)) { Expressions(args); } Expect(34); @@ -2211,7 +2217,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 33) { Get(); IToken openParen = t; args = new List(); func = true; - if (StartOf(9)) { + if (StartOf(8)) { Expressions(args); } Expect(34); @@ -2221,13 +2227,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 56) { Get(); x = t; - if (StartOf(9)) { + if (StartOf(8)) { Expression(out ee); e0 = ee; if (la.kind == 100) { Get(); anyDots = true; - if (StartOf(9)) { + if (StartOf(8)) { Expression(out ee); e1 = ee; } @@ -2246,15 +2252,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee); } - } else SynErr(171); + } else SynErr(172); } else if (la.kind == 100) { Get(); anyDots = true; - if (StartOf(9)) { + if (StartOf(8)) { Expression(out ee); e1 = ee; } - } else SynErr(172); + } else SynErr(173); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -2278,7 +2284,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(57); - } else SynErr(173); + } else SynErr(174); } void DisplayExpr(out Expression e) { @@ -2289,7 +2295,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 6) { Get(); x = t; elements = new List(); - if (StartOf(9)) { + if (StartOf(8)) { Expressions(elements); } e = new SetDisplayExpr(x, elements); @@ -2297,12 +2303,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 56) { Get(); x = t; elements = new List(); - if (StartOf(9)) { + if (StartOf(8)) { Expressions(elements); } e = new SeqDisplayExpr(x, elements); Expect(57); - } else SynErr(174); + } else SynErr(175); } void MultiSetExpr(out Expression e) { @@ -2315,7 +2321,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 6) { Get(); elements = new List(); - if (StartOf(9)) { + if (StartOf(8)) { Expressions(elements); } e = new MultiSetDisplayExpr(x, elements); @@ -2326,9 +2332,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e); e = new MultiSetFormingExpr(x, e); Expect(34); - } else if (StartOf(19)) { + } else if (StartOf(18)) { SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); - } else SynErr(175); + } else SynErr(176); } void MapExpr(out Expression e) { @@ -2342,7 +2348,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 56) { Get(); elements = new List(); - if (StartOf(9)) { + if (StartOf(8)) { MapLiteralExpressions(out elements); } e = new MapDisplayExpr(x, elements); @@ -2360,9 +2366,9 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo QSep(); Expression(out body); e = new MapComprehension(x, bvars, range, body); - } else if (StartOf(19)) { + } else if (StartOf(18)) { SemErr("map must be followed by literal in brackets or comprehension."); - } else SynErr(176); + } else SynErr(177); } void ConstAtomExpression(out Expression/*!*/ e) { @@ -2439,7 +2445,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(34); break; } - default: SynErr(177); break; + default: SynErr(178); break; } } @@ -2475,7 +2481,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 106) { Get(); - } else SynErr(178); + } else SynErr(179); } void MatchExpression(out Expression/*!*/ e) { @@ -2506,7 +2512,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 103 || la.kind == 104) { Exists(); x = t; - } else SynErr(179); + } else SynErr(180); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body); @@ -2576,7 +2582,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 102) { Get(); - } else SynErr(180); + } else SynErr(181); } void Exists() { @@ -2584,7 +2590,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 104) { Get(); - } else SynErr(181); + } else SynErr(182); } void AttributeBody(ref Attributes attrs) { @@ -2595,7 +2601,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(5); Expect(1); aName = t.val; - if (StartOf(20)) { + if (StartOf(19)) { AttributeArg(out aArg); aArgs.Add(aArg); while (la.kind == 20) { @@ -2622,7 +2628,6 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo static readonly bool[,]/*!*/ set = { {T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x}, {x,x,x,x, x,x,x,x, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, {x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, {T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, T,T,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, 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}, @@ -2774,79 +2779,80 @@ public class Errors { case 106: s = "\"\\u2022\" expected"; break; case 107: s = "??? expected"; break; case 108: s = "invalid Dafny"; break; - case 109: s = "this symbol not expected in ClassDecl"; break; - case 110: s = "this symbol not expected in DatatypeDecl"; break; - case 111: s = "invalid DatatypeDecl"; break; - case 112: s = "this symbol not expected in DatatypeDecl"; break; - case 113: s = "this symbol not expected in ArbitraryTypeDecl"; break; - case 114: s = "invalid ClassMemberDecl"; break; - case 115: s = "this symbol not expected in FieldDecl"; break; + case 109: s = "invalid SubModuleDecl"; break; + case 110: s = "this symbol not expected in ClassDecl"; break; + case 111: s = "this symbol not expected in DatatypeDecl"; break; + case 112: s = "invalid DatatypeDecl"; break; + case 113: s = "this symbol not expected in DatatypeDecl"; break; + case 114: s = "this symbol not expected in ArbitraryTypeDecl"; break; + case 115: s = "invalid ClassMemberDecl"; break; case 116: s = "this symbol not expected in FieldDecl"; break; - case 117: s = "invalid FunctionDecl"; break; + case 117: s = "this symbol not expected in FieldDecl"; break; case 118: s = "invalid FunctionDecl"; break; case 119: s = "invalid FunctionDecl"; break; - case 120: s = "this symbol not expected in MethodDecl"; break; - case 121: s = "invalid MethodDecl"; break; + case 120: s = "invalid FunctionDecl"; break; + case 121: s = "this symbol not expected in MethodDecl"; break; case 122: s = "invalid MethodDecl"; break; - case 123: s = "invalid TypeAndToken"; break; - case 124: s = "this symbol not expected in MethodSpec"; break; + case 123: s = "invalid MethodDecl"; break; + case 124: s = "invalid TypeAndToken"; break; case 125: s = "this symbol not expected in MethodSpec"; break; case 126: s = "this symbol not expected in MethodSpec"; break; case 127: s = "this symbol not expected in MethodSpec"; break; - case 128: s = "invalid MethodSpec"; break; - case 129: s = "this symbol not expected in MethodSpec"; break; - case 130: s = "invalid MethodSpec"; break; - case 131: s = "invalid ReferenceType"; break; - case 132: s = "this symbol not expected in FunctionSpec"; break; + case 128: s = "this symbol not expected in MethodSpec"; break; + case 129: s = "invalid MethodSpec"; break; + case 130: s = "this symbol not expected in MethodSpec"; break; + case 131: s = "invalid MethodSpec"; break; + case 132: s = "invalid ReferenceType"; break; case 133: s = "this symbol not expected in FunctionSpec"; break; case 134: s = "this symbol not expected in FunctionSpec"; break; case 135: s = "this symbol not expected in FunctionSpec"; break; case 136: s = "this symbol not expected in FunctionSpec"; break; - case 137: s = "invalid FunctionSpec"; break; - case 138: s = "invalid PossiblyWildFrameExpression"; break; - case 139: s = "invalid PossiblyWildExpression"; break; - case 140: s = "this symbol not expected in OneStmt"; break; - case 141: s = "invalid OneStmt"; break; - case 142: s = "this symbol not expected in OneStmt"; break; - case 143: s = "invalid OneStmt"; break; - case 144: s = "invalid AssertStmt"; break; - case 145: s = "invalid UpdateStmt"; break; + case 137: s = "this symbol not expected in FunctionSpec"; break; + case 138: s = "invalid FunctionSpec"; break; + case 139: s = "invalid PossiblyWildFrameExpression"; break; + case 140: s = "invalid PossiblyWildExpression"; break; + case 141: s = "this symbol not expected in OneStmt"; break; + case 142: s = "invalid OneStmt"; break; + case 143: s = "this symbol not expected in OneStmt"; break; + case 144: s = "invalid OneStmt"; break; + case 145: s = "invalid AssertStmt"; break; case 146: s = "invalid UpdateStmt"; break; - case 147: s = "invalid IfStmt"; break; + case 147: s = "invalid UpdateStmt"; break; case 148: s = "invalid IfStmt"; break; - case 149: s = "invalid WhileStmt"; break; + case 149: s = "invalid IfStmt"; break; case 150: s = "invalid WhileStmt"; break; - case 151: s = "invalid Rhs"; break; - case 152: s = "invalid Lhs"; break; - case 153: s = "invalid Guard"; break; - case 154: s = "this symbol not expected in LoopSpec"; break; + case 151: s = "invalid WhileStmt"; break; + case 152: s = "invalid Rhs"; break; + case 153: s = "invalid Lhs"; break; + case 154: s = "invalid Guard"; break; case 155: s = "this symbol not expected in LoopSpec"; break; case 156: s = "this symbol not expected in LoopSpec"; break; case 157: s = "this symbol not expected in LoopSpec"; break; case 158: s = "this symbol not expected in LoopSpec"; break; - case 159: s = "this symbol not expected in Invariant"; break; - case 160: s = "invalid AttributeArg"; break; - case 161: s = "invalid EquivOp"; break; - case 162: s = "invalid ImpliesOp"; break; - case 163: s = "invalid AndOp"; break; - case 164: s = "invalid OrOp"; break; - case 165: s = "invalid RelOp"; break; - case 166: s = "invalid AddOp"; break; - case 167: s = "invalid UnaryExpression"; break; - case 168: s = "invalid MulOp"; break; - case 169: s = "invalid NegOp"; break; - case 170: s = "invalid EndlessExpression"; break; - case 171: s = "invalid Suffix"; break; + case 159: s = "this symbol not expected in LoopSpec"; break; + case 160: s = "this symbol not expected in Invariant"; break; + case 161: s = "invalid AttributeArg"; break; + case 162: s = "invalid EquivOp"; break; + case 163: s = "invalid ImpliesOp"; break; + case 164: s = "invalid AndOp"; break; + case 165: s = "invalid OrOp"; break; + case 166: s = "invalid RelOp"; break; + case 167: s = "invalid AddOp"; break; + case 168: s = "invalid UnaryExpression"; break; + case 169: s = "invalid MulOp"; break; + case 170: s = "invalid NegOp"; break; + case 171: s = "invalid EndlessExpression"; break; case 172: s = "invalid Suffix"; break; case 173: s = "invalid Suffix"; break; - case 174: s = "invalid DisplayExpr"; break; - case 175: s = "invalid MultiSetExpr"; break; - case 176: s = "invalid MapExpr"; break; - case 177: s = "invalid ConstAtomExpression"; break; - case 178: s = "invalid QSep"; break; - case 179: s = "invalid QuantifierGuts"; break; - case 180: s = "invalid Forall"; break; - case 181: s = "invalid Exists"; break; + case 174: s = "invalid Suffix"; break; + case 175: s = "invalid DisplayExpr"; break; + case 176: s = "invalid MultiSetExpr"; break; + case 177: s = "invalid MapExpr"; break; + case 178: s = "invalid ConstAtomExpression"; break; + case 179: s = "invalid QSep"; break; + case 180: s = "invalid QuantifierGuts"; break; + case 181: s = "invalid Forall"; break; + case 182: s = "invalid Exists"; break; default: s = "error " + n; break; } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index f0990aa0..22a0a299 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -63,7 +63,10 @@ namespace Microsoft.Dafny { public class Resolver : ResolutionErrorReporter { readonly BuiltIns builtIns; - Dictionary/*!*/ classes; // can map to AmbiguousTopLevelDecl + //Dictionary/*!*/ classes; // can map to AmbiguousTopLevelDecl + //Dictionary importedNames; // the imported modules, as a map. + ModuleNameInformation moduleInfo = null; + class AmbiguousTopLevelDecl : TopLevelDecl // only used with "classes" { readonly TopLevelDecl A; @@ -88,13 +91,13 @@ namespace Microsoft.Dafny { return nm; } } - Dictionary> allDatatypeCtors; + //Dictionary> allDatatypeCtors; readonly Dictionary/*!*/>/*!*/ classMembers = new Dictionary/*!*/>(); readonly Dictionary/*!*/>/*!*/ datatypeMembers = new Dictionary/*!*/>(); readonly Dictionary/*!*/>/*!*/ datatypeCtors = new Dictionary/*!*/>(); readonly Graph/*!*/ importGraph = new Graph(); - + private ModuleNameInformation[] moduleNameInfo; public Resolver(Program prog) { Contract.Requires(prog != null); builtIns = prog.BuiltIns; @@ -110,43 +113,9 @@ namespace Microsoft.Dafny { public void ResolveProgram(Program prog) { Contract.Requires(prog != null); - // register 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 refines and imports - foreach (var m in prog.Modules) { - importGraph.AddVertex(m); - 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); - } else if (other == m) { - Error(m, "module must not import itself: {0}", imp); - } else { - Contract.Assert(other != null); // follows from postcondition of TryGetValue - importGraph.AddEdge(m, other); - m.Imports.Add(other); - } - } - } + + BindModuleNames(prog.DefaultModule, new ModuleBindings(null), prog.Modules, importGraph); + // check for cycles in the import graph List cycle = importGraph.TryFindCycle(); if (cycle != null) { @@ -156,7 +125,7 @@ namespace Microsoft.Dafny { cy = m.Name + sep + cy; sep = " -> "; } - Error(cycle[0], "import graph contains a cycle: {0}", cy); + Error(cycle[0], "import graph contains a cycle (note: parent modules implicitly depend on submodules): {0}", cy); return; // give up on trying to resolve anything else } @@ -168,11 +137,10 @@ namespace Microsoft.Dafny { m.Height = h; h++; } - // register top-level declarations Rewriter rewriter = new AutoContractsRewriter(); var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule.TopLevelDecls); - var moduleNameInfo = new ModuleNameInformation[h]; + moduleNameInfo = new ModuleNameInformation[h]; foreach (var m in mm) { rewriter.PreResolve(m); if (m.RefinementBase != null) { @@ -180,18 +148,18 @@ namespace Microsoft.Dafny { transformer.Construct(m); } moduleNameInfo[m.Height] = RegisterTopLevelDecls(m.TopLevelDecls); - // set up environment - ModuleNameInformation info = ModuleNameInformation.Merge(m, systemNameInfo, moduleNameInfo); + moduleInfo = ModuleNameInformation.Merge(m, systemNameInfo, moduleNameInfo); + /* classes = info.Classes; + importedNames = info.ImportedNames; allDatatypeCtors = info.Ctors; + */ // resolve var datatypeDependencies = new Graph(); ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies); ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies); // tear down - classes = null; - allDatatypeCtors = null; // give rewriter a chance to do processing rewriter.PostResolve(m); } @@ -216,9 +184,88 @@ namespace Microsoft.Dafny { } } - class ModuleNameInformation + private class ModuleBindings { + private ModuleBindings parent; + private Dictionary modules; + + public ModuleBindings(ModuleBindings p) { + parent = p; + modules = new Dictionary(); + } + public bool BindName(string name, ModuleDecl subModule) { + if (modules.ContainsKey(name)) { + return false; + } else { + modules.Add(name, subModule); + return true; + } + } + public bool TryLookup(string name, out ModuleDecl m) { + if (modules.TryGetValue(name, out m)) + return true; + else if (parent != null) { + return parent.TryLookup(name, out m); + } else return false; + } + } + private void BindModuleNames(ModuleDecl moduleDecl, ModuleBindings parentBindings, List globalModuleList, Graph importGraph) { + // a dictionary of submodules at the current scope. + var modules = new Dictionary(); + var moduleList = new List(); + var bindings = new ModuleBindings(parentBindings); + foreach (var tld in moduleDecl.TopLevelDecls) { + var submodule = tld as SubModuleDecl; + if (submodule != null) { + var name = submodule.SubModule.Name; + if (!bindings.BindName(name, submodule.SubModule)) { + Error(submodule.Module, "Duplicate module name: {0}", name); + } else { + moduleList.Add(submodule.SubModule); + } + } + } + + // resolve refines and imports + foreach (var m in moduleList) { + importGraph.AddVertex(m); + if (m.RefinementBaseName != null) { + ModuleDecl other; + if (!bindings.TryLookup(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 (!bindings.TryLookup(imp, out other)) { + Error(m, "module {0} named among imports does not exist", imp); + } else if (other == m) { + Error(m, "module must not import itself: {0}", imp); + } else { + Contract.Assert(other != null); // follows from postcondition of TryGetValue + importGraph.AddEdge(m, other); + m.Imports.Add(other); + } + } + foreach (var dep in m.Dependencies) { + importGraph.AddEdge(m, dep); + } + } + foreach (var m in moduleList) { + BindModuleNames(m, bindings, globalModuleList, importGraph); + } + globalModuleList.AddRange(moduleList); + } + + public class ModuleNameInformation { public readonly Dictionary Classes = new Dictionary(); + public readonly Dictionary ImportedNames = new Dictionary(); public readonly Dictionary> Ctors = new Dictionary>(); public static ModuleNameInformation Merge(ModuleDecl m, ModuleNameInformation system, ModuleNameInformation[] modules) { @@ -234,6 +281,7 @@ namespace Microsoft.Dafny { foreach (var im in m.Imports) { Contract.Assume(0 <= im.Height && im.Height < m.Height); var import = modules[im.Height]; + info.ImportedNames.Add(im.Name, im); // classes: foreach (var kv in import.Classes) { TopLevelDecl d; @@ -278,8 +326,9 @@ namespace Microsoft.Dafny { } else { info.Classes.Add(d.Name, d); } - - if (d is ArbitraryTypeDecl) { + if (d is SubModuleDecl) { + // do Nothing + } else if (d is ArbitraryTypeDecl) { // nothing more to register } else if (d is ClassDecl) { @@ -370,6 +419,8 @@ namespace Microsoft.Dafny { // nothing to do } else if (d is ClassDecl) { ResolveClassMemberTypes((ClassDecl)d); + } else if (d is SubModuleDecl) { + // TODO: what goes here? } else { ResolveCtorTypes((DatatypeDecl)d, datatypeDependencies); } @@ -436,6 +487,7 @@ namespace Microsoft.Dafny { Scope/*!*/ labeledStatements = new Scope(); List loopStack = new List(); // the enclosing loops (from which it is possible to break out) readonly Dictionary inSpecOnlyContext = new Dictionary(); // invariant: domain contain union of the domains of "labeledStatements" and "loopStack" + /// /// Assumes type parameters have already been pushed @@ -963,7 +1015,7 @@ namespace Microsoft.Dafny { } Error(t.ModuleName, "Undeclared module name: {0} (did you forget a module import?)", t.ModuleName.val); DONE_WITH_QUALIFIED_NAME: ; - } else if (!classes.TryGetValue(t.Name, out d)) { + } else if (!moduleInfo.Classes.TryGetValue(t.Name, out d)) { Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget a module import?)", t.Name); } @@ -2622,7 +2674,7 @@ namespace Microsoft.Dafny { } else if (expr is DatatypeValue) { DatatypeValue dtv = (DatatypeValue)expr; TopLevelDecl d; - if (!classes.TryGetValue(dtv.DatatypeName, out d)) { + if (!moduleInfo.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()); @@ -3512,9 +3564,11 @@ 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) - // - unamibugous type name (class or datatype or arbitrary-type) (if two imported types have the same name, an error message is produced here) + // - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) 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.") + // - imported module name + // - field name (with implicit receiver) (if the field is occluded 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 // be changed in the language when modules are given more attention. Expression r = null; // resolved version of e @@ -3524,6 +3578,7 @@ namespace Microsoft.Dafny { Tuple pair; Dictionary members; MemberDecl member; + ModuleDecl module; var id = e.Tokens[0]; if (scope.Find(id.val) != null) { // ----- root is a local variable, parameter, or bound variable @@ -3531,7 +3586,7 @@ namespace Microsoft.Dafny { ResolveExpression(r, twoState); r = ResolveSuffix(r, e, 1, twoState, allowMethodCall, out call); - } else if (classes.TryGetValue(id.val, out decl)) { + } else if (moduleInfo.Classes.TryGetValue(id.val, out decl)) { 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) { @@ -3547,6 +3602,13 @@ namespace Microsoft.Dafny { var cd = (ClassDecl)decl; r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, twoState, allowMethodCall, out call); + } else if (decl is SubModuleDecl) { + // ----- root is a submodule + module = ((SubModuleDecl)decl).SubModule; + if (!(1 < e.Tokens.Count)) { + Error(e.tok, "module {0} is not an expression", module.Name); + } + call = ResolveIdentifierSequenceModuleScope(e, 1, moduleNameInfo[module.Height], twoState, allowMethodCall); } else { // ----- root is a datatype var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl @@ -3558,7 +3620,7 @@ namespace Microsoft.Dafny { } } - } else if (allDatatypeCtors.TryGetValue(id.val, out pair)) { + } else if (moduleInfo.Ctors.TryGetValue(id.val, out pair)) { // ----- root is a datatype constructor if (pair.Item2) { // there is more than one constructor with this name @@ -3572,6 +3634,11 @@ namespace Microsoft.Dafny { } } + } else if (moduleInfo.ImportedNames.TryGetValue(id.val, out module)) { + if (e.Tokens.Count <= 1) { + Error(e.tok, "module {0} is not an expression", module.Name); + } + call = ResolveIdentifierSequenceModuleScope(e, 1, moduleNameInfo[module.Height], twoState, allowMethodCall); } else if (classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member)) { // ----- field, function, or method Expression receiver; @@ -3604,6 +3671,61 @@ namespace Microsoft.Dafny { return call; } + CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleNameInformation info, bool twoState, bool allowMethodCall) { + // Look up "id" as follows: + // - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or arbitrary-type) + // (if two imported types have the same name, an error message is produced here) + // This is used to look up names that appear after a dot in a sequence identifier. For example, in X.M.*, M should be looked up in X, but + // should not consult the local scope. This distingushes this from the above, in that local scope, imported modules, etc. are ignored. + Contract.Requires(p < e.Tokens.Count); + Expression r = null; // resolved version of e + CallRhs call = null; + + TopLevelDecl decl; + ModuleDecl module; + var id = e.Tokens[p]; + if (info.Classes.TryGetValue(id.val, out decl)) { + if (decl is AmbiguousTopLevelDecl) { + Error(id, "The name {0} ambiguously refers to a something in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames()); + } else if (decl is ClassDecl) { + // ----- root is a class + var cd = (ClassDecl)decl; + r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, p + 1, twoState, allowMethodCall, out call); + + } else if (decl is SubModuleDecl) { + // ----- root is a submodule + module = ((SubModuleDecl)decl).SubModule; + if (!(p + 1 < e.Tokens.Count)) { + Error(e.tok, "module {0} is not an expression", module.Name); + } + call = ResolveIdentifierSequenceModuleScope(e, p+1, moduleNameInfo[module.Height], twoState, allowMethodCall); + } else { + // ----- root is a datatype + var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl + var args = (e.Tokens.Count == p + 2 ? e.Arguments : null) ?? new List(); + r = new DatatypeValue(id, id.val, e.Tokens[p + 1].val, args); + ResolveExpression(r, twoState); + if (e.Tokens.Count != p + 2) { + r = ResolveSuffix(r, e, p + 2, twoState, allowMethodCall, out call); + } + } + } else { + Error(id, "unresolved identifier: {0}", id.val); + // resolve arguments, if any + if (e.Arguments != null) { + foreach (var arg in e.Arguments) { + ResolveExpression(arg, twoState); + } + } + } + + if (r != null) { + e.ResolvedExpression = r; + e.Type = r.Type; + } + return call; + } + /// /// Given resolved expression "r" and unresolved expressions e.Tokens[p..] and e.Arguments. /// Returns a resolved version of the expression: diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index c05d9a38..cb154729 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -331,6 +331,8 @@ namespace Microsoft.Dafny { // nothing to do--this is treated just like a type parameter } else if (d is DatatypeDecl) { AddDatatype((DatatypeDecl)d); + } else if (d is SubModuleDecl) { + // submodules have already been added as a top level module, ignore this. } else { AddClassMembers((ClassDecl)d); } @@ -843,7 +845,7 @@ namespace Microsoft.Dafny { Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight())), etran.InMethodContext()); // useViaCanCall: f#canCall(args) - Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullName + "#canCall", Bpl.Type.Bool); + Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool); Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), args); // ante := useViaCanCall || (useViaContext && typeAnte && pre) @@ -948,7 +950,7 @@ namespace Microsoft.Dafny { Contract.Requires(0 <= layer && layer < 3); Contract.Ensures(Contract.Result() != null); - string name = f.FullName; + string name = f.FullCompileName; switch (layer) { case 2: name += "#2"; break; case 0: name += "#limited"; break; @@ -1446,8 +1448,8 @@ namespace Microsoft.Dafny { if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); } } - string axiomComment = "frame axiom for " + f.FullName; - Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType))); + string axiomComment = "frame axiom for " + f.FullCompileName; + Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullCompileName, TrType(f.ResultType))); while (fn != null) { Bpl.Expr F0 = new Bpl.NAryExpr(f.tok, fn, f0args); Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args); @@ -1569,7 +1571,7 @@ namespace Microsoft.Dafny { } } } - Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(), + Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullCompileName, typeParams, inParams, new Bpl.VariableSeq(), req, new Bpl.IdentifierExprSeq(), ens, etran.TrAttributes(f.Attributes, null)); sink.TopLevelDeclarations.Add(proc); @@ -1631,7 +1633,7 @@ namespace Microsoft.Dafny { // don't fall through to postcondition checks bodyCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False)); } else { - Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType))); + Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullCompileName, TrType(f.ResultType))); Bpl.ExprSeq args = new Bpl.ExprSeq(); args.Add(etran.HeapExpr); foreach (Variable p in implInParams) { @@ -1982,7 +1984,7 @@ namespace Microsoft.Dafny { // check well-formedness of the other parameters r = BplAnd(r, CanCallAssumption(e.Args, etran)); // get to assume canCall - Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullName + "#canCall", Bpl.Type.Bool); + Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullCompileName + "#canCall", Bpl.Type.Bool); ExprSeq args = etran.FunctionInvocationArguments(e); Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args); r = BplAnd(r, canCallFuncAppl); @@ -2414,7 +2416,7 @@ namespace Microsoft.Dafny { } } // all is okay, so allow this function application access to the function's axiom, except if it was okay because of the self-call allowance. - Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullName + "#canCall", Bpl.Type.Bool); + Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullCompileName + "#canCall", Bpl.Type.Bool); ExprSeq args = etran.FunctionInvocationArguments(e); Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args); builder.Add(new Bpl.AssumeCmd(expr.tok, allowance == null ? canCallFuncAppl : Bpl.Expr.Or(allowance, canCallFuncAppl))); @@ -2790,7 +2792,7 @@ namespace Microsoft.Dafny { if (classes.TryGetValue(cl, out cc)) { Contract.Assert(cc != null); } else { - cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.FullName, predef.ClassNameType), true); + cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.FullCompileName, predef.ClassNameType), true); classes.Add(cl, cc); } return cc; @@ -2857,7 +2859,7 @@ namespace Microsoft.Dafny { } else { // const unique f: Field ty; Bpl.Type ty = predef.FieldName(f.tok, TrType(f.Type)); - fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullName, ty), true); + fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullCompileName, ty), true); fields.Add(f, fc); // axiom FDim(f) == 0 && DeclType(f) == C; Bpl.Expr fdim = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FDim, ty, Bpl.Expr.Ident(fc)), Bpl.Expr.Literal(0)); @@ -2888,7 +2890,7 @@ namespace Microsoft.Dafny { Bpl.Type receiverType = f.EnclosingClass is ClassDecl ? predef.RefType : predef.DatatypeType; args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", receiverType), true)); Bpl.Formal result = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, ty), false); - ff = new Bpl.Function(f.tok, f.FullName, args, result); + ff = new Bpl.Function(f.tok, f.FullCompileName, args, result); fieldFunctions.Add(f, ff); // treat certain fields specially if (f.EnclosingClass is ArrayClassDecl) { @@ -2930,7 +2932,7 @@ namespace Microsoft.Dafny { args.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)), true)); } Bpl.Formal res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, TrType(f.ResultType)), false); - Bpl.Function func = new Bpl.Function(f.tok, f.FullName, typeParams, args, res); + Bpl.Function func = new Bpl.Function(f.tok, f.FullCompileName, typeParams, args, res); sink.TopLevelDeclarations.Add(func); if (f.IsRecursive) { @@ -2939,7 +2941,7 @@ namespace Microsoft.Dafny { } res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false); - Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullName + "#canCall", args, res); + Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullCompileName + "#canCall", args, res); sink.TopLevelDeclarations.Add(canCallF); } @@ -3046,10 +3048,10 @@ namespace Microsoft.Dafny { Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs); string name; switch (kind) { - case 0: name = "CheckWellformed$$" + m.FullName; break; - case 1: name = m.FullName; break; - case 2: name = string.Format("RefinementCall_{0}$${1}", m.EnclosingClass.Module.Name, m.FullName); break; - case 3: name = string.Format("RefinementImpl_{0}$${1}", m.EnclosingClass.Module.Name, m.FullName); break; + case 0: name = "CheckWellformed$$" + m.FullCompileName; break; + case 1: name = m.FullCompileName; break; + case 2: name = string.Format("RefinementCall_{0}$${1}", m.EnclosingClass.Module.Name, m.FullCompileName); break; + case 3: name = string.Format("RefinementImpl_{0}$${1}", m.EnclosingClass.Module.Name, m.FullCompileName); break; default: Contract.Assert(false); throw new cce.UnreachableException(); // unexpected kind } Bpl.Procedure proc = new Bpl.Procedure(m.tok, name, typeParams, inParams, outParams, req, mod, ens); @@ -4417,9 +4419,9 @@ namespace Microsoft.Dafny { // Make the call string name; if (RefinementToken.IsInherited(method.tok, currentModule)) { - name = string.Format("RefinementCall_{0}$${1}", currentModule.Name, method.FullName); + name = string.Format("RefinementCall_{0}$${1}", currentModule.Name, method.FullCompileName); } else { - name = method.FullName; + name = method.FullCompileName; } Bpl.CallCmd call = new Bpl.CallCmd(tok, name, ins, outs); builder.Add(call); @@ -7004,7 +7006,7 @@ namespace Microsoft.Dafny { // Note that "body" does not contain limited calls. // F#canCall(args) - Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullName + "#canCall", Bpl.Type.Bool); + Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool); ExprSeq args = etran.FunctionInvocationArguments(fexp); Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args); -- cgit v1.2.3 From 9a73d13a15f88a8dbf3b89b04d57a4a38efa7710 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Tue, 19 Jun 2012 14:35:22 -0700 Subject: Dafny: disallow declare identifiers starting with underscore (_) It is still possible to reference names containing an underscore, but it is not possible to make a variable, method, class, bound variable, type, or module name beginning with one. --- Source/Dafny/Dafny.atg | 40 +++++++++++++++++++++++++--------------- Source/Dafny/Parser.cs | 40 +++++++++++++++++++++++++--------------- 2 files changed, 50 insertions(+), 30 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 7ffdcbbc..4b76f9b4 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -175,7 +175,7 @@ SubModuleDecl } - Ident (. .) + NoUSIdent (. .) [ "refines" Ident ] [ "imports" Idents ] (. module = new ModuleDecl(id, id.val, isOverallModuleGhost, idRefined == null ? null : idRefined.val, theImports, attrs); parent.Dependencies.Add(module); .) @@ -209,7 +209,7 @@ ClassDecl SYNC "class" { Attribute } - Ident + NoUSIdent [ GenericParameters ] "{" (. bodyStart = t; .) { ClassMemberDecl @@ -250,7 +250,7 @@ DatatypeDecl | "codatatype" (. co = true; .) ) { Attribute } - Ident + NoUSIdent [ GenericParameters ] "=" (. bodyStart = t; .) DatatypeMemberDecl @@ -272,7 +272,7 @@ DatatypeMemberDecl<.List/*!*/ ctors.> List formals = new List(); .) { Attribute } - Ident + NoUSIdent [ FormalsOptionalIds ] (. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .) . @@ -297,7 +297,7 @@ ArbitraryTypeDecl .) "type" { Attribute } - Ident (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .) + NoUSIdent (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .) SYNC ";" . GIdentType @@ -311,14 +311,14 @@ GIdentType = (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.) - Ident + NoUSIdent ":" Type . LocalIdentTypeOptional = (. IToken/*!*/ id; Type/*!*/ ty; Type optType = null; .) - Ident + NoUSIdent [ ":" Type (. optType = ty; .) ] (. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .) @@ -326,7 +326,7 @@ LocalIdentTypeOptional IdentTypeOptional = (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null; .) - Ident + NoUSIdent [ ":" Type (. optType = ty; .) ] (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .) @@ -362,8 +362,8 @@ GenericParameters<.List/*!*/ typeArgs.> = (. Contract.Requires(cce.NonNullElements(typeArgs)); IToken/*!*/ id; .) "<" - Ident (. typeArgs.Add(new TypeParameter(id, id.val)); .) - { "," Ident (. typeArgs.Add(new TypeParameter(id, id.val)); .) + NoUSIdent (. typeArgs.Add(new TypeParameter(id, id.val)); .) + { "," NoUSIdent (. typeArgs.Add(new TypeParameter(id, id.val)); .) } ">" . @@ -407,7 +407,7 @@ MethodDecl } .) { Attribute } - Ident + NoUSIdent ( [ GenericParameters ] Formals @@ -567,7 +567,7 @@ FunctionDecl (. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); } .) { Attribute } - Ident + NoUSIdent ( [ GenericParameters ] Formals @@ -584,7 +584,7 @@ FunctionDecl (. if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); } .) { Attribute } - Ident + NoUSIdent ( [ GenericParameters ] [ Formals @@ -694,10 +694,10 @@ OneStmt | MatchStmt | ParallelStmt | "label" (. x = t; .) - Ident ":" + NoUSIdent ":" OneStmt (. s.Labels = new LList