Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Erase PartialEq::eq to Stainless equality #137

Open
yannbolliger opened this issue Apr 15, 2021 · 0 comments
Open

Erase PartialEq::eq to Stainless equality #137

yannbolliger opened this issue Apr 15, 2021 · 0 comments
Labels
enhancement Improvement to an existing feature extraction Feature or bug with the extraction phase

Comments

@yannbolliger
Copy link
Collaborator

yannbolliger commented Apr 15, 2021

This is a related problem to #136.

Contrary to Scala, Rust does not have an equality operation on all types by default. Comparison operators are only defined on primitive types, for all other types, the == operator is desugared to std::cmp::PartialEq::eq. Most types provide a #[derive(PartialEq)] implementation that performs structural comparison.

This poses a problem for Stainless, where Scala-like structural equality exists on all types. In order to deal with the trait method, the frontend needs to extract the implementations of PartialEq with the type class mechanism. This is not only costly but also forces users to provide an actual implementation for equality that Stainless can extract and understand.

To make this more pleasant to use and more efficient, the idea is to replace calls to std::cmp::PartialEq::eq directly by Stainless ==. This is only correct under the assumption that the PartialEq implementation has been derived. Hence, the frontend needs to check for this.

The same problem with generic functions as in #136 arises.

@yannbolliger yannbolliger added enhancement Improvement to an existing feature extraction Feature or bug with the extraction phase labels Apr 15, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement Improvement to an existing feature extraction Feature or bug with the extraction phase
Projects
None yet
Development

No branches or pull requests

1 participant