flux-rs / flux

Refinement Types for Rust
MIT License
632 stars 17 forks source link

Allow refining `Self` #589

Closed ranjitjhala closed 8 months ago

ranjitjhala commented 8 months ago

Updates the Generics type to include Self as base for trait, so the following now works:

#[flux::generics(Self as base)]
pub trait MyTrait {
    #[flux::sig(fn<refine p: Self -> bool>(&Self{v: p(v)}) -> Self{v: p(v)})]
    fn foo(&self) -> Self;
}

#[flux::sig(fn<T as base, refine q: T -> bool> (&T{v:q(v)}) -> T{v: q(v)})]
pub fn bar<T: MyTrait>(x: &T) -> T {
    x.foo()
}
ranjitjhala commented 8 months ago

@nilehmann I think I've addressed the issues would be good to take a look

nilehmann commented 8 months ago

I'm going to merge this myself because I have some big changes that are going to conflict.

ranjitjhala commented 8 months ago

thanks!