Generation of Java AST classes

[wadoon]

Related Issue

This PR supersedes/continues the discussion from the KaKeY meeting on writing
KeY-Java-AST. No dedicated issue; tracking happens in this PR.

Intended Change

Writing the KeY Java AST by hand is tedious and error-prone (ExtList/ImmutableArray
plumbing, equals+hashCode+computeHashCode for every node). This PR generates the
AST node classes and the necessary visitor infrastructure from a single, small metamodel file
using JavaParser.

• New Gradle module key.ncore.java (settings.gradle: include 'key.ncore.java'):
  • src/adt/java-ast.java — the metamodel (declared style, ~180 types; imports reference
    existing KeY types like KeyType, SchemaVariable, ...)
  • src/generator/java/org/key_project/ncore/java/ — the generator (5 files:
    Generator, PreSteps, NodeSteps, PostSteps, ReadAllHierarchy) and a
    runGenerator Gradle task that regenerates the AST
  • src/generated/java/org/key_project/java/ast/ — the generated output (AST nodes,
    visitor package with Visitor/ArgVisitor/VoidVisitor/CopyVisitor/
    CopyOnWriteVisitor)
  • src/main/java/org/key_project/java/ast/ — small hand-written support types
    (Matchable, Visitable, MatchHelper, Root, EqEx, Internal, ...)
• The generated AST compiles cleanly — ./gradlew :key.ncore.java:classes is
  BUILD SUCCESSFUL with 0 errors. (This was the current iteration's goal; it replaces
  the previous state with ~1250 linker/type errors.)

Java AST features/decisions

• All fields are immutable.
  • Getter in record style, e.g. String name();
  • Lists are ImmutableList from org.key_project.util.collection.
• Inner AST nodes are interfaces.
  • @Root node is the single abstract base class JavaSourceElement
    (implements Visitable, Matchable); everything else is a (sealed) interface or a
    concrete final class.
• Inner AST nodes are sealed for pattern matching support. Marker types without any
  metamodel subtype (e.g. IGuard, LoopInitializer, IExecutionContext) are generated as
  plain (non-sealed) interfaces.
• Type-safe builder for each node (node.builder()...build(), plus withXyz setters).
• equals/hashCode/toString and structural match(...) are generated.
• Visitors: Visitor<R> (with return value), VoidVisitor, visitor with default methods,
  ArgVisitor<R, A>, CopyVisitor and CopyOnWriteVisitor (structural copy,
  identity-preserving copy-on-write).
• The metamodel's implements clauses on abstract types are preserved (merged into the
  extends clause of the generated sealed interfaces, since interfaces cannot have
  implements); concrete classes derive their implemented interfaces from the metamodel
  hierarchy.

Plan

• AST generation pipeline (metamodel → generated classes + visitors) working
• Generated AST compiles (:key.ncore.java:classes, 0 errors)
• Metamodel fixes: missing type declarations, sealed-hierarchy/orphan handling,
  faithfulness to the hand-written AST, dead code removal
• Generator bug fixes reviewed and covered by tests
• Add key.ncore.java to the CI test matrix in .github/workflows/tests.yml
• Migrate de.uka.ilkd.key.java.ast usages onto the generated AST (follow-up, e.g. a
  key.core.java module feeding the same metamodel)
• Code cleanup
• Document the changes (incl. the metamodel format for contributors)
• Final KaKeY discussion on remaining design aspects

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code
• There are changes to the deployment/CI infrastructure (gradle, github, ...)

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 have tested the feature as follows: ./gradlew :key.ncore.java:runGenerator and
  ./gradlew :key.ncore.java:classes succeed; generated code compiles with 0 errors.
• I have checked that runtime performance has not deteriorated (no hot paths affected yet;
  the generated AST is not yet wired into the prover).

Additional information and contact(s)

This is a DRAFT; the branch is weigl/javaastgen. The metamodel is the single source of
truth and is also intended to feed the planned key.core.java module (generator + support
classes get copied there once the ncore variant is stable).

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