% tv.pl - cria tabela-verdade para formula proposicional

:- op(900, fy,  não).
:- op(901, yfx, e).
:- op(902, yfx, ou).
:- op(903, yfx, então).

tv(Formula) :-
    titulos(Formula, Titulos, Formato, Proposicoes),
    ansi_format([fg(red)], Titulos, []),
    forall(maplist(associa, Proposicoes, Interpretacao),
           exibe_linha(Formula, Interpretacao, Formato)).

titulos(Formula, Titulos, Formato, Proposicoes) :-
    proposicoes(Formula, [], Proposicoes0),
    reverse(Proposicoes0, Proposicoes),
    term_to_atom(Formula, Resultado),
    reverse([Resultado|Proposicoes0], Titulo0),
    maplist(formato, Titulo0, Formato0, Separador0),
    atomic_list_concat(Formato0, '|', Format1),
    atomic_concat(Format1, '\n', Formato),
    atomic_list_concat(Separador0, '+', Separador),
    format(atom(Titulo1), Formato, Titulo0),
    atomic_list_concat(['\n', Titulo1, Separador, '\n'], Titulos).

proposicoes(Formula, Proposicoes0, Proposicoes) :-
    (   compound(Formula)
    ->  Formula =.. [_|Argumentos],
        foldl(proposicoes, Argumentos, Proposicoes0, Proposicoes)
    ;   member(Formula, Proposicoes0)
    ->  Proposicoes = Proposicoes0
    ;   Proposicoes = [Formula|Proposicoes0] ).

formato(Proposicao, Formato, Separador) :-
    atom_length(Proposicao, Comprimento),
    N is Comprimento + 2,
    format(atom(Formato), '~~|~~t~~w~~t~~~w+', [N]),
    format(atom(Separador), '~*c', [N, 0'-]).

associa(Proposicao, Proposicao-Valor) :-
    member(Valor, ['F', 'V']).

exibe_linha(Formula, Interpretacao, Formato) :-
    val(Formula, Interpretacao, Resultado),
    maplist(arg(2), Interpretacao, Valoracao),
    append(Valoracao, [Resultado], Linha),
    ansi_format([fg(blue)], Formato, Linha).


val(P,         A, W) :- atom(P), !, memberchk(P-W, A).
val(não P,     A, W) :- ( val(P, A, 'F')                   -> W = 'V' ; W = 'F').
val(P e Q,     A, W) :- ((val(P, A, 'V') , val(Q, A, 'V')) -> W = 'V' ; W = 'F').
val(P ou Q,    A, W) :- ((val(P, A, 'V') ; val(Q, A, 'V')) -> W = 'V' ; W = 'F').
val(P então Q, A, W) :- ((val(P, A, 'F') ; val(Q, A, 'V')) -> W = 'V' ; W = 'F').