[DRAFT] Do not generate import of modules in Java

[olivier-aws]

What was changed?

This change updates the Java code generated from Dafny to remove
import Module.*;
commands. These imports were useless as the generated code emits fully qualified names for each class and create bad Java code when the package and class names are the same. On the example for dafny-lang#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)

// Class A
// Dafny class A compiled into Java
package A;

public class A {
  public A () {
  }

// [...]

  private static final A theDefault = A.A.create();
  public static A Default() {
    return theDefault;
  }
  public static A create() {
    return new A();
  }
  public static A create_Foo() {
    return create();
  }
  public boolean is_Foo() { return true; }
  public static java.util.ArrayList<A> AllSingletonConstructors() {
    java.util.ArrayList<A> singleton_iterator = new java.util.ArrayList<>();
    singleton_iterator.add(new A());
    return singleton_iterator;
  }
}

// Class __default
// Dafny class __default compiled into Java
package B;

import A.*;

public class __default {
  public __default() {
  }
  public static void __Main(dafny.DafnySequence<? extends dafny.DafnySequence<? extends dafny.CodePoint>> args) {
    __default.Main(args);
  }
  public static A.A bar()
  {
    return A.A.Default();
  }
}

The expression A.A.Default does not compile in Java, as the first A. is resolved to be the name of the class and not the name of the package, because of the import A.*; upfront. Also, in file A.java, the expression A.A.create(); does not compile because it is within the class A already.

This change modifies the Java generation to remove the import statements and ensure that the correct fully qualified name is used everywhere.

How has this been tested?

Added a testcase: IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy

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