% A node in the AVL tree has the following structure
% avl(Value, Ballance, LeftSubtree, RightSubtree).
% we use the constant 'nil' as a substitute for 'no subtree'.

% Finds the given value in the AVL tree
% avlmember(X, Tree)
avlmember(X, avl(X, _, _, _)).
avlmember(X, avl(Y, _, L, _)) :- X @< Y, avlmember(X, L).
avlmember(X, avl(Y, _, _, R)) :- X @> Y, avlmember(X, R).

avladd(X, T, T1) :- avladd1(X, T, T1, _).

avladd(X, T, T) :-
    T = avl(X, _, _, _).
% avladd1 - helper predicate for appending to the AVL tree.
% avladd(Item, OriginalTree, NewTree, Difference)
avladd1(X, nil, T, 1) :-
    avlinit(X, T).
avladd1(X, avl(Y, B, L, R), T, C) :- X == Y,
    T = avl(Y, B, L, R), C = 0.
avladd1(X, avl(Y, B, L, R), T, C) :- X @< Y,
    avladd1(X, L, L1, C1),
    B1 is B - C1,
    avlballance(avl(Y, B1, L1, R), T, C1, C).
avladd1(X, avl(Y, B, L, R), T, C) :- X @> Y,
    avladd1(X, R, R1, C1),
    B1 is B + C1,
    avlballance(avl(Y, B1, L, R1), T, C1, C).

% avlballance(Tin, Tout, PrevChange, Change)
avlballance(T, T, C, C) :-
    T = avl(_, -1, _, _);
    T = avl(_,  0, _, _);
    T = avl(_,  1, _, _).
avlballance(T, T1, _, 0) :- T = avl(_, -2, Ta, _), Ta = avl(_, -1, _, _),
    avlrotater(T, T1).
avlballance(T, T1, _, 0) :- T = avl(X, -2, Ta, R), Ta = avl(_, 1, _, _),
    avlrotatel(Ta, Ta1),
    avlrotater(avl(X, -2, Ta1, R), T1).
avlballance(T, T1, _, 0) :- T = avl(_, 2, _, Ta), Ta = avl(_, 1, _, _),
    avlrotatel(T, T1).
avlballance(T, T1, _, 0) :- T = avl(X, 2, L, Ta), Ta = avl(_, -1, _, _),
    avlrotater(Ta, Ta1),
    avlrotatel(avl(X, 2, L, Ta1), T1).
    
avlinit(X, avl(X, 0, nil, nil)).

min(A, B, A) :- A =< B.
min(A, B, B) :- A > B.
max(A, B, A) :- A >= B.
max(A, B, B) :- A < B.

avlrotatel(avl(Xb, Bb, C, avl(Xa, Ba, D, E)),
	    avl(Xa, Ba1, avl(Xb, Bb1, C, D), E)) :-
    min(Bb, 0, Bb_1), Ba1 is Ba - 1 + Bb_1,
    max(Ba, 0, Ba_1), Bb1 is Bb - 1 - Ba_1.
avlrotater(avl(Xd, Bd, avl(Xb, Bb, A, C), E),
	    avl(Xb, Bb1, A, avl(Xd, Bd1, C, E))) :-
    min(Bb, 0, Bb_1), Bd1 is Bd + 1 - Bb_1,
    max(Bd, 0, Bd_1), Bb1 is Bb + 1 + Bd_1.