flux-rs / flux

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

Add support for `extern_spec` for `enum` #586

Closed ranjitjhala closed 8 months ago

ranjitjhala commented 8 months ago

The following now works

#[extern_spec]
#[flux::refined_by(b:bool)]
enum Option<T> {
    #[flux::variant(Option<T>[false])]
    None,
    #[flux::variant({T} -> Option<T>[true])]
    Some(T),
}

#[flux::sig(fn(x:Option<T>[true]) -> T)]
pub fn my_unwrap<T>(x: Option<T>) -> T {
    match x {
        Option::Some(v) => v,
        Option::None => never(0),
    }
}

pub fn test3() {
    let x = Option::Some(42);
    let y = my_unwrap(x);
    assert(y == 42);
}