// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.ProjectionElem.html
// ConstantIndex
// [-]
// These indices are generated by slice patterns. Easiest to explain by example:

// [X, _, .._, _, _] => { offset: 0, min_length: 4, from_end: false },
// [_, X, .._, _, _] => { offset: 1, min_length: 4, from_end: false },
// [_, _, .._, X, _] => { offset: 2, min_length: 4, from_end: true },
// [_, _, .._, _, X] => { offset: 1, min_length: 4, from_end: true },

fn test1() {
    let a = [1, 2, 3, 4];
    match a {
        [x, _, _, _] => assert!(x == 1),
    }
    match a {
        [_, x, _, _] => assert!(x == 2),
    }
}

fn test2() {
    let a = [1, 2, 3, 4];
    match a {
        [x, .., _] => assert!(x == 1),
    }
    match a {
        [x, ..] => assert!(x == 1),
    }
    match a {
        [.., x, _, _] => assert!(x == 2),
    }
    match a {
        [_, x, ..] => assert!(x == 2),
    }
    match a {
        [_, .., x, _] => assert!(x == 3),
    }
    match a {
        [.., x, _] => assert!(x == 3),
    }
    match a {
        [_, _, x, ..] => assert!(x == 3),
    }
    match a {
        [.., x] => assert!(x == 4),
    }
}

fn test3(a: &[i64]) {
    match a {
        [x, .., _] => assert!(*x == 1),
        _ => assert!(false),
    }
    match a {
        [x, ..] => assert!(*x == 1),
        _ => assert!(false),
    }
    match a {
        [.., x, _, _] => assert!(*x == 2),
        _ => assert!(false),
    }
    match a {
        [_, x, ..] => assert!(*x == 2),
        _ => assert!(false),
    }
    match a {
        [_, .., x, _] => assert!(*x == 3),
        _ => assert!(false),
    }
    match a {
        [.., x, _] => assert!(*x == 3),
        _ => assert!(false),
    }
    match a {
        [_, _, x, ..] => assert!(*x == 3),
        _ => assert!(false),
    }
    match a {
        [.., x] => assert!(*x == 4),
        _ => assert!(false),
    }
}

fn encode_utf8_raw(code: u32, dst: &mut [u8]) -> u8 {
    match (code, &mut dst[..]) {
        (1, [a, ..]) => *a,
        _ => panic!(),
    }
}

fn test4() {
    let code = 1;
    let dst: &mut [u8] = &mut [0u8; 4];
    assert!(encode_utf8_raw(code, dst) == 0);
}

#[kani::proof]
fn main() {
    test1();
    test2();
    test3(&[1, 2, 3, 4]);
    test4();
}