// Insertion/deletion distance (no substitutions)
// Source: HeytingLean.CodingTheory.InsDel.Distance
// Theorem preserved: insDelDist_nil_left, insDelDist_nil_right, insDelDist_self

pub fn ins_del_dist<T: Eq>(xs: &[T], ys: &[T]) -> usize {
    let (xn, yn) = (xs.len(), ys.len());
    let mut prev = (0..=yn).collect::<Vec<_>>();
    let mut curr = vec![0usize; yn + 1];

    for i in 1..=xn {
        curr[0] = i;
        for j in 1..=yn {
            if xs[i - 1] == ys[j - 1] {
                curr[j] = prev[j - 1];
            } else {
                curr[j] = 1 + prev[j].min(curr[j - 1]);
            }
        }
        std::mem::swap(&mut prev, &mut curr);
    }
    prev[yn]
}

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

    #[test]
    fn test_dist_self() {
        assert_eq!(ins_del_dist(&[1u8, 2, 3], &[1, 2, 3]), 0);
    }

    #[test]
    fn test_dist_nil_left() {
        let empty: &[u8] = &[];
        assert_eq!(ins_del_dist(empty, &[1, 2, 3]), 3);
    }

    #[test]
    fn test_dist_nil_right() {
        let empty: &[u8] = &[];
        assert_eq!(ins_del_dist(&[1u8, 2], empty), 2);
    }

    #[test]
    fn test_dist_single_deletion() {
        assert_eq!(ins_del_dist(&[1u8, 2, 3], &[1, 3]), 1);
    }
}