"""Ejemplo 1 - Un evaluador de logica proposicional en Python puro."""

from itertools import product

# Una formula se representa como un arbol: ("op", izq, der) o el nombre de una variable.
# Ejemplo:  P -> Q   se escribe   ("->", "P", "Q")


def evaluar(formula, mundo):
    """Devuelve el valor de verdad de la formula en un mundo dado."""
    if isinstance(formula, str):          # es una variable proposicional
        return mundo[formula]

    op = formula[0]
    if op == "no":
        return not evaluar(formula[1], mundo)

    izq = evaluar(formula[1], mundo)
    der = evaluar(formula[2], mundo)

    if op == "y":
        return izq and der
    if op == "o":
        return izq or der
    if op == "->":
        return (not izq) or der          # el condicional solo es falso si V -> F
    if op == "<->":
        return izq == der
    raise ValueError(f"Operador desconocido: {op}")


def variables(formula):
    """Recolecta las variables que aparecen en la formula."""
    if isinstance(formula, str):
        return {formula}
    if formula[0] == "no":
        return variables(formula[1])
    return variables(formula[1]) | variables(formula[2])


def tabla_de_verdad(formula, nombre=""):
    vs = sorted(variables(formula))
    print(f"\nTabla de verdad de {nombre}")
    print("  ".join(vs) + "  |  resultado")
    print("-" * (3 * len(vs) + 13))
    filas = []
    for valores in product([True, False], repeat=len(vs)):
        mundo = dict(zip(vs, valores))
        r = evaluar(formula, mundo)
        filas.append(r)
        marcas = "  ".join("V" if mundo[v] else "F" for v in vs)
        print(f"{marcas}  |  {'V' if r else 'F'}")
    if all(filas):
        print(">> La formula es una TAUTOLOGIA: verdadera en todo mundo posible.")
    elif not any(filas):
        print(">> La formula es una CONTRADICCION: falsa en todo mundo posible.")
    else:
        print(">> La formula es CONTINGENTE: depende del mundo.")


# 1. El modus ponens es valido: ((P -> Q) y P) -> Q
modus_ponens = ("->", ("y", ("->", "P", "Q"), "P"), "Q")
tabla_de_verdad(modus_ponens, "((P -> Q) y P) -> Q")

# 2. La falacia de afirmar el consecuente NO es valida: ((P -> Q) y Q) -> P
falacia = ("->", ("y", ("->", "P", "Q"), "Q"), "P")
tabla_de_verdad(falacia, "((P -> Q) y Q) -> P")