#!/usr/bin/env python3

import argparse
import json
import subprocess
import sys
from pathlib import Path


def run_fold(fold_bin: Path, compile_db: str, source: str) -> subprocess.CompletedProcess[str]:
    return subprocess.run(
        [
            str(fold_bin),
            "scan",
            "--compile-db",
            compile_db,
            "--format",
            "json",
            source,
        ],
        check=False,
        capture_output=True,
        text=True,
    )


def main() -> int:
    parser = argparse.ArgumentParser(
        description="Prototype loop invariant demo for fold's fixedpoint API"
    )
    parser.add_argument("source", help="Source file containing the loop under test")
    parser.add_argument("--compile-db", required=True, help="Path to compile_commands.json")
    parser.add_argument(
        "--fold-bin",
        default="build/release/fold",
        help="Path to the fold executable (default: build/release/fold)",
    )
    args = parser.parse_args()

    fold_bin = Path(args.fold_bin)
    result = run_fold(fold_bin, args.compile_db, args.source)
    print(f"fold exit code: {result.returncode}")

    findings = []
    if result.stdout.strip():
        try:
            payload = json.loads(result.stdout)
            findings = payload.get("runs", [{}])[0].get("results", [])
        except json.JSONDecodeError:
            pass

    print(f"scan findings reported: {len(findings)}")
    if result.stderr.strip():
        print("fold stderr:")
        print(result.stderr.strip())

    print("loop invariant inference: prototype wired, no invariant extracted yet")
    return 0


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