diff options
author | Rustan Leino <leino@microsoft.com> | 2012-07-04 03:09:20 -0700 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2012-07-04 03:09:20 -0700 |
commit | e6c93427a01f67a780c4227a27cddd5d38a9672d (patch) | |
tree | 74f661c1bda5eafd58c35f4f522354cae30c8e20 /Source/Dafny/DafnyAst.cs | |
parent | 8ebd0af61c08737d21226d3e4738a2b799a4db90 (diff) | |
parent | fd1ed2e958a2af3606969c7111387f5236a70bd7 (diff) |
Merge
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index df6fc2a6..032891ce 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -39,7 +39,7 @@ namespace Microsoft.Dafny { public class BuiltIns
{
- public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null);
+ public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, true);
Dictionary<int, ClassDecl/*!*/> arrayTypeDecls = new Dictionary<int, ClassDecl>();
public readonly ClassDecl ObjectDecl;
public BuiltIns() {
@@ -840,6 +840,7 @@ namespace Microsoft.Dafny { public readonly Dictionary<string, TopLevelDecl> TopLevels = new Dictionary<string, TopLevelDecl>();
public readonly Dictionary<string, Tuple<DatatypeCtor, bool>> Ctors = new Dictionary<string, Tuple<DatatypeCtor, bool>>();
+ public readonly Dictionary<string, MemberDecl> StaticMembers = new Dictionary<string, MemberDecl>();
public ModuleDefinition ModuleDef; // Note: this is null if this signature does not correspond to a specific definition (i.e.
// it is abstract). Otherwise, it points to that definition.
public ModuleSignature Refines;
@@ -868,14 +869,14 @@ namespace Microsoft.Dafny { public int Height; // height in the topological sorting of modules; filled in during resolution
public readonly bool IsGhost;
public readonly bool IsAbstract; // True iff this module represents an abstract interface
-
+ private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled.
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(TopLevelDecls));
Contract.Invariant(CallGraph != null);
}
- public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List<IToken> refinementBase, Attributes attributes)
+ public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List<IToken> refinementBase, Attributes attributes, bool isBuiltinName)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
@@ -884,6 +885,7 @@ namespace Microsoft.Dafny { IsAbstract = isAbstract;
RefinementBaseRoot = null;
RefinementBase = null;
+ IsBuiltinName = isBuiltinName;
}
public virtual bool IsDefaultModule {
get {
@@ -894,7 +896,10 @@ namespace Microsoft.Dafny { new public string CompileName {
get {
if (compileName == null) {
- compileName = "_" + Height.ToString() + "_" + NonglobalVariable.CompilerizeName(Name);
+ if (IsBuiltinName)
+ compileName = Name;
+ else
+ compileName = "_" + Height.ToString() + "_" + NonglobalVariable.CompilerizeName(Name);
}
return compileName;
}
@@ -916,7 +921,7 @@ namespace Microsoft.Dafny { }
public class DefaultModuleDecl : ModuleDefinition {
- public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null) {
+ public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null, false) {
}
public override bool IsDefaultModule {
get {
@@ -1093,7 +1098,7 @@ namespace Microsoft.Dafny { Contract.Requires(EnclosingDatatype != null);
Contract.Ensures(Contract.Result<string>() != null);
- return "#" + EnclosingDatatype.FullName + "." + Name;
+ return "#" + EnclosingDatatype.FullCompileName + "." + Name;
}
}
}
|