Add Polymorphic Sorts and Functions

[Drodt]

Related Issue

Based on #3384. Thanks, @mattulbrich @wadoon

Intended Change

Adds polymorphic sorts as proposed by Ulbrich and Weigl and adds polymorphic functions as an obvious extension. This PR also adds matching logic, which has been tested in RustyKeY and JavaKeY.

The syntax is very verbose right now. Generic parameters are written as <[E1, E2, E3]>. As an example, see polymorphic sequences:

\sorts {
    \generic E;
    PSeq<[E]>;
}

\functions {
    // getters
    E pseqGet<[E]>(PSeq<[E]>, int);
}

In the future, the syntax may be simplified and parameters may be partially inferred.

Additionally, polymorphic datatypes are supported:

\datatypes {
	List<[E]> = Nil | Cons(E head, List<[E]> tail);
}

The taclet generation for data types is changed accordingly.

To allow for taclets where an input is required (e.g., induction over List<[int]>), we had to modify the input for terms and instantiations in proof files to allow sort specification, i.e., x:List<[int]>. Consequently, the sort is also now emitted for all instantiations in all proof files.

Plan

• Test changes
• Documentation
• Remove SortDependingFunction? (Also simplifies grammar!) (Future work)
• Make sequences, sets, etc. polymorphic? (Future work)

Type of pull request

• 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

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.

[Drodt]

I added an example with polymorphic sequences (based on heap/simple/seq.key) and completed the proof. That should show that the matching logic works

[Drodt]

Hmm, the slicing tests fail due to a parser error, seemingly in sliced proof files. @WolframPfeifer do you interact at all with the inst tags in the saved proof?

[Drodt]

I tested some of the runAllProofs tests that fail on the CI. They work on my machine. I don't know what the issue is

[Drodt]

All tests pass now. This PR is ready for review.