To clone a type in Rust, it must have an implementation of std::clone::Clone, which is usually derived from a macro. The derived implementation recursively clones the fields of a type. So, by default, the clone operation preserves equality. However, that is impossible for Stainless to understand because the behaviour is provided by two different type classes (Clone and PartialEq) that have no type or parameter dependency.
As a first step to deal with the problem, this PR proposes to erase:
all calls to Clone::clone with identity, and
all impl std::clone::Clone for X blocks, because they are no longer called.
To do
[x] Should also erase evidence arguments for Clone instances.
This allows progress on some benchmarks but is not sound in all cases. Details can be found in #136.
To clone a type in Rust, it must have an implementation of
std::clone::Clone, which is usually derived from a macro. The derived implementation recursively clones the fields of a type. So, by default, the clone operation preserves equality. However, that is impossible for Stainless to understand because the behaviour is provided by two different type classes (CloneandPartialEq) that have no type or parameter dependency.As a first step to deal with the problem, this PR proposes to erase:
Clone::clonewith identity, andimpl std::clone::Clone for Xblocks, because they are no longer called.To do
This allows progress on some benchmarks but is not sound in all cases. Details can be found in #136.