#!/usr/bin/env python3
"""Run formalsw's end-to-end tests."""

from __future__ import annotations

import json
import re
import subprocess
import sys
import textwrap
import time
from dataclasses import dataclass
from pathlib import Path


REPO = Path(__file__).resolve().parent
FORMALSW = REPO / "formalsw"


@dataclass(frozen=True)
class TestCase:
    """One formalsw subprocess-backed test case."""

    name: str
    source: Path
    expected_returncode: int
    expected_output: str | tuple[str, ...] | None = None


@dataclass(frozen=True)
class TestResult:
    """The result of one subprocess-backed test."""

    case: TestCase
    passed: bool
    command: list[str]
    returncode: int
    stdout: str
    stderr: str
    elapsed: float


def run_formalsw(source: Path) -> subprocess.CompletedProcess[str]:
    """Run formalsw on a repo-relative source path."""
    return subprocess.run(
        [str(FORMALSW), str(source)],
        cwd=REPO,
        text=True,
        stdout=subprocess.PIPE,
        stderr=subprocess.PIPE,
        check=False,
    )


def run_case(case: TestCase) -> TestResult:
    """Run one test case and compare status plus optional diagnostic text."""
    start = time.perf_counter()
    completed = run_formalsw(case.source)
    elapsed = time.perf_counter() - start
    output = completed.stdout + completed.stderr
    passed = completed.returncode == case.expected_returncode
    if case.expected_output is not None:
        expected = (case.expected_output,) if isinstance(case.expected_output, str) else case.expected_output
        passed = passed and all(fragment in output for fragment in expected)
    return TestResult(
        case=case,
        passed=passed,
        command=completed.args,
        returncode=completed.returncode,
        stdout=completed.stdout,
        stderr=completed.stderr,
        elapsed=elapsed,
    )


def print_result(result: TestResult) -> None:
    """Print one test result, including diagnostics for failures."""
    status = "PASS" if result.passed else "FAIL"
    print(f"{status} {result.case.source} ({result.elapsed:.2f}s)", flush=True)
    if result.passed:
        return
    print(f"  command: {' '.join(result.command)}")
    print(f"  exit: {result.returncode}")
    print(f"  expected exit: {result.case.expected_returncode}")
    if result.case.expected_output is not None:
        print(f"  expected output: {result.case.expected_output}")
    if result.stdout:
        print("  stdout:")
        print(textwrap.indent(result.stdout.rstrip(), "    "))
    if result.stderr:
        print("  stderr:")
        print(textwrap.indent(result.stderr.rstrip(), "    "))


def main() -> int:
    """Run all tests and return a process exit status."""
    cases = [
        TestCase("shared heap helper calls", Path("tests/py/heap_calls.py"), 0, "All 4 checks passed"),
        TestCase("shared heap range loops", Path("tests/py/heap_ranges.py"), 0, "All 2 checks passed"),
        TestCase("positional scalar maximum", Path("tests/py/maximum.py"), 0, "All 1 checks passed"),
        TestCase("immutable scalar default arguments", Path("tests/py/defaults.py"), 0, "All 3 checks passed"),
        TestCase("deadlock, livelock, and joined worker termination", Path("tests/py/parallel_liveness.py"), 0),
        TestCase("mutable global lists, aliases, and exceptional state", Path("tests/py/mutable_globals.py"), 0),
        TestCase("global inputs and normal/exceptional state", Path("tests/py/globals.py"), 0),
        TestCase("dictionary globals are explicitly unsupported", Path("tests/py/fail/global_mutable.py"), 1,
                 "supported state is int, str, bool, or homogeneous scalar lists"),
        TestCase("legacy equivalence cannot discard globals", Path("tests/py/fail/global_legacy.py"), 1,
                 "legacy Function properties omit globals"),
        TestCase("parallel calls with different signatures and arguments", Path("tests/py/parallel_calls.py"), 0),
        TestCase("shared counter synchronization and lost update", Path("tests/py/parallel_shared_counter.py"), 0),
        TestCase(
            "missing synchronization invalidates the guarantee",
            Path("tests/py/fail/parallel_missing_lock.py"),
            1,
            "Tactic `native_decide` evaluated that the proposition",
        ),
        TestCase("termination and divergence", Path("tests/py/termination.py"), 0),
        TestCase("recursive scalar calls and short circuiting", Path("tests/py/recursive_calls.py"), 0),
        TestCase("simultaneous tuple assignment and evaluation order", Path("tests/py/tuple_assignments.py"), 0),
        TestCase("stepped range iteration with calls and early returns", Path("tests/py/stepped_ranges.py"), 0),
        TestCase("module and multiple preconditions", Path("tests/py/requires_module.py"), 0),
        TestCase("execution preconditions across short and raw specifications", Path("tests/py/requires.py"), 0),
        TestCase("local helper calls and reused source proofs", Path("tests/py/linked_calls.py"), 0, "All 2 checks passed"),
        TestCase("variable and signed integer division", Path("tests/py/division.py"), 0, "All 4 checks passed"),
        TestCase("nested break, continue, and loop else scopes", Path("tests/py/loop_control.py"), 0, "All 10 checks passed"),
        TestCase("scalar string conversion, indexing, and slices", Path("tests/py/strings.py"), 0, "All 12 checks passed"),
        TestCase("immutable byte literals, repetition, slices and heap values", Path("tests/py/bytes_literals.py"), 0, "All 6 checks passed"),
        TestCase("integer powers and partial execution coverage", Path("tests/py/powers.py"), 0, "All 14 checks passed"),
        TestCase("integer bit lengths and receiver exceptions", Path("tests/py/int_bit_length.py"), 0),
        TestCase("generator sum scoping, filters, ranges and exceptions", Path("tests/py/generator_sums.py"), 0),
        TestCase("integer square root and imported builtin aliases", Path("tests/py/math_isqrt.py"), 0),
        TestCase("integer gcd and imported builtin aliases", Path("tests/py/math_gcd.py"), 0),
        TestCase("math module imports and heap calls", Path("tests/py/math_modules.py"), 0, "All 6 checks passed"),
        TestCase("range_sum passes", Path("tests/py/range_sum.py"), 0),
        TestCase("typed, object, and return sort equivalence", Path("tests/py/sort.py"), 0),
        TestCase("equivalent throws pass", Path("tests/py/equiv_throw.py"), 0),
        TestCase("Throws can be proved", Path("tests/py/throws.py"), 0),
        TestCase("annotations restrict comparison inputs", Path("tests/py/typing.py"), 0),
        TestCase("raw Lean requirement passes", Path("tests/py/raw_lean.py"), 0),
        TestCase(
            "this_function rejects unsupported arity",
            Path("tests/py/fail/this_function_arity.py"),
            1,
            "only plain positional arguments without variadics are supported",
        ),
        TestCase(
            "this_function rejects unsupported argument annotations",
            Path("tests/py/fail/this_function_annotation.py"),
            1,
            "needs a supported int, str, bool, or list annotation",
        ),
        TestCase(
            "sorrys are rejected",
            Path("tests/py/fail/sorry.py"),
            1,
            "declaration uses `sorry`",
        ),
        TestCase(
            "unproven properties are rejected",
            Path("tests/py/fail/missing_required.py"),
            1,
            "missing proof",
        ),
        TestCase(
            "missing proof files are rejected",
            Path("tests/py/fail/missing_lean.py"),
            1,
            "missing proof file",
        ),
        TestCase(
            "unsupported proofs are diagnosed while supported proofs continue",
            Path("tests/py/fail/unsupported"),
            1,
            (
                "equivalent.«Not Equiv(unsupported_call)»: unsupported Python constructs",
                "equivalent -> unsupported_call",
                "Try statements are unsupported",
            ),
        ),
        TestCase(
            "directories check all Python files",
            Path("tests/py/fail/dir"),
            1,
            "tests/py/fail/dir/fail.py",
        ),
    ]
    for builtin_model in sorted(Path("lang/py/builtin/type").glob("*.py")):
        cases.append(TestCase(f"plain-Python builtin model {builtin_model.stem}", builtin_model, 0))
    cases.append(TestCase(
        "plain-Python builtin function model",
        Path("lang/py/builtin/function.py"),
        0,
    ))
    results = []
    for case in cases:
        print(f"RUN  {case.source}", flush=True)
        result = run_case(case)
        results.append(result)
        print_result(result)

    stub_completed = subprocess.run(
        [str(FORMALSW), "--stub", "tests/py/range_sum.py"],
        cwd=REPO,
        text=True,
        stdout=subprocess.PIPE,
        stderr=subprocess.PIPE,
        check=False,
    )
    stub_passed = (
        stub_completed.returncode == 0
        and not stub_completed.stderr
        and 'import «.formalsw».tests.py.«range_sum.py.ast»' in stub_completed.stdout
        and "namespace tests.py.range_sum" in stub_completed.stdout
        and "theorem sum.«Equiv(sum_naive)» :" in stub_completed.stdout
        and "theorem sum.«BigO(1)» :" in stub_completed.stdout
        and "theorem sum.«ReturnType» :" in stub_completed.stdout
        and "theorem sum_naive.«Returns» :" in stub_completed.stdout
        and "theorem sum_naive.«BigO(n)» :" in stub_completed.stdout
        and "end tests.py.range_sum" in stub_completed.stdout
        and stub_completed.stdout.count("  sorry") == 5
    )
    print(f"{'PASS' if stub_passed else 'FAIL'} Lean proof stub generation", flush=True)

    ast_json_path = REPO / ".formalsw/tests/py/range_sum.py.ast.json"
    ast_bridge_path = REPO / ".formalsw/tests/py/range_sum.py.ast.lean"
    sort_ast_json_path = REPO / ".formalsw/tests/py/sort.py.ast.json"
    try:
        ast_document = json.loads(ast_json_path.read_text())
        sort_ast_document = json.loads(sort_ast_json_path.read_text())
        json_ast_passed = (
            ast_document["schema_version"] == 1
            and ast_document["ast"]["type"] == "Module"
            and ast_document["ast"]["body"][1]["type"] == "FunctionDef"
            and "pyast_from_json%" in ast_bridge_path.read_text()
            and any(
                statement.get("type") == "ClassDef"
                and statement.get("name") == "str"
                for statement in sort_ast_document["ast"]["body"]
            )
        )
    except (FileNotFoundError, json.JSONDecodeError, KeyError, IndexError, TypeError):
        json_ast_passed = False
    print(
        f"{'PASS' if json_ast_passed else 'FAIL'} generated JSON AST import",
        flush=True,
    )
    source_tree_clean = not any((REPO / "tests/py").rglob("*.olean"))
    print(
        f"{'PASS' if source_tree_clean else 'FAIL'} no Lean objects in source tree",
        flush=True,
    )
    builtin_coverage = subprocess.run(
        [sys.executable, "tests/py/builtin_coverage"],
        cwd=REPO,
        text=True,
        stdout=subprocess.PIPE,
        stderr=subprocess.PIPE,
        check=False,
    )
    builtin_coverage_passed = builtin_coverage.returncode == 0
    print(
        f"{'PASS' if builtin_coverage_passed else 'FAIL'} builtin documentation coverage",
        flush=True,
    )
    if not builtin_coverage_passed:
        if builtin_coverage.stdout:
            print(textwrap.indent(builtin_coverage.stdout.rstrip(), "  "))
        if builtin_coverage.stderr:
            print(textwrap.indent(builtin_coverage.stderr.rstrip(), "  "))
    builtin_models = subprocess.run(
        ["lake", "env", "lean", "tests/py/builtin_models.lean"],
        cwd=REPO,
        text=True,
        stdout=subprocess.PIPE,
        stderr=subprocess.PIPE,
        check=False,
    )
    builtin_models_passed = builtin_models.returncode == 0
    print(
        f"{'PASS' if builtin_models_passed else 'FAIL'} builtin model behavior",
        flush=True,
    )
    if not builtin_models_passed:
        output = builtin_models.stdout + builtin_models.stderr
        if output:
            print(textwrap.indent(output.rstrip(), "  "))
    throws_syntax = subprocess.run(
        ["lake", "env", "lean", "-DwarningAsError=true", "tests/py/throws_syntax.lean"],
        cwd=REPO,
        text=True,
        stdout=subprocess.PIPE,
        stderr=subprocess.PIPE,
        check=False,
    )
    throws_syntax_passed = throws_syntax.returncode == 0
    print(
        f"{'PASS' if throws_syntax_passed else 'FAIL'} Throws, Returns, and Halts syntax",
        flush=True,
    )
    if not throws_syntax_passed:
        output = throws_syntax.stdout + throws_syntax.stderr
        if output:
            print(textwrap.indent(output.rstrip(), "  "))
    builtin_python_models = subprocess.run(
        [sys.executable, "tests/py/builtin_python_models.py"],
        cwd=REPO,
        text=True,
        stdout=subprocess.PIPE,
        stderr=subprocess.PIPE,
        check=False,
    )
    builtin_python_models_passed = builtin_python_models.returncode == 0
    print(
        f"{'PASS' if builtin_python_models_passed else 'FAIL'} plain-Python builtin behavior",
        flush=True,
    )
    if not builtin_python_models_passed:
        output = builtin_python_models.stdout + builtin_python_models.stderr
        if output:
            print(textwrap.indent(output.rstrip(), "  "))
    graph_results = [subprocess.run(
        command, cwd=REPO, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False,
    ) for command in (
        [sys.executable, "tests/py/object_equivalence.py"],
        [sys.executable, "tests/py/globals.py"],
        [sys.executable, "tests/py/mutable_globals.py"],
        ["lake", "env", "lean", "-DwarningAsError=true", "tests/py/object_equivalence.lean"],
        [sys.executable, "tests/py/graph_equivalence_checks"],
        [sys.executable, "tests/py/mutable_global_checks"],
    )]
    graph_passed = all(result.returncode == 0 for result in graph_results)
    print(f"{'PASS' if graph_passed else 'FAIL'} interpreted Python object-graph equivalence", flush=True)
    if not graph_passed:
        for result in graph_results:
            print(textwrap.indent((result.stdout + result.stderr).rstrip(), "  "))
    support_checks = subprocess.run(
        [sys.executable, "tests/py/support_checks"],
        cwd=REPO, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False,
    )
    support_checks_passed = support_checks.returncode == 0
    print(f"{'PASS' if support_checks_passed else 'FAIL'} unsupported source validation", flush=True)
    if not support_checks_passed:
        print(textwrap.indent((support_checks.stdout + support_checks.stderr).rstrip(), "  "))
    parallel_semantics = subprocess.run(
        ["lake", "env", "lean", "-DwarningAsError=true", "tests/py/parallel_semantics.lean"],
        cwd=REPO, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False,
    )
    parallel_liveness = subprocess.run(
        ["lake", "env", "lean", "-DwarningAsError=true", "tests/py/parallel_liveness.lean"],
        cwd=REPO, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False,
    )
    parallel_runtime = subprocess.run(
        [sys.executable, "tests/py/parallel_checks"],
        cwd=REPO, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False,
        timeout=30,
    )
    quotations = subprocess.run(
        [sys.executable, "tests/py/quotation_checks"],
        cwd=REPO, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False,
        timeout=120,
    )
    parallel_passed = (parallel_semantics.returncode == 0 and parallel_liveness.returncode == 0 and parallel_runtime.returncode == 0
                       and quotations.returncode == 0)
    print(f"{'PASS' if parallel_passed else 'FAIL'} parallel semantics and real-thread data structures", flush=True)
    if not parallel_passed:
        for completed in (parallel_semantics, parallel_liveness, parallel_runtime, quotations):
            print(textwrap.indent((completed.stdout + completed.stderr).rstrip(), "  "))
    call_checks = subprocess.run(
        [sys.executable, "tests/py/call_checks"],
        cwd=REPO, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False,
    )
    call_checks_passed = call_checks.returncode == 0
    print(f"{'PASS' if call_checks_passed else 'FAIL'} recursive call coverage", flush=True)
    if not call_checks_passed:
        print(textwrap.indent((call_checks.stdout + call_checks.stderr).rstrip(), "  "))
    project_checks = subprocess.run(
        [sys.executable, "tests/py/project_checks"],
        cwd=REPO, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False,
    )
    project_checks_passed = project_checks.returncode == 0
    print(f"{'PASS' if project_checks_passed else 'FAIL'} external projects and numeric filenames", flush=True)
    if not project_checks_passed:
        print(textwrap.indent((project_checks.stdout + project_checks.stderr).rstrip(), "  "))
    contract_checks = subprocess.run(
        [sys.executable, "tests/py/contract_checks"],
        cwd=REPO, text=True, capture_output=True,
    )
    contract_checks_passed = contract_checks.returncode == 0
    print(f"{'PASS' if contract_checks_passed else 'FAIL'} guarded contracts and imported references", flush=True)
    if not contract_checks_passed:
        print(textwrap.indent((contract_checks.stdout + contract_checks.stderr).rstrip(), "  "))
    setup_checks = subprocess.run(
        [sys.executable, "tests/py/setup_checks"],
        cwd=REPO, text=True, capture_output=True,
    )
    setup_checks_passed = setup_checks.returncode == 0
    print(f"{'PASS' if setup_checks_passed else 'FAIL'} Python specification setup", flush=True)
    if not setup_checks_passed:
        print(textwrap.indent((setup_checks.stdout + setup_checks.stderr).rstrip(), "  "))
    link_checks = subprocess.run(
        [sys.executable, "tests/py/link_checks"],
        cwd=REPO, text=True, capture_output=True,
    )
    link_checks_passed = link_checks.returncode == 0
    print(f"{'PASS' if link_checks_passed else 'FAIL'} local helper dependencies", flush=True)
    if not link_checks_passed:
        print(textwrap.indent((link_checks.stdout + link_checks.stderr).rstrip(), "  "))
    raw_docs = (REPO / "README.adoc").read_text().split("=== Raw Lean specification\n", 1)[1].split("\n== How it works", 1)[0]
    raw_headers = re.findall(r"^==== (.+)$", raw_docs, re.MULTILINE)
    raw_ids = re.findall(r"^\[\[(raw-lean-[^\]]+)\]\]\n==== ", raw_docs, re.MULTILINE)
    raw_docs_passed = (
        raw_headers == sorted(raw_headers, key=str.casefold)
        and len(raw_ids) == len(raw_headers) == len(set(raw_ids))
    )
    print(f"{'PASS' if raw_docs_passed else 'FAIL'} alphabetical Raw Lean sections with unique IDs", flush=True)
    return 0 if (
        all(result.passed for result in results)
        and stub_passed
        and json_ast_passed
        and source_tree_clean
        and builtin_coverage_passed
        and builtin_models_passed
        and throws_syntax_passed
        and builtin_python_models_passed
        and graph_passed
        and support_checks_passed
        and parallel_passed
        and raw_docs_passed
        and project_checks_passed
        and contract_checks_passed
        and setup_checks_passed
        and link_checks_passed
        and call_checks_passed
    ) else 1


if __name__ == "__main__":
    sys.exit(main())
