fix: Apply name mangling to datatype names in Python more often (#5476)

Fixes #5469 --------- Co-authored-by: Remy Willems <[email protected]>
dafny-lang · May 22, 2024 · 412f10e · 412f10e
1 parent 4ce2f7e
commit 412f10e
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 1 deletion.
diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
@@ -346,7 +346,7 @@ private void DatatypeFieldsAndConstructor(DatatypeCtor ctor, ConcreteSyntaxTree
 
     private string DtCtorDeclarationName(DatatypeCtor ctor, bool full = false) {
       var dt = ctor.EnclosingDatatype;
-      return $"{(full ? dt.GetFullCompileName(Options) : dt.GetCompileName(Options))}_{ctor.GetCompileName(Options)}";
+      return $"{(full ? dt.GetFullCompileName(Options) : IdProtect(dt.GetCompileName(Options)))}_{ctor.GetCompileName(Options)}";
     }
 
     protected IClassWriter DeclareType(TopLevelDecl d, SubsetTypeDecl.WKind witnessKind, Expression witness, ConcreteSyntaxTree wr) {

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy
@@ -0,0 +1,15 @@
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s"
+
+module SomeDependencyModule {
+  datatype None = None
+}
+
+module SomeModule {
+  import SomeDependencyModule
+
+  const test := SomeDependencyModule.None
+}
+
+method Main() {
+  print SomeModule.test, "\n";
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.expect
@@ -0,0 +1 @@
+SomeDependencyModule.None.None
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.rs.check
@@ -0,0 +1 @@
+CHECK: error
diff --git a/docs/dev/news/5476.fix b/docs/dev/news/5476.fix
@@ -0,0 +1 @@
+Apply name mangling to datatype names in Python more often