summaryrefslogtreecommitdiff
path: root/Source/Dafny/DafnyAst.cs
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-07-04 03:09:20 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2012-07-04 03:09:20 -0700
commite6c93427a01f67a780c4227a27cddd5d38a9672d (patch)
tree74f661c1bda5eafd58c35f4f522354cae30c8e20 /Source/Dafny/DafnyAst.cs
parent8ebd0af61c08737d21226d3e4738a2b799a4db90 (diff)
parentfd1ed2e958a2af3606969c7111387f5236a70bd7 (diff)
Merge
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r--Source/Dafny/DafnyAst.cs17
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;
}
}
}