# Constriant vs Index

#[qualifiers(MyQ1)]
#[sig(fn(&mut {RVec<Particle>[@len] | 1 <= len}))]
pub fn simulation(vec: &mut RVec<Particle>) {
    let n = vec.len();
    let mut i = 0;
    while i < n {
        let mut j = i + 1;
        let mut idx = VecBorrows::new(vec);
        assert(1 + 1 + 1 == 3);
        let a = idx.gett(i);
        while j < n {
            let b = idx.gett(j);
            a.collision(b);
            j += 1;
        }
        i += 1;
    }
}

## Constraint generic

// get: forall av. fn(MultiIdx[p], idx: isize{av(idx)}) -> &T
// ensures MultiIdx[|k| av(k) && k != idx]

let idx = MultiIdx::new(...)      
// idx: MultiIdx[|k| true]
idx.get(i); // (1)
// idx: MultiIdx[|k| $k0(k)[i, n] && k != i]
simulation_step(idx, i, i + 1, n) // (2)
pub fn simulation_step(
    mut idx: MultiIdx[|k| $k1(k)[j, i, n]], 
    i: usize,
    j: usize, 
    n: usize
)  {
    if j >= n {
        return;
    }
    let b = idx.get(j); // (3)
    // idx: MultiIdx[|k| $k2(k)[j, i, n] && k != j]
    simulation_step(idx, a, j + 1, n); // (4)
}

pub fn sim_step(
    mut idx: MultiIdx[@av], 
    i: usize,
    j: usize, 
    n: usize,
) 
    requires forall k. j <= k => av(k)
{ 
   if j >= n {
        return;
    }
    
    // idx: MultiIdx[|k| av(k)]        ALSO NEED av(j'), forall j <= j'
    let b = idx.get(j); 
    
    // idx: MultiIdx[|k| av(k) && k != j]
    sim_step(idx, a, j + 1, n);   
}

fn get<av: int -> bool>(self: &strg Self[av], idx: usize{ av(idx) }) -> &'a mut T 
   ensures self: Self[|i| av(i) && i != idx];



fn getI(self: &strg Self[@av], idx: usize{ av(idx) }) -> &'a mut T 
   ensures self: Self[|i| av(i) && i != idx];


fn sim_base(
)
{
    let i = ...;
    let n = ...;
    let idx = MultiIdx::new(...);
    // idx: MultiIdx[|k| true]
    let _ = idx.getI(i);
    // idx: MultiIdx[|k| true && k != i]
    sim_step(idx, i, i + 1, n)
    // forall k. k != i <=/=> i + 1 <= k
}

pub fn sim_step(
    mut idx: MultiIdx[|k| j <= k], 
    i: usize,
    j: usize, 
    n: usize,
) 
{ 
   if j >= n {
        return;
    }
    
    // idx: MultiIdx[|k| j <= k] 
    let b = idx.get(j); 
    
    // idx: MultiIdx[|k| j <= k && k != j]
    sim_step(idx, a, j + 1, n);   
}

    






// forall i,n.
//   $k0(i)[i, n]                                                  (1)
//   forall k. true <=> $k0(k)[i, n]                               (1)
//   forall k. $k0(k)[i, n] && k != i <=> $k1(k)[i + 1, i, n]      (2)
//   forall j.
//     $k2(j)[j, i, n]                                             (3)
//     forall k. $k1(k)[j, i, n] <=> $k2(k)[j, i, n]               (3)
//     forall k. $k2(k)[j, i, n] && k != j <=> $k1(k)[j + 1, i, n] (4)
//
//   $k0(k)[j, i, n] = $k1(k)[j, i, n] = (0 <= k && k < i) || (j <= k && k < n)

## Index generic (doesn't work)

let idx = MultiIdx::new(...)       
// idx: MultiIdx[|k| true]
idx.get(i); // (1)
// idx: MultiIdx[|k| ?p0(k) && k != i]
simulation_step1(idx, i, i + 1, n) // (2)
pub fn simulation_step(
    mut idx: MultiIdx[?p1], 
    i: usize,
    j: usize, 
    n: usize
) {
    if j >= n {
        return;
    }
    let b = idx.get(j); //(3)
    // idx: MultiIdx[|k| ?p2(k) && k != j]
    simulation_step1(idx, a, j + 1, n); // (4)
}
// forall i,n.
//   ?p0(i)                                (1) 
//   forall k. true <=> ?p0(k)             (1) ?p0 ≡ |k| true
//   forall k. ?p0(k) && k != i <=> ?p1(k) (2) ?p1 ≡ |k| ?p0(k) && k != i
//   ?p2(j)                                (3)
//   forall k. ?p1(k) <=> ?p2(k)           (3) ?p1 ≡ ?p2
//   forall k. ?p2(k) && k != j <=> ?p1(k) (4)

## Generalize

let idx = MultiIdx::new(...)       
// idx: MultiIdx[|k| true]
idx.get(i);
// idx: MultiIdx[|k| true && k != i]
simulation_step1(idx, i + 1) // (1)
pub fn simulation_step(
    // mut idx: MultiIdx[@p], 
    mut idx: MultiIdx[|k| (0 <= k && k < i) || (j <= k && k < n) ], 
    i: usize,
    j: usize, 
    n: usize,
) 
requires forall k. j <= k => p(k)
{
    if j >= n {
        return;
    }
    let b = idx.get(j); // (2)
    // idx: MultiIdx[|k| p(k) && k != j]
    a.collision(b);
    simulation_step1(idx, a, j + 1); // (3)
}




// forall i, n.
//   forall k. i + 1 <= k => k != i            (1)
//   forall p, j.
//     H: (forall k. j <= k => p(k))
//     p(j)                                    (2) by (H j)
//     forall k. j + 1 <= k => p(k) && k != j  (3) by (H k)

## Mixing Constraint and index

struct S[p: int -> bool];


fn negate(s: S[@p]) -> S[|x| !p(x)];

fn constraint_generic<refine p : int -> bool>(x: S) -> S[p];

fn require_true(x: S[|x| true]);

let a = constraint_generic(x); // S[|x| $k(x)]
let b = a.negate(); // S[|x| !$k(x)]
require_true(b); // !k(x) <=> true

## Index generics cannot be flow sensitive

struct S[f: int -> int];

fn add(x: i32) -> S[|y| y + x];

fn foo(b: bool) {
    let s = if b {
        add(2);
    } else {
        add(1);
    };
}