Dafny: fully qualify (with module names) names of types in the translation into Boogie

Dafny: started cloning of refined classes
Dafny: added /rprint switch to print the (syntax of the) resolved Dafny program

1 files changed, 8 insertions, 3 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 7884b40c..357b2b60 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -570,7 +570,6 @@ namespace Microsoft.Dafny {
     [Pure]

     public override string ToString() {

       Contract.Ensures(Contract.Result<string>() != null);

-

       return Name;

     }

   }

@@ -668,6 +667,12 @@ namespace Microsoft.Dafny {
       Module = module;

       TypeArgs = typeArgs;

     }

+

+    public string FullName {

+      get {

+        return Module.Name + "." + Name;

+      }

+    }

   }

 

   public class ClassDecl : TopLevelDecl {

@@ -776,7 +781,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(EnclosingDatatype != null);

         Contract.Ensures(Contract.Result<string>() != null);

 

-        return "#" + EnclosingDatatype.Name + "." + Name;

+        return "#" + EnclosingDatatype.FullName + "." + Name;

       }

     }

   }

@@ -799,7 +804,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(EnclosingClass != null);

         Contract.Ensures(Contract.Result<string>() != null);

 

-        return EnclosingClass.Name + "." + Name;

+        return EnclosingClass.FullName + "." + Name;

       }

     }

   }