Avoid java compilation error when user code defines Get in a codatatype

Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs

@@ -50,6 +50,10 @@ public JavaCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(op
     const string DafnyMultiArrayClassPrefix = "dafny.Array";
     const string DafnyTupleClassPrefix = "dafny.Tuple";
 
+    // Reserved name for Get method in co-datatypes. Starts with _ to avoid name clash
+    // with user-defined method
+    const string CoDatatypeGet = "_Get";
+
     string DafnyMultiArrayClass(int dim) => DafnyMultiArrayClassPrefix + dim;
     string DafnyTupleClass(int size) => DafnyTupleClassPrefix + size;
 
@@ -1995,7 +1999,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
         }
       }
       if (dt is CoDatatypeDecl) {
-        wr.WriteLine($"public abstract {DtT_protected} Get();");
+        wr.WriteLine($"public abstract {DtT_protected} {CoDatatypeGet}();");
       }
       if (dt.HasFinitePossibleValues) {
         Contract.Assert(dt.TypeArgs.Count == 0);
@@ -2029,7 +2033,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
           if (dt.IsRecordType) {
             wDtor.WriteLine($"return this.{FieldName(arg, 0)};");
           } else {
-            wDtor.WriteLine("{0} d = this{1};", DtT_protected, dt is CoDatatypeDecl ? ".Get()" : "");
+            wDtor.WriteLine("{0} d = this{1};", DtT_protected, dt is CoDatatypeDecl ? "." + CoDatatypeGet + "()" : "");
             var compiledConstructorsProcessed = 0;
             for (var i = 0; i < dtor.EnclosingCtors.Count; i++) {
               var ctor_i = dtor.EnclosingCtors[i];
@@ -2095,8 +2099,8 @@ void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx) {
         var wCtorBody = w.NewBlock($"public {dt.GetCompileName(Options)}__Lazy({wCtorParams}{sep}Computer c)");
         wCtorBody.WriteLine($"super({wBaseCallArguments});");
         wCtorBody.WriteLine("this.c = c;");
-        w.WriteLine($"public {dt.GetCompileName(Options)}{typeParams} Get() {{ if (c != null) {{ d = c.run(); c = null; }} return d; }}");
-        w.WriteLine("public String toString() { return Get().toString(); }");
+        w.WriteLine($"public {dt.GetCompileName(Options)}{typeParams} {CoDatatypeGet}() {{ if (c != null) {{ d = c.run(); c = null; }} return d; }}");
+        w.WriteLine("public String toString() { return " + CoDatatypeGet + "().toString(); }");
       }
     }
 
@@ -2137,7 +2141,7 @@ void DatatypeFieldsAndConstructor(DatatypeCtor ctor, int constructorIndex, Concr
       }
       if (dt is CoDatatypeDecl) {
         string typeParams = TypeParameters(dt.TypeArgs);
-        wr.WriteLine($"public {dt.GetCompileName(Options)}{typeParams} Get() {{ return this; }}");
+        wr.WriteLine($"public {dt.GetCompileName(Options)}{typeParams} {CoDatatypeGet}() {{ return this; }}");
       }
       // Equals method
       wr.WriteLine();
@@ -3352,7 +3356,7 @@ protected override void EmitDestructor(Action<ConcreteSyntaxTree> source, Formal
       }
       wr.Write("(({0})", DtCtorName(ctor, getTypeArgs(), wr));
       source(wr);
-      wr.Write("{0}).{1}", ctor.EnclosingDatatype is CoDatatypeDecl ? ".Get()" : "", dtorName);
+      wr.Write("{0}).{1}", ctor.EnclosingDatatype is CoDatatypeDecl ? "." + CoDatatypeGet + "()" : "", dtorName);
     }
 
     private void CreateLambdaFunctionInterface(int i, ConcreteSyntaxTree outputWr) {

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

@@ -0,0 +1,12 @@
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" 
+
+codatatype NameclashCo = CoCtor(x: int)
+{
+  method Get() returns (u: int) { return 79; }
+}
+
+
+method Main() {
+    print "Hello!\n";
+}
+

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

@@ -0,0 +1 @@
+Hello!

docs/news/fix.4153

@@ -0,0 +1 @@
+Avoid name clashes when compiling a codatatype with a Get method in Java