#!/usr/bin/env python3
"""Decompose selector 2:0 field maps against previous route selectors."""
from __future__ import annotations

import argparse
import html
import itertools
import json
from pathlib import Path
from typing import Any


ROOT = Path(__file__).resolve().parents[1]
OUT = ROOT / "out"
SOURCE = "map1_01a"
TARGET = "map2_02d"
SOURCE_SELECTOR = "0:0"
PREDECESSOR_SELECTOR = "1:0"
CURRENT_SELECTOR = "2:0"
FAILED_SELECTOR_SET_DECOMPOSITION_GATE_IDS = [
    "source-current-control-flow",
    "predecessor-state-persistence",
    "real-selector-2:0-or-selected-root-runtime",
    "strict-source-hotspot",
]
SELECTOR_SET_DECOMPOSITION_MISSING_EVIDENCE = [
    "VM/control-flow execution from source-side selector 0:0 into current selector 2:0",
    "target-side predecessor 1:0 state persistence into the current 2:0 frontier reader",
    "real selector 2:0 gameplay savedata or selected-pointer runtime trace",
    "strict map1_01a source coordinate or hotspot for map2_02d",
]
SELECTOR_SET_DECOMPOSITION_EVIDENCE_REFS = [
    {
        "path": "out/save_scene_selectors.json",
        "fields": ["group", "slot", "selectedPointerHex", "fieldMaps"],
    },
    {
        "path": "out/playable_progress.json",
        "fields": ["reachableFromStart", "reachableCount"],
    },
    {
        "path": "out/save_selector_predecessor_persistence_gap.json",
        "fields": ["persistenceProven", "selectorMergeGapOpen", "routeOrderProven"],
    },
    {
        "path": "out/save_selector_selected_root_execution_gap.json",
        "fields": ["selectedRootExecutionRefFound", "proofFound", "missingEvidence"],
    },
    {
        "path": "out/map1_01a_strict_source_hotspot_context.json",
        "fields": ["proofFound", "strictSourceCoordinateFound", "tileHotspotConfirmed"],
    },
]


def load_json(path: Path, fallback: Any) -> Any:
    if not path.exists():
        return fallback
    return json.loads(path.read_text(encoding="utf-8"))


def selector_key(row: dict) -> str:
    return f"{row.get('group')}:{row.get('slot')}"


def find_selector(selectors: list[dict], key: str) -> dict:
    for row in selectors:
        if selector_key(row) == key:
            return row
    raise ValueError(f"selector {key} not found")


def selector_record(row: dict, current_maps: set[str], confirmed_maps: set[str]) -> dict:
    field_maps = row.get("fieldMaps") or []
    field_set = set(field_maps)
    return {
        "selector": selector_key(row),
        "rootHex": row.get("selectedPointerHex"),
        "fieldMaps": field_maps,
        "containsSource": SOURCE in field_set,
        "containsTarget": TARGET in field_set,
        "isSubsetOfCurrent": field_set <= current_maps,
        "extraVsCurrent": sorted(field_set - current_maps),
        "missingVsCurrent": sorted(current_maps - field_set),
        "confirmedOverlap": sorted(field_set & confirmed_maps),
    }


def pair_record(left: dict, right: dict, current_maps: set[str]) -> dict:
    left_maps = set(left.get("fieldMaps") or [])
    right_maps = set(right.get("fieldMaps") or [])
    union = left_maps | right_maps
    return {
        "selectors": [selector_key(left), selector_key(right)],
        "roots": [left.get("selectedPointerHex"), right.get("selectedPointerHex")],
        "unionMaps": sorted(union),
        "unionEqualsCurrent": union == current_maps,
        "unionCoversCurrent": current_maps <= union,
        "extraVsCurrent": sorted(union - current_maps),
        "missingVsCurrent": sorted(current_maps - union),
        "containsSource": SOURCE in union,
        "containsTarget": TARGET in union,
    }


def build_summary(selectors: list[dict], playable_progress: dict | None = None) -> dict:
    playable_progress = playable_progress or {}
    confirmed_maps = set(playable_progress.get("reachableFromStart") or [])
    source_row = find_selector(selectors, SOURCE_SELECTOR)
    predecessor_row = find_selector(selectors, PREDECESSOR_SELECTOR)
    current_row = find_selector(selectors, CURRENT_SELECTOR)
    current_order = (current_row.get("group"), current_row.get("slot"))
    current_maps = set(current_row.get("fieldMaps") or [])
    predecessor_maps = set(predecessor_row.get("fieldMaps") or [])
    source_maps = set(source_row.get("fieldMaps") or [])
    previous_rows = [
        row
        for row in selectors
        if row.get("fieldMaps")
        and (row.get("group"), row.get("slot")) < current_order
    ]
    previous_records = [selector_record(row, current_maps, confirmed_maps) for row in previous_rows]
    pair_rows = [pair_record(left, right, current_maps) for left, right in itertools.combinations(previous_rows, 2)]
    source_predecessor_pair = next(
        (
            row for row in pair_rows
            if row.get("selectors") == [SOURCE_SELECTOR, PREDECESSOR_SELECTOR]
        ),
        {},
    )
    exact_pairs = [row for row in pair_rows if row.get("unionEqualsCurrent")]
    current_equals_predecessor_plus_source = current_maps == (predecessor_maps | {SOURCE})
    source_selector_extra = sorted(source_maps - current_maps)
    current_omits_source_selector_extra = all(item not in current_maps for item in source_selector_extra)
    list_recomposition_pattern_found = (
        current_equals_predecessor_plus_source
        and bool(source_selector_extra)
        and source_predecessor_pair.get("unionCoversCurrent") is True
        and source_predecessor_pair.get("missingVsCurrent") == []
    )
    conclusion = (
        f"Selector {CURRENT_SELECTOR} can be explained as the target-side predecessor selector "
        f"{PREDECESSOR_SELECTOR} plus {SOURCE}, while omitting the source selector's extra confirmed-start map "
        f"{', '.join(source_selector_extra) or 'none'}. The previous {SOURCE_SELECTOR}+{PREDECESSOR_SELECTOR} "
        "union covers the current selector but over-covers it by that extra source-side map, and no previous selector "
        "pair exactly equals the current route-pair map set. This supports a list-recomposition shape, but it still "
        "does not prove that gameplay executes 0:0, then 1:0, then 2:0 or that the map1_01a->map2_02d edge has a "
        "strict source hotspot."
    )
    return {
        "source": SOURCE,
        "target": TARGET,
        "sourceSelector": SOURCE_SELECTOR,
        "predecessorSelector": PREDECESSOR_SELECTOR,
        "currentSelector": CURRENT_SELECTOR,
        "sourceRootHex": source_row.get("selectedPointerHex"),
        "predecessorRootHex": predecessor_row.get("selectedPointerHex"),
        "currentRootHex": current_row.get("selectedPointerHex"),
        "sourceMaps": source_row.get("fieldMaps") or [],
        "predecessorMaps": predecessor_row.get("fieldMaps") or [],
        "currentMaps": current_row.get("fieldMaps") or [],
        "confirmedReachableFromStart": sorted(confirmed_maps),
        "previousSelectors": previous_records,
        "previousPairUnions": pair_rows,
        "exactPreviousSelectorUnionCount": len(exact_pairs),
        "exactPreviousSelectorUnions": exact_pairs,
        "sourcePredecessorUnionCoversCurrent": source_predecessor_pair.get("unionCoversCurrent"),
        "sourcePredecessorUnionExtraMaps": source_predecessor_pair.get("extraVsCurrent") or [],
        "sourcePredecessorUnionMissingMaps": source_predecessor_pair.get("missingVsCurrent") or [],
        "currentEqualsPredecessorPlusSource": current_equals_predecessor_plus_source,
        "sourceSelectorExtraMapsOmittedByCurrent": source_selector_extra,
        "currentOmitsSourceSelectorExtraMaps": current_omits_source_selector_extra,
        "listRecompositionPatternFound": list_recomposition_pattern_found,
        "executionOrderProven": False,
        "strictHotspotFound": False,
        "proofFound": False,
        "selectorSetDecompositionProofFound": False,
        "failedSelectorSetDecompositionGateIds": FAILED_SELECTOR_SET_DECOMPOSITION_GATE_IDS,
        "missingEvidence": SELECTOR_SET_DECOMPOSITION_MISSING_EVIDENCE,
        "evidenceRefs": SELECTOR_SET_DECOMPOSITION_EVIDENCE_REFS,
        "evidenceRefCount": len(SELECTOR_SET_DECOMPOSITION_EVIDENCE_REFS),
        "promotionStatus": "blocked",
        "remainingProofs": SELECTOR_SET_DECOMPOSITION_MISSING_EVIDENCE,
        "conclusion": conclusion,
    }


def markdown(summary: dict) -> str:
    lines = [
        "# Save Selector Set Decomposition",
        "",
        f"- route: `{summary['source']} -> {summary['target']}`",
        f"- source selector: `{summary['sourceSelector']}` root `{summary['sourceRootHex']}`",
        f"- predecessor selector: `{summary['predecessorSelector']}` root `{summary['predecessorRootHex']}`",
        f"- current selector: `{summary['currentSelector']}` root `{summary['currentRootHex']}`",
        f"- current equals predecessor plus source: {summary['currentEqualsPredecessorPlusSource']}",
        f"- source+predecessor union covers current: {summary['sourcePredecessorUnionCoversCurrent']}",
        f"- source+predecessor union extra maps: {', '.join(summary['sourcePredecessorUnionExtraMaps']) or 'none'}",
        f"- exact previous selector union count: {summary['exactPreviousSelectorUnionCount']}",
        f"- list recomposition pattern found: {summary['listRecompositionPatternFound']}",
        f"- execution order proven: {summary['executionOrderProven']}",
        f"- proof found: {summary['proofFound']}",
        f"- failed selector-set decomposition gates: {', '.join(summary['failedSelectorSetDecompositionGateIds'])}",
        f"- missing evidence count: {len(summary['missingEvidence'])}",
        f"- evidence refs: {summary.get('evidenceRefCount')}",
        f"- promotion status: `{summary['promotionStatus']}`",
        "",
        summary["conclusion"],
        "",
        "## Previous Selectors",
        "",
        "| selector | root | maps | subset of current | extra | missing | confirmed overlap |",
        "| --- | --- | --- | --- | --- | --- | --- |",
    ]
    for row in summary["previousSelectors"]:
        lines.append(
            f"| `{row['selector']}` | `{row['rootHex']}` | {', '.join(row['fieldMaps'])} | "
            f"{row['isSubsetOfCurrent']} | {', '.join(row['extraVsCurrent']) or '-'} | "
            f"{', '.join(row['missingVsCurrent']) or '-'} | {', '.join(row['confirmedOverlap']) or '-'} |"
        )
    lines.extend([
        "",
        "## Pair Unions",
        "",
        "| selectors | equals current | covers current | extra | missing |",
        "| --- | --- | --- | --- | --- |",
    ])
    for row in summary["previousPairUnions"]:
        lines.append(
            f"| `{row['selectors'][0]}` + `{row['selectors'][1]}` | {row['unionEqualsCurrent']} | "
            f"{row['unionCoversCurrent']} | {', '.join(row['extraVsCurrent']) or '-'} | "
            f"{', '.join(row['missingVsCurrent']) or '-'} |"
        )
    lines.extend(["", "## Remaining Proofs", ""])
    lines.extend(f"- {item}" for item in summary["remainingProofs"])
    lines.append("")
    return "\n".join(lines)


def html_page(summary: dict) -> str:
    previous_rows = "\n".join(
        "<tr>"
        f"<td><code>{html.escape(row['selector'])}</code></td>"
        f"<td><code>{html.escape(row['rootHex'])}</code></td>"
        f"<td>{html.escape(', '.join(row['fieldMaps']))}</td>"
        f"<td>{row['isSubsetOfCurrent']}</td>"
        f"<td>{html.escape(', '.join(row['extraVsCurrent']) or '-')}</td>"
        f"<td>{html.escape(', '.join(row['missingVsCurrent']) or '-')}</td>"
        f"<td>{html.escape(', '.join(row['confirmedOverlap']) or '-')}</td>"
        "</tr>"
        for row in summary["previousSelectors"]
    )
    pair_rows = "\n".join(
        "<tr>"
        f"<td><code>{html.escape(row['selectors'][0])}</code> + <code>{html.escape(row['selectors'][1])}</code></td>"
        f"<td>{row['unionEqualsCurrent']}</td>"
        f"<td>{row['unionCoversCurrent']}</td>"
        f"<td>{html.escape(', '.join(row['extraVsCurrent']) or '-')}</td>"
        f"<td>{html.escape(', '.join(row['missingVsCurrent']) or '-')}</td>"
        "</tr>"
        for row in summary["previousPairUnions"]
    )
    proofs = "".join(f"<li>{html.escape(item)}</li>" for item in summary["remainingProofs"])
    return "\n".join([
        "<!doctype html>",
        '<html lang="en">',
        "<head>",
        '  <meta charset="utf-8">',
        '  <meta name="viewport" content="width=device-width, initial-scale=1">',
        "  <title>Save Selector Set Decomposition</title>",
        "  <style>body{font-family:system-ui,sans-serif;background:#111;color:#eee;margin:24px}table{border-collapse:collapse;width:100%;max-width:1180px}td,th{border:1px solid #333;padding:6px 8px;text-align:left;vertical-align:top}th{background:#1f1f1f}code{color:#9bd4ff}</style>",
        "</head>",
        "<body>",
        "  <h1>Save Selector Set Decomposition</h1>",
        f"  <p>route <code>{summary['source']} -> {summary['target']}</code>; source <code>{summary['sourceSelector']}</code>; predecessor <code>{summary['predecessorSelector']}</code>; current <code>{summary['currentSelector']}</code>; promotion status <code>{summary['promotionStatus']}</code>.</p>",
        f"  <p>current equals predecessor plus source: {summary['currentEqualsPredecessorPlusSource']}; source+predecessor union covers current: {summary['sourcePredecessorUnionCoversCurrent']}; source+predecessor union extra maps: {html.escape(', '.join(summary['sourcePredecessorUnionExtraMaps']) or 'none')}; exact previous selector union count: {summary['exactPreviousSelectorUnionCount']}; list recomposition pattern found: {summary['listRecompositionPatternFound']}; execution order proven: {summary['executionOrderProven']}.</p>",
        f"  <p>proof found <code>{summary['proofFound']}</code>; failed selector-set decomposition gates <code>{html.escape(','.join(summary['failedSelectorSetDecompositionGateIds']))}</code>; missing evidence <code>{len(summary['missingEvidence'])}</code>; evidence refs <code>{summary.get('evidenceRefCount')}</code>.</p>",
        f"  <p>{html.escape(summary['conclusion'])}</p>",
        "  <h2>Previous Selectors</h2>",
        "  <table><thead><tr><th>selector</th><th>root</th><th>maps</th><th>subset</th><th>extra</th><th>missing</th><th>confirmed overlap</th></tr></thead><tbody>",
        previous_rows,
        "  </tbody></table>",
        "  <h2>Pair Unions</h2>",
        "  <table><thead><tr><th>selectors</th><th>equals current</th><th>covers current</th><th>extra</th><th>missing</th></tr></thead><tbody>",
        pair_rows,
        "  </tbody></table>",
        "  <h2>Remaining Proofs</h2>",
        f"  <ul>{proofs}</ul>",
        "</body>",
        "</html>",
        "",
    ])


def write_outputs(summary: dict, out_dir: Path = OUT) -> None:
    out_dir.mkdir(parents=True, exist_ok=True)
    (out_dir / "save_selector_set_decomposition.json").write_text(
        json.dumps(summary, ensure_ascii=False, indent=2) + "\n",
        encoding="utf-8",
    )
    (out_dir / "save_selector_set_decomposition.html").write_text(html_page(summary), encoding="utf-8")


def main() -> None:
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument("--out-dir", type=Path, default=OUT)
    args = parser.parse_args()
    summary = build_summary(
        load_json(args.out_dir / "save_scene_selectors.json", []),
        load_json(args.out_dir / "playable_progress.json", {}),
    )
    write_outputs(summary, args.out_dir)
    print(f"wrote save selector set decomposition -> {args.out_dir / 'save_selector_set_decomposition.html'}")


if __name__ == "__main__":
    main()