Fix name clash in generated CS files when module and types have same name

[olivier-aws]

What was changed?

This change updates the CS code generated from Dafny to fix name clashes between namespace and class when a module defines a datatype with the same name. On the example for #6014, we have:

module A {

  datatype A = Foo. // Notice the name of the datatype is the name of the module

}

module B {

   import opened A

   const bar: A

   method Main() {
     print "Hello!\n";
  }
}

which generated the code (simlified for readability)

namespace A {

  public interface _IA {
    bool is_Foo { get; }
    _IA DowncastClone();
  }
  public class A : _IA {
    public A() {
    }
    // [...]

    public static _IA create() {
      return new A();
    }

    private static readonly A._IA theDefault = create();

   // [...]

    }
  }
} // end of namespace A

namespace B {

  public partial class __default {
    public static void _Main(Dafny.ISequence<Dafny.ISequence<Dafny.Rune>> __noArgsParameter)
    {
      Dafny.Helpers.Print((Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Hello!\n")).ToVerbatimString(false));
    }
    public static A._IA bar { get {
      return A.A.Default();
    } }
  }
} // end of namespace B

The expression A._IA theDefault does not compile in C#, as the first A. is resolved to be the name of the class and not the name of the namespace. One solution could be to ensure we have _IA here instead of A._IA as for the create method, but the code to generate this type name is used at other places where the A._IA is required (e.g in bar method in namespace B).

This change changes the name of the namespace A to _NA when there is a name clash with a datatype declared in A.

How has this been tested?

Updated test gith-issues-6014.dfy

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

This is great thank. One more less C# compiler bug in sight !

More test cases: it looks like the module name contains all the dots, whereas the inner declarations don't. Hence, the test file covering only top-level modules and declarations with the same name might not accurately represent all test cases.
Could you please add a test case like this one?

module Enclosing {
  module A {
    datatype A = Foo
  }
}

module Enclosing.A {
  datatype A = Foo
}

I think these cases won't pass and yet they are likely, as mentioned in this article

Also, for compatibility, we often wish that adding unrelated Dafny code does not change the API of existing generated code, i.e. that changes are possibly local. However, with this solution, a diff like that in Dafny

 module A {
   function ComputeThis(): int { ... }
+  datatype A = Foo
 }

would result in a non-local diff like that in the generated code.

-namespace A {
+namespace _NA {
   class _default {
     static int ComputeThis() { ... }
+  interface _IFoo { ... }
+  class Foo: _IFoo { ... }
 }

which would break any library calling into A._default.ComputeThis(). Well, one might argue that it's good to break calling code so that they are aware that the Dafny code is doing something not very C# compatible, but if that was important, I think we would prefer to reject the Dafny program at resolution time.

Would you mind flipping the fix over and renaming the datatype if it conflicts with the module name? I know this is extra hard work but I hope I have convinced you that it might be preferable. You could reuse the same "_N" prefix.

[MikaelMayer]

A few comments, otherwise I find this solution very adequate. Thanks for addressing all my previous comment.

[MikaelMayer]

Suggested change

	return "class_" + className;
	return "_class_" + className;

That way we are sure we don't clash with something named "class_..." already in the dafny code.

[olivier-aws]

The "class_" + className encoding was the one already done by the CppCodeGenerator. I'm not sure I want to take the risk to modify it in this change, maybe a subsequent one?

[MikaelMayer]

Ok, let's postpone it for a subsequent one, perhaps either proactively or if someone hits this issue. It's not a soundness issue anyway, just annoying if it happened, but it's unlikely in practice.