"""mutation_generator.py — Generate mutated Lean files from manifest.json.

Each mutation takes a theorem, applies a text-based transformation
(flip = → ≠, swap mul → add, etc.), and writes the mutated .lean file.
The runner then attempts to build it and expects failure.
"""
import json, re, shutil
from pathlib import Path
from typing import Any

REPO = Path(__file__).resolve().parents[2]
MUTATIONS = REPO / "scripts" / "qc_flag" / "mutations"
MANIFEST = REPO / "scripts" / "qc_flag" / "manifest.json"

def load_manifest() -> dict[str, Any]:
    return json.loads(MANIFEST.read_text())

def apply_mutation(text: str, diff: str) -> str:
    if "\u2192" in diff:
        parts = diff.split("\u2192")
        return text.replace(parts[0].strip(), parts[1].strip())
    return text

def generate_all(manifest: dict[str, Any] | None = None) -> dict[str, list[Path]]:
    if manifest is None:
        manifest = load_manifest()
    MUTATIONS.mkdir(parents=True, exist_ok=True)
    result: dict[str, list[Path]] = {}
    for src_rel, cfg in manifest["sources"].items():
        src = REPO / src_rel
        if not src.exists():
            continue
        orig = src.read_text()
        paths: list[Path] = []
        for tname, tcfg in cfg["theorems"].items():
            for m in tcfg["mutations"]:
                mutated = apply_mutation(orig, m["diff"])
                p = MUTATIONS / f"{m['id']}_{src.stem}.lean"
                p.write_text(mutated)
                paths.append(p)
        result[str(src)] = paths
    return result

if __name__ == "__main__":
    gen = generate_all()
    total = sum(len(v) for v in gen.values())
    print(f"Generated {total} mutations")