Dafny: support opening modules into the local scope

1 files changed, 9 insertions, 7 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index a019f068..0dcbcf11 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -804,10 +804,12 @@ namespace Microsoft.Dafny {
   {

     public ModuleSignature Signature; // filled in by resolution, in topological order.

     public int Height;

-    public ModuleDecl(IToken tok, string name, ModuleDefinition parent)

+    public readonly bool Opened;

+    public ModuleDecl(IToken tok, string name, ModuleDefinition parent, bool opened)

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

         Height = -1;

-        Signature = null;

+      Signature = null;

+      Opened = opened;

     }

   }

   // Represents module X { ... }

@@ -815,7 +817,7 @@ namespace Microsoft.Dafny {
   {

     public readonly ModuleDefinition ModuleDef;

     public LiteralModuleDecl(ModuleDefinition module, ModuleDefinition parent)

-      : base(module.tok, module.Name, parent) {

+      : base(module.tok, module.Name, parent, false) {

       ModuleDef = module;

     }

   }

@@ -826,8 +828,8 @@ namespace Microsoft.Dafny {
                                        // be detected and warned.

     public readonly List<IToken> Path; // generated by the parser, this is looked up

     public ModuleDecl Root;            // the moduleDecl that Path[0] refers to.

-    public AliasModuleDecl(List<IToken> path, IToken name, ModuleDefinition parent)

-      : base(name, name.val, parent) {

+    public AliasModuleDecl(List<IToken> path, IToken name, ModuleDefinition parent, bool opened)

+      : base(name, name.val, parent, opened) {

        Contract.Requires(path != null && path.Count > 0);

        Path = path;

        ModuleReference = null;

@@ -842,8 +844,8 @@ namespace Microsoft.Dafny {
     public readonly List<IToken> CompilePath;

     public ModuleSignature OriginalSignature;

     

-    public AbstractModuleDecl(List<IToken> path, IToken name, ModuleDefinition parent, List<IToken> compilePath)

-      : base(name, name.val, parent) {

+    public AbstractModuleDecl(List<IToken> path, IToken name, ModuleDefinition parent, List<IToken> compilePath, bool opened)

+      : base(name, name.val, parent, opened) {

       Path = path;

       Root = null;

       CompilePath = compilePath;