// VT code decoding (specification-level brute-force search)
// Source: HeytingLean.CodingTheory.VT.Decode
// Theorem preserved: vtDecode_correct

use crate::hamming_basic::Bit;
use crate::vt_basic::vt_code_member;
use crate::operations::ins_nth;

pub fn vt_decode(n: usize, a: usize, m: usize, y: &[Bit]) -> Option<Vec<Bit>> {
    if y.len() + 1 != n { return None; }

    let mut found: Option<Vec<Bit>> = None;
    for pos in 0..=y.len() {
        for b in 0..=1u8 {
            let candidate = ins_nth(y, pos, b);
            if vt_code_member(&candidate, n, a, m) {
                if found.is_some() { return None; } // not unique
                found = Some(candidate);
            }
        }
    }
    found
}

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

    #[test]
    fn test_vt_decode_roundtrip() {
        // VT(3, 0, 4): find codewords, delete one bit, decode
        let codewords: Vec<Vec<Bit>> = (0..8u8).map(|bits| {
            vec![(bits >> 0) & 1, (bits >> 1) & 1, (bits >> 2) & 1]
        }).filter(|x| vt_code_member(x, 3, 0, 4)).collect();

        for cw in &codewords {
            for pos in 0..cw.len() {
                let received = del_nth(cw, pos);
                if let Some(decoded) = vt_decode(3, 0, 4, &received) {
                    assert_eq!(&decoded, cw, "decode mismatch");
                }
                // If None, it means non-unique — acceptable for some codes
            }
        }
    }
}