small fixes to datatype handling

[mattulbrich]

Related Issue

#3662 Parsing problem in \datatypes with no 'self' selectors

Intended Change

Small changes in data type treatment:

• error messaging improved
• consistent naming scheme
• corrected EQ taclet in correct order (a=b became b=a at one point)
• fixed bug in the Axiom taclet for datatypes which crashed KeY while loading.
• added generated deconstructor rules to "simplify" ruleset

Plan

Small fixes: done.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• Refactoring (behaviour should not change or only minimally change)
• There are changes to the (Java) code
• There are changes to the taclet rule base [only to taclets created at load time for datatype declarations]

Ensuring quality

• Pair programming
• I added new test case(s) for new functionality. Manually.

Additional information and contact(s)

Co-authored by @WolframPfeifer

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

[codecov]

Codecov Report

❌ Patch coverage is 81.48148% with 5 lines in your changes missing coverage. Please review.
✅ Project coverage is 47.03%. Comparing base (28025d8) to head (b425891).
⚠️ Report is 23 commits behind head on main.

Files with missing lines	Patch %	Lines
.../key/nparser/builder/FunctionPredicateBuilder.java	42.85%	2 Missing and 2 partials ⚠️
.../uka/ilkd/key/proof/mgt/RuleJustificationInfo.java	0.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3661      +/-   ##
============================================
- Coverage     47.16%   47.03%   -0.14%     
+ Complexity    15801    15790      -11     
============================================
  Files          1673     1675       +2     
  Lines         96171    96341     +170     
  Branches      15397    15434      +37     
============================================
- Hits          45359    45312      -47     
- Misses        45641    45866     +225     
+ Partials       5171     5163       -8     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[wadoon]

The description says that tests were added, but in the diff, I cannot spot new test cases.

[Drodt]

Looks good, but I agree with @wadoon that a new test case would be good.

[WolframPfeifer]

There are build errors which prevent the PR from being merged. It seems to be related to SSL/TLS, and seems to appear in random phases of the build. Two examples:

Run keyproject/setup-smt@v0
read ECONNRESET
Waiting 19 seconds before trying again
read ECONNRESET
Waiting 13 seconds before trying again
node:internal/process/promises:391
    triggerUncaughtException(err, true /* fromPromise */);
    ^

Error: read ECONNRESET
    at TLSWrap.onStreamRead (node:internal/stream_base_commons:218:20) {
  errno: -4077,
  code: 'ECONNRESET',
  syscall: 'read'
}

Execution failed for task ':key.util:compileTestJava'.
> Could not resolve all files for configuration ':key.util:testCompileClasspath'.
   > Could not resolve org.junit:junit-bom:5.13.4.
     Required by:
         project ':key.util'
      > Could not resolve org.junit:junit-bom:5.13.4.
         > Could not get resource 'https://repo.maven.apache.org/maven2/org/junit/junit-bom/5.13.4/junit-bom-5.13.4.pom'.
            > Could not GET 'https://repo.maven.apache.org/maven2/org/junit/junit-bom/5.13.4/junit-bom-5.13.4.pom'.
               > Got socket exception during request. It might be caused by SSL misconfiguration
                  > Connection reset
   > Could not find org.junit.jupiter:junit-jupiter-api:.
     Required by:
         project ':key.util'
   > Could not find org.junit.jupiter:junit-jupiter-params:.
     Required by:
         project ':key.util'

Does anybody have an idea what is happening here?

[mattulbrich]

Does anybody have an idea what is happening here?

Sometimes random tasks fail at the moment. This happens on other PRs as well. On #3664 I was able to rerun individual tests that failed, and they then succeeded. But this cannot be done for the merge step I assume. And this other PR can also not be merged.