// Hamming basics: Bit type, distance, weight, repetition code
// Source: HeytingLean.CodingTheory.Hamming.Basic
// Theorem preserved: repetition_encode_mem, repetitionDecode_encode, onesCount_const

pub type Bit = u8; // ZMod 2: values 0 or 1

pub fn bit_add(a: Bit, b: Bit) -> Bit { (a + b) & 1 }

pub fn hamming_dist(x: &[Bit], y: &[Bit]) -> usize {
    x.iter().zip(y.iter()).filter(|(a, b)| a != b).count()
}

pub fn hamming_weight(x: &[Bit]) -> usize {
    x.iter().filter(|&&b| b != 0).count()
}

pub fn repetition_encode(n: usize, b: Bit) -> Vec<Bit> {
    vec![b; n]
}

pub fn ones_count(x: &[Bit]) -> usize {
    x.iter().filter(|&&b| b == 1).count()
}

pub fn majority_bit(x: &[Bit]) -> Bit {
    if 2 * ones_count(x) > x.len() { 1 } else { 0 }
}

pub fn repetition_decode(x: &[Bit]) -> Bit {
    majority_bit(x)
}

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

    #[test]
    fn test_repetition_roundtrip_zero() {
        let enc = repetition_encode(7, 0);
        assert_eq!(repetition_decode(&enc), 0);
    }

    #[test]
    fn test_repetition_roundtrip_one() {
        let enc = repetition_encode(7, 1);
        assert_eq!(repetition_decode(&enc), 1);
    }

    #[test]
    fn test_hamming_dist_self() {
        let x = vec![1, 0, 1, 1, 0];
        assert_eq!(hamming_dist(&x, &x), 0);
    }

    #[test]
    fn test_hamming_dist_pair() {
        let x = vec![1, 0, 1, 1, 0];
        let y = vec![1, 1, 1, 0, 0];
        assert_eq!(hamming_dist(&x, &y), 2);
    }
}