// LCS-based Levenshtein distance (insertion/deletion only)
// Source: HeytingLean.CodingTheory.InsDel.Levenshtein
// Theorem preserved: lcsLength_self, levDist_self

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

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

pub fn lev_dist<T: Eq>(xs: &[T], ys: &[T]) -> usize {
    xs.len() + ys.len() - 2 * lcs_length(xs, ys)
}

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

    #[test]
    fn test_lcs_self() {
        let xs = vec![1u8, 2, 3, 4];
        assert_eq!(lcs_length(&xs, &xs), 4);
    }

    #[test]
    fn test_lev_dist_self() {
        let xs = vec![1u8, 2, 3];
        assert_eq!(lev_dist(&xs, &xs), 0);
    }

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

    #[test]
    fn test_lcs_known() {
        assert_eq!(lcs_length(&[1u8, 3, 5], &[1, 2, 3, 4, 5]), 3);
    }
}