# Example for typing rules v2

## Example in rust

#[flux::sig(fn(bool) -> i32{v : v >= 0})]
fn ref_join(b: bool) -> i32 {
    let mut x = 1;
    let mut y = 2;
    let r = if b {
        &mut x
    } else {
        &mut y
    };
    decr(r);
    x
}

#[flux::sig(fn(&mut i32{v : v >= 0}))]
fn decr(r: &mut i32);

## Lambda_flux

let ref_join = rec f〈a0〉(b) :=
    let x = new(ρx) in
    let y = new(ρy) in
    x := 1;
    y := 2;
    let r = if b {
        &mut x
    } else {
        &mut y
    } in
    call decr(r);
    *x


decr : fn(&mut i32{v : v >= 0}) -> ↯

## Typechecking
Comments show the state of the checker _after_ the statement

let ref_join = rec f〈a0〉(b) := // t-fun with type ∀a0:bool. fn(bool〈a0〉) -> i32{v : v ≥ 0}
    // Δ := a0:bool
    // T := ∅
    // Γ := b:bool〈a0〉   // technically Γ also contains f: ∀a0:bool. fn(bool〈a0〉) -> i32{v : v ≥ 0}, which I'm going to omit...

    let x = new(ρx) in  // t-new
      // a0:bool, ρx:loc
      // ρx↦↯
      // b:bool〈a0〉, x:ptr(ρx)

    let y = new(ρy) in // t-new
      // a0:bool, ρx:loc, ρy:loc                  
      // ρx↦↯, ρy↦↯
      // b:bool〈a0〉, x:ptr(ρx), y:ptr(ρy)                   

    x := 1; // t-assign-strg
      // a0:bool, ρx:loc, ρy:loc 
      // ρx↦i32〈1〉, ρy↦↯
      // b:bool〈a0〉, x:ptr(ρx), y:ptr(ρy)

    y := 2; // t-assign-strg            
      // a0:bool, ρx:loc, ρy:loc 
      // ρx → i32〈1〉, ρy → i32〈2〉
      // b:bool〈a0〉, x:ptr(ρx), y:ptr(ρy)                    

    let r = if b { // t-if
      // a0:bool, ρx:loc, ρy:loc, a0 
      // ρx → i32〈1〉, ρy → i32〈2〉
      // b:bool〈a0〉, x:ptr(ρx), y:ptr(ρy)  

        &mut x // t-strg-mut-rebor
          // a0:bool, ρx:loc, ρy:loc, a0 
          // ρx↦{v. i32〈v〉 | v ≥ 0}, ρy↦i32〈2〉
          // b:bool〈a0〉, x:ptr(ρx), y:ptr(ρy)
          // 
          // ρx:loc, ρy:loc ⊢ i32〈1〉 <: {v. i32〈v〉 | v ≥ 0}
    } else { // t-if
      // a0:bool, ρx:loc, ρy:loc, ~a0 
      // ρx → i32〈1〉, ρy → i32〈2〉
      // b:bool〈a0〉, x:ptr(ρx), y:ptr(ρy)    
        
        &mut y  // t-strg-mut-rebor       
           // a0:bool, ρx:loc, ρy:loc, ~a0             
           // ρx↦i32〈1〉, ρy↦{v. i32〈v〉 | v ≥ 0}
           // b:bool〈a0〉, x:ptr(ρx), y:ptr(ρy)             
           //
           // a0: bool, ρx:loc, ρy:loc ⊢ i32〈2〉 <: {v. i32〈v〉 | v ≥ 0}             
    } in // t-if + t-let
      // a0:bool, ρx:loc, ρy:loc                
      // b:bool〈a0〉, ρx↦{v. i32〈v〉 | v ≥ 0}, ρy↦{v. i32〈v〉 | v ≥ 0}
      // x:ptr(ρx), y:ptr(ρy), r:&mut {v. i32〈v〉 | v ≥ 0}

    call decr(r); // t-call
      // a0:bool, ρx:loc, ρy:loc                
      // b:bool〈a0〉, ρx↦{v. i32〈v〉 | v ≥ 0}, ρy↦{v. i32〈v〉 | v ≥ 0}
      // x:ptr(ρx), y:ptr(ρy), r:&mut {v. i32〈v〉 | v ≥ 0}
      //
      // arg subtyping:
      //   a0:bool, ρx:loc, ρy:loc ⊢ &mut {v. i32〈v〉 | v ≥ 0} <: &mut {v. i32〈v〉 | v ≥ 0}

    *x // t-deref-strg + t-fun
      //
      // return type:
      //   a0: bool, ρx:loc, ρy:loc, a1:int, a1 ≥ 0 ⊢ {v. i32〈v〉 | v ≥ 0} <: i32{v. i32〈v〉 | v ≥ 0}

let init_zeros = rec f<a0>(n) :=
  let x = new(ρx) in
  let vec = new(ρv) in
  x := 0;
  vec := Vec<f32>::new();
  let k = rec k<a, b>() :=
    if i < n {
        Vec::push<ρv,b>(vec, 0);
        i := *i + 1;
        call k<a+1, b+1>()
    } else {
        *vec
    } 
  in
  call k<0, 0>()
}