:- module(mini_nat, [{}/1]).

% {Korlat}: Korlat fenn�ll.
{Korlat} :-
        korlat_cel(Korlat, Cel), call(Cel).

		     
% plusz(X, Y, Z): X+Y=Z (Peano sz�mokkal).
:- block plusz(-, ?, -).
plusz(0, Y, Y).
plusz(s(X), Y, s(Z)) :-
        plusz(X, Y, Z).

% +(X, Y, Z): X+Y=Z (Peano sz�mokkal). Hat�konyabb, mert
% tov�bbl�p, ha b�rmelyik argumentum behelyettes�tett.
:- block +(-, -, -).
+(X, Y, Z) :-
        nonvar(X), !, plusz(X, Y, Z).
+(X, Y, Z) :- 
        plusz(Y, X, Z).  % \+((var(Y),var(Z)))

% X-Y=Z, ahol X, Y �s Z Peano sz�mok.
-(X, Y, Z) :-
        +(Y, Z, X).

% X*Y=Z, ahol X, Y �s Z Peano sz�mok. Blokkol, ha nincs t�m�r argumentuma.
*(X, Y, Z) :-
        when( (ground(X);ground(Y);ground(Z)),
              szorzat(X, Y, Z)
            ).

% X*Y=Z, ahol X, Y �s Z Peano sz�mok. Legal�bb egyik argumentuma t�m�r.
szorzat(X, Y, Z) :-
        (   ground(X) -> szorzat1(X, Y, Z)
        ;   ground(Y) -> szorzat1(Y, X, Z)
        ;   /* Z t�m�r! */
            Z == 0 -> szorzatuk_nulla(X, Y)
        ;   X = s(_), +(X, _, Z), % 1 =< X =< Z
            szorzat1(X, Y, Z)
        ).

% X*Y=0, ahol X �s Y Peano sz�mok.
szorzatuk_nulla(X, Y) :-
        (   X = 0 
        ;   Y = 0
        ).

% szorzat1(X, Y, Z): X*Y=Z, ahol X, Y �s Z peano sz�mok. X t�m�r.
szorzat1(0, _X, 0).
szorzat1(s(X), Y, Z) :-
        szorzat1(X, Y, Z1),
        +(Z1, Y, Z).

% korlat_cel(Korlat, Cel): Korlat v�grehajthat� 
% alakja a Cel c�lsorozat.
korlat_cel(Kif1=Kif2, (C1,C2)) :-
        kiertekel(Kif1, E, C1), % Kif1 �rt�k�t E-ben 
                                % el��ll�t� c�l C1 
        kiertekel(Kif2, E, C2).
korlat_cel(Kif1 =< Kif2, Cel) :-
        korlat_cel(Kif1+_ = Kif2, Cel).
korlat_cel(Kif1 < Kif2, Cel) :-
        korlat_cel(s(Kif1) =< Kif2, Cel).
korlat_cel(Kif1 >= Kif2, Cel) :-
        korlat_cel(Kif2 =< Kif1, Cel).
korlat_cel(Kif1 > Kif2, Cel) :-
        korlat_cel(Kif2 < Kif1, Cel).
korlat_cel((K1,K2), (C1,C2)) :-
        korlat_cel(K1, C1), korlat_cel(K2, C2).

% kiertekel(Kif, E, Cel): A Kif aritmetikai kifejez�s �rt�k�t E-ben
% el��ll�t� c�l Cel. Kif eg�szekb�l a +, -, �s * oper�torokkal �p�l fel.
kiertekel(Kif, E, (C1,C2,Rel)) :-
        compound(Kif), Kif =.. [Op,Kif1,Kif2], !,
        kiertekel(Kif1, E1, C1), kiertekel(Kif2, E2, C2),
        Rel =.. [Op,E1,E2,E].
kiertekel(N, Kif, true) :-
        number(N), !, int_to_peano(N, Kif).
kiertekel(Kif, Kif, true).

% int_to_peano(N, P): N term�szetes sz�m Peano alakja P.
int_to_peano(0, 0).
int_to_peano(N, s(P)) :-
        N > 0, N1 is N-1,
        int_to_peano(N1, P).

% Peano sz�mok ki�r�s�nak form�z�sa
user:portray(Peano) :-
        write_peano(Peano, 0).
% felf�ggesztett c�lok ki�rat�s�nak form�z�sa
user:portray(_:Rel) :-
        Rel =.. [Pred,A,B,C],
	predikatum_operator(Pred, Op),
        Fun =.. [Op,A,B],
        print({Fun=C}).

predikatum_operator(plusz, +).
predikatum_operator(+, +).
predikatum_operator(*, *).

% Ha P Peano szam, kiirjuk P+N0 erteket.
write_peano(P, N0) :-
        P == 0, !, write(N0).
write_peano(P, N0) :-
        nonvar(P), P = s(P1), !,
	N1 is N0+1,
	write_peano(P1, N1).
write_peano(P, N0) :-
	N0 > 0, 
	write('('), write(P+N0), write(')').
