#!/usr/bin/env python3
"""Observe-stage rule checks for 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- (pilot #2).

Notation: S(r) := 0^inf 11 D> <r> 0^inf, r a word over digits L=110, 0=000, 1=100 (left to right).
Sweep rule: S(r) -->+ S(eat(r)), one cell further left (wall moves left by 1 per sweep).
eat = SOMDCv6.v TM7's RIncs (hx, k=0) plus two new clauses: every L the eater meets adds +1
to the rest of the word (little-endian binary over the 0/1 digits, L digits skipped).

Run:  python3 -B check_rules.py [max_steps]     (default 1e9; ~20 s)
      python3 -B check_rules.py --orbit 2000      (abstract sweeps only, no TM simulation)
      python3 -B check_rules.py --lentry          (only the A1 / L-entry rules, ours vs TM7)
"""
import itertools
import random
import re
import sys

sys.path.insert(0, "[local working file]")
import sim  # noqa: E402

TM = "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---"
TM7 = "1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---"   # SOMDCv6 TM7: same except A1 = 0RC
INV = {"L": "110", "0": "000", "1": "100"}
DIG = {v: k for k, v in INV.items()}


# ---------- abstract rules ----------
def add(r, i, p):
    """Add p to the little-endian number formed by the non-L digits of r[i:] (in place; may append)."""
    carry, j = p, i
    while carry and j < len(r):
        if r[j] != "L":
            t = (r[j] == "1") + carry
            r[j] = "1" if t % 2 else "0"
            carry = t // 2
        j += 1
    while carry:
        r.append("1" if carry % 2 else "0")
        carry //= 2


def inc(x):
    r = list(x)
    add(r, 0, 1)
    return "".join(r)


def eat(r0, new_clauses=True):
    """TM7 RIncs(hx,0,r) as a function; new_clauses=False gives TM7/TM8 exactly. None = outside the domain."""
    r, out, tp, k, i, p = list(r0), [], "hx", 0, 0, 0
    while True:
        if p and (i == len(r) or r[i] != "L"):   # lazy: L digits are never changed by +1
            add(r, i, p)
            p = 0
        if i == len(r):
            if tp == "hx":
                return None
            while True:  # count mode at the right end: write k in TM7's digit code
                if k == 0:
                    out.append("1")
                    return "".join(out)
                if k % 2:
                    out.append("0"); k = (k - 1) // 2
                else:
                    out.append("1"); k = (k - 2) // 2
        d = r[i]; i += 1
        if tp == "hx":                      # eater
            if d == "L":
                out.append("L"); k += 1; p += new_clauses        # NEW: +1 to the rest
            elif d == "0":
                out.append("L"); k += 1
            else:
                out.append("L"); tp = "h1"
        else:                               # count mode, k passes
            if k == 0:
                return None
            if d == "L":
                out.append("L"); tp = "hx"; p += new_clauses        # NEW: +1 to the rest
            elif d == "1":
                out.append("L"); k -= 1
            elif k % 2:
                out.append("0"); k = (k - 1) // 2
            else:
                out.append("1"); k = (k - 2) // 2


# ---------- checks ----------
def from_blank(max_steps):
    m = sim.parse(TM)
    seq = []
    for ev in sim.events(m, max_steps=max_steps, on_record=True, snapshot=True):
        if ev.side != "L":
            continue
        c = ev.config
        tape, h = "".join(map(str, c.tape)), c.head
        assert c.state == "D" and tape[h] == "0" and tape[h + 1] == "0"
        r = tape[h + 2:].rstrip("0")
        r += "0" * ((-len(r)) % 3)
        seq.append((ev.step + 2, ev.pos + 2, "".join(DIG.get(r[i:i + 3], "?") for i in range(0, len(r), 3))))
    ok = sum(eat(r0) == r1 and p1 == p0 - 1 for (_, p0, r0), (_, p1, r1) in zip(seq, seq[1:]))
    ok_tm7 = sum(eat(r0, False) == r1 for (_, p0, r0), (_, p1, r1) in zip(seq, seq[1:]))
    return seq, ok, len(seq) - 1, ok_tm7


def next_S(m, r, cap=5 * 10**7):
    """Simulate (own dict simulator) from S(r) to the next S-shaped configuration."""
    T = {}
    for qi, part in enumerate(TM.split("_")):
        for s in range(2):
            t = part[3 * s:3 * s + 3]
            T[(qi, s)] = None if t[2] == "-" else (int(t[0]), 1 if t[1] == "R" else -1, ord(t[2]) - 65)
    tape = {-2: 1, -1: 1}
    for i, d in enumerate(r):
        for j, ch in enumerate(INV[d]):
            tape[3 * i + j] = int(ch)
    pos, q, lo = 0, 3, -2
    for _ in range(cap):
        tr = T[(q, tape.get(pos, 0))]
        if tr is None:
            return "HALT", None
        w, mv, q = tr
        tape[pos] = w
        pos += mv
        lo = min(lo, pos)
        if q == 3 and mv == 1 and tape.get(pos - 1) == 1 and tape.get(pos - 2) == 1 and \
                all(tape.get(k, 0) == 0 for k in range(lo, pos - 2)):
            cells = "".join(str(tape.get(k, 0)) for k in range(pos, max(tape) + 1)).rstrip("0")
            cells += "0" * ((-len(cells)) % 3)
            return "".join(DIG.get(cells[i:i + 3], "?") for i in range(0, len(cells), 3)), pos
    return "TIMEOUT", None


def random_halves(seed=7):
    """S(L X) -> S(0 inc X) (same cell) and S(0 X) -> S(eat(0 X)) (one cell left), random X."""
    random.seed(seed)
    tail = lambda n: "".join(random.choice("L01") for _ in range(n - 1)) + "1"  # noqa: E731
    res = {"P1": [0, 0], "P2": [0, 0]}
    for _ in range(120):
        X = random.choice([tail(random.randint(1, 40)), "L" * random.randint(0, 120) + tail(random.randint(1, 12)),
                           "L" * random.randint(0, 30) + "".join(random.choice("11L") for _ in range(random.randint(0, 15))) + "1"])
        got = next_S(None, "L" + X)
        res["P1"][0] += 1; res["P1"][1] += got == ("0" + inc(X), 0)
    n2 = 0
    while n2 < 174:
        X = random.choice([tail(random.randint(1, 30)), "L" * random.randint(0, 80) + tail(random.randint(1, 10)),
                           "L" * random.randint(5, 60) + tail(random.randint(2, 9))])
        pred = eat("0" + X)
        if pred is None:
            continue                         # outside the rule's domain (not reachable shape)
        n2 += 1
        got = next_S(None, "0" + X)
        res["P2"][0] += 1; res["P2"][1] += got == (pred, -1)
    return res


def norm(cfg):
    t = cfg.trimmed()
    tape, h = "".join(map(str, t.tape)), t.head
    lo, hi = 0, len(tape)
    while lo < h and tape[lo] == "0":
        lo += 1
    while hi > h + 1 and tape[hi - 1] == "0":
        hi -= 1
    return t.state, tape[lo:hi], h - lo


def low_level(seed=11):
    m = sim.parse(TM)
    random.seed(seed)
    def check(lhs, rhs, steps, **v):
        r = sim.run(m, sim.Config.parse(lhs, **v), steps, engine="py")
        return (not r.halted) and r.step == steps and norm(r.final) == norm(sim.Config.parse(rhs, **v))
    rules = {
        "eat0":      ("0^inf 1^(b+2) D> 000^a 100 0^inf", "0^inf 1^(b+2) 111^a D> 100 0^inf", lambda a, b: 3 * a),
        "carry":     ("0^inf 1^b B> 100^a 000 100 0^inf", "0^inf 1^b 000^a <C 100 100 0^inf", lambda a, b: 3 * a + 1),
        "carry_end": ("0^inf 1^b B> 100^a 0^inf", "0^inf 1^b 000^a <C 1 0^inf", lambda a, b: 3 * a + 1),
        "skipL":     ("0^inf 1^b B> 110^a 100 0^inf", "0^inf 1^b 011^a B> 100 0^inf", lambda a, b: 3 * a),
        "ret0":      ("0^inf 1^(b+1) 000^a <C 100 0^inf", "0^inf 1^(b+1) <C 000^a 100 0^inf", lambda a, b: 3 * a),
        "retL":      ("0^inf 1^(b+1) 011^a <C 100 0^inf", "0^inf 1^(b+1) <C 110^a 100 0^inf", lambda a, b: 3 * a),
    }
    out = {}
    for name, (lhs, rhs, f) in rules.items():
        ok = tot = 0
        for _ in range(3):
            for a in [random.randint(0, 3) for _ in range(4)] + [random.randint(4, 40) for _ in range(6)] + \
                     [random.randint(100, 1500) for _ in range(5)]:
                b = random.randint(0, 50)
                tot += 1; ok += check(lhs, rhs, f(a, b), a=a, b=b)
        out[name] = (tot, ok)
    ok = tot = 0
    for _ in range(150):   # eater meets L: 1 D> 110 X  -->  1 111 D> inc(X), 6j+13 steps
        n = random.choice([random.randint(0, 6), random.randint(7, 40), random.randint(41, 200)])
        X = "".join(random.choice("L01" if random.random() > 0.3 else "L1") for _ in range(n)) + "1"
        b = random.randint(0, 30)
        j = len(X.split("0")[0]) if "0" in X else len(X)
        lhs = "0^inf 1^%d D> 110 %s 0^inf" % (b + 2, "".join(INV[d] for d in X))
        rhs = "0^inf 1^%d 111 D> %s 0^inf" % (b + 2, "".join(INV[d] for d in inc(X)))
        tot += 1; ok += check(lhs, rhs, 6 * j + 13)
    out["eatL_inc"] = (tot, ok)
    return out


def l_entry(n_random=300, seed=5):
    """A1 fires once each time an L (110) is entered: by the eater (1 D> 110 X) or by a drain pass (B> 1 110 X).
    Ours: -> 1 111 D> inc(X) in 6j+13 (eater) / 6j+12 (drain) steps, j = digits before the first 000 in X.
    TM7:  -> 1 111 D> X in 11 / 10 steps. X = every word of <= 6 digits, plus n_random random words of 7-60."""
    random.seed(seed)
    words = ["".join(w) for n in range(7) for w in itertools.product("L01", repeat=n)]
    words += ["".join(random.choice("L01") for _ in range(random.randint(7, 60))) for _ in range(n_random)]
    enc = lambda w: " ".join(INV[d] for d in w)  # noqa: E731
    out = {}
    for tm, name in ((TM, "ours"), (TM7, "tm7")):
        m = sim.parse(tm)
        for ctx, lead, k in (("eater", "1 D> 110", 13), ("drain", "B> 1 110", 12)):
            ok = 0
            for X in words:
                b = random.randint(0, 20)
                j = len(X.split("0")[0]) if "0" in X else len(X)
                Y, steps = (inc(X), 6 * j + k) if tm == TM else (X, k - 2)
                lhs = f"0^inf 1^{b + 1} {lead} {enc(X)} 0^inf"
                rhs = f"0^inf 1^{b + 1} 1 111 D> {enc(Y)} 0^inf"
                r = sim.run(m, sim.Config.parse(lhs), steps, engine="py")
                ok += (not r.halted) and r.step == steps and norm(r.final) == norm(sim.Config.parse(rhs))
            out[f"{name}_{ctx}"] = (len(words), ok)
    return out


def orbit(max_sweeps, max_seconds=200):
    """Iterate the abstract sweep map from S(L1) (step 16); report whether it ever leaves eat's domain."""
    import time
    t0, r = time.time(), "L1"
    for i in range(max_sweeps):
        r2 = eat(r)
        if r2 is None:
            return f"LEFT THE DOMAIN after {i} sweeps at r={r[:80]}"
        r = r2
        if time.time() - t0 > max_seconds:
            break
    n = len(re.match("L*", r).group(0))
    return f"{i + 1} sweeps in domain; now S(L^{n} {r[n:]})"


if __name__ == "__main__":
    if len(sys.argv) > 1 and sys.argv[1] == "--lentry":
        print("L entry (A1), (instances, passed):", l_entry())
        sys.exit()
    if len(sys.argv) > 2 and sys.argv[1] == "--orbit":
        print(orbit(int(sys.argv[2])))
        sys.exit()
    N = int(float(sys.argv[1])) if len(sys.argv) > 1 else 10**9
    seq, ok, tot, ok_tm7 = from_blank(N)
    n_L = len(re.match("L*", seq[-1][2]).group(0))
    print(f"from blank: {len(seq)} left records to {N:.0e}; sweep rule {ok}/{tot}; TM7 rule alone {ok_tm7}/{tot}; "
          f"last S(L^{n_L} {seq[-1][2][n_L:]}) at step {seq[-1][0]}")
    print("random halves:", random_halves())
    print("low-level:", low_level())
    print("L entry (A1), (instances, passed):", l_entry())