diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 768 |
1 files changed, 571 insertions, 197 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 22a0a299..63f2f9e9 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -65,13 +65,13 @@ namespace Microsoft.Dafny { //Dictionary<string/*!*/,TopLevelDecl/*!*/>/*!*/ classes; // can map to AmbiguousTopLevelDecl
//Dictionary<string, ModuleDecl> importedNames; // the imported modules, as a map.
- ModuleNameInformation moduleInfo = null;
+ ModuleSignature moduleInfo = null;
class AmbiguousTopLevelDecl : TopLevelDecl // only used with "classes"
{
readonly TopLevelDecl A;
readonly TopLevelDecl B;
- public AmbiguousTopLevelDecl(ModuleDecl m, TopLevelDecl a, TopLevelDecl b)
+ public AmbiguousTopLevelDecl(ModuleDefinition m, TopLevelDecl a, TopLevelDecl b)
: base(a.tok, a.Name + "/" + b.Name, m, new List<TypeParameter>(), null) {
A = a;
B = b;
@@ -96,8 +96,7 @@ namespace Microsoft.Dafny { readonly Dictionary<ClassDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>/*!*/ classMembers = new Dictionary<ClassDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>();
readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>/*!*/ datatypeMembers = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>();
readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>/*!*/ datatypeCtors = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>();
- readonly Graph<ModuleDecl/*!*/>/*!*/ importGraph = new Graph<ModuleDecl/*!*/>();
- private ModuleNameInformation[] moduleNameInfo;
+ readonly Graph<ModuleDecl/*!*/>/*!*/ dependencies = new Graph<ModuleDecl/*!*/>();
public Resolver(Program prog) {
Contract.Requires(prog != null);
builtIns = prog.BuiltIns;
@@ -106,66 +105,109 @@ namespace Microsoft.Dafny { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(builtIns != null);
- Contract.Invariant(cce.NonNullElements(importGraph));
+ Contract.Invariant(cce.NonNullElements(dependencies));
Contract.Invariant(cce.NonNullDictionaryAndValues(classMembers) && Contract.ForAll(classMembers.Values, v => cce.NonNullDictionaryAndValues(v)));
Contract.Invariant(cce.NonNullDictionaryAndValues(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullDictionaryAndValues(v)));
}
public void ResolveProgram(Program prog) {
Contract.Requires(prog != null);
-
- BindModuleNames(prog.DefaultModule, new ModuleBindings(null), prog.Modules, importGraph);
-
+ var bindings = new ModuleBindings(null);
+ var b = BindModuleNames(prog.DefaultModuleDef, bindings);
+ bindings.BindName("_module", prog.DefaultModule , b);
+ if (ErrorCount > 0) { return; } // if there were errors, then the implict ModuleBindings data structure invariant
+ // is violated, so Processing dependencies will not succeed.
+ ProcessDependencies(prog.DefaultModule, b, dependencies);
// check for cycles in the import graph
- List<ModuleDecl> cycle = importGraph.TryFindCycle();
+ List<ModuleDecl> cycle = dependencies.TryFindCycle();
if (cycle != null) {
- string cy = "";
- string sep = "";
- foreach (ModuleDecl m in cycle) {
- cy = m.Name + sep + cy;
- sep = " -> ";
- }
- 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
+ var cy = Util.Comma(" -> ", cycle, m => m.Name);
+ Error(cycle[0], "module definition contains a cycle (note: parent modules implicitly depend on submodules): {0}", cy);
}
+ if (ErrorCount > 0) { return; } // give up on trying to resolve anything else
// fill in module heights
- List<ModuleDecl> mm = importGraph.TopologicallySortedComponents();
- Contract.Assert(mm.Count == prog.Modules.Count); // follows from the fact that there are no cycles
+ List<ModuleDecl> sortedDecls = dependencies.TopologicallySortedComponents();
int h = 0;
- foreach (ModuleDecl m in mm) {
+ foreach (ModuleDecl m in sortedDecls) {
m.Height = h;
+ if (m is LiteralModuleDecl) {
+ var mdef = ((LiteralModuleDecl)m).ModuleDef;
+ mdef.Height = h;
+ prog.Modules.Add(mdef);
+ }
h++;
}
+ var mm = prog.Modules;
// register top-level declarations
- Rewriter rewriter = new AutoContractsRewriter();
- var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule.TopLevelDecls);
- moduleNameInfo = new ModuleNameInformation[h];
- foreach (var m in mm) {
- rewriter.PreResolve(m);
- if (m.RefinementBase != null) {
- var transformer = new RefinementTransformer(this);
- transformer.Construct(m);
- }
- moduleNameInfo[m.Height] = RegisterTopLevelDecls(m.TopLevelDecls);
- // set up environment
- moduleInfo = ModuleNameInformation.Merge(m, systemNameInfo, moduleNameInfo);
- /*
- classes = info.Classes;
- importedNames = info.ImportedNames;
- allDatatypeCtors = info.Ctors;
- */
- // resolve
- var datatypeDependencies = new Graph<IndDatatypeDecl>();
- ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);
- ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
- // tear down
- // give rewriter a chance to do processing
- rewriter.PostResolve(m);
+
+ //Rewriter rewriter = new AutoContractsRewriter();
+ var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);
+ foreach (var decl in sortedDecls) {
+ if (decl is LiteralModuleDecl) {
+ // The declaration is a literal module, so it has members and such that we need
+ // to resolve. First we do refinement transformation. Then we construct the signature
+ // of the module. This is the public, externally visible signature. Then we add in
+ // everything that the system defines, as well as any "import" (i.e. "opened" modules)
+ // directives (currently not supported, but this is where we would do it.) This signature,
+ // which is only used while resolving the members of the module is stored in the (basically)
+ // global variable moduleInfo. Then the signatures of the module members are resolved, followed
+ // by the bodies.
+ var literalDecl = (LiteralModuleDecl)decl;
+ var m = (literalDecl).ModuleDef;
+ //rewriter.PreResolve(m);
+ if (m.RefinementBaseRoot != null) {
+ ModuleSignature sig;
+ if (ResolvePath(m.RefinementBaseRoot, m.RefinementBaseName, out sig)) {
+ if (sig.ModuleDef != null) {
+ m.RefinementBase = sig.ModuleDef;
+ var transformer = new RefinementTransformer(this);
+ transformer.Construct(m);
+ } else {
+ Error(m.RefinementBaseName[0], "module ({0}) named as refinement base is not a literal module or reference to a literal module", Util.Comma(".", m.RefinementBaseName, x => x.val));
+ }
+ } else {
+ Error(m.RefinementBaseName[0], "module ({0}) named as refinement base does not exist", Util.Comma(".", m.RefinementBaseName, x => x.val));
+ }
+ }
+ literalDecl.Signature = RegisterTopLevelDecls(m);
+ // set up environment
+ moduleInfo = MergeSignature(literalDecl.Signature, systemNameInfo);
+ // resolve
+ var datatypeDependencies = new Graph<IndDatatypeDecl>();
+ ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);
+ ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
+ // give rewriter a chance to do processing
+ //rewriter.PostResolve(m);
+ } else if (decl is AliasModuleDecl) {
+ var alias = (AliasModuleDecl)decl;
+ // resolve the path
+ ModuleSignature p;
+ if (ResolvePath(alias.Root, alias.Path, out p)) {
+ alias.Signature = p;
+ } else {
+ alias.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature
+ }
+ } else if (decl is AbstractModuleDecl) {
+ var abs = (AbstractModuleDecl)decl;
+ ModuleSignature p; ModuleDefinition mod;
+ if (ResolvePath(abs.Root, abs.Path, out p)) {
+ abs.Signature = MakeAbstractSignature(p, abs.Name, abs.Height, out mod);
+ moduleInfo = MergeSignature(abs.Signature, systemNameInfo);
+ // resolve
+ var datatypeDependencies = new Graph<IndDatatypeDecl>();
+ ResolveTopLevelDecls_Signatures(mod.TopLevelDecls, datatypeDependencies);
+ ResolveTopLevelDecls_Meat(mod.TopLevelDecls, datatypeDependencies);
+ prog.Modules.Add(mod);
+ } else {
+ abs.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature
+ }
+ } else { Contract.Assert(false); }
+ Contract.Assert(decl.Signature != null);
}
// compute IsRecursive bit for mutually recursive functions
- foreach (ModuleDecl m in mm) {
+ foreach (ModuleDefinition m in mm) {
foreach (TopLevelDecl decl in m.TopLevelDecls) {
ClassDecl cl = decl as ClassDecl;
if (cl != null) {
@@ -182,152 +224,153 @@ namespace Microsoft.Dafny { }
}
}
+
}
- private class ModuleBindings {
+
+ public class ModuleBindings {
private ModuleBindings parent;
private Dictionary<string, ModuleDecl> modules;
+ private Dictionary<string, ModuleBindings> bindings;
public ModuleBindings(ModuleBindings p) {
parent = p;
- modules = new Dictionary<string,ModuleDecl>();
+ modules = new Dictionary<string, ModuleDecl>();
+ bindings = new Dictionary<string, ModuleBindings>();
}
- public bool BindName(string name, ModuleDecl subModule) {
+ public bool BindName(string name, ModuleDecl subModule, ModuleBindings b) {
if (modules.ContainsKey(name)) {
return false;
} else {
modules.Add(name, subModule);
+ bindings.Add(name, b);
return true;
}
}
- public bool TryLookup(string name, out ModuleDecl m) {
- if (modules.TryGetValue(name, out m))
+ public bool TryLookup(IToken name, out ModuleDecl m) {
+ Contract.Requires(name != null);
+ if (modules.TryGetValue(name.val, out m)) {
return true;
- else if (parent != null) {
+ } else if (parent != null) {
return parent.TryLookup(name, out m);
} else return false;
}
+ public IEnumerable<ModuleDecl> ModuleList {
+ get { return modules.Values; }
+ }
+ public ModuleBindings SubBindings(string name) {
+ ModuleBindings v = null;
+ bindings.TryGetValue(name, out v);
+ return v;
+ }
}
- private void BindModuleNames(ModuleDecl moduleDecl, ModuleBindings parentBindings, List<ModuleDecl> globalModuleList, Graph<ModuleDecl> importGraph) {
- // a dictionary of submodules at the current scope.
- var modules = new Dictionary<string, ModuleDecl>();
- var moduleList = new List<ModuleDecl>();
+ private ModuleBindings BindModuleNames(ModuleDefinition moduleDecl, ModuleBindings parentBindings) {
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);
+ if (tld is LiteralModuleDecl) {
+ var subdecl = (LiteralModuleDecl)tld;
+ var subBindings = BindModuleNames(subdecl.ModuleDef, bindings);
+ subdecl.ModuleDef.Bindings = subBindings;
+ if (!bindings.BindName(subdecl.Name, subdecl, subBindings)) {
+ Error(subdecl.Module, "Duplicate module name: {0}", subdecl.Name);
}
- }
- }
-
- // 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;
+ } else if (tld is AbstractModuleDecl) {
+ var subdecl = (AbstractModuleDecl)tld;
+ if (!bindings.BindName(subdecl.Name, subdecl, null)) {
+ Error(subdecl.Module, "Duplicate module name: {0}", subdecl.Name);
}
- }
- 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);
+ } else if (tld is AliasModuleDecl) {
+ var subdecl = (AliasModuleDecl)tld;
+ if (!bindings.BindName(subdecl.Name, subdecl, null)) {
+ Error(subdecl.Module, "Duplicate module name: {0}", subdecl.Name);
}
}
- foreach (var dep in m.Dependencies) {
- importGraph.AddEdge(m, dep);
- }
- }
- foreach (var m in moduleList) {
- BindModuleNames(m, bindings, globalModuleList, importGraph);
}
- globalModuleList.AddRange(moduleList);
+ return bindings;
}
- public class ModuleNameInformation
- {
- public readonly Dictionary<string, TopLevelDecl> Classes = new Dictionary<string, TopLevelDecl>();
- public readonly Dictionary<string, ModuleDecl> ImportedNames = new Dictionary<string, ModuleDecl>();
- public readonly Dictionary<string, Tuple<DatatypeCtor, bool>> Ctors = new Dictionary<string,Tuple<DatatypeCtor,bool>>();
-
- 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];
- info.ImportedNames.Add(im.Name, im);
- // 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<DatatypeCtor, bool> pair;
- if (info.Ctors.TryGetValue(kv.Key, out pair)) {
- // mark it as a duplicate
- info.Ctors[kv.Key] = new Tuple<DatatypeCtor, bool>(pair.Item1, true);
- } else {
- // add new
- info.Ctors.Add(kv.Key, kv.Value);
- }
- }
+ private void ProcessDependenciesDefinition(ModuleDecl decl, ModuleDefinition m, ModuleBindings bindings, Graph<ModuleDecl> dependencies) {
+ if (m.RefinementBaseName != null) {
+ ModuleDecl other;
+ if (!bindings.TryLookup(m.RefinementBaseName[0], out other)) {
+ Error(m, "module {0} named as refinement base does not exist", m.RefinementBaseName[0].val);
+ } else if (other is LiteralModuleDecl && ((LiteralModuleDecl)other).ModuleDef == m) {
+ Error(m, "module cannot refine itself: {0}", m.RefinementBaseName[0].val);
+ } else {
+ Contract.Assert(other != null); // follows from postcondition of TryGetValue
+ dependencies.AddEdge(decl, other);
+ m.RefinementBaseRoot = other;
}
- // 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 toplevel in m.TopLevelDecls) {
+ if (toplevel is ModuleDecl) {
+ var d = (ModuleDecl)toplevel;
+ dependencies.AddEdge(decl, d);
+ var subbindings = bindings.SubBindings(d.Name);
+ ProcessDependencies(d, subbindings ?? bindings, dependencies);
}
- foreach (var kv in modules[m.Height].Ctors) {
- info.Ctors[kv.Key] = kv.Value;
+ }
+ }
+ private void ProcessDependencies(ModuleDecl moduleDecl, ModuleBindings bindings, Graph<ModuleDecl> dependencies) {
+ // resolve refines and imports
+ if (moduleDecl is LiteralModuleDecl) {
+ ProcessDependenciesDefinition(moduleDecl, ((LiteralModuleDecl)moduleDecl).ModuleDef, bindings, dependencies);
+ } else if (moduleDecl is AliasModuleDecl) {
+ var alias = moduleDecl as AliasModuleDecl;
+ ModuleDecl root;
+ if (!bindings.TryLookup(alias.Path[0], out root))
+ Error(alias.tok, "module {0} does not exist", Util.Comma(".", alias.Path, x => x.val));
+ else {
+ dependencies.AddEdge(moduleDecl, root);
+ alias.Root = root;
+ }
+ } else if (moduleDecl is AbstractModuleDecl) {
+ var abs = moduleDecl as AbstractModuleDecl;
+ ModuleDecl root;
+ if (!bindings.TryLookup(abs.Path[0], out root))
+ Error(abs.tok, "module {0} does not exist", Util.Comma(".", abs.Path, x => x.val));
+ else {
+ dependencies.AddEdge(moduleDecl, root);
+ abs.Root = root;
}
- return info;
}
}
- ModuleNameInformation RegisterTopLevelDecls(List<TopLevelDecl> declarations) {
- Contract.Requires(declarations != null);
- var info = new ModuleNameInformation();
+ public static ModuleSignature MergeSignature(ModuleSignature m, ModuleSignature system) {
+ var info = new ModuleSignature();
+ // add the system-declared information, among which we know there are no duplicates
+ foreach (var kv in system.TopLevels) {
+ info.TopLevels.Add(kv.Key, kv.Value);
+ }
+ foreach (var kv in system.Ctors) {
+ info.Ctors.Add(kv.Key, kv.Value);
+ }
+ // add for the module itself
+ foreach (var kv in m.TopLevels) {
+ info.TopLevels[kv.Key] = kv.Value;
+ }
+ foreach (var kv in m.Ctors) {
+ info.Ctors[kv.Key] = kv.Value;
+ }
+ return info;
+ }
+ ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef) {
+ Contract.Requires(moduleDef != null);
+ var sig = new ModuleSignature();
+ sig.ModuleDef = moduleDef;
+ List<TopLevelDecl> declarations = moduleDef.TopLevelDecls;
foreach (TopLevelDecl d in declarations) {
Contract.Assert(d != null);
- // register the class/datatype name
- if (info.Classes.ContainsKey(d.Name)) {
+ // register the class/datatype/module name
+ if (sig.TopLevels.ContainsKey(d.Name)) {
Error(d, "Duplicate name of top-level declaration: {0}", d.Name);
} else {
- info.Classes.Add(d.Name, d);
+ sig.TopLevels.Add(d.Name, d);
}
- if (d is SubModuleDecl) {
- // do Nothing
+ if (d is ModuleDecl) {
+ // nothing to do
} else if (d is ArbitraryTypeDecl) {
// nothing more to register
@@ -378,12 +421,12 @@ namespace Microsoft.Dafny { // also register the constructor name globally
Tuple<DatatypeCtor, bool> pair;
- if (info.Ctors.TryGetValue(ctor.Name, out pair)) {
+ if (sig.Ctors.TryGetValue(ctor.Name, out pair)) {
// mark it as a duplicate
- info.Ctors[ctor.Name] = new Tuple<DatatypeCtor, bool>(pair.Item1, true);
+ sig.Ctors[ctor.Name] = new Tuple<DatatypeCtor, bool>(pair.Item1, true);
} else {
// add new
- info.Ctors.Add(ctor.Name, new Tuple<DatatypeCtor, bool>(ctor, false));
+ sig.Ctors.Add(ctor.Name, new Tuple<DatatypeCtor, bool>(ctor, false));
}
}
}
@@ -405,9 +448,331 @@ namespace Microsoft.Dafny { }
}
}
- return info;
+ return sig;
+ }
+
+ private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, out ModuleDefinition mod) {
+ mod = new ModuleDefinition(Token.NoToken, Name+".Abs", true, true, null, null);
+ mod.Height = Height;
+ foreach (var kv in p.TopLevels) {
+ mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod));
+ }
+ return RegisterTopLevelDecls(mod);
+ }
+ TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) {
+ Contract.Requires(d != null);
+ Contract.Requires(m != null);
+
+ if (d is ArbitraryTypeDecl) {
+ var dd = (ArbitraryTypeDecl)d;
+ return new ArbitraryTypeDecl(dd.tok, dd.Name, m, null);
+ } else if (d is IndDatatypeDecl) {
+ var dd = (IndDatatypeDecl)d;
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var ctors = dd.Ctors.ConvertAll(CloneCtor);
+ var dt = new IndDatatypeDecl(dd.tok, dd.Name, m, tps, ctors, null);
+ return dt;
+ } else if (d is CoDatatypeDecl) {
+ var dd = (CoDatatypeDecl)d;
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var ctors = dd.Ctors.ConvertAll(CloneCtor);
+ var dt = new CoDatatypeDecl(dd.tok, dd.Name, m, tps, ctors, null);
+ return dt;
+ } else if (d is ClassDecl) {
+ var dd = (ClassDecl)d;
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var mm = dd.Members.ConvertAll(CloneMember);
+ var cl = new ClassDecl(dd.tok, dd.Name, m, tps, mm, null);
+ return cl;
+ } else if (d is ModuleDecl) {
+ if (d is LiteralModuleDecl) {
+ return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m);
+ } else if (d is AliasModuleDecl) {
+ var a = (AliasModuleDecl)d;
+ var alias = new AliasModuleDecl(a.Path, a.tok, m);
+ alias.ModuleReference = a.ModuleReference;
+ alias.Signature = a.Signature;
+ return alias;
+ }
+ Contract.Assert(false); // unexpected declaration
+ return null; // to please compiler
+ } else {
+ Contract.Assert(false); // unexpected declaration
+ return null; // to please compiler
+ }
+ }
+ MemberDecl CloneMember(MemberDecl member) {
+ if (member is Field) {
+ var f = (Field)member;
+ return new Field(f.tok, f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null);
+ } else if (member is Function) {
+ var f = (Function)member;
+ return CloneFunction(f.tok, f, f.IsGhost);
+ } else {
+ var m = (Method)member;
+ return CloneMethod(m);
+ }
+ }
+ TypeParameter CloneTypeParam(TypeParameter tp) {
+ return new TypeParameter(tp.tok, tp.Name);
+ }
+
+ DatatypeCtor CloneCtor(DatatypeCtor ct) {
+ return new DatatypeCtor(ct.tok, ct.Name, ct.Formals.ConvertAll(CloneFormal), null);
+ }
+ Formal CloneFormal(Formal formal) {
+ return new Formal(formal.tok, formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost);
+ }
+ Type CloneType(Type t) {
+ if (t is BasicType) {
+ return t;
+ } else if (t is SetType) {
+ var tt = (SetType)t;
+ return new SetType(CloneType(tt.Arg));
+ } else if (t is SeqType) {
+ var tt = (SeqType)t;
+ return new SeqType(CloneType(tt.Arg));
+ } else if (t is MultiSetType) {
+ var tt = (MultiSetType)t;
+ return new MultiSetType(CloneType(tt.Arg));
+ } else if (t is MapType) {
+ var tt = (MapType)t;
+ return new MapType(CloneType(tt.Domain), CloneType(tt.Range));
+ } else if (t is UserDefinedType) {
+ var tt = (UserDefinedType)t;
+ return new UserDefinedType(tt.tok, tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.ModuleName == null ? null : tt.ModuleName);
+ } else if (t is InferredTypeProxy) {
+ return new InferredTypeProxy();
+ } else {
+ Contract.Assert(false); // unexpected type (e.g., no other type proxies are expected at this time)
+ return null; // to please compiler
+ }
+ }
+ Function CloneFunction(IToken tok, Function f, bool isGhost) {
+
+ var tps = f.TypeArgs.ConvertAll(CloneTypeParam);
+ var formals = f.Formals.ConvertAll(CloneFormal);
+ var req = f.Req.ConvertAll(CloneExpr);
+ var reads = f.Reads.ConvertAll(CloneFrameExpr);
+ var decreases = CloneSpecExpr(f.Decreases);
+
+ var ens = f.Ens.ConvertAll(CloneExpr);
+
+ Expression body = CloneExpr(f.Body);
+
+ if (f is Predicate) {
+ return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,
+ req, reads, ens, decreases, body, false, null, false);
+ } else {
+ return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),
+ req, reads, ens, decreases, body, null, false);
+ }
+ }
+ Method CloneMethod(Method m) {
+ Contract.Requires(m != null);
+
+ var tps = m.TypeArgs.ConvertAll(CloneTypeParam);
+ var ins = m.Ins.ConvertAll(CloneFormal);
+ var req = m.Req.ConvertAll(CloneMayBeFreeExpr);
+ var mod = CloneSpecFrameExpr(m.Mod);
+ var decreases = CloneSpecExpr(m.Decreases);
+
+ var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr);
+
+ if (m is Constructor) {
+ return new Constructor(m.tok, m.Name, tps, ins,
+ req, mod, ens, decreases, null, null, false);
+ } else {
+ return new Method(m.tok, m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),
+ req, mod, ens, decreases, null, null, false);
+ }
+ }
+ Specification<Expression> CloneSpecExpr(Specification<Expression> spec) {
+ var ee = spec.Expressions == null ? null : spec.Expressions.ConvertAll(CloneExpr);
+ return new Specification<Expression>(ee, null);
+ }
+ Specification<FrameExpression> CloneSpecFrameExpr(Specification<FrameExpression> frame) {
+ var ee = frame.Expressions == null ? null : frame.Expressions.ConvertAll(CloneFrameExpr);
+ return new Specification<FrameExpression>(ee, null);
+ }
+ FrameExpression CloneFrameExpr(FrameExpression frame) {
+ return new FrameExpression(CloneExpr(frame.E), frame.FieldName);
+ }
+ MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) {
+ return new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree);
+ }
+ BoundVar CloneBoundVar(BoundVar bv) {
+ return new BoundVar((bv.tok), bv.Name, CloneType(bv.Type));
+ }
+ Expression CloneExpr(Expression expr) {
+ if (expr == null) {
+ return null;
+ } else if (expr is LiteralExpr) {
+ var e = (LiteralExpr)expr;
+ if (e.Value == null) {
+ return new LiteralExpr((e.tok));
+ } else if (e.Value is bool) {
+ return new LiteralExpr((e.tok), (bool)e.Value);
+ } else {
+ return new LiteralExpr((e.tok), (BigInteger)e.Value);
+ }
+
+ } else if (expr is ThisExpr) {
+ if (expr is ImplicitThisExpr) {
+ return new ImplicitThisExpr((expr.tok));
+ } else {
+ return new ThisExpr((expr.tok));
+ }
+
+ } else if (expr is IdentifierExpr) {
+ var e = (IdentifierExpr)expr;
+ return new IdentifierExpr((e.tok), e.Name);
+
+ } else if (expr is DatatypeValue) {
+ var e = (DatatypeValue)expr;
+ return new DatatypeValue((e.tok), e.DatatypeName, e.MemberName, e.Arguments.ConvertAll(CloneExpr));
+
+ } else if (expr is DisplayExpression) {
+ DisplayExpression e = (DisplayExpression)expr;
+ if (expr is SetDisplayExpr) {
+ return new SetDisplayExpr((e.tok), e.Elements.ConvertAll(CloneExpr));
+ } else if (expr is MultiSetDisplayExpr) {
+ return new MultiSetDisplayExpr((e.tok), e.Elements.ConvertAll(CloneExpr));
+ } else {
+ Contract.Assert(expr is SeqDisplayExpr);
+ return new SeqDisplayExpr((e.tok), e.Elements.ConvertAll(CloneExpr));
+ }
+
+ } else if (expr is MapDisplayExpr) {
+ MapDisplayExpr e = (MapDisplayExpr)expr;
+ List<ExpressionPair> pp = new List<ExpressionPair>();
+ foreach (ExpressionPair p in e.Elements) {
+ pp.Add(new ExpressionPair(CloneExpr(p.A), CloneExpr(p.B)));
+ }
+ return new MapDisplayExpr((expr.tok), pp);
+ } else if (expr is ExprDotName) {
+ var e = (ExprDotName)expr;
+ return new ExprDotName((e.tok), CloneExpr(e.Obj), e.SuffixName);
+
+ } else if (expr is FieldSelectExpr) {
+ var e = (FieldSelectExpr)expr;
+ return new FieldSelectExpr((e.tok), CloneExpr(e.Obj), e.FieldName);
+
+ } else if (expr is SeqSelectExpr) {
+ var e = (SeqSelectExpr)expr;
+ return new SeqSelectExpr((e.tok), e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1));
+
+ } else if (expr is MultiSelectExpr) {
+ var e = (MultiSelectExpr)expr;
+ return new MultiSelectExpr((e.tok), CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr));
+
+ } else if (expr is SeqUpdateExpr) {
+ var e = (SeqUpdateExpr)expr;
+ return new SeqUpdateExpr((e.tok), CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value));
+
+ } else if (expr is FunctionCallExpr) {
+ var e = (FunctionCallExpr)expr;
+ return new FunctionCallExpr((e.tok), e.Name, CloneExpr(e.Receiver), e.OpenParen == null ? null : (e.OpenParen), e.Args.ConvertAll(CloneExpr));
+
+ } else if (expr is OldExpr) {
+ var e = (OldExpr)expr;
+ return new OldExpr((e.tok), CloneExpr(e.E));
+
+ } else if (expr is MultiSetFormingExpr) {
+ var e = (MultiSetFormingExpr)expr;
+ return new MultiSetFormingExpr((e.tok), CloneExpr(e.E));
+
+ } else if (expr is FreshExpr) {
+ var e = (FreshExpr)expr;
+ return new FreshExpr((e.tok), CloneExpr(e.E));
+
+ } else if (expr is AllocatedExpr) {
+ var e = (AllocatedExpr)expr;
+ return new AllocatedExpr((e.tok), CloneExpr(e.E));
+
+ } else if (expr is UnaryExpr) {
+ var e = (UnaryExpr)expr;
+ return new UnaryExpr((e.tok), e.Op, CloneExpr(e.E));
+
+ } else if (expr is BinaryExpr) {
+ var e = (BinaryExpr)expr;
+ return new BinaryExpr((e.tok), e.Op, CloneExpr(e.E0), CloneExpr(e.E1));
+
+ } else if (expr is ChainingExpression) {
+ var e = (ChainingExpression)expr;
+ return CloneExpr(e.E); // just clone the desugaring, since it's already available
+
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ return new LetExpr((e.tok), e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body));
+
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ var tk = (e.tok);
+ var bvs = e.BoundVars.ConvertAll(CloneBoundVar);
+ var range = CloneExpr(e.Range);
+ var term = CloneExpr(e.Term);
+ if (e is ForallExpr) {
+ return new ForallExpr(tk, bvs, range, term, null);
+ } else if (e is ExistsExpr) {
+ return new ExistsExpr(tk, bvs, range, term, null);
+ } else if (e is MapComprehension) {
+ return new MapComprehension(tk, bvs, range, term);
+ } else {
+ Contract.Assert(e is SetComprehension);
+ return new SetComprehension(tk, bvs, range, term);
+ }
+
+ } else if (expr is WildcardExpr) {
+ return new WildcardExpr((expr.tok));
+
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ if (e is AssertExpr) {
+ return new AssertExpr((e.tok), CloneExpr(e.Guard), CloneExpr(e.Body));
+ } else {
+ Contract.Assert(e is AssumeExpr);
+ return new AssumeExpr((e.tok), CloneExpr(e.Guard), CloneExpr(e.Body));
+ }
+
+ } else if (expr is ITEExpr) {
+ var e = (ITEExpr)expr;
+ return new ITEExpr((e.tok), CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els));
+
+ } else if (expr is ParensExpression) {
+ var e = (ParensExpression)expr;
+ return CloneExpr(e.E); // skip the parentheses in the clone
+
+ } else if (expr is IdentifierSequence) {
+ var e = (IdentifierSequence)expr;
+ var aa = e.Arguments == null ? null : e.Arguments.ConvertAll(CloneExpr);
+ return new IdentifierSequence(e.Tokens.ConvertAll(tk => (tk)), e.OpenParen == null ? null : (e.OpenParen), aa);
+
+ } else if (expr is MatchExpr) {
+ var e = (MatchExpr)expr;
+ return new MatchExpr((e.tok), CloneExpr(e.Source),
+ e.Cases.ConvertAll(c => new MatchCaseExpr((c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))));
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
+ }
}
+ private bool ResolvePath(ModuleDecl root, List<IToken> Path, out ModuleSignature p) {
+ p = root.Signature;
+ int i = 1;
+ while (i < Path.Count) {
+ ModuleSignature pp;
+ if (p.FindSubmodule(Path[i].val, out pp)) {
+ p = pp;
+ i++;
+ } else {
+ Error(Path[i], "module {0} does not exist", Path[i].val);
+ break;
+ }
+ }
+ return i == Path.Count;
+ }
public void ResolveTopLevelDecls_Signatures(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<IndDatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
Contract.Requires(declarations != null);
Contract.Requires(datatypeDependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(datatypeDependencies));
@@ -419,7 +784,7 @@ namespace Microsoft.Dafny { // nothing to do
} else if (d is ClassDecl) {
ResolveClassMemberTypes((ClassDecl)d);
- } else if (d is SubModuleDecl) {
+ } else if (d is ModuleDecl) {
// TODO: what goes here?
} else {
ResolveCtorTypes((DatatypeDecl)d, datatypeDependencies);
@@ -999,23 +1364,15 @@ 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 = null;
if (t.ModuleName != null) {
- foreach (var imp in currentClass.Module.Imports) {
- if (imp.Name == t.ModuleName.val) {
- // now search among the types declared in module "imp"
- foreach (var tld in imp.TopLevelDecls) { // this search is slow, but oh well
- if (tld.Name == t.Name) {
- // found the class
- d = tld;
- goto DONE_WITH_QUALIFIED_NAME;
- }
- }
- Error(t.tok, "Undeclared class name {0} in module {1}", t.Name, t.ModuleName.val);
- goto DONE_WITH_QUALIFIED_NAME;
+ ModuleDecl m;
+ if (currentClass.Module.Bindings.TryLookup(t.ModuleName, out m)) {
+ if (!m.Signature.TopLevels.TryGetValue(t.Name, out d)) {
+ Error(t.tok, "The name does not exist in the given module");
}
+ } else {
+ Error(t.ModuleName, "Undeclared module name: {0} (did you forget a module import?)", t.ModuleName.val);
}
- Error(t.ModuleName, "Undeclared module name: {0} (did you forget a module import?)", t.ModuleName.val);
- DONE_WITH_QUALIFIED_NAME: ;
- } else if (!moduleInfo.Classes.TryGetValue(t.Name, out d)) {
+ } else if (!moduleInfo.TopLevels.TryGetValue(t.Name, out d)) {
Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget a module import?)", t.Name);
}
@@ -2234,13 +2591,14 @@ namespace Microsoft.Dafny { // Resolution termination check
if (method.EnclosingClass != null && callee.EnclosingClass != null) {
- ModuleDecl callerModule = method.EnclosingClass.Module;
- ModuleDecl calleeModule = callee.EnclosingClass.Module;
+ ModuleDefinition callerModule = method.EnclosingClass.Module;
+ ModuleDefinition calleeModule = callee.EnclosingClass.Module;
if (callerModule == calleeModule) {
// intra-module call; this is allowed; add edge in module's call graph
callerModule.CallGraph.AddEdge(method, callee);
} else {
- Contract.Assert(importGraph.Reaches(callerModule, calleeModule));
+ //Contract.Assert(dependencies.Reaches(callerModule, calleeModule));
+ //
}
}
}
@@ -2674,7 +3032,7 @@ namespace Microsoft.Dafny { } else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
TopLevelDecl d;
- if (!moduleInfo.Classes.TryGetValue(dtv.DatatypeName, out d)) {
+ if (!moduleInfo.TopLevels.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());
@@ -2952,7 +3310,7 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Eq:
case BinaryExpr.Opcode.Neq:
- if (!CouldPossiblyBeSameType(e.E0.Type, e.E1.Type)) {
+ if (!ComparableTypes(e.E0.Type, e.E1.Type)) {
if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
}
@@ -3347,6 +3705,31 @@ namespace Microsoft.Dafny { }
}
+ private bool ComparableTypes(Type A, Type B) {
+ if (A.IsArrayType && B.IsArrayType) {
+ Type a = UserDefinedType.ArrayElementType(A);
+ Type b = UserDefinedType.ArrayElementType(B);
+ return CouldPossiblyBeSameType(a, b);
+ } else
+ if (A is UserDefinedType && B is UserDefinedType) {
+ UserDefinedType a = (UserDefinedType)A;
+ UserDefinedType b = (UserDefinedType)B;
+ if (a.ResolvedClass != null && b.ResolvedClass != null && a.ResolvedClass.Name == b.ResolvedClass.Name) {
+ if (a.TypeArgs.Count != b.TypeArgs.Count) {
+ return false; // this probably doesn't happen if the classes are the same.
+ }
+ for (int i = 0; i < a.TypeArgs.Count; i++) {
+ if (!CouldPossiblyBeSameType(a.TypeArgs[i], b.TypeArgs[i]))
+ return false;
+ }
+ // all parameters could be the same
+ return true;
+ }
+ // either we don't know what class it is yet, or the classes mismatch
+ return false;
+ }
+ return false;
+ }
private bool CouldPossiblyBeSameType(Type A, Type B) {
if (A.IsTypeParameter || B.IsTypeParameter) {
return true;
@@ -3541,8 +3924,8 @@ namespace Microsoft.Dafny { // Resolution termination check
if (currentFunction != null && currentFunction.EnclosingClass != null && function.EnclosingClass != null) {
- ModuleDecl callerModule = currentFunction.EnclosingClass.Module;
- ModuleDecl calleeModule = function.EnclosingClass.Module;
+ ModuleDefinition callerModule = currentFunction.EnclosingClass.Module;
+ ModuleDefinition calleeModule = function.EnclosingClass.Module;
if (callerModule == calleeModule) {
// intra-module call; this is allowed; add edge in module's call graph
callerModule.CallGraph.AddEdge(currentFunction, function);
@@ -3550,7 +3933,7 @@ namespace Microsoft.Dafny { currentFunction.IsRecursive = true; // self recursion (mutual recursion is determined elsewhere)
}
} else {
- Contract.Assert(importGraph.Reaches(callerModule, calleeModule));
+ //Contract.Assert(dependencies.Reaches(callerModule, calleeModule));
}
}
}
@@ -3578,7 +3961,6 @@ namespace Microsoft.Dafny { Tuple<DatatypeCtor, bool> pair;
Dictionary<string, MemberDecl> 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
@@ -3586,7 +3968,7 @@ namespace Microsoft.Dafny { ResolveExpression(r, twoState);
r = ResolveSuffix(r, e, 1, twoState, allowMethodCall, out call);
- } else if (moduleInfo.Classes.TryGetValue(id.val, out decl)) {
+ } else if (moduleInfo.TopLevels.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) {
@@ -3602,13 +3984,12 @@ namespace Microsoft.Dafny { var cd = (ClassDecl)decl;
r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, twoState, allowMethodCall, out call);
- } else if (decl is SubModuleDecl) {
+ } else if (decl is ModuleDecl) {
// ----- root is a submodule
- module = ((SubModuleDecl)decl).SubModule;
if (!(1 < e.Tokens.Count)) {
- Error(e.tok, "module {0} is not an expression", module.Name);
+ Error(e.tok, "module {0} cannot be used here", ((ModuleDecl)decl).Name);
}
- call = ResolveIdentifierSequenceModuleScope(e, 1, moduleNameInfo[module.Height], twoState, allowMethodCall);
+ call = ResolveIdentifierSequenceModuleScope(e, 1, ((ModuleDecl)decl).Signature, twoState, allowMethodCall);
} else {
// ----- root is a datatype
var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl
@@ -3634,11 +4015,6 @@ 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;
@@ -3671,7 +4047,7 @@ namespace Microsoft.Dafny { return call;
}
- CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleNameInformation info, bool twoState, bool allowMethodCall) {
+ CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature 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)
@@ -3682,9 +4058,8 @@ namespace Microsoft.Dafny { CallRhs call = null;
TopLevelDecl decl;
- ModuleDecl module;
var id = e.Tokens[p];
- if (info.Classes.TryGetValue(id.val, out decl)) {
+ if (info.TopLevels.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) {
@@ -3692,13 +4067,12 @@ namespace Microsoft.Dafny { var cd = (ClassDecl)decl;
r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, p + 1, twoState, allowMethodCall, out call);
- } else if (decl is SubModuleDecl) {
+ } else if (decl is ModuleDecl) {
// ----- 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);
+ Error(e.tok, "module {0} cannot be used here", ((ModuleDecl)decl).Name);
}
- call = ResolveIdentifierSequenceModuleScope(e, p+1, moduleNameInfo[module.Height], twoState, allowMethodCall);
+ call = ResolveIdentifierSequenceModuleScope(e, p + 1, ((ModuleDecl)decl).Signature, twoState, allowMethodCall);
} else {
// ----- root is a datatype
var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl
@@ -4513,7 +4887,7 @@ namespace Microsoft.Dafny { class CoCallResolution
{
- readonly ModuleDecl currentModule;
+ readonly ModuleDefinition currentModule;
readonly Function currentFunction;
readonly bool dealsWithCodatatypes;
|