#!/usr/bin/env python3
"""Finite examples for the written residual/locality theorem, not its proof."""
from dataclasses import dataclass
from itertools import product
import json


def words(alphabet, maximum):
    return [''.join(w) for n in range(maximum + 1) for w in product(alphabet, repeat=n)]


@dataclass(frozen=True)
class Rope:
    kind: str
    meaning: str
    transform: tuple
    children: tuple = ()


# Three-state DFA for words ending in ab; tags are full transformations.
TRANSITIONS = {'a': (1, 1, 1), 'b': (0, 2, 0)}


def transformation(w):
    answer = (0, 1, 2)
    for c in w:
        answer = tuple(TRANSITIONS[c][q] for q in answer)
    return answer


EMPTY = Rope('E', '', (0, 1, 2))
LETTERS = {c: Rope(c, c, TRANSITIONS[c]) for c in 'ab'}


def join(x, y):
    # Only the two finite root tags and old root handles are used.
    mu = tuple(y.transform[q] for q in x.transform)
    return Rope('Cat', x.meaning + y.meaning, mu, (x, y))


def build(w):
    h = EMPTY
    for c in w:
        h = join(h, LETTERS[c])
    return h


def flatten(h):
    if h.kind == 'Cat':
        return flatten(h.children[0]) + flatten(h.children[1])
    return '' if h.kind == 'E' else h.kind


@dataclass(frozen=True)
class Stack:
    bracket: str
    tail: object


@dataclass(frozen=True)
class Configuration:
    error: bool
    stack: object


INITIAL = Configuration(False, None)


def step(h, c):
    if c in '([':
        return Configuration(h.error, Stack(c, h.stack))
    if h.stack is None:
        return Configuration(True, None)
    expected = '(' if c == ')' else '['
    return Configuration(h.error or h.stack.bracket != expected, h.stack.tail)


def query(h):
    return not h.error and h.stack is None


def dyck_reference(w):
    stack = []
    for c in w:
        if c in '([':
            stack.append(c)
        elif not stack or stack.pop() != ('(' if c == ')' else '['):
            return False
    return not stack


def view(h, radius):
    # Root header at depth0, stack top at depth1; no pointer-identity facts.
    def stack_view(s, remaining):
        if s is None:
            return ('bottom',)
        if remaining == 0:
            return (s.bracket,)
        return (s.bracket, stack_view(s.tail, remaining - 1))
    return ('header', h.error) if radius == 0 else ('header', h.error, stack_view(h.stack, radius - 1))


def run():
    ws = words('ab', 5)
    hs = {w: build(w) for w in ws}
    join_cases = 0
    for x, y in product(ws, repeat=2):
        old_x, old_y = hs[x], hs[y]
        h = join(old_x, old_y)
        assert h.transform == transformation(x + y)
        assert flatten(h) == x + y
        assert (h.transform[0] == 2) == (x + y).endswith('ab')
        assert old_x.meaning == x and old_y.meaning == y
        join_cases += 1
    # Reached state alone fails the finite-algebra test: epsilon and b agree
    # from q0, but differ when used as right operands after a.
    assert transformation('')[0] == transformation('b')[0]
    assert not 'a'.endswith('ab') and 'ab'.endswith('ab')
    streaming_cases = 0
    for w in words('()[]', 7):
        h = INITIAL
        retained = [(h, '')]
        for i, c in enumerate(w, 1):
            h = step(h, c)
            retained.append((h, w[:i]))
        assert query(h) == dyck_reference(w)
        for old, prefix in retained:
            assert query(old) == dyck_reference(prefix)
            fork = step(old, '(')
            assert not query(fork)
            assert query(old) == dyck_reference(prefix)
        streaming_cases += 1
    examples = []
    for radius in range(7):
        x, y = '[' + '(' * radius, '(' + '(' * radius
        hx, hy = INITIAL, INITIAL
        for c in x:
            hx = step(hx, c)
        for c in y:
            hy = step(hy, c)
        assert view(hx, radius) == view(hy, radius)
        z = ')' * radius + ']'
        assert dyck_reference(x + z) and not dyck_reference(y + z)
        examples.append({'radius': radius, 'x': x, 'y': y, 'suffix': z})
    def balance(w):
        total, low = 0, 0
        for c in w:
            total += 1 if c == '(' else -1
            low = min(low, total)
        return total, low
    scalar_cases = 0
    for x, y in product(words('()', 4), repeat=2):
        bx, mx = balance(x)
        by, my = balance(y)
        joined = (bx + by, min(mx, bx + my))
        assert joined == balance(x + y)
        assert (joined[0] == 0 and joined[1] >= 0) == dyck_reference(x + y)
        scalar_cases += 1
    return {'scope': 'Finite example models only. All binary words through length5 paired in a transition-monoid-tagged rope model; Dyck2 streaming words through length7 with retained-version/fork controls; seven same-view distinct-future stack examples. The models do not implement a local Dyck join, quantify over arbitrary representations, or formally prove the universal theorem.',
            'regular_join_cases': join_cases,
            'Dyck_streaming_cases': streaming_cases,
            'same_view_distinct_future_examples': examples,
            'growing_integer_Dyck1_control': {'word_length_limit_per_operand': 4, 'pairs': scalar_cases,
                                             'scope': 'Unit-cost unbounded integers, outside the fixed finite-label theorem.'},
            'finite_state_only_right_operand_control': 'epsilon and b reach the same DFA state from q0, but a and ab have different acceptance',
            'formal_verification': 'No proof assistant; universal argument is written separately.'}


if __name__ == '__main__':
    print(json.dumps(run(), indent=2))