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.
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 tostd::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
PartialEqwith 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::eqdirectly by Stainless==. This is only correct under the assumption that thePartialEqimplementation has been derived. Hence, the frontend needs to check for this.The same problem with generic functions as in #136 arises.