//@ [coq] aeneas-args=-use-fuel
//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
//@ [fstar] aeneas-args=-split-files
//! Exercise the translation of arrays, with features supported by Eurydice

pub enum AB {
    A,
    B,
}

pub fn incr(x: &mut u32) {
    *x += 1;
}

// Nano-tests
// ----------

// The suffix `_` prevents name collisions in some backends
pub fn array_to_shared_slice_<T>(s: &[T; 32]) -> &[T] {
    s
}

// The suffix `_` prevents name collisions in some backends
pub fn array_to_mut_slice_<T>(s: &mut [T; 32]) -> &mut [T] {
    s
}

pub fn array_len<T>(s: [T; 32]) -> usize {
    s.len()
}

pub fn shared_array_len<T>(s: &[T; 32]) -> usize {
    s.len()
}

pub fn shared_slice_len<T>(s: &[T]) -> usize {
    s.len()
}

pub fn index_array_shared<T>(s: &[T; 32], i: usize) -> &T {
    &s[i]
}

// Remark: can't move out of an array
// Also: can't move out of a slice.

pub fn index_array_u32(s: [u32; 32], i: usize) -> u32 {
    s[i]
}

pub fn index_array_copy(x: &[u32; 32]) -> u32 {
    x[0]
}

pub fn index_mut_array<T>(s: &mut [T; 32], i: usize) -> &mut T {
    &mut s[i]
}

pub fn index_slice<T>(s: &[T], i: usize) -> &T {
    &s[i]
}

pub fn index_mut_slice<T>(s: &mut [T], i: usize) -> &mut T {
    &mut s[i]
}

pub fn slice_subslice_shared_(x: &[u32], y: usize, z: usize) -> &[u32] {
    &x[y..z]
}

pub fn slice_subslice_mut_(x: &mut [u32], y: usize, z: usize) -> &mut [u32] {
    &mut x[y..z]
}

pub fn array_to_slice_shared_(x: &[u32; 32]) -> &[u32] {
    x
}

pub fn array_to_slice_mut_(x: &mut [u32; 32]) -> &mut [u32] {
    x
}

pub fn array_subslice_shared_(x: &[u32; 32], y: usize, z: usize) -> &[u32] {
    &x[y..z]
}

pub fn array_subslice_mut_(x: &mut [u32; 32], y: usize, z: usize) -> &mut [u32] {
    &mut x[y..z]
}

pub fn index_slice_0<T>(s: &[T]) -> &T {
    &s[0]
}

pub fn index_array_0<T>(s: &[T; 32]) -> &T {
    &s[0]
}

/*
// Unsupported by Aeneas for now
pub fn index_index_slice<'a, T>(s: &'a [&[T]], i: usize, j: usize) -> &'a T {
    &s[i][j]
}
*/

pub fn index_index_array(s: [[u32; 32]; 32], i: usize, j: usize) -> u32 {
    s[i][j]
}

/*
// Unsupported by Aeneas for now
pub fn update_update_slice(s: &mut [&mut [u32]], i: usize, j: usize) {
    s[i][j] = 0;
}
*/

pub fn update_update_array(mut s: [[u32; 32]; 32], i: usize, j: usize) {
    s[i][j] = 0;
}

pub fn array_local_deep_copy(x: &[u32; 32]) {
    let _y = *x;
}

pub fn take_array(_: [u32; 2]) {}
pub fn take_array_borrow(_: &[u32; 2]) {}
pub fn take_slice(_: &[u32]) {}
pub fn take_mut_slice(_: &mut [u32]) {}

pub fn const_array() -> [u32; 2] {
    [0, 0]
}

pub fn const_slice() {
    let _: &[u32] = &[0, 0];
}

/*
// This triggers a special case in the constant expressions
pub fn const_string() {
    let _ = "hello";
}*/

pub fn take_all() {
    let mut x: [u32; 2] = [0, 0];
    // x is deep copied (copy node appears in Charon, followed by a move)
    take_array(x);
    take_array(x);
    // x passed by address, there is a reborrow here
    take_array_borrow(&x);
    // automatic cast from array to slice (spanning entire array)
    take_slice(&x);
    // note that both appear as SliceNew expressions, meaning the SliceNew UnOp is overloaded for
    // mut and non-mut cases
    take_mut_slice(&mut x);
}

pub fn index_array(x: [u32; 2]) -> u32 {
    x[0]
}
pub fn index_array_borrow(x: &[u32; 2]) -> u32 {
    x[0]
}

pub fn index_slice_u32_0(x: &[u32]) -> u32 {
    x[0]
}

pub fn index_mut_slice_u32_0(x: &mut [u32]) -> u32 {
    x[0]
}

pub fn index_all() -> u32 {
    let mut x: [u32; 2] = [0, 0];
    if true {
        let _y: [u32; 2] = [0, 0];
    } else {
        let _z: [u32; 1] = [0];
    }
    index_array(x)
        + index_array(x)
        + index_array_borrow(&x)
        + index_slice_u32_0(&x)
        + index_mut_slice_u32_0(&mut x)
}

pub fn update_array(mut x: [u32; 2]) {
    x[0] = 1
}
pub fn update_array_mut_borrow(x: &mut [u32; 2]) {
    x[0] = 1
}
pub fn update_mut_slice(x: &mut [u32]) {
    x[0] = 1
}

pub fn update_all() {
    let mut x: [u32; 2] = [0, 0];
    update_array(x);
    update_array(x);
    update_array_mut_borrow(&mut x);
    update_mut_slice(&mut x);
}

// Nano-tests, with ranges
// -----------------------

pub fn range_all() {
    let mut x: [u32; 4] = [0, 0, 0, 0];
    // CONFIRM: there is no way to shrink [T;N] into [T;M] with M<N?
    update_mut_slice(&mut x[1..3]);
}

// Nano-tests, with dereferences
// -----------------------------

pub fn deref_array_borrow(x: &[u32; 2]) -> u32 {
    let x: [u32; 2] = *x;
    x[0]
}

pub fn deref_array_mut_borrow(x: &mut [u32; 2]) -> u32 {
    let x: [u32; 2] = *x;
    x[0]
}

// Non-copiable arrays
// -------------------

pub fn take_array_t(_: [AB; 2]) {}

pub fn non_copyable_array() {
    let x: [AB; 2] = [AB::A, AB::B];
    // x is moved (not deep copied!)
    // TODO: determine whether the translation needs to be aware of that and pass by ref instead of by copy
    take_array_t(x);

    // this fails, naturally:
    // take_array_t(x);
}

// Larger, random tests
// --------------------

pub fn sum(s: &[u32]) -> u32 {
    let mut sum = 0;
    let mut i = 0;
    while i < s.len() {
        sum += s[i];
        i += 1;
    }
    sum
}

pub fn sum2(s: &[u32], s2: &[u32]) -> u32 {
    let mut sum = 0;
    assert!(s.len() == s2.len());
    let mut i = 0;
    while i < s.len() {
        sum += s[i] + s2[i];
        i += 1;
    }
    sum
}

pub fn f0() {
    let s: &mut [u32] = &mut [1, 2];
    s[0] = 1;
}

pub fn f1() {
    let mut s: [u32; 2] = [1, 2];
    s[0] = 1;
}

pub fn f2(_: u32) {}

pub fn f3() -> u32 {
    let a: [u32; 2] = [1, 2];
    f2(a[0]);
    let b = [0; 32];
    sum2(&a, f4(&b, 16, 18))
}

pub fn f4(x: &[u32; 32], y: usize, z: usize) -> &[u32] {
    &x[y..z]
}

pub const SZ: usize = 32;

// There is something slightly annoying here: the SZ constant gets inlined
pub fn f5(x: &[u32; SZ]) -> u32 {
    x[0]
}

// To avoid lifetime shortening
pub fn ite() {
    let mut x: [u32; 2] = [0, 0];
    if true {
        let mut y: [u32; 2] = [0, 0];
        index_mut_slice_u32_0(&mut x);
        index_mut_slice_u32_0(&mut y);
    }
}

pub fn zero_slice(a: &mut [u8]) {
    let mut i: usize = 0;
    let len = a.len();
    while i < len {
        a[i] = 0;
        i += 1;
    }
}

pub fn iter_mut_slice(a: &mut [u8]) {
    let len = a.len();
    let mut i = 0;
    while i < len {
        i += 1;
    }
}

pub fn sum_mut_slice(a: &mut [u32]) -> u32 {
    let mut i = 0;
    let mut s = 0;
    while i < a.len() {
        s += a[i];
        i += 1;
    }
    s
}