# Example for typing rules

## Example in rust

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

## Lambda_flux

let foo = reref_join〈a0〉(b) :=
    let x = new(ρx) in
    let y = new(ρy) in
    x := 1;
    y := 2;
    let r = if * {
        &mut x
    } else {
        &mut y
    } in
    let t1 = *r in
    unpack(t1, a1) in
    r := call add〈a1, 1〉(t1, 1);
    *x

add : ∀a:int, b:int. fn(int〈a〉, int〈b〉) -> int〈a + b〉

# Type checking
Comments show the state of the checker _after_ the statement

let foo = reref_join〈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}

    let t1 = *r in // t-deref + 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}, t1:{v. i32〈1〉 | v ≥ 0}                   

    unpack(t1, a1) in  // t-unpack
      // a0:bool, ρx:loc, ρy:loc, a1:int, a1 ≥ 0                   
      // 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}, t1:i32〈a1〉                   

    r := call add〈a1, 1〉(t1, 1);  // t-call + t-assign   
      // a0:bool, ρx:loc, ρy:loc, a1:int, a1 ≥ 0                  
      // ρx↦{v. i32〈v〉 | v ≥ 0}, ρy↦{v. i32〈v〉 | v ≥ 0}
      // b:bool〈a0〉, x:ptr(ρx), y:ptr(ρy), r:&mut {v. i32〈v〉 | v ≥ 0}, t1:i32〈a1〉  
      // 
      // args: 
      //   a0: bool, ρx:loc, ρy:loc, a1:int, a1 ≥ 0 ⊢ i32〈a1〉 <: i32〈a1〉                               
      //   a0: bool, ρx:loc, ρy:loc, a1:int, a1 ≥ 0 ⊢ i32〈1〉 <: i32〈1〉   
      //    
      // assignment: 
      //   a0: bool, ρx:loc, ρy:loc, a1:int, a1 ≥ 0 ⊢ i32〈a1 + 1〉 <: i32{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}

## Alternative syntax for unpack

I've been thinking that we could have a slightly different version of unpack that would make the example shorter, albeit, incresing
cognitive load per line. But this version of `unpack` has a less weird typing rule imo.

e ::= ...
   |  let (x, a) = unpack(e1) in e2 

let foo = rec f(b) :=
    let x = new(ρx) in
    let y = new(ρy) in
    x := 1;
    y := 2;
    let r = if * {
        &mut x
    } else {
        &mut y
    } in
    let t1 = *r in
    let (t2, a1) = unpack(t1) in
    r := call add〈a1, 1〉(t1, 1);
    *x