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.

[WolframPfeifer]

I am trying to use the feature from this PR to implement a polymorphic theory of sets. How can I instantiate the generic sort with a concrete one?

I declared sets like this (internally in the rules shipped with KeY, because of \generic):

\sorts {
    /*! @defaultValue(sEmpty) */
    \generic T;
    Set<[T]>;
}

\functions {
    \unique Set<[T]> sEmpty;

    // other constructors
    Set<[T]> sSingleton(T);
    Set<[T]> sIntersect(Set<[T]>, Set<[T]>);
}

\predicates {
    sElementOf(T, Set<[T]>);
}

\rules { ... }

Then, I tried to load a problem:

\problem {
\forall Set<[int]> s1; (\forall Set<[int]> s2;
       (sIntersect(s1, s2) = sEmpty <-> \forall int a; (sElementOf(a, s1) -> !sElementOf(a, s2))))
}

The definitions and rules seem to load correctly. However, when trying to load the problem, I get this exception:

Could not build term on: sIntersect(s1,s2) at .../setExample.key:4:9  Caused by: org.key_project.logic.TermCreationException: Building a term failed. Normally there is an arity mismatch or one of the subterms' sorts is not compatible (e.g. like the '2' in "true & 2") The top level operator was sIntersect(Sort: Set<[T]>); its expected arg sorts were: 1.) sort: Set<[T]>, sort hash: 1030768850
2.) sort: Set<[T]>, sort hash: 1030768850

The subterms were:
1.) s1(sort: Set<[int]>, sort hash: 329215882)
2.) s2(sort: Set<[int]>, sort hash: 329215882) 

@Drodt What am I doing wrong? How does instantiation of a polymorphic sort work?

[Drodt]

@Drodt What am I doing wrong? How does instantiation of a polymorphic sort work?

The problem is that sEmpty, sSingleton, and sIntersect are not polymorphic functions; they are regular functions that happen to have a (partially) generic return sort.

The definitions should be:

   \unique Set<[T]> sEmpty<[T]>;

    // other constructors
    Set<[T]> sSingleton<[T]>(T);
    Set<[T]> sIntersect<[T]>(Set<[T]>, Set<[T]>);

Right now, we need this verbose syntax for KeY to know that these functions are parametric.

It is unclear, however, that what you wrote is an error. Perhaps one really wants to define such functions.

[mattulbrich]

It is unclear, however, that what you wrote is an error. Perhaps one really wants to define such functions.

Since T is a generic type, I would argue that Set<[T]> would be a bad toplevel type reference

I agree that sEmpty profits from an explicit type argument. [Relieves us from having to do type inference and with subtyping that can also be challenging, esp. if we do not necessarily have a lattice.]

I would argue that sSingleton can go without the type argument if the static type of the first argument is meant.
But that is some kind of pretty printing then. I would assume.

[Drodt]

Since T is a generic type, I would argue that Set<[T]> would be a bad toplevel type reference

Do we currently prohibit a function with a generic return sort? If so, I can add a check for the parametric case.

I would argue that sSingleton can go without the type argument if the static type of the first argument is meant. But that is some kind of pretty printing then. I would assume.

This very primitive type inference is something we can add later on. I would suggest after #3773, which kind of validates the parametric function approach.

[WolframPfeifer]

The problem is that sEmpty, sSingleton, and sIntersect are not polymorphic functions; they are regular functions that happen to have a (partially) generic return sort.

Ah, of course 🤦! Thanks for the explanation (and also the work to implement this nice and long-desired feature)!

I implemented a basic theory of polymorphic sets in #3777 now. However, one question remains: At the moment, polymorphic types are unusable in JML, right? Do you have an idea what needs to be done there?

[WolframPfeifer]

This very primitive type inference is something we can add later on. I would suggest after #3773, which kind of validates the parametric function approach.

I think the verbosity is not a problem. It is similar to other tools (e.g. VeriFast), and in my opinion inherent with parametric types. But I agree that some primitive inference would be nice here.

However, two following points that came to my mind:

• With the current treatment of sorts with \generic (they are erased from the namespaces after loading the internal .key files, right?), it is not possible to have a user-defined problem with a parametric sort. I.e., you cannot prove a property generically, but have to instantiate the generic sort with a concrete one, as far as I understand. In particular, this means that it is not possible to add user-defined rules for polymorphic sorts, right?
• An idea for a future feature: In Java, class List<T> "automatically" declares the generic sort T, similar in VeriFast: //@ predicate p<T>(T t, ...). Maybe we could have something similar in the future ...

[Drodt]

Ah, of course 🤦! Thanks for the explanation (and also the work to implement this nice and long-desired feature)!

Thanks for using it :)

I implemented a basic theory of polymorphic sets in #3777 now. However, one question remains: At the moment, polymorphic types are unusable in JML, right? Do you have an idea what needs to be done there?

I'm not sure how sort integration into JML works at the moment in general. It should be possible to use the Java generic syntax on DL functions (i.e., \dl_sSingleton<int>(0)) and similarly for any parametric sorts in the "standard library" of KeY. The question there is more: Should we do this now or wait for the JavaJMLParser? How far off, roughly, is the latter @wadoon?

[Drodt]

* With the current treatment of sorts with `\generic` (they are erased from the namespaces after loading the internal .key files, right?), it is not possible to have a user-defined problem with a parametric sort. I.e., you cannot prove a property generically, but have to instantiate the generic sort with a concrete one, as far as I understand. In particular, this means that it is not possible to add user-defined rules for polymorphic sorts, right?

Not sure if I understand exactly what you mean but generic sorts are fine in taclets, even in parametric sorts and functions. See the examples I added in this PR.

* An idea for a future feature: In Java, `class List<T>` "automatically" declares the generic sort `T`, similar in VeriFast: `//@ predicate p<T>(T t, ...)`. Maybe we could have something similar in the future ...

That's exactly what I do in RustyKeY 😄. I did not do this here because (1) it was not part of @mattulbrich's origina design and (2) then we need a new syntax for \extends of generic parameters. We can definitely do it. Let's discuss at the next KeY meeting.

[WolframPfeifer]

Not sure if I understand exactly what you mean but generic sorts are fine in taclets, even in parametric sorts and functions. See the examples I added in this PR.

Yes, I have seen these. But these are not user files, right? That is, if you try to load them in the KeY GUI, you get an exception (Sth like "Generic sort not allowed"), because the generic sorts have been removed already. So it is not possible to have a \problem block that refers to a polymorphic sort (only to concrete instances), and likewise with a \rules block in a user file. That is what I mean by adding rules later.