"""test_lean_witnesses.py — Verify Lean #eval witnesses match expected values.

Each module has #eval statements with -- expect: comments. This script
builds each module, captures the #eval output, and checks against expectations.
"""

from __future__ import annotations

import re
import subprocess
import unittest
from pathlib import Path

REPO_ROOT = Path(__file__).resolve().parent.parent

# Modules to test: (module_name, build_target, timeout_s)
LEAN_MODULES = [
    ("SilverSight.FeasibleSet.Theorem", "SilverSightRRC", 60),
    ("SilverSight.FeasibleSet.QUBORelaxation", "SilverSightRRC", 60),
    ("SilverSight.CollectiveIntelligence.CostTransparency", "SilverSightRRC", 60),
    ("SilverSight.RRC.Emit", "SilverSightRRC", 120),
    ("SilverSight.RRC.Q16_16Manifold", "SilverSightRRC", 120),
    ("CoreFormalism.FixedPoint", "SilverSightFormal", 60),
    ("CoreFormalism.SidonSets", "SilverSightFormal", 60),
    ("CoreFormalism.InteractionGraphSidon", "SilverSightFormal", 60),
    ("SilverSight.PIST.Spectral", "SilverSightRRC", 120),
    ("SilverSight.PIST.FisherRigidity", "SilverSightRRC", 60),
    ("SilverSight.HachimojiN8", "SilverSightRRC", 60),
    ("SilverSight.HachimojiN8Bridge", "SilverSightRRC", 60),
    ("SilverSight.AVMIsa.Emit", "SilverSightRRC", 120),
    ("SilverSight.ReceiptCore", "SilverSightRRC", 60),
    ("SilverSight.RRC.ReceiptDensity", "SilverSightRRC", 60),
    ("SilverSight.PIST.Classify", "SilverSightRRC", 120),
    ("SilverSight.PIST.CartanConnection", "SilverSightRRC", 120),
    ("SilverSight.PIST.YangBaxter", "SilverSightRRC", 60),
]


def lake_build(target: str, timeout_s: int) -> tuple[int, str]:
    try:
        r = subprocess.run(
            ["lake", "build", target],
            cwd=REPO_ROOT, capture_output=True, text=True, timeout=timeout_s,
        )
        return r.returncode, r.stdout + r.stderr
    except subprocess.TimeoutExpired:
        return -1, "TIMEOUT"
    except FileNotFoundError:
        return -2, "lake not found"


def extract_eval_output(build_output: str) -> list[str]:
    """Extract #eval output lines from lake build output."""
    lines = []
    for line in build_output.split("\n"):
        if "info:" in line and "#eval" not in line:
            # info lines contain eval results: "info: file.lean:123:4: <value>"
            parts = line.split(":", 3)
            if len(parts) >= 4:
                val = parts[-1].strip()
                if val and val not in ("0",):
                    lines.append(val)
    return lines


class TestLeanModules(unittest.TestCase):
    """Build each Lean module and verify compilation."""

    def test_all_modules_compile(self):
        """All Lean modules must compile (lake build)."""
        failures = []
        for module, target, timeout in LEAN_MODULES:
            rc, out = lake_build(module, timeout)
            if rc != 0:
                failures.append(f"{module} (exit {rc}): {out[-200:]}")
        
        if failures:
            self.fail("\n".join(failures[:5]))
    
    def test_specific_milestone_outputs(self):
        """Key #eval outputs must match expected values."""
        # Build specific modules and check their eval output
        test_cases = [
            # (target, expected_eval_output_contains)
            ("SilverSight.RRC.Emit", "compatibleStructuralProjection"),
            ("SilverSight.RRC.Emit", "alignedExact"),
            ("SilverSight.FeasibleSet.Theorem", "Built"),
        ]
        for target, expected in test_cases:
            rc, out = lake_build(target, 120)
            self.assertEqual(rc, 0, f"{target} build failed")
            self.assertIn(expected, out, f"{target} eval output missing '{expected}'")


class TestLeanHachimoji(unittest.TestCase):
    """Hachimoji N8 correctness."""

    def test_n8_compiles(self):
        rc, out = lake_build("SilverSight.HachimojiN8", 60)
        self.assertEqual(rc, 0, f"Build failed:\n{out[-300:]}")


class TestLeanFeasibleSet(unittest.TestCase):
    """Feasible-Set Theorem and QUBO Relaxation."""

    def test_theorem_compiles(self):
        rc, out = lake_build("SilverSight.FeasibleSet.Theorem", 60)
        self.assertEqual(rc, 0, f"Build failed:\n{out[-300:]}")

    def test_qubo_relaxation_compiles(self):
        rc, out = lake_build("SilverSight.FeasibleSet.QUBORelaxation", 60)
        self.assertEqual(rc, 0, f"Build failed:\n{out[-300:]}")

    def test_cost_transparency_compiles(self):
        rc, out = lake_build("SilverSight.CollectiveIntelligence.CostTransparency", 60)
        self.assertEqual(rc, 0, f"Build failed:\n{out[-300:]}")


class TestRrcEmit(unittest.TestCase):
    """RRC Emit alignment gate."""

    def test_emit_compiles(self):
        rc, out = lake_build("SilverSight.RRC.Emit", 120)
        self.assertEqual(rc, 0, f"Build failed:\n{out[-300:]}")

    def test_q16_manifold_compiles(self):
        rc, out = lake_build("SilverSight.RRC.Q16_16Manifold", 120)
        self.assertEqual(rc, 0, f"Build failed:\n{out[-300:]}")


class TestCoreFormalism(unittest.TestCase):
    """CoreFormalism modules."""

    def test_fixedpoint_compiles(self):
        rc, out = lake_build("CoreFormalism.FixedPoint", 60)
        self.assertEqual(rc, 0, f"Build failed:\n{out[-300:]}")

    def test_sidon_sets(self):
        rc, out = lake_build("CoreFormalism.SidonSets", 60)
        self.assertEqual(rc, 0, f"Build failed:\n{out[-300:]}")

    def test_interaction_graph_sidon(self):
        rc, out = lake_build("CoreFormalism.InteractionGraphSidon", 60)
        self.assertEqual(rc, 0, f"Build failed:\n{out[-300:]}")


if __name__ == "__main__":
    unittest.main()