search

flux-rs / flux

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

WF Checks on Associated Predicates #599

Closed ranjitjhala closed 7 months ago

ranjitjhala commented 7 months ago

PR adds a bunch of WF/desugaring checks on Associated/Alias Predicates, which is a stepping stone to #598

The main technical bit is to

  1. Use the Spec of an AssocPredicate (i.e. the Sort given in the trait), to
  2. Determine the Impl's sort (by substituting the GenericArgs sorts).
ranjitjhala commented 7 months ago

@nilehmann -- I've now added code to also so this PR (almost) fixes #598 -- the one little thing I couldn't figure out is how to get this

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

To work because it wasn't clear how to "collect" the name MyTrait -- the desugar/resolve thing currently barfs on the MyTrait ... I'm guessing this is quite easy?

ranjitjhala commented 7 months ago

Also, keep an eye out for the const_name_gen shenanigans :-)