:- op(500, yfx, @).
:- op(550, xfx, /\).
:- op(550, xfx, =>).
:- op(600, xfy, ^).

%%%%%%%%%%%%%
% Interface %
%%%%%%%%%%%%%

analisa(Expressão) :-
        categoria(Categoria),
        (   (Categoria = n; Categoria = v)
        ->  Regra =.. [Categoria, _, Sem]
        ;   Regra =.. [Categoria, 1, _, Sem]
        ),
        phrase(Regra, Expressão, []),
        nl,
        apresenta(0, Sem).

categoria(s).
categoria(sn).
categoria(sv).
categoria(det).
categoria(n).
categoria(v).

apresenta(N, [X, []]) :-
     tab(N),
     write(X),
     nl,
     !.
apresenta(N, [X|Y]) :-
     tab(N),
     X \= [_|_],
     write(X),
     apresenta_aux(N, Y),
     !.
apresenta(N, X) :-
     apresenta_lista(N, X).

apresenta_aux(_, []) :-
     !.
apresenta_aux(N, [X|Y]) :-
     X \= [_|_],
     nl,
     tab(N),
     write('<== '),
     write(X),
     apresenta_aux(N, Y).
apresenta_aux(N, [X|Y]) :-
     nl,
     M is N + 7,
     apresenta(M, X),
     apresenta_lista(M, Y).

apresenta_lista(_, []).
apresenta_lista(N, [X|Y]) :-
     nl,
     apresenta(N, X),
     apresenta_lista(N, Y).

%%%%%%%%%%%%%
% Gramática %
%%%%%%%%%%%%%

% Regras sintagmáticas

s(X1, X3, S) --> sn(X1, X2, SN), sv(X2, X3, SV),
     {SN = [SN1|_], SV = [SV1|_], reduz_lista([SN1@SV1, [SN, SV]], S)}.

sn(X1, X2, [x(X1)^x(X1)@N1, N]) --> n(p, N), {N = [N1|_], X2 is X1 + 1}.
sn(X1, X2, SN) --> det(X1, X2, Det), n(c, N),
     {Det = [Det1|_], N = [N1|_], reduz_lista([Det1@N1, [Det, N]], SN)}.

sv(X, X, V) --> v(i, V).
sv(X1, X4, SV) --> v(t, V), sn(X1, X2, SN),
     {V = [V1|_], SN = [SN1|_],
      X3 is X2 + 1, X4 is X3 + 1,
      reduz_lista([x(X2)^SN1@(x(X3)^V1@x(X3)@x(X2)), [V, SN]], SV)}.

% Itens Lexicais

det(X1, X4, [x(X1)^x(X2)^algum(x(X3), x(X1)@x(X3) /\ x(X2)@x(X3)), []]) --> [um],
     {X2 is X1 + 1, X3 is X2 + 1, X4 is X3 + 1}.
det(X1, X4, [x(X1)^x(X2)^qualquer(x(X3), x(X1)@x(X3) => x(X2)@x(X3)), []]) --> [todo],
     {X2 is X1 + 1, X3 is X2 + 1, X4 is X3 + 1}.

n(c, [b, []]) --> [buraco].
n(c, [m, []]) --> [menino].
n(p, [p, []]) --> [pedro].

v(i, [d, []]) --> [dormiu].
v(t, [s, []]) --> [saltou].

%%%%%%%%%%%%%%%%
% Redução-beta %
%%%%%%%%%%%%%%%%

% reduz_lista(Lista, Reduzido)
% ******************************************
% * Reduzido é o resultado da redução-beta *
% * recorrente do primeiro Termo da Lista  *
% ******************************************
reduz_lista(Lista, Reduzido) :-
     Lista = [Termo|_],
     reduz_termo(Termo, Resultado),
     reduz_lista([Resultado|Lista], Reduzido),
     !.
reduz_lista(Resultado, Resultado).

% reduz_termo(Termo1, Termo2)
% **************************************************
% * Termo2 é o resultado da redução-beta do Termo1 *
% **************************************************
% Aplicação
reduz_termo(Termo1@Termo2, Termo1@Resultado) :-
     reduz_termo(Termo2, Resultado).
reduz_termo(Termo1@Termo2, Resultado@Termo2) :-
     reduz_termo(Termo1, Resultado).
reduz_termo((Var^Termo)@Arg, Resultado) :-
     substitui(Termo, Var, Arg, Resultado).
% Abstração
reduz_termo(Var^Termo, Var^Resultado) :-
     reduz_termo(Termo, Resultado).
% Conjunção
reduz_termo(Termo1 /\ Termo2, Termo1 /\ Resultado) :-
     reduz_termo(Termo2, Resultado).
reduz_termo(Termo1 /\ Termo2, Resultado /\ Termo2) :-
     reduz_termo(Termo1, Resultado).
% Implicação
reduz_termo(Termo1 => Termo2, Termo1 => Resultado) :-
     reduz_termo(Termo2, Resultado).
reduz_termo(Termo1 => Termo2, Resultado => Termo2) :-
     reduz_termo(Termo1, Resultado).
% Quantificação existencial
reduz_termo(algum(Var, Termo), algum(Var, Resultado)) :-
     reduz_termo(Termo, Resultado).
% Quantificação universal
reduz_termo(qualquer(Var, Termo), qualquer(Var, Resultado)) :-
     reduz_termo(Termo, Resultado).

% substitui(Termo1, Var, Termo2, Termo3)
% ***************************************************************
% * Termo3 é o resultado de substituir Var por Termo2 no Termo1 *
% ***************************************************************
% Variável
substitui(x(M), x(N), Termo2, Termo3) :-
     (   x(M) \= x(N)
     ->  Termo3 = x(M)
     ;   Termo3 = Termo2
     ).
% Constante
substitui(Termo3, _, _, Termo3) :-
     atom(Termo3).
% Aplicação
substitui(Termo1a@Termo1b, Var, Termo2, Termo3a@Termo3b) :-
     substitui(Termo1a, Var, Termo2, Termo3a),
     substitui(Termo1b, Var, Termo2, Termo3b).
% Abstração
substitui(Var1^Termo1, Var, Termo2, Termo3) :-
     (	 Var1 = Var
     ->	 Termo3 = Var1^Termo1
     ;	 substitui(Termo1, Var, Termo2, Resultado),
         Termo3 = Var1^Resultado
     ).
% Conjunção
substitui(Termo1a /\ Termo1b, Var, Termo2, Termo3a /\ Termo3b) :-
     substitui(Termo1a, Var, Termo2, Termo3a),
     substitui(Termo1b, Var, Termo2, Termo3b).
% Implicação
substitui(Termo1a => Termo1b, Var, Termo2, Termo3a => Termo3b) :-
     substitui(Termo1a, Var, Termo2, Termo3a),
     substitui(Termo1b, Var, Termo2, Termo3b).
% Quantificação existencial
substitui(algum(Var1, Termo1), Var, Termo2, Termo3) :-
     (	 Var1 = Var
     ->	 Termo3 = algum(Var1, Termo1)
     ;	 substitui(Termo1, Var, Termo2, Resultado),
         Termo3 = algum(Var1, Resultado)
     ).
% Quantificação universal
substitui(qualquer(Var1, Termo1), Var, Termo2, Termo3) :-
     (	 Var1 = Var
     ->	 Termo3 = qualquer(Var1, Termo1)
     ;	 substitui(Termo1, Var, Termo2, Resultado),
         Termo3 = qualquer(Var1, Resultado)
     ).