diff options
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index a019f068..0dcbcf11 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/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;
|