//! Mutation-driven test strengthening.
//!
//! The verifier is only as good as the held-out tests. Random inputs can fail to
//! exercise a program's logic, so a wrong-but-close program would pass. To
//! prevent that, for each kept program we synthesize *mutants* (operator swaps,
//! constant tweaks) and check that the tests catch every mutant whose behaviour
//! actually differs from the reference. When one slips through, we add the probe
//! input that exposes it. Each record then ships with tests provably
//! discriminative against this mutant family — a real strengthening of the
//! execution-based verification the thesis rests on.

use crate::sandbox::Sandbox;
use crate::spec::IoPair;
use crate::value::LValue;

const OP_SWAPS: &[(&str, &str)] = &[
    (" + ", " - "),
    (" - ", " + "),
    (" * ", " + "),
    (" // ", " % "),
    (" % ", " // "),
    (" == ", " ~= "),
    (" ~= ", " == "),
    (" < ", " >= "),
    (" <= ", " < "),
    (" > ", " <= "),
    (" >= ", " > "),
    (" and ", " or "),
    (" or ", " and "),
];

const OP_CAP: usize = 24;
const INT_CAP: usize = 8;

/// All mutants of a source. Operators are emitted with single spaces around them
/// (the generator controls this), so `" <= "` never matches inside `" < "` etc.
pub fn mutants(source: &str) -> Vec<String> {
    let mut out = Vec::new();
    for (from, to) in OP_SWAPS {
        for (idx, _) in source.match_indices(from) {
            let mut m = String::with_capacity(source.len());
            m.push_str(&source[..idx]);
            m.push_str(to);
            m.push_str(&source[idx + from.len()..]);
            out.push(m);
            if out.len() >= OP_CAP {
                break;
            }
        }
    }
    out.extend(int_literal_mutants(source));
    out
}

/// Replace one integer literal `k` with `k+1`, for the first few literals. Skips
/// digits inside identifiers (`v10`) and float fractions.
fn int_literal_mutants(source: &str) -> Vec<String> {
    let bytes = source.as_bytes();
    let mut out = Vec::new();
    let mut i = 0;
    while i < bytes.len() {
        let c = bytes[i] as char;
        let prev = if i == 0 { ' ' } else { bytes[i - 1] as char };
        let standalone = c.is_ascii_digit()
            && !(prev.is_ascii_alphanumeric() || prev == '_' || prev == '.');
        if standalone {
            let mut j = i;
            while j < bytes.len() && (bytes[j] as char).is_ascii_digit() {
                j += 1;
            }
            let next = if j < bytes.len() { bytes[j] as char } else { ' ' };
            if next != '.' {
                if let Ok(val) = source[i..j].parse::<i64>() {
                    let mut m = String::new();
                    m.push_str(&source[..i]);
                    m.push_str(&(val + 1).to_string());
                    m.push_str(&source[j..]);
                    out.push(m);
                    if out.len() >= INT_CAP {
                        break;
                    }
                }
            }
            i = j;
        } else {
            i += 1;
        }
    }
    out
}

#[derive(Debug, Clone)]
pub struct GateResult {
    pub tests: Vec<IoPair>,
    pub added: usize,
    pub mutants_total: usize,
    pub mutants_distinct: usize,
}

/// Outcome of running `f` (already loaded) on one input.
fn run_one(sb: &Sandbox, input: &[LValue], budget: i64) -> Option<LValue> {
    sb.call_f(input, budget).ok()
}

/// Run `f` over many inputs, loading `source` once.
fn run_all(sb: &Sandbox, source: &str, inputs: &[Vec<LValue>], budget: i64) -> Option<Vec<Option<LValue>>> {
    sb.load_program(source, budget).ok()?;
    Some(inputs.iter().map(|i| run_one(sb, i, budget)).collect())
}

/// Strengthen `tests` so they catch every behaviorally-distinct mutant. Returns
/// None if it would need to add more than `max_added` tests (treated as a weak,
/// rejected program — rare).
pub fn strengthen(
    sb: &Sandbox,
    source: &str,
    mut tests: Vec<IoPair>,
    probes: &[Vec<LValue>],
    budget: i64,
    max_added: usize,
) -> Option<GateResult> {
    // Reference behaviour on the probe set.
    let ref_probe = run_all(sb, source, probes, budget)?;

    let muts = mutants(source);
    let mut added = 0usize;
    let mut distinct = 0usize;

    for m in &muts {
        // Mutant must at least load to be a meaningful behavioural counterexample.
        let mut_probe = match run_all(sb, m, probes, budget) {
            Some(v) => v,
            None => continue, // mutant doesn't compile; trivially not a threat
        };

        // Find a probe where the mutant diverges from the reference (different
        // value, or errors where the reference succeeds).
        let mut distinguishing: Option<usize> = None;
        for (k, rp) in ref_probe.iter().enumerate() {
            if let Some(rv) = rp {
                match &mut_probe[k] {
                    Some(mv) if mv == rv => {}
                    _ => {
                        distinguishing = Some(k);
                        break;
                    }
                }
            }
        }
        let Some(k) = distinguishing else { continue }; // mutant behaves identically
        distinct += 1;

        // Do the current tests already catch it? (mutant must be re-loaded since
        // run_all above loaded the reference last.)
        let mut_on_tests = {
            let inputs: Vec<Vec<LValue>> = tests.iter().map(|t| t.input.clone()).collect();
            run_all(sb, m, &inputs, budget)?
        };
        let caught = tests.iter().enumerate().any(|(ti, t)| match &mut_on_tests[ti] {
            Some(mv) => mv != &t.output,
            None => true, // mutant errored on a test input
        });

        if !caught {
            if added >= max_added {
                return None; // give up: tests too weak to make discriminative cheaply
            }
            // Add the distinguishing probe with the reference's output.
            tests.push(IoPair {
                input: probes[k].clone(),
                output: ref_probe[k].clone().unwrap(),
            });
            added += 1;
        }
    }

    Some(GateResult { tests, added, mutants_total: muts.len(), mutants_distinct: distinct })
}

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

    #[test]
    fn operator_and_const_mutants_generated() {
        let src = "function f(v1)\n  return (v1 + 2)\nend\n";
        let ms = mutants(src);
        assert!(ms.iter().any(|m| m.contains("v1 - 2")), "should swap +");
        assert!(ms.iter().any(|m| m.contains("v1 + 3")), "should bump constant");
        // No mutant should equal the original.
        assert!(ms.iter().all(|m| m != src));
    }

    #[test]
    fn does_not_corrupt_two_char_ops() {
        let src = "function f(v1)\n  return (v1 <= 2)\nend\n";
        let ms = mutants(src);
        // `<=` becomes `<`, never a malformed `< =`.
        assert!(ms.iter().any(|m| m.contains("v1 < 2")));
        assert!(ms.iter().all(|m| !m.contains("< =")));
    }

    #[test]
    fn gate_makes_weak_tests_catch_a_slipping_mutant() {
        use crate::verify::{verify, Verdict};
        let sb = Sandbox::new().unwrap();
        let reference = "function f(v1) return (v1 * 2) end";

        // A single weak test at v1=2, where the `* -> +` mutant coincidentally
        // agrees (2*2 == 2+2 == 4), so it would slip past.
        let weak = vec![IoPair { input: vec![LValue::Int(2)], output: LValue::Int(4) }];
        let mutant = "function f(v1) return (v1 + 2) end";
        assert_eq!(verify(&sb, mutant, &weak, 100_000), Verdict::Pass, "weak tests miss it");

        // Probes that include values other than 2.
        let probes: Vec<Vec<LValue>> =
            (-3..=3).filter(|&v| v != 2).map(|v| vec![LValue::Int(v)]).collect();
        let g = strengthen(&sb, reference, weak, &probes, 100_000, 8).unwrap();
        assert!(g.added >= 1, "gate should add a distinguishing test");

        // Now the strengthened tests catch the mutant.
        assert_eq!(verify(&sb, mutant, &g.tests, 100_000), Verdict::Wrong, "gate caught it");
    }
}