KeYProject
Add Polymorphic Sorts and Functions
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
- [x] Test changes
- [x] 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.
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
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?
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