Generation of Java AST classes

[wadoon]

Intended Change

As discussed in KaKeY meeting, writing KeY-Java-AST is a bit hassly, e.g., ExtList stuff, equals + hashCode + computeHashcode. This PR generates the AST and necessary Visitor classes on the basis of the Java file java-ast.java using our JavaParser.

Java AST features/decisions

• All fields are immutable
  • Getter in record style, e.g., String name();
  • Lists are RoList an abstraction of ImmutableArray allowing for more special cases like (emptiness, and singleton).
• Inner AST nodes are all interfaces. Allows more flexibility and recursive equals, cf. Kotlin data class
• Inner AST nodes are sealed for Pattern matching support
• Type-safe builder for each node
• Equals, HashCode, and ToString generated implementations
• Visitors
  • Visitor with return value
  • VoidVisitor w/o return value
  • Visitor with default method and return type
  • ArgVisitor with return type and an additional argument
  • CopyVisitor, which automatically goes down, constructing new AST nodes.
  • CopyOnWriteVisitor, which automatically goes down, constructing new AST nodes, if something was updated.

• Discussion
• Document the changes

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• Refactoring (behaviour should not change or only minimally change)
• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to change)
• There are changes to the (Java) code
• There are changes to the taclet rule base
• There are changes to the deployment/CI infrastructure (gradle, github, ...)
• Other:

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: ...
• I have checked that runtime performance has not deteriorated.
• For new Gradle modules: I added the Gradle module to the test matrix in
  .github/workflows/tests.yml

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.