Make truth table in Markdown/LaTeX

gentable.py

term = input("Term: ")

mode = None
while mode not in ("md", "latex", "sat"):
    mode = input("Mode (md/latex/sat): ")


def name(t):
    n = ""
    while t[0] not in " )":
        n += t[0]
        t = t[1:]

    while t[0] == " ":
        t = t[1:]

    return n, t


def parse(t):
    if t[0] != "(":
        n, t = name(t)
        return n, t

    t = t[1:]
    op, t = name(t)
    ex = [op]

    while t[0] != ")":
        op, t = parse(t)
        ex.append(op)

    t = t[1:]
    if len(t) > 0:
        while t[0] == " ":
            t = t[1:]

    return ex, t


expr = parse(term)[0]

vs = set()


def walk(ex):
    for e in ex[1:]:
        if isinstance(e, str):
            vs.update(e)
        else:
            walk(e)


walk(expr)

vs = list(vs)
vs = sorted(vs)


def hashexpr(ex):
    if isinstance(ex, str):
        return ex
    else:
        return "(" + ex[0] + (" " if len(ex) > 1 else "") + " ".join(
            [hashexpr(x) for x in ex[1:]]) + ")"


columns = {}
for v in vs:
    columns[hashexpr(v)] = None


def walk(ex):
    for e in ex[1:]:
        if isinstance(e, list):
            walk(e)

    op = ex[0]
    args = ex[1:]
    match op:
        case "imp":
            assert len(args) == 2
            columns[hashexpr(ex)] = [lambda x, y: not x or y, args[0], args[1]]
        case "not":
            assert len(args) == 1
            columns[hashexpr(ex)] = [lambda x: not x, args[0]]
        case "eq":
            assert len(args) == 2
            columns[hashexpr(ex)] = [lambda x, y: x == y, args[0], args[1]]
        case "or":
            columns[hashexpr(ex)] = [lambda *x: any(x), *args]
        case "and":
            columns[hashexpr(ex)] = [lambda *x: all(x), *args]
        case _:
            raise ValueError(f"Unknown operation '{op}'")


walk(expr)


def render(ex, top=False):
    if top:
        if ex[0] == "(":
            ex = parse(ex)[0]

    r = ""
    if top:
        r += "$"

    if isinstance(ex, str):
        r += ex
    else:
        if not top:
            r += "("

        op = ex[0]
        args = ex[1:]
        match op:
            case "imp":
                r += render(args[0]) + " \\rightarrow " + render(args[1])
            case "not":
                r += "\\lnot " + render(args[0])
            case "eq":
                r += render(args[0]) + " \\leftrightarrow " + render(args[1])
            case "or":
                r += " \\vee ".join([render(x) for x in args])
            case "and":
                r += " \\wedge ".join([render(x) for x in args])
            case _:
                raise ValueError(f"Unknown operation '{op}'")

        if not top:
            r += ")"

    if top:
        r += "$"

    return r


varmap = {}
i = len(vs) - 1
for v in vs:
    varmap[v] = i
    i -= 1
maxstate = 2**len(vs)

match mode:
    case "md":
        print("|" + "|".join([render(x, True) for x in columns.keys()]) + "|")
        print("-".join("|" * (len(columns.keys()) + 1)))
    case "latex":
        print("\\begin{tabular}{ |" + "|".join("c" * len(columns.keys())) +
              "| }")
        print(" \\hline")
        print(" " + " & ".join([render(x, True)
                                for x in columns.keys()]) + " \\\\")
        print(" \\hline")

i = 0
while i < maxstate:
    state = {}
    for v in vs:
        state[hashexpr(v)] = bool(i & (1 << varmap[v]))

    for k, v in columns.items():
        if v is None:
            continue

        state[k] = v[0](*[state[hashexpr(x)] for x in v[1:]])

    match mode:
        case "md":
            print("|" + "|".join(["1" if x else "0"
                                  for x in state.values()]) + "|")
        case "latex":
            print(" " + " & ".join(["1" if x else "0"
                                    for x in state.values()]) + " \\\\")
        case "sat":
            if not list(state.values())[-1]:
                print("unsat", tuple([1 if state[hashexpr(v)] else 0 for v in vs]))
                exit(0)

    i += 1

match mode:
    case "latex":
        print(" \\hline")
        print("\\end{tabular}")
    case "sat":
        print("sat")