"""
Recensorium corpus census - Tier A mechanical verifier.
Re-executes every deterministically checkable claim in the 70-paper corpus.
Emits rc_audit/results.json with one row per paper.
"""
import json, os, re, itertools
from math import comb, floor, ceil, log

BODIES = r"C:\Users\jack\rc_corpus\bodies"
OUT    = r"C:\Users\jack\rc_audit\results.json"

# ---------- generic helpers ----------

def fences(body):
    """Return list of (lang_line, content) for each fenced block."""
    out = []
    parts = re.split(r"^```(\S*)[ \t]*\r?\n", body, flags=re.M)
    # parts: [pre, lang, content, pre, lang, content, ...]
    for i in range(1, len(parts) - 1, 2):
        out.append((parts[i], parts[i + 1]))
    return out

def parse_int_blocks(content):
    """Parse lines of integers -> list of tuples; None if not integer lines."""
    lines = [l.strip() for l in content.strip().splitlines() if l.strip()]
    rows = []
    for l in lines:
        if not re.fullmatch(r"[0-9 \t]+", l):
            return None
        rows.append(tuple(int(x) for x in l.split()))
    return rows if rows else None

def parse_bitstrings(content):
    lines = [l.strip() for l in content.strip().splitlines() if l.strip()]
    rows = []
    for l in lines:
        if not re.fullmatch(r"[01]+", l):
            return None
        rows.append(l)
    return rows if rows else None

# ---------- domain checks ----------

def check_cwc(rows, n, d, w):
    """Constant-weight code: rows are position tuples."""
    errs = []
    M = len(rows)
    if len(set(rows)) != M: errs.append("duplicate codewords")
    for r in rows:
        if len(r) != w: errs.append(f"weight {len(r)} != {w}")
        if min(r) < 0 or max(r) >= n: errs.append(f"index out of range: {max(r)} >= n={n}")
    t = w - d // 2          # max allowed intersection
    bad = 0
    for a, b in itertools.combinations(rows, 2):
        if len(set(a) & set(b)) > t: bad += 1
    if bad: errs.append(f"{bad} pairs exceed intersection {t}")
    return {"valid": not errs, "M": M, "errors": errs[:5], "pairs_bad": bad}

def check_binary(rows, n, d):
    errs = []
    M = len(rows)
    if len(set(rows)) != M: errs.append("duplicate codewords")
    lens = set(len(r) for r in rows)
    if lens != {n}: errs.append(f"lengths {sorted(lens)} != {n}")
    bad = 0
    for a, b in itertools.combinations(rows, 2):
        dist = sum(x != y for x, y in zip(a, b))
        if dist < d: bad += 1
    if bad: errs.append(f"{bad} pairs below distance {d}")
    return {"valid": not errs, "M": M, "errors": errs[:5], "pairs_bad": bad}

def schonheim(n, w, lam):
    """Iterated Schoenheim-type packing bound P(n,w,lam). Verified against quoted values."""
    def P(nn, ww, ll):
        if ll <= 0: return nn // ww
        return (nn * P(nn - 1, ww - 1, ll - 1)) // ww   # floor of product chain
    return P(n, w, lam)

def check_sorting_network(content, claimed_comps=None, n_guess=None):
    """Parse comparators 'i j' per line; simulate on all 2^n inputs."""
    comps = []
    maxidx = -1
    for l in content.strip().splitlines():
        l = l.strip()
        m = re.fullmatch(r"(\d+)\s+(\d+)", l)
        if not m: return None
        a, b = int(m.group(1)), int(m.group(2))
        if a == b: return None
        comps.append((a, b)); maxidx = max(maxidx, a, b)
    n = n_guess or (maxidx + 1)
    if n > 16: return None
    fails = 0
    for bits in range(1 << n):
        v = [(bits >> (n - 1 - i)) & 1 for i in range(n)]
        for a, b in comps:
            if v[a] > v[b]: v[a], v[b] = v[b], v[a]
        if any(v[i] > v[i + 1] for i in range(n - 1)):
            fails += 1
            if fails > 3: break
    return {"n": n, "comparators": len(comps), "valid": fails == 0,
            "claimed": claimed_comps, "fails": fails}

def check_coloring_ap(content, n=None, k=None, L=7):
    """Lines of k symbols over Z_n; check no monochromatic L-term AP."""
    lines = [l.strip() for l in content.strip().splitlines() if l.strip()]
    if len(lines) != 1: 
        grid = "".join(lines)
    else:
        grid = lines[0]
    if not re.fullmatch(r"[A-Za-z0-9]+", grid): return None
    colors = sorted(set(grid))
    kk = k or len(colors)
    N = n or len(grid)
    if len(grid) != N: return None
    viol = []
    for c in colors[:kk]:
        pos = [i for i, ch in enumerate(grid) if ch == c]
        s = set(pos)
        for a in range(N):
            for step in range(1, (N - 1) // (L - 1) + 1):
                if a + step * (L - 1) >= N: break
                if all(a + j * step in s for j in range(L)):
                    viol.append((c, a, step))
                    if len(viol) > 3: break
    return {"N": N, "colors_used": len(colors), "valid": not viol, "violations": viol[:3],
            "L": L}

# ---------- claim extraction ----------

NUM = lambda s: int(s.replace(",", ""))

def extract_cwc_claim(text):
    """Find (n, d, w, size) from title+abstract."""
    t = text
    ns = re.findall(r"\bn\s*=\s*(\d+)", t)
    ds = re.findall(r"\bd\s*=\s*(\d+)", t)
    ws = re.findall(r"\bw\s*=\s*(\d+)", t)
    sz = re.search(r"\bsize[^\d]{0,10}(\d+)", t, re.I)
    sz2 = re.search(r"\b(\d+)[-\s]?(?:word|codeword)", t, re.I)
    sz3 = re.search(r"(?:of|with parameters[^\]]*?)\bsize\s+(\d+)", t, re.I)
    if ns and ds and ws and (sz or sz2 or sz3):
        size = NUM(sz.group(1)) if sz else (NUM(sz2.group(1)) if sz2 else NUM(sz3.group(1)))
        return dict(n=NUM(ns[0]), d=NUM(ds[0]), w=NUM(ws[0]), size=size)
    return None

def extract_schoenheim_quotes(text):
    """Quoted Schoenheim bound values."""
    vals = []
    for m in re.finditer(r"Sch[oö]nh(?:e|eim)[^.\n]{0,80}?(\d{1,4})", text, re.I):
        vals.append(NUM(m.group(1)))
    return vals

def classify_paper(p):
    body = p.get("body", "") or ""
    text = p.get("title", "") + " " + (p.get("abstract") or "")
    fcls = []
    for lang, content in fences(body):
        rows = parse_int_blocks(content)
        bits = parse_bitstrings(content)
        cwc_claim = extract_cwc_claim(text)
        entry = {"lang": lang, "kind": "unknown", "lines": len([l for l in content.splitlines() if l.strip()])}
        if rows and cwc_claim and all(len(r) == cwc_claim["w"] for r in rows if r):
            entry["kind"] = "int_rows"
            entry["data"] = rows
        elif bits:
            entry["kind"] = "bits"
            entry["data"] = bits
        elif rows:
            entry["kind"] = "int_rows_generic"
            entry["data"] = rows
        else:
            net = check_sorting_network(content)
            if net:
                entry["kind"] = "sorting_network"; entry["result"] = net
            else:
                col = check_coloring_ap(content)
                if col:
                    entry["kind"] = "coloring"; entry["result"] = col
        fcls.append(entry)
    return fcls

def main():
    papers = []
    for fn in sorted(os.listdir(BODIES)):
        if fn.endswith(".json"):
            papers.append(json.load(open(os.path.join(BODIES, fn), encoding="utf-8")))

    results = []
    for p in papers:
        pid = p["paper_id"]
        body = p.get("body", "") or ""
        text = p.get("title", "") + " || " + (p.get("abstract") or "") + " || " + body[:3000]
        row = {"paper_id": pid, "title": p.get("title"), "field": p.get("field"),
               "status": p.get("status"), "agent": (p.get("agent") or {}).get("id"),
               "checks": [], "tierA": False}
        fcls = classify_paper(p)
        cwc_claim = extract_cwc_claim(text)

        for fe in fcls:
            chk = {"block_kind": fe["kind"]}
            if fe["kind"] == "int_rows" and cwc_claim:
                res = check_cwc(fe["data"], **{k: cwc_claim[k] for k in ("n", "d", "w")})
                chk.update(check="constant_weight_code", params=cwc_claim, result=res)
                claimed_M = cwc_claim["size"]
                res["size_matches_claim"] = (res["M"] == claimed_M)
                row["tierA"] = True
            elif fe["kind"] == "bits":
                ns = re.findall(r"\bn\s*=\s*(\d+)", text); ds = re.findall(r"\bd\s*=\s*(\d+)", text)
                Ms = re.findall(r"\bsize[^\d]{0,10}(\d+)", text, re.I)
                if ns and ds:
                    n, d = NUM(ns[0]), NUM(ds[0])
                    res = check_binary(fe["data"], n, d)
                    chk.update(check="binary_code", params={"n": n, "d": d}, result=res)
                    if Ms: res["size_matches_claim"] = (res["M"] == NUM(Ms[0]))
                    row["tierA"] = True
            elif fe["kind"] == "sorting_network":
                chk.update(check="sorting_network", result=fe.get("result"))
                row["tierA"] = True
            elif fe["kind"] == "coloring":
                chk.update(check="coloring", result=fe.get("result"))
                row["tierA"] = True
            row["checks"].append(chk)

        # Schoenheim quote check for CWC papers
        if cwc_claim:
            lam = cwc_claim["w"] - cwc_claim["d"] // 2
            U = schonheim(cwc_claim["n"], cwc_claim["w"], lam)
            quotes = extract_schoenheim_quotes(text)
            row["schoenheim"] = {"computed": U, "quoted": quotes,
                                 "match": (U in quotes) if quotes else None}
        results.append(row)

    os.makedirs(os.path.dirname(OUT), exist_ok=True)
    json.dump(results, open(OUT, "w", encoding="utf-8"), indent=1)
    n_tierA = sum(1 for r in results if r["tierA"])
    print(f"papers={len(results)} tierA_re-executable={n_tierA}")
    for r in results:
        if r["tierA"]:
            line = f"{r['paper_id']} :: "
            for c in r["checks"]:
                res = c.get("result") or {}
                if c.get("check") == "constant_weight_code":
                    line += f"CWC M={res.get('M')} valid={res.get('valid')} match={res.get('size_matches_claim')} | "
                elif c.get("check") == "binary_code":
                    line += f"BIN M={res.get('M')} valid={res.get('valid')} | "
                elif c.get("check") == "sorting_network":
                    line += f"SORT n={res.get('n')} comps={res.get('comparators')} valid={res.get('valid')} | "
            if "schoenheim" in r:
                s = r["schoenheim"]; line += f"SCH comp={s['computed']} quoted={s['quoted']} match={s['match']}"
            print(line)

if __name__ == "__main__":
    main()