#!/usr/bin/env python3
"""Atlas UMMO: finite calculations, not a recovered UMMO logic.

Python 3, standard library only. Run with --output resultats.json to save.
Source conventions and scope: README.md. All sets use the independent
frozenset implementation here; the website uses bit masks.
"""
import argparse
import itertools
import json
from pathlib import Path

VALUES = ("T", "F", "B", "N")
BITS = {"T": (1, 0), "F": (0, 1), "B": (1, 1), "N": (0, 0)}
FROM_BITS = {v: k for k, v in BITS.items()}
U = frozenset("abcd")
S = {"T": frozenset("ac"), "F": frozenset("bc"), "B": frozenset("c"), "N": frozenset("d")}

def neg(p):
    t, f = BITS[p]
    return FROM_BITS[(f, t)]

def conjunction(p, q):
    pt, pf = BITS[p]; qt, qf = BITS[q]
    return FROM_BITS[(pt and qt, pf or qf)]

def disjunction(p, q):
    pt, pf = BITS[p]; qt, qf = BITS[q]
    return FROM_BITS[(pt or qt, pf and qf)]

def designated(p):
    return BITS[p][0] == 1

def encode(s):
    return sum(1 << i for i, name in enumerate("abcd") if name in s)

def check_law(name, cases):
    rows = list(cases)
    assert all(rows), name
    return {"name": name, "assignments": len(rows), "passed": True}

def main():
    checks = []
    checks.append(check_law("FDE: double negation", (neg(neg(p)) == p for p in VALUES)))
    checks.append(check_law("FDE: idempotence AND and OR", (conjunction(p,p)==p and disjunction(p,p)==p for p in VALUES)))
    checks.append(check_law("FDE: two De Morgan laws", (neg(conjunction(p,q))==disjunction(neg(p),neg(q)) and neg(disjunction(p,q))==conjunction(neg(p),neg(q)) for p,q in itertools.product(VALUES,repeat=2))))
    checks.append(check_law("FDE: two distributivity laws", (conjunction(p,disjunction(q,r))==disjunction(conjunction(p,q),conjunction(p,r)) and disjunction(p,conjunction(q,r))==conjunction(disjunction(p,q),disjunction(p,r)) for p,q,r in itertools.product(VALUES,repeat=3))))
    # Independently transcribed Table 1, Coniglio et al., 2212.01677v1, p.4.
    # Reordered from (T,B,N,F) to (T,F,B,N).
    paper_and = [list(x) for x in ("TFBN", "FFFF", "BFBF", "NFFN")]
    paper_or = [list(x) for x in ("TTTT", "TFBN", "TBBT", "TNTN")]
    fde_and = [[conjunction(p,q) for q in VALUES] for p in VALUES]
    fde_or = [[disjunction(p,q) for q in VALUES] for p in VALUES]
    assert fde_and == paper_and
    assert fde_or == paper_or
    checks.append({"name":"FDE: 32 cells of published AND/OR tables", "assignments":32,"passed":True})
    sets = [frozenset(c) for n in range(5) for c in itertools.combinations("abcd", n)]
    checks.append(check_law("Set complement: involution", (U-(U-a)==a for a in sets)))
    checks.append(check_law("Sets: absorption and De Morgan", (a|(a&b)==a and a&(a|b)==a and U-(a|b)==(U-a)&(U-b) and U-(a&b)==(U-a)|(U-b) for a,b in itertools.product(sets,repeat=2))))
    closure = set(S.values())
    while True:
        old = set(closure)
        closure |= {U-a for a in old}
        closure |= {a&b for a,b in itertools.product(old,repeat=2)}
        closure |= {a|b for a,b in itertools.product(old,repeat=2)}
        if closure == old: break
    assert closure == set(sets)
    nanty_and = [[encode(S[p]&S[q]) for q in VALUES] for p in VALUES]
    nanty_or = [[encode(S[p]|S[q]) for q in VALUES] for p in VALUES]
    # Article 8, displayed AND and OR tables (including composite entries).
    assert nanty_and == [[5,4,4,0],[4,6,4,0],[4,4,4,0],[0,0,0,8]]
    assert nanty_or == [[5,7,5,13],[7,6,6,14],[5,6,4,12],[13,14,12,8]]
    assert [encode(U-S[p]) for p in VALUES] == [10,9,11,7]
    checks.append({"name":"Nanty: 36 cells of published NOT/AND/OR tables", "assignments":36,"passed":True})
    discrepancies = [
        {"expression":"T ∨ N = ¬F", "left":encode(S['T']|S['N']),"right":encode(U-S['F']),"correction":"T ∨ N = ¬f"},
        {"expression":"F ∨ N = ¬T", "left":encode(S['F']|S['N']),"right":encode(U-S['T']),"correction":"F ∨ N = ¬t"},
        {"expression":"N ∨ B = N", "left":encode(S['N']|S['B']),"right":encode(S['N']),"correction":"N ∨ B = ¬(t ∨ f)"},
        {"expression":"F ↔ F = N", "left":encode((U-S['N'])&(U-S['N'])),"right":encode(S['N']),"correction":"F ↔ F = ¬N, given the stated axiom F → F = ¬N"},
    ]
    assert all(x['left']!=x['right'] for x in discrepancies)
    cases = list(itertools.product(VALUES,repeat=2))
    explosion = [{"p":p,"q":q} for p,q in cases if designated(p) and designated(neg(p)) and not designated(q)]
    elimination = [{"p":p,"q":q} for p,q in cases if designated(conjunction(p,q)) and not designated(p)]
    syllogism = [{"p":p,"q":q} for p,q in cases if designated(disjunction(p,q)) and designated(neg(p)) and not designated(q)]
    assert explosion == [{"p":"B","q":"F"},{"p":"B","q":"N"}]
    assert elimination == []
    assert syllogism == [{"p":"B","q":"F"},{"p":"B","q":"N"}]
    complement_rows = []
    for atom in "abcd":
        start = frozenset(atom)
        once = U-start
        repeated = frozenset().union(*(U-frozenset(x) for x in once))
        assert repeated == U
        complement_rows.append({"input":encode(start),"once":encode(once),"set_twice":encode(U-once),"relation_twice":encode(repeated)})
    return {
        "date":"2026-09-17", "scope":"FDE reference; finite set realization of Nanty's NOT/AND/OR fragment; explicitly chosen extensions of NR20 complementation. No recovered complete UMMO logic.",
        "order":list(VALUES), "bits":BITS,
        "fde":{"not":[neg(p) for p in VALUES],"and":fde_and,"or":fde_or,"designated":["T","B"],"excluded_middle":[disjunction(p,neg(p)) for p in VALUES],"explosion_countermodels":explosion,"and_elimination_countermodels":elimination,"disjunctive_syllogism_countermodels":syllogism},
        "nanty":{"sets":{k:encode(v) for k,v in S.items()},"not":[encode(U-S[p]) for p in VALUES],"and":nanty_and,"or":nanty_or,"closure_size":len(closure),"closure_masks":sorted(encode(v) for v in closure),"text_discrepancies":discrepancies},
        "nr20_complement":complement_rows,"checks":checks,
    }

if __name__ == '__main__':
    parser=argparse.ArgumentParser(description=__doc__)
    parser.add_argument('--output', type=Path)
    args=parser.parse_args()
    data=json.dumps(main(),ensure_ascii=False,indent=2)+'\n'
    if args.output:
        args.output.write_text(data,encoding='utf-8')
        print('Calculs reproduits et contrôlés :',args.output)
    else:
        print(data,end='')