from formulas import *

def avalia(fi, contexto=None):
    if contexto is None:
        contexto = {}
    átomos = sorted([psi for psi in subfórmulas(fi) if é_atômica(psi)])

    # Completar o contexto, pedindo pro usuário os valores das subfórmulas atômicas
    # de fi que estiverem faltando:
    for psi in átomos:
        if psi not in contexto:
            while True:
                valor_psi = input(f"Qual o valor de {psi} no contexto?\n(Verdadeiro ou Falso, V ou F, True ou False, T ou F)?\n")
                if valor_psi.lower().strip() in {'verdadeiro','v','t','true'}:
                    contexto[psi] = 'V'
                    break
                if valor_psi.lower().strip() in {'falso','f','false'}:
                    contexto[psi] = 'F'
                    break

    if é_atômica(fi):
        return contexto[fi]

    psi = fi[1]
    valor_psi = avalia(psi, contexto)

    if é_negação(fi):
        if valor_psi == 'V':
            return 'F'
        return 'V'

    beta = fi[2]
    valor_beta = avalia(beta, contexto)

    if é_conjunção(fi):
        if valor_psi == 'F':
            return 'F'
        return valor_beta

    if é_disjunção(fi):
        if valor_psi == 'V':
            return 'V'
        return valor_beta

    if é_implicação(fi):
        if valor_psi == 'V' and valor_beta == 'F':
            return 'F'
        return 'V'

    if é_biimplicação(fi):
        if valor_psi == valor_beta:
            return 'V'
        return 'F'

def gera_todos_contextos(lista):
    if len(lista) == 0:
        return []

    p = lista[0]

    if len(lista) == 1:
        return [{p:'V'}, {p:'F'}]
    
    res = []
    contextos_para_o_resto = gera_todos_contextos(lista[1:])
    for d in contextos_para_o_resto:
        for valor_p in {'V', 'F'}:
            novo = d.copy()
            novo[p] = valor_p
            res.append(novo)
    return res

def é_válida(fi):
    atômicas = [p for p in subfórmulas(fi) if é_atômica(p)]
    contextos = gera_todos_contextos(atômicas)
    for contexto in contextos:
        if avalia(fi,contexto) == 'F':
            return False
    return True

def testa(n=10):
    i = 0
    while True:
        i += 1
        fi = fórmula_aleatória(n)
        if é_válida(fi):
            return i

def testa2(n=10,iter=10**3):
    s = 0
    for _ in range(iter):
        s += testa(n)
    return s/iter
