// Hamming(7,4) code: encode, syndrome, decode, single-error correction
// Source: HeytingLean.CodingTheory.Hamming.Hamming74
// Theorem preserved: hamming74Syndrome_encode, hamming74Decode_corrects_single_error
// Theorem preserved: hamming74Message_encode, hamming74Encode_message_of_codeword

use crate::hamming_basic::{Bit, bit_add};

pub fn hamming74_encode(m: &[Bit; 4]) -> [Bit; 7] {
    let (d0, d1, d2, d3) = (m[0], m[1], m[2], m[3]);
    let p1 = bit_add(bit_add(d0, d1), d3);
    let p2 = bit_add(bit_add(d0, d2), d3);
    let p4 = bit_add(bit_add(d1, d2), d3);
    [p1, p2, d0, p4, d1, d2, d3]
}

pub fn hamming74_syndrome(x: &[Bit; 7]) -> [Bit; 3] {
    [
        bit_add(bit_add(bit_add(x[0], x[2]), x[4]), x[6]),
        bit_add(bit_add(bit_add(x[1], x[2]), x[5]), x[6]),
        bit_add(bit_add(bit_add(x[3], x[4]), x[5]), x[6]),
    ]
}

fn syndrome_to_index(s: &[Bit; 3]) -> Option<usize> {
    let idx = s[0] as usize + 2 * s[1] as usize + 4 * s[2] as usize;
    if idx == 0 { None } else if idx <= 7 { Some(idx - 1) } else { None }
}

pub fn flip_bit(x: &mut [Bit; 7], pos: usize) {
    x[pos] = bit_add(x[pos], 1);
}

pub fn hamming74_decode(x: &mut [Bit; 7]) {
    let s = hamming74_syndrome(x);
    if let Some(pos) = syndrome_to_index(&s) {
        flip_bit(x, pos);
    }
}

pub fn hamming74_message(x: &[Bit; 7]) -> [Bit; 4] {
    [x[2], x[4], x[5], x[6]]
}

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

    #[test]
    fn test_encode_decode_roundtrip() {
        for bits in 0u8..16 {
            let m = [(bits >> 0) & 1, (bits >> 1) & 1, (bits >> 2) & 1, (bits >> 3) & 1];
            let enc = hamming74_encode(&m);
            let msg = hamming74_message(&enc);
            assert_eq!(msg, m, "message extraction failed for {:?}", m);
        }
    }

    #[test]
    fn test_syndrome_of_codeword_is_zero() {
        for bits in 0u8..16 {
            let m = [(bits >> 0) & 1, (bits >> 1) & 1, (bits >> 2) & 1, (bits >> 3) & 1];
            let enc = hamming74_encode(&m);
            let s = hamming74_syndrome(&enc);
            assert_eq!(s, [0, 0, 0], "syndrome nonzero for {:?}", m);
        }
    }

    #[test]
    fn test_single_error_correction() {
        for bits in 0u8..16 {
            let m = [(bits >> 0) & 1, (bits >> 1) & 1, (bits >> 2) & 1, (bits >> 3) & 1];
            let enc = hamming74_encode(&m);
            for pos in 0..7 {
                let mut corrupted = enc;
                flip_bit(&mut corrupted, pos);
                hamming74_decode(&mut corrupted);
                assert_eq!(corrupted, enc, "correction failed for {:?} pos {}", m, pos);
            }
        }
    }
}