from random import randrange, choice

símbolos_proposicionais = {'p', 'q', 'r', 's', 't', 'u'}

fi = 'p'
psi = ('¬', fi)
beta = ('→', fi, fi)
mi = ('∨', psi, beta)
eta = ('↔', beta, mi)
alfa = ('∧', mi, 'q')

def é_atômica(fi):
    return isinstance(fi, str)

def é_negação(fi):
    return isinstance(fi, tuple) and len(fi) == 2 and fi[0] == '¬'

def é_conjunção(fi):
    return isinstance(fi, tuple) and len(fi) == 3 and fi[0] == '∧'

def é_disjunção(fi):
    return isinstance(fi, tuple) and len(fi) == 3 and fi[0] == '∨'

def é_implicação(fi):
    return isinstance(fi, tuple) and len(fi) == 3 and fi[0] == '→'

def é_biimplicação(fi):
    return isinstance(fi, tuple) and len(fi) == 3 and fi[0] == '↔'

def subfórmulas(fi):
    if é_atômica(fi):
        return {fi}
    
    if é_negação(fi):
        psi = fi[1]
        return {fi}.union(subfórmulas(psi))
    
    # fi é psi*beta
    psi, beta = fi[1:]
    return {fi}.union(subfórmulas(psi)).union(subfórmulas(beta))

def printa(fi, prefixo='', tem_irmão=False):
    rótulo = fi[0]
    if prefixo=='':
        print(f"{rótulo}")
    elif tem_irmão:
        print(f"{prefixo[:-2]}├╴{rótulo}")
    else:
        print(f"{prefixo[:-2]}└╴{rótulo}")

    if é_atômica(fi):
        return

    psi = fi[1]
    if é_negação(fi):
        printa(psi, prefixo+'  ',False)
        return

    beta = fi[2]
    printa(psi, prefixo+'│ ',True)
    printa(beta, prefixo+'  ',False)
    
def fórmula_aleatória(profundidade_max=8):
    profundidade = randrange(0,profundidade_max + 1)
        
    if profundidade == 0:
        # se a fórmula deve ter profundidade 0, tem que ser atômica
        return choice(list(símbolos_proposicionais))
    
    conectivo = choice(['¬', '∧', '∨', '→', '↔'])

    # recursivamente geramos um primeiro filho com profundidade menor
    filho_esquerdo = fórmula_aleatória(profundidade-1)
    
    if conectivo == '¬':
        return (conectivo, filho_esquerdo)

    # se não é negação, então também geramos um segundo filho com
    # profundidade menor
    filho_direito = fórmula_aleatória(profundidade-1)
    return (conectivo, filho_esquerdo, filho_direito)