From 412f10eb6746c06c388dbab01c7d9602c9562ec9 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 22 May 2024 14:49:51 +0200 Subject: [PATCH] fix: Apply name mangling to datatype names in Python more often (#5476) Fixes #5469 --------- Co-authored-by: Remy Willems --- .../Backends/Python/PythonCodeGenerator.cs | 2 +- .../LitTest/git-issues/git-issue-5469.dfy | 15 +++++++++++++++ .../LitTest/git-issues/git-issue-5469.dfy.expect | 1 + .../git-issues/git-issue-5469.dfy.rs.check | 1 + docs/dev/news/5476.fix | 1 + 5 files changed, 19 insertions(+), 1 deletion(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.rs.check create mode 100644 docs/dev/news/5476.fix diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs index 39ba59fd09..a4d93a820e 100644 --- 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 new file mode 100644 index 0000000000..f55fe494d5 --- /dev/null +++ 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"; +} \ No newline at end of file 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 new file mode 100644 index 0000000000..2954079eab --- /dev/null +++ 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 new file mode 100644 index 0000000000..2e0db5d532 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.rs.check @@ -0,0 +1 @@ +CHECK: error \ No newline at end of file diff --git a/docs/dev/news/5476.fix b/docs/dev/news/5476.fix new file mode 100644 index 0000000000..156ae3c64f --- /dev/null +++ b/docs/dev/news/5476.fix @@ -0,0 +1 @@ +Apply name mangling to datatype names in Python more often