From feee8f3d095a0e9e65e5bd6247296055d7bf410d 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 --- Dafny/Resolver.cs | 186 ++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 144 insertions(+), 42 deletions(-) (limited to 'Dafny/Resolver.cs') diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 4f62745d..d5b0bba6 100644 --- a/Dafny/Resolver.cs +++ b/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); -- cgit v1.2.3