Make ModuleDefinition inherit from TopLevelDecl instead of just Declaration

5 files changed, 9 insertions, 9 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index b6da3dd4..93237acc 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -14,7 +14,7 @@ namespace Microsoft.Dafny
       if (m is DefaultModuleDecl) {

         nw = new DefaultModuleDecl();

       } else {

-        nw = new ModuleDefinition(Tok(m.tok), name, m.IsAbstract, m.IsFacade, m.RefinementBaseName, CloneAttributes(m.Attributes), true);

+        nw = new ModuleDefinition(Tok(m.tok), name, m.IsAbstract, m.IsFacade, m.RefinementBaseName, m.Module, CloneAttributes(m.Attributes), true);

       }

       foreach (var d in m.TopLevelDecls) {

         nw.TopLevelDecls.Add(CloneDeclaration(d, nw));

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index c7bae4b5..db0b09e8 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -232,7 +232,7 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
     { Attribute<ref attrs> }

     NoUSIdent<out id>                          

     

-      [ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, attrs, false); .)

+      [ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false); .)

        "{"                                       (. module.BodyStartTok = t; .)

         { SubModuleDecl<module, out sm>                (. module.TopLevelDecls.Add(sm); .)

         | ClassDecl<module, out c>                     (. module.TopLevelDecls.Add(c); .)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index a0ea57b7..8f89b1cd 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -68,7 +68,7 @@ namespace Microsoft.Dafny {
 

   public class BuiltIns

   {

-    public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, true);

+    public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, null, true);

     Dictionary<int, ClassDecl> arrayTypeDecls = new Dictionary<int, ClassDecl>();

     public readonly ClassDecl ObjectDecl;

     public BuiltIns() {

@@ -1000,7 +1000,7 @@ namespace Microsoft.Dafny {
     

       

   }

-  public class ModuleDefinition : Declaration {

+  public class ModuleDefinition : TopLevelDecl {

     public readonly List<IToken> RefinementBaseName;  // null if no refinement base

     public ModuleDecl RefinementBaseRoot; // filled in early during resolution, corresponds to RefinementBaseName[0]

     public ModuleDefinition RefinementBase;  // filled in during resolution (null if no refinement base)

@@ -1018,8 +1018,8 @@ namespace Microsoft.Dafny {
       Contract.Invariant(CallGraph != null);

     }

 

-    public ModuleDefinition(IToken tok, string name, bool isAbstract, bool isFacade, List<IToken> refinementBase, Attributes attributes, bool isBuiltinName)

-      : base(tok, name, attributes) {

+    public ModuleDefinition(IToken tok, string name, bool isAbstract, bool isFacade, List<IToken> refinementBase, ModuleDefinition parent, Attributes attributes, bool isBuiltinName)

+      : base(tok, name, parent, new List<TypeParameter>(), attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       RefinementBaseName = refinementBase;

@@ -1130,7 +1130,7 @@ namespace Microsoft.Dafny {
   }

 

   public class DefaultModuleDecl : ModuleDefinition {

-    public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null, true) {

+    public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null, null, true) {

     }

     public override bool IsDefaultModule {

       get {

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index ced17284..ea209e0e 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -317,7 +317,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 				Get();

 				QualifiedName(out idRefined);

 			}

-			module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, attrs, false); 

+			module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false); 

 			Expect(8);

 			module.BodyStartTok = t; 

 			while (StartOf(1)) {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 6c8386aa..047df719 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -963,7 +963,7 @@ namespace Microsoft.Dafny
     }

 

     private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, List<ModuleDefinition> mods) {

-      var mod = new ModuleDefinition(Token.NoToken, Name + ".Abs", true, true, null, null, false);

+      var mod = new ModuleDefinition(Token.NoToken, Name + ".Abs", true, true, null, null, null, false);

       mod.Height = Height;

       foreach (var kv in p.TopLevels) {

         mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod, mods, Name));