# Flux Closures

Staring at the MIR it looks like (roughly speaking)

## Representation in MIR

"lambdas" are represented as a package `AggregateKind::Closure`
which looks like the `(fun-id, tuple-over-free-vars)` and
extra type substitutions e.g. for the tyvars map.

For example, source like

pub fn test(c: Option<bool>) -> Option<i32> {
    let mut x = 0;
    let mut y = false;
    c.map(|b| if b { x += 1; x } else { y = true; x })
}

is transformed, roughly, into a representation

// map : Option<T>, 

// pub fn map<T, U, F>(Option<T>, f: F) -> Option<U>
//   where 
//     F: FnOnce(T) -> U,
//
// map : (Option<T>, FnOnce) -> Option<U>

fn test(c: Option<bool>) -> Option<i32> {
                             // env: t_env (fresh)
    let env.0 = &mut x;      //  t_x <: t_env.0
    let env.1 = &mut y;      //  t_y <: t_env.1 
    let clos = CLOSURE( lam_fn, env ); // Fn(t_in) -> t_out
    map<T=t,U=u>(c, clos)        // Fn(t_in) -> T_out
        ==> output type of map with t/u
    Fn(T) -> U
    
    Fn(t') -> u' // fresh template from t, u
    env'         // fresh template from env
    CHECK: lam_fn impl (t', env') -> u' 
    
    ISSUE: have to check TWO fun-body in SAME VC!
    
    
}

// extra 'env' represented via a struct (ish) ..
type env_ty = (&mut i32, &mut bool);

// ... explicitly passed into separate func
fn lam_fn(b: bool, t: test_ty) -> Option<i32> {
    if b {
         let tmp = t.0;
        *tmp = *tmp + 1;
        *tmp
    } else {
        let tmp = t.0;
        *tmp = true;
        *t.0
    })
}

## Approach

1. Generate fresh "templates" (distinct kvar for each refinement)

* free-vars tuple: `t_tuple`
* fun-id-signature: `(t_sig_in) -> t_sig_out`

2. Check `lam_fn` impl `(t_sig_in, t_tuple) -> t_sig_out`
* `check_fn_body`

3. Check `env` impl `t_tuple`

(_5.0: &mut i32) = move _6;     
(_5.1: &i32)     = move _7;

Fn(T) -> U

## MIR

fn test(_1: std::option::Option<bool>) -> std::option::Option<i32> {
    let mut _0: std::option::Option<i32>; 
    let mut _2: i32;                     
    let mut _3: bool;                
    let mut _4: std::option::Option<bool>; 
    let mut _5: [closure@attic/asdf.rs:7:11: 7:14]; 
    let mut _6: &mut i32;                
    let mut _7: &mut bool;               

    bb0: {
        _2 = const 0_i32;                
        _3 = const false;                
        _4 = _1;                         
        _6 = &mut _2;                    
        _7 = &mut _3;                    
        _5 = [closure@attic/asdf.rs:7:11: 7:14] { x: move _6, y: move _7 }; 
        _0 = std::option::Option::<bool>::map::<i32, [closure@attic/asdf.rs:7:11: 7:14]>(move _4, move _5) -> [return: bb1, unwind: bb2]; 
    }

    bb1: {
        return;                         
    }

    bb2 (cleanup): {
        resume;                          
    }
}

### Closure substs

We need to get the closure "fields" (i.e., captured environment) from an `AggregateKind::Closure(did, substs)`

* We can call [`substs.as_closure()`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/list/struct.List.html#method.as_closure) to get a [`ClosureSubsts`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.ClosureSubsts.html)
* Then we can get an iterator over the fields of the struct with [`ClosureSubsts::upvar_tys`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.ClosureSubsts.html#method.upvar_tys)

## Nico's Formulation from Slack

(Nico): I think I know how to interpret the different strategies we discussed

So for the example

fn foo(opt: Option<bool>) -> Option<i32> {
    opt.map(|b| if b { 0 } else { 1 } )
}

This lowers to something like

struct Closure0<A, B> { ... }

fn foo(opt: Option<bool>) -> Option<i32> {
    let closure = Closure0<A = bool, B = i32> { ... };
    map<T=bool, U=i32, F=Closure0>(opt, closure)
}

Note that the struct Closure0 is generic on the type of input (A) and output (B)
We can then instantiate parameters with kvars

struct Closure0<A, B> { ... }

fn foo(opt: Option<bool>) -> Option<i32> {
    let closure = Closure0<A = bool{$k0}, B = i32{$k1}> { ... };
    map<T=bool{$k2}, U=i32{$k3}, F=Closure0>(opt, closure)
}

At the call site we need to prove that Closure0 implements the trait FnOnce(bool{$k2}) -> i32{$k3}. The trick is that we can "generate" an implementation of the trait as we wish

### Option 1

Generate a single implementation at the point we create the closure and then check subtyping. So the implementation is something like

impl FnOnce<bool{$k0}> -> i32{$k1} for Closure0<A=bool{$k0}, B=i32{$k1}> {
    fn call(b: bool{$k0}) -> i32{$k1} {
        if b { 0 } else { 1 }
    }
}

And then we argue that the subtyping constraint fn(bool{$k0}) -> i32{$k1} <: fn(bool{$k2}) -> i32{$k3} implies Closure0<A = bool{$k0}, B = i32{$k1}>: FnOnce(bool{$k2}) -> i32{$k3}.

### Option 2

Generate an implementation at the call site as

impl FnOnce<bool{$k2}> -> i32{$k3} for Closure0<A=bool{$k2}, B=i32{$k3}> {
    fn call(b: bool{$k2}) -> i32{$k3} {
        if b { 0 } else { 1 }
    }
}

This is a bit more sketchy because we are dropping the $k0 and the $k1 , but I think the way to argue it's ok is that we are actually creating a different closure/struct at every use site (edited)

I understand what you mean, we need to recover that

closure(DefId(0:5 ~ closure00[e82c]::test0::{closure#0}), [i32, Binder(FnSig { inputs_and_output: [(bool), i32] }, []), ()], ) implement FnOnce(T) -> U

I just hope this information is not somehow “erased” in the HIR because that will be a real PITA (edited)

https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/ty/context/struct.TyCtxt.html#method.predicates_defined_on
https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/ty/context/struct.TyCtxt.html#method.predicates_of

fn map<T,U,F>(Option<T>, F) -> Option<U>
    where F: FnOnce(T) -> U

forall F, T, U

TRACE: closure_obligs = DefId(2:7540 ~ core[1ad7]::option::{impl#0}::map) with GenericPredicates 
    { parent: Some(DefId(2:7524 ~ core[1ad7]::option::{impl#0})), 
      predicates: [ 
          
          (Binder(~const TraitPredicate(<F as std::ops::FnOnce<(T,)>>, polarity:Positive), []), 
          
          (Binder(ProjectionPredicate(AliasTy { substs: [F, (T,)], 
                                                def_id: DefId(2:2923 ~ core[1ad7]::ops::function::FnOnce::Output) 
                                              }, 
                                      Term::Ty(U)), []), 
          
          
impl<T> FnOnce<(T, )> for Closure0 { ... }

* To get the id for the traits we can use [`TyCtxt::require_lang_item`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.TyCtxt.html#method.require_lang_item)

### Closure Body Surgery

1. MAKE body accessible to CHECKER

-- flux-driver::callbacks.rs
let mir = unsafe { mir_storage::retrieve_mir_body(self.genv.tcx, def_id).body };

specifically the WHOLE module `mir_storage` module including `retrieve_mir_body`

should move to flux-middle (so its accessible to the flux-refineck / checker)

closure-impl (clos9)

fn clos9(b) { if b { 1 } else { 2 } }

closure-client (test0)

pub fn test0(c: Option<bool>) -> Option<i32> {
    c.map(... clos9 ...)
}

When REFINE-PHASE in `test0` (i.e. client) have we ALREADY completed the SHAPE-PHASE for

1. ALL functions ?

2. For `clos9` ?

See the below -- must be updated/extended to work for a top-level "client" + all the closure-impl that it uses.

pub struct Inference<'a> {
bb_envs: &'a mut FxHashMap<BasicBlock, TypeEnvInfer>,
}

pub struct Check<'a> {
bb_envs: FxHashMap<BasicBlock, BasicBlockEnv>,
kvars: &'a mut KVarStore,
}

fn foo(x:i32[n]) -> Opt<i32[n+5]> {
    let z = Some(5);
    
    z.map(|val| {val + x});
    z
}

fn clos(val:i32, cap_x:i32) {
    val + cap_x
} 

id :: a -> a;


let x = id;

fn foo(x:i32[n]) -> Opt<i32[n+5]> {
    let z = Some(5);
    
    let closure = Closure { cap_x: x } ///
    ...
    
    // check_call 
    z.map(closure); // rcx: n: int, ...., 
    // check_call 
    
    
    z.map(closure);
}

fn clos(val:i32, closure: Closure) {
    val + closure.cap_x
}