epfl-lara / rust-stainless

An experimental Rust frontend for Stainless
Apache License 2.0
6 stars 2 forks source link

Support trait bounds on regular impls #81

Closed yannbolliger closed 3 years ago

yannbolliger commented 3 years ago

Regular impls are not extracted as classes. However, their trait bounds need to be handled. How?

Example:

trait Equals { fn eq(&self, other: &Self) -> bool; }

impl<T: Equals> List<T> {
    fn contains(&self, x: &T) -> bool {
        match self {
            List::Cons(y, tail) => x.eq(y) || tail.contains(x),
            _ => false,
        }
    }
}

Here, the list is not extracted as type class but as an ADT. Therefore, the trait bound induced evidence argument likely has to go on the function itself.

def contains(self: List[T], x: T)(ev0: Equals[T])?