Fix: Support for user-defined module fmt for all compilers (#5441)

This PR fixes #5283
I added the corresponding test.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -2573,11 +2573,77 @@ protected class ClassWriter : IClassWriter {
  }
  }
 
+ /* Obtained by running the following on the console on the page https://pkg.go.dev/std :
+ var lineLength = 0; copy([...document.querySelectorAll(
+ "td > div.UnitDirectories-pathCell > div > span, "+
+ "td > div.UnitDirectories-pathCell > div > a")]
+ .map((e, i) => {
+ var res = JSON.stringify(e.textContent);
+ if(lineLength + res.length > 94) {
+ lineLength = res.length;
+ res = ",\n " + res;
+ } else if(i > 0) {
+ res = "," + res;
+ lineLength += res.length;
+ }
+ return res;
+ }).join(""))
+ */
+ public readonly HashSet<string> ReservedModuleNames = new() {
+ "c",
+ "archive",
+ "bufio",
+ "builtin",
+ "bytes",
+ "cmp",
+ "compress",
+ "container",
+ "context",
+ "crypto",
+ "database",
+ "debug",
+ "embed",
+ "encoding",
+ "errors",
+ "expvar",
+ "flag",
+ "fmt",
+ "go",
+ "hash",
+ "html",
+ "image",
+ "index",
+ "internal",
+ "io",
+ "log",
+ "maps",
+ "math",
+ "mime",
+ "net",
+ "os",
+ "path",
+ "plugin",
+ "reflect",
+ "regexp",
+ "runtime",
+ "slices",
+ "sort",
+ "strconv",
+ "strings",
+ "sync",
+ "syscall",
+ "testing",
+ "text",
+ "time",
+ "unicode",
+ "unsafe"
+ };
+
  public string PublicModuleIdProtect(string name) {
- if (name == "C") {
- return "_C";
+ if (ReservedModuleNames.Contains(name.ToLower())) {
+ return "_" + name;
  } else {
- return name;
+ return IdProtect(name);
  }
  }
 

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -83,7 +83,7 @@ class PythonCodeGenerator : SinglePassCodeGenerator {
 
  protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
  string libraryName, ConcreteSyntaxTree wr) {
- moduleName = IdProtect(moduleName);
+ moduleName = PublicModuleIdProtect(moduleName);
  var file = wr.NewFile($"{moduleName}.py");
  EmitImports(moduleName, file);
  return file;
@@ -170,7 +170,7 @@ class PythonCodeGenerator : SinglePassCodeGenerator {
  }
 
  protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, ConcreteSyntaxTree wr) {
- var cw = (ClassWriter)CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), IdName(iter), false,
+ var cw = (ClassWriter)CreateClass(PublicModuleIdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), IdName(iter), false,
  iter.FullName, iter.TypeArgs, iter, null, iter.tok, wr);
  var constructorWriter = cw.ConstructorWriter;
  var w = cw.MethodWriter;
@@ -686,8 +686,11 @@ private class ClassWriter : IClassWriter {
  }
 
  private string FullName(TopLevelDecl decl) {
- var localDefinition = decl.EnclosingModuleDefinition == enclosingModule;
- return IdProtect(localDefinition ? decl.GetCompileName(Options) : decl.GetFullCompileName(Options));
+ var segments = new List<string> { IdProtect(decl.GetCompileName(Options)) };
+ if (decl.EnclosingModuleDefinition != enclosingModule) {
+ segments = decl.EnclosingModuleDefinition.GetCompileName(Options).Split('.').Select(PublicModuleIdProtect).Concat(segments).ToList();
+ }
+ return string.Join('.', segments);
  }
 
  protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree wr, IToken tok,
@@ -1154,6 +1157,18 @@ private class ClassWriter : IClassWriter {
  };
  }
 
+
+ private readonly HashSet<string> ReservedModuleNames = new() {
+ "itertools", "math", "typing", "sys"
+ };
+
+ private string PublicModuleIdProtect(string name) {
+ if (ReservedModuleNames.Contains(name)) {
+ return "_" + name;
+ }
+ return IdProtect(name);
+ }
+
  protected override string FullTypeName(UserDefinedType udt, MemberDecl member = null) {
  if (udt is ArrowType) {
  //TODO: Add deeper types

Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md

@@ -104,7 +104,7 @@ and then right-click the test you wish to debug and select
 so you may wish to remove the calls you are not interested in first, e.g. if you are debugging an issue with a specific compiler.
 
 ## Updating test expect files
-If you set the static field `DiffCommand.UpdateExpectFile` to true instead of false, then the `diff` command in tests will not do a comparison but instead overwrite the expected file with the actual contents. This can be useful when you need to update expect files.
+If you set the environment variable `DAFNY_INTEGRATION_TESTS_UPDATE_EXPECT_FILE` to `true`, then the `diff` command in tests will not do a comparison but instead overwrite the expected file with the actual contents. This can be useful when you need to update expect files.
 
 ## Updating compiler-specific test expect files
 To update compiler-specific error-aware output files for tests running with `%forEachDafnyCompiler`,

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5283.dfy

@@ -0,0 +1,60 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+/* Obtained from
+https://pkg.go.dev/std
+by running on the console
+copy([...document.querySelectorAll(
+ "td > div.UnitDirectories-pathCell > div > span, "+
+ "td > div.UnitDirectories-pathCell > div > a")]
+ .map(e => "module " + e.textContent + " {}").join("\n"))
+*/
+module archive {}
+module bufio {}
+module builtin {}
+module bytes {}
+module cmp {}
+module compress {}
+module container {}
+module context {}
+module crypto {}
+module database {}
+module debug {}
+module embed {}
+module encoding {}
+module errors {}
+module expvar {}
+module flag {}
+module fmt {}
+module go {}
+module hash {}
+module html {}
+module image {}
+module index {}
+module internal {}
+module io {}
+module log {}
+module maps {}
+module math {}
+module mime {}
+module net {}
+module os {}
+module path {}
+module plugin {}
+module reflect {}
+module regexp {}
+module runtime {}
+module slices {}
+module sort {}
+module strconv {}
+module strings {}
+module sync {}
+module syscall {}
+module testing {}
+module text {}
+module time {}
+module unicode {}
+module unsafe {}
+
+method Main(){
+ print "done\n";
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5283.dfy.expect

@@ -0,0 +1 @@
+done

docs/dev/news/5283.fix

@@ -0,0 +1 @@
+Avoid name clashes with Go built-in modules