Associated Predicates

[ranjitjhala]

Here's a starting point, I still need to implement a bunch of checks, namely: checking the sort of the impl-pred against the trait spec, but the below works now, which should be good to make progress on Vec.

In fact, I am tempted to merge this and move onto the Vec stuff first, because in this "fast-and-loose" version, we can make some progress without associating the predicates with the trait but directly with the impl.

// Step 1 : declare -------------------------------
#[flux::generics(Self as base)]
#[flux::predicate{ f : (Self) -> bool }]
pub trait MyTrait {
    fn method(&self) -> i32;
}

// Step 2 : implement -----------------------------
#[flux::predicate{ f : |x:int| { 0 < x } }] // TODO: check against trait-def
impl MyTrait for i32 {
    fn method(&self) -> i32 {
        10
    }
}

// Step 3 : abstract ------------------------------
#[flux::trusted] // TODO: subtyping with alias_pred on lhs
#[flux::sig(fn<T as base>(&{T[@x] | <T as MyTrait>::f(x)}))] // TODO: check against trait-spec
pub fn bob<T: MyTrait>(x: &T) {
    x.method();
}

// Step 4 : concretize ----------------------------
pub fn test() {
    let z0 = 0;
    bob(&z0); //~ ERROR refinement type
    let z1 = 1;
    bob(&z1);
}

[ranjitjhala]

Ok I think I addressed all the comments -- except the checking-signatures ("making the following definition work without trusting") -- which I presumed you meant separate from the comments; have factored that into a separate issue and I'll work on it next, thanks!