// List deletion/insertion operations
// Source: HeytingLean.CodingTheory.InsDel.Operations
// Theorem preserved: delNth_subseq, length_delNth, insNth_delNth_get

pub fn del_nth<T: Clone>(xs: &[T], n: usize) -> Vec<T> {
    if n >= xs.len() {
        return xs.to_vec();
    }
    let mut result = Vec::with_capacity(xs.len() - 1);
    result.extend_from_slice(&xs[..n]);
    result.extend_from_slice(&xs[n + 1..]);
    result
}

pub fn ins_nth<T: Clone>(xs: &[T], n: usize, a: T) -> Vec<T> {
    let pos = n.min(xs.len());
    let mut result = Vec::with_capacity(xs.len() + 1);
    result.extend_from_slice(&xs[..pos]);
    result.push(a);
    result.extend_from_slice(&xs[pos..]);
    result
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_del_nth() {
        assert_eq!(del_nth(&[1u8, 2, 3, 4], 0), vec![2, 3, 4]);
        assert_eq!(del_nth(&[1u8, 2, 3, 4], 2), vec![1, 2, 4]);
    }

    #[test]
    fn test_ins_del_roundtrip() {
        let xs = vec![1u8, 2, 3, 4, 5];
        for n in 0..xs.len() {
            let deleted = del_nth(&xs, n);
            let restored = ins_nth(&deleted, n, xs[n]);
            assert_eq!(restored, xs);
        }
    }
}