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 negação(fi):
    return ('¬', fi)

def conjunção(fi,psi):
    return ('∧',fi,psi)

def disjunção(fi,psi):
    return ('∨',fi,psi)

def implicação(fi,psi):
    return ('→',fi,psi)

def biimplicação(fi,psi):
    return ('↔',fi,psi)

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_linear(fi, raiz = True, par = '<>', end='\n'):
    parênteses = ['()','[]','{}','<>']
    novopar = parênteses[(parênteses.index(par) + 1)%len(parênteses)]
    
    if é_atômica(fi):
       if raiz:
           print(fi,end=end)
           return
       else:
           return fi
    else:
        conectivo = fi[0]
        psi = fi[1]
        if é_negação(fi):
            if é_atômica(psi):
                s = f'¬{psi}'
                if raiz:
                    print(s, end=end)
                    return
            elif é_negação(psi):
                s = f'¬{printa_linear(psi, False,novopar)}'
                if raiz:
                    print(s,end=end)
                    return
            else:
                s = f'¬{printa_linear(psi, False,novopar)}'
                if raiz:
                    print(s,end=end)
                    return
        else:
            theta = fi[2]
            s = f'{printa_linear(psi,False,novopar)} {conectivo} {printa_linear(theta,False,novopar)}'
    if raiz:    
        print(s,end=end)
    else:
        return f'{par[0]}{s}{par[1]}'

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)