/*  ARRAYS.PL  */
 
 
:- module arrays.
 
 
:- public new_array/1,
          is_array/1,
          array_is_empty/1,
          array_insert/4,
          array_insert_or_replace/5,
          array_delete/4,
          array_member/3,
          array_value/3,
          array_first/3,
          array_last/3,
          list_to_array/2,
          array_to_list/2,
          array_ranged_to_list/4,
          array_filtered_to_list/5,
          array_length/2,
          for_in_array/4,
          for_ranged_in_array/6,
          portray_array/1.
 
 
/*
SPECIFICATION
-------------
 
This module exports predicates for handling what are, essentially,
updatable sparse arrays. The array subscript, or "key" must be an
integer. The element, or "entry", can be any Prolog term. Subscripts do
not need to be contiguous. Mathematically, you can think of these
structures as implementing partial functions from the integers to
arbitrary terms. The arrays are actually implemented as AVL trees (see
implementation part for detail). This gives an average time to find an
element proportional to the logarithm of the number of elements in the
array.
 
The most common things you will want to do are to create arrays, insert
or delete key-entry pairs, and look up entries from keys. Here are some
examples. In showing what they do, I'll represent arrays as follows
    { -10:herring, -5:sardine, 6:plaice, 12:pilchard, 23:anchovy }
showing the keys and entries in ascending order of key. Unlike arrays
in languages like Pascal, these ones are not of fixed length. An array
does not contain a key until you insert one.
 
    ?- new_array(A).
    A = {}
 
    ?- new_array(A0),
       array_insert( A0, 1,tuna, A1 ),
       array_insert( A1, -3,salmon, A2 ),
       array_insert( A2, 7,cod, A3 ),
       array_insert( A3, -100,mackerel, A ).
    A = { -100:mackerel, -3:salmon, 1:tuna, 7:cod }
 
    ?- array_value( A, 1, E )
    E = tuna
    if A has the same value as above.
 
PUBLIC new_array( A- ):
D becomes a new, empty, array.
 
 
PUBLIC array_is_empty( A+ ):
True if D contains no entries.
 
 
PUBLIC is_array( A+ ):
True if A is an array.
 
 
PUBLIC array_insert( A+, K+, E+, A1- ):
"A contains a key-entry pair K,_; A1 contains the pair K,E and is
otherwise the same as A".
 
Inserts the pair K,E into A giving A1. Undefined if A already contains
key K.
 
 
PUBLIC array_insert_or_replace( A+, K+, E+, A1-, ChangeType? ):
"A contains a key-entry pair K,E0; A1 contains the pair K,E and is
otherwise the same as A; and ChangeType = 'replaced(E0)';
or A does not contain a pair K,_; A1 contains the pair K,E and is
otherwise the same as A; and ChangeType = 'inserted'".
 
This predicate is an extension of array_insert. It either replaces or
inserts the pair K,E to A giving A1, and unifies ChangeType with
'inserted' if A did contain K, 'replaced' if not.
 
ChangeType can be instantiated on call. If it is, this controls how the
predicate is to act if it finds an entry with the same K. If it does,
and ChangeType is 'inserted', then array_insert_or_replace fails,
otherwise inserts it. If ChangeType is 'replaced(E0)',
array_insert_or_replace will fail should A _not_ contain such an entry,
and otherwise instantiate E0 to the old entry.
 
 
PUBLIC array_delete( A+, K+, E-, A1- ):
"A1 is the result of deleting pair K,E from A".
 
 
PUBLIC array_member( K?, E?, A+ ):
"The pair K,E is a member of A".
 
array_member is to AVLs as member is to lists. It visits the elements of A
in ascending order of key.
 
 
PUBLIC array_value( A+, K+, E? ):
"E is the entry for key K in A".
 
 
PUBLIC array_first( A+, K?, E? ) :
"The key and entry for the smallest key in A are K and E".
 
 
PUBLIC array_last( A+, K?, E? ) :
"The key and entry for the greatest key in A are K and E".
 
 
PUBLIC array_length( A+, L? ):
This is the analogue of length/2. L is the number of key-entry pairs
in A.
 
 
PUBLIC list_to_array( L+, A- ):
L must be a fully instantiated list. Each element must be of the form
K-E where K is an integer; there should not be more than one element
with the same K. A will be unified with the corresponding array.
 
 
PUBLIC array_to_list( A+, L- ):
The converse of list_to_array. The list will consist of pairs K-E,
sorted in ascending order of K.
 
 
PUBLIC array_ranged_to_list( A+, Low+, High+, L- ):
As array_to_list, but the list will only contain elements whose keys
lie between Low and High inclusive.
 
 
PUBLIC array_filtered_to_list( A+, K-, E-, Goal+, L- ):
As array_to_list, but the list will only contain elements for which
Goal succeeds when K and E are bound to the key and entry.
 
 
PUBLIC for_in_array( K-, E-, A+, Goal+ ):
This is the analogue of for_in_list (USEFUL.PL). 'for_in_list' calls
Goal for K and E bound to each key-entry pair of A, in order, and then
succeeds. If Goal fails, the action is undefined (a call to 'bug'). Not
resatisfiable. K, E, and all variables in Goal, are unbound on exit.
 
 
PUBLIC for_ranged_in_array( K-, E-, Low+, High+, A+, Goal+ ):
As for_in_array, but only loops over those elements whose key lies
between Low and High inclusive.
 
 
PUBLIC portray_array( A+ ):
Write A in the form
    {}
or
    { -10:herring, -5:sardine, 6:plaice, 12:pilchard, 23:anchovy }
using 'print' to write the keys and entries
 
 
In fact, subscripts need not be integers. They can be any term
(preferably one that's completely instantiated). Arrays are implemented
as binary trees, storing key-entry pairs in the ascending order defined
by the term comparison operator @< on keys. These operators work for any
term; the order in which predicates such as 'array_first' and
'array_member' visit keys will be the order defined by those operators.
 
Note that if you have some keys that are reals and some that are
integers, this order may not be what you expect. See the documentation
on these operators for details.
*/
 
 
/*
IMPLEMENTATION
--------------
 
These "arrays" are implemented as AVL trees. For an explanation, read on.
 
 
The least-effort way to implement them would be to use lists, making
each pair of elements represent a key and its associated entry:
    array_insert( [], K, E, [K,E] ) :- !.
    array_insert( [K,_|Rest], K, E, [K,E|Rest] ) :- !.
    array_insert( [Head|Rest], K, E, [Head|NewRest] ) :-
        array_insert( Rest, K, E, NewRest ).
 
    array_value( [K,E|_], K, E ) :- !.
    array_value( [_,_|Rest], K, E ) :-
        array_value( Rest, K, E ).
 
This is logically correct, but hardly efficient. Locating a given key
will take on average a time proportional to N/2, for a list of length N.
It could be made somewhat faster by keeping the lists sorted by key, but
the average time would still be proportional to length. The very first
version of the Tutor did do this, because it enabled me to get the
editor working within a short time, leaving me free to experiment with
the user interface. But it was too slow for serious use.
 
 
The current version of this module represents arrays as ordered binary
trees. A tree can be represented as a term
    t( Left, K, E, Right )
or (if empty) as the atom "nil". Left and Right are themselves trees. To
make locating keys more efficient, we stipulate that Left can only
contain keys less than K; Right can only contain keys greater than K.
This must hold for the top of the tree, and for all its subtrees.
 
We can then rewrite the predicates shown above like this:
    array_insert( nil, K, E, t(nil,K,E,nil) ) :- !.
    array_insert( t(Left,K,_,Right), K, E, t(Left,K,E,Right) ) :- !.
    array_insert( t(Left,K0,E0,Right), K, E, t(NewLeft,K0,E0,Right) ) :-
        K < K0,
        !,
        array_insert( Left, K, E, NewLeft ).
    array_insert( t(Left,K0,E0,Right), K, E, t(Left,K0,E0,NewRight) ) :-
        K > K0,
        !,
        array_insert( Right, K, E, NewRight ).
 
    array_value( t(_,K,E,_), K, E ) :- !.
    array_value( t(Left,K0,_,_), K, E ) :-
        K < K0,
        !,
        array_value( Left, K, E ).
    array_value( t(_,K0,_,Right), K, E ) :-
        K > K0,
        !,
        array_value( Right, K, E ).
 
Using ordered binary trees like this, the time taken to locate a key is
proportional not to the number of elements, but to their logarithm. This
is a well-known result in computing, and such trees are routinely
deployed as data structures.
 
Ordered binary trees have another desirable property --- it's possible
to read out the entries in ascending (or descending) order of key. Were
this not possible, we would have to find another representation for
storing facts. There are many predicates in the module which generate
sequences of entries, whether
 
(1) Explicitly, as lists.
 
(2) Implicitly, as the sequence of values passed to some variable or
    stream (as in "for_in_array", "portray_array").
 
(3) Implicitly, as the sequence of solutions offered when backtracking
    (as in "array_member").
 
These predicates all work in ascending order of key. This is done by
traversing the trees in "pre-order": given tree
    t( Left, K, E, Right )
we visit Left, then K and E, then Right.
 
 
The trouble with trees is that they become lop-sided. If we do
    ?- array_insert( nil, 1, one, T1 ),
       array_insert( T1, 2, two, T2 ),
       array_insert( T2, 3, three, T3 ),
       array_insert( T3, 4, four, T4 ),
       array_insert( T4, 5, five, T5 ).
we end up with a tree whose elements are all down the right-hand side,
and looking for a key again takes a time proportional to the number of
elements. This might not matter for five elements. But a typical session
at the Tutor could involve the insertion of some thirty or forty facts,
and there it does matter. Besides, we might want in the future to use
trees for storing something other than facts. I have tried this, and the
Tutor's response did slow noticeably as facts were appended.
 
We could avoid the trees becoming lopsided if, after each insertion, we
re-arranged them so that the number of entries on the left of each node
is roughly the same as that on the right. It is possible to do this
without spoiling the ordering, because there are several different
shapes representing the same order, all of which abide by the condition
mentioned earlier that given any subtree of
    t( Left, K, E, Right )
the keys in Left are all less than K and those in Right are all
greater. This condition must be preserved for array_value to function
correctly.
 
Collectively, trees where the number of elements on both sides of each
node are roughly equal are called balanced trees. There are various
schemes for keeping trees balanced. The one I use is "height balancing",
where the "height" of a tree is defined as the length of the longest
path between the root and any descendant. Such trees are known as AVL
trees from the inventors' initials; implementations are described in the
standard computing science books.
 
My representation was taken from Bratko's book on "Prolog Programming
for Artificial Intelligence", augmented with the method for deletion
described in "Handbook of Algorithms and Data Structures" by Gaston H.
Gonnet Addison-Wesley. There is incidentally a later, dual-author,
version of Gonnet's book, published 1990 or so.
 
 
It is certainly possible to improve my code: for example, better
indexing could probably be achieved by not storing the zero height of
nil. This would allow indexing to distinguish between empty and
non-empty trees, and would mean that the height of non-empty trees
could be moved back into the main array(...) structure, thus saving
some space. I believe the Quintus library does this, but of course it's
not freely available. Send me a better implementation if you have one.
*/
 
 
:- needs bug / 2, max / 3.
 
 
/*  Will also need the @< and other term-comparison operators
    if your system doesn't provide them.
*/
 
 
/*  Creating arrays.  */
 
 
new_array( nil/0 ).
 
 
/*  Inserting and replacing elements.  */
 
 
array_insert(  nil/0,
               K,E,
               avl( nil/0, K,E, nil/0 )/1
            ) :- !.
 
array_insert(  avl(L0,K0,E0,R0)/_,
               K,E,
               TF
            ) :-
    K@<K0,
    !,
    array_insert( L0, K,E, avl(L1,K1,E1,R1)/_ ),
    avl_combine( L1, K1,E1, R1, K0,E0, R0, TF ).
 
array_insert(  avl(L0,K0,E0,R0)/_,
               K,E,
               TF
            ):-
    K@>K0,
    !,
    array_insert( R0, K, E, avl(L1,K1,E1,R1)/_ ),
    avl_combine( L0, K0,E0, L1, K1,E1, R1, TF ).
 
array_insert( Old, K,E, _ ) :-
    bug( 'array_insert/4: unexpected failure', [Old,K,E] ).
 
 
array_insert_or_replace(
               nil/0,
               K,E,
               avl( nil/0, K,E, nil/0 )/1,
               ChangeType
           ) :-
    !, ChangeType = inserted.
 
array_insert_or_replace(
               avl( L, K, E0, R )/H,
               K,E,
               avl( L, K, E, R )/H,
               ChangeType
            ) :-
    !, ChangeType = replaced(E0).
 
array_insert_or_replace(
               avl(L0,K0,E0,R0)/H0,
               K,E,
               TF,
               ChangeType
            ) :-
    K@<K0,
    !,
    array_insert_or_replace( L0, K,E, avl(L1,K1,E1,R1)/H1, ChangeType ),
    (
        ChangeType = inserted
    ->
        avl_combine( L1, K1,E1, R1, K0,E0, R0, TF )
    ;
        TF = avl( avl(L1,K1,E1,R1)/H1, K0,E0, R0 )/H0
    ).
 
array_insert_or_replace(
               avl(L0,K0,E0,R0)/H0,
               K,E,
               TF,
               ChangeType
            ):-
    K@>K0,
    !,
    array_insert_or_replace( R0, K, E, avl(L1,K1,E1,R1)/H1, ChangeType ),
    (
        ChangeType = inserted
    ->
        avl_combine( L0, K0,E0, L1, K1,E1, R1, TF )
    ;
        TF = avl( L0, K0,E0, avl(L1,K1,E1,R1)/H1 )/H0
    ).
 
 
/*  Deleting elements.  */
 
 
array_delete( avl(nil/0,K,E,R0)/_, K, E, R0 ) :- !.
 
array_delete( avl(L0,K,E,nil/0)/_, K, E, L0 ) :- !.
 
array_delete( avl(L0,K,E,R0)/_, K, E, avl(L1,K1,E1,R1)/H1 ) :-
    !,
    array_delete1( K, E, L0,K,E,R0, L1,K1,E1,R1,H1 ).
    /*  Here if K is in the top node, but both sons are not empty. */
 
array_delete( avl(L0,K0,E0,R0)/_, K, E, avl(L1,K1,E1,R1)/H1 ) :-
    /*  K0 \= K  */
    array_delete( K, E, L0,K0,E0,R0, L1,K1,E1,R1,H1 ).
 
 
/*  array_delete( K+,E?, L0+,K0+,E0+,R0+, L1-,K1-,E1-,R1-,H1- ):
        Called to delete a key from a tree when that key is not
        in the topmost node.
*/
array_delete( K, E, L0,K0,E0,Rt0/Rh0, Lt1/Lh1,K0,E0,Rt0/Rh0,H1 ) :-
    K @< K0,
    !,
    array_delete( L0, K, E, Lt1/Lh1 ),
    max1( Lh1, Rh0, H1 ).
 
array_delete( K, E, Lt0/Lh0,K0,E0,R0, Lt0/Lh0,K0,E0,Rt1/Rh1,H1 ) :-
    /*  K @> K0  */
    !,
    array_delete( R0, K, E, Rt1/Rh1 ),
    max1( Lh0, Rh1, H1 ).
 
 
/*
        Both left and right descendants are non-empty, so
        result will cntain at least two elements.
*/
array_delete1( K, E, L0,K,E,R0, LF,KF,EF,RF,HF ) :-
    avl_higher( L0, R0 ),
    !,
    avl_lrot_if_nec( L0, L0_ ),
    avl_rrot( L0_,K,E,R0, L1,K1,E1,R1,_ ),
    array_delete( K, E, L1,K1,E1,R1, LF,KF,EF,RF,HF ).
 
array_delete1( K, E, L0,K,E,R0, LF,KF,EF,RF,HF ) :-
    /* not avl_higher( L0, R0 ), */
    !,
    avl_rrot_if_nec( R0, R0_ ),
    avl_lrot( L0,K,E,R0_, L1,K1,E1,R1,_ ),
    array_delete( K, E, L1,K1,E1,R1, LF,KF,EF,RF,HF ).
 
 
/*  Arrays to- and from lists.  */
 
 
list_to_array( L, T ) :-
    list_to_array( L, nil/0, T ).
 
 
list_to_array( [], T, T ) :- !.
 
list_to_array( [K-E|Tail], T0, TF ) :-
    array_insert( T0, K, E, T1 ),
    list_to_array( Tail, T1, TF ).
 
 
array_to_list( T, L ) :-
    array_to_list( T, [], L ).
 
 
array_to_list( nil/_, L, L ) :- !.
 
array_to_list( avl(Left,K,E,Right)/_, L0, L ) :-
    array_to_list( Right, L0, L1 ),
    array_to_list( Left, [K-E|L1], L ).
 
 
array_ranged_to_list( T, Lub, Upb, L ) :-
    array_ranged_to_list( T, Lub, Upb, [], L ).
 
 
array_ranged_to_list( nil/_, _, _, L, L ) :- !.
 
array_ranged_to_list( avl(Left,K,E,Right)/_, Lub, Upb, L0, L ) :-
    (
        Upb @=< K
    ->
        L1 = L0
    ;
        array_ranged_to_list( Right, Lub, Upb, L0, L1 )
    ),
    (
        Lub @=< K, K @=< Upb
    ->
        L2 = [K-E|L1]
    ;
        L2 = L1
    ),
    (
        Lub @>= K
    ->
        L = L2
    ;
        array_ranged_to_list( Left, Lub, Upb, L2, L )
    ).
 
 
array_filtered_to_list( T, K, E, Filter, L ) :-
    array_filtered_to_list( T, K, E, Filter, [], L ).
 
 
array_filtered_to_list( nil/_, _, _, _, L, L ) :- !.
 
array_filtered_to_list( avl(Left,K0,E0,Right)/_, K, E, Filter , L0, L ) :-
    array_filtered_to_list( Right, K, E, Filter, L0, L1 ),
    (
        not(( K=K0, E=E0, Filter ))
    ->
        L2 = L1
    ;
        L2 = [K0-E0|L1]
    ),
    array_filtered_to_list( Left, K, E, Filter, L2, L ).
 
 
/*  Looping over arrays  */
 
 
for_in_array( K, E, avl(Left,K0,E0,Right)/_, Goal ) :-
    for_in_array(K,E,Left,Goal),
    fail.
 
for_in_array( K, E, avl(_,K0,E0,_)/_, Goal ) :-
    K=K0,
    E=E0,
    (
        Goal
    ->
        true
    ;
        bug('for_in_array: goal failed', Goal)
    ),
    fail.
 
for_in_array( K, E, avl(Left,K0,E0,Right)/_, Goal ) :-
    for_in_array(K,E,Right,Goal),
    fail.
 
for_in_array( _, _, _, _ ).    
 
 
for_ranged_in_array( K, E, Lub, Upb, avl(Left,K0,E0,_)/_, Goal ) :-
    Lub @< K0,
    for_ranged_in_array(K,E,Lub,Upb,Left,Goal),
    fail.
 
for_ranged_in_array( K, E, Lub, Upb, avl(_,K0,E0,_)/_, Goal ) :-
    K0 @>= Lub, K0 @=< Upb,
    K=K0,
    E=E0,
    (
        Goal
    ->
        true
    ;
        bug('for_ranged_in_array: goal failed', Goal)
    ),
    fail.
 
for_ranged_in_array( K, E, Lub, Upb, avl(_,K0,E0,Right)/_, Goal ) :-
    Upb @> K0,
    for_ranged_in_array(K,E,Lub,Upb,Right,Goal),
    fail.
 
for_ranged_in_array( _, _, _, _, _, _ ).
 
 
/*  Miscellaneous predicates.  */
 
 
array_is_empty( nil/0 ).
 
 
is_array( nil/0 ) :- !.
is_array( avl(_,_,_,_)/_ ).
 
 
array_member( K, E, avl(L0,K0,E0,R0)/_ ) :-
    array_member( K, E, L0 )
    ;
    K=K0, E=E0
    ;
    array_member( K, E, R0 ).
 
 
array_value( avl(Left,K0,E0,Right)/_, K, E ) :-
    (
        K = K0
    ->
        E = E0
    ;
        array_value( Left, K, E )
    ->
        true
    ;
        array_value( Right, K, E )
    ->
        true
    ;
        fail
    ).
 
 
array_first( avl( nil/0, K,E, _)/_, K, E ) :- !.
 
array_first( avl(L,_,_,_)/_, K, E ) :-
    array_first( L, K, E ).
 
 
array_last( avl( _, K,E, nil/0 )/_, K, E ) :- !.
 
array_last( avl(_,_,_,R)/_, K, E ) :-
    array_last( R, K, E ).
 
 
array_length( T, L ) :-
    array_length( T, 0, L ).
 
 
array_length( nil/0, L, L ) :- !.
 
array_length( avl(Left,_,_,Right), L0, L ) :-
    array_length( Left, L0, L1 ),
    array_length( Right, L1, L2 ),
    L is L2 + 1.
 
 
/*
Writing arrays.
---------------
 
As usual with sequences of things, we have to be careful about the
"gaps" (this causes problems so frequently, I'm inclined to suspect a
fundamental bug in the Universe. A better-designed universe would have
in each sequence the same number of gaps and elements).
 
Anyway, when writing sequences, the gaps are the separators between
elements. We must make sure there's a comma between each pair of
elements, but not before the first or after the last. To do this,
portray_array/3 has its second and third arguments:
    portray_array( T, Prefix0+, Prefix- )
where Prefix0 is the prefix ( '{' or ',' ) to be written _before_ the
next key-and-entry that portray_array writes; Prefix is the prefix to be
written after the next element _following the call of_ portray_array.
 
If the code for 'portray_array' seems mysterious, think of it as being
derived from this code just below for 'funny_portray_array', where
instead of placing a '{' before the first element, and a ',' before all
the others, we place the element's position in the sequence. So in
    funny_portray_array( T, P0+, P- )
P0 is the position of the next element to be written, and P will be the
number of the next element following the call of funny_portray_array.
 
    funny_portray_array( nil/0 ) :- !.
 
    funny_portray_array( T ) :-
        funny_portray_array( T, 1, _ ).
 
 
    funny_portray_array( nil/0, P, P ) :- !.
 
    funny_portray_array( avl(Left,K,E,Right)/_, P0, P ) :-
        funny_portray_array( Left, P0, P1 ),
        write(' '), write( P1 ), write(' '),
        print(K), write(':'), print(E),
        P2 is P1 + 1,
        funny_portray_array( Right, P2, P ).
 
All we're doing in portray_array is to collapse the counting code above
by saying that only two values of P matter: 1 and not-1.
*/
 
 
portray_array( nil/0 ) :-
    !,
    write( '{}' ).
 
portray_array( T ) :-
    portray_array( T, '{', _ ),
    write( '}' ).
 
 
portray_array( nil/0, Prefix, Prefix ) :- !.
 
portray_array( avl(Left,K,E,Right)/_, Prefix0, Prefix ) :-
    portray_array( Left, Prefix0, Prefix1 ),
    write( Prefix1 ), print(K), write(':'), print(E),
    portray_array( Right, ',' , Prefix ).
 
 
/*
AVL-tree utilities - rotating and re-balancing.
-----------------------------------------------
*/
 
 
avl_combine(
         T0/H0,
         K1,E1,
         avl( L2, K2,E2, R2 )/H2,
         K3,E3,
         T4/H4,
         avl(
             avl( T0/H0, K1,E1, L2 )/Ha,
             K2,E2,
             avl( R2, K3,E3, T4/H4 )/Hc
         )/HF
       ):-
    H2 > H0,
    H2 > H4,
    Ha is H0+1,
    Hc is H4+1,
    HF is Ha+1.
 
 
avl_combine( T0/H0, K1,E1, T2/H2, K3,E3, T4/H4,
             avl(LF,KF,EF,RF)/HF
           ):-
    H0 >= H2,
    H0 >= H4,
    !,
    avl_rrot( T0/H0, K1,E1, T2/H2, K3,E3, T4/H4, LF,KF,EF,RF,HF ).
 
avl_combine( T0/H0, K1,E1, T2/H2, K3,E3, T4/H4,
             avl(LF,KF,EF,RF)/HF
           ) :-
    H4 >= H2,
    H4 >= H0,
    !,
    avl_lrot( T0/H0, K1,E1, T2/H2, K3,E3, T4/H4, LF,KF,EF,RF,HF ).
 
avl_combine( TH0, K1,E1, TH2, K3,E3, TH4, _ ) :-
    bug( 'avl_combine/8: unexpected failure', [TH0,K1,E1,TH2,K3,E3,TH4] ).
 
 
avl_lrot( avl(L0,K0,E0,R0)/_, avl(LF,KF,EF,RF)/HF ) :-
    !,
    avl_lrot( L0,K0,E0,R0, LF,KF,EF,RF,HF ).
 
avl_lrot( T0, _ ) :-
    bug( 'avl_lrot/2: unexpected failure', T0 ).
 
 
avl_lrot( L0, K0,E0, avl(L1,K1,E1,R1)/_,
          LF, KF,EF, RF, HF
        ) :-
    avl_lrot( L0, K0,E0, L1, K1,E1, R1,
              LF, KF,EF, RF, HF
            ).
 
 
avl_lrot( T0/H0, K1,E1, T2/H2, K3,E3, T4/H4,
          avl(T0/H0,K1,E1,T2/H2)/Ha, K3,E3, T4/H4, HF
        ) :-
    max1( H0, H2, Ha ),
    max1( Ha, H4, HF ).
 
 
avl_rrot( avl(L0,K0,E0,R0)/_, avl(LF,KF,EF,RF)/HF ) :-
    !,
    avl_rrot( L0,K0,E0,R0, LF,KF,EF,RF,HF ).
 
avl_rrot( T0, _ ) :-
    bug( 'avl_rrot/2: unexpected failure', T0 ).
 
 
avl_rrot( avl(L1,K1,E1,R1)/_, K0,E0, R0,
          LF, KF,EF, RF, HF
    ) :-
    avl_rrot( L1, K1,E1, R1, K0,E0, R0,
              LF, KF,EF, RF, HF
            ).
 
 
avl_rrot( T0/H0, K1,E1, T2/H2, K3,E3, T4/H4,
          T0/H0, K1,E1, avl(T2/H2,K3,E3,T4/H4)/Ha, HF
        ) :-
    max1( H4, H2, Ha ),
    max1( Ha, H0, HF ).
 
 
avl_lrot_if_nec( avl(L0,K0,E0,R0)/_, avl(LF,KF,EF,RF)/HF ) :-
    avl_lower( L0, R0 ),
    !,
    avl_lrot( L0,K0,E0,R0, LF,KF,EF,RF,HF ).
 
avl_lrot_if_nec( T, T ).
 
 
avl_rrot_if_nec( avl(L0,K0,E0,R0)/_, avl(LF,KF,EF,RF)/HF ) :-
    avl_higher( L0, R0 ),
    !,
    avl_rrot( L0,K0,E0,R0, LF,KF,EF,RF,HF ).
 
avl_rrot_if_nec( T, T ).
 
 
/*
Other AVL tree utilities.
-------------------------
*/
 
 
/*  max1( A+, B+, C- ):
        C = 1+max(A,B)
*/
max1( A, B, C ):-
    max( A, B, C0 ),
    C is C0 + 1.
 
 
/*  avl_higher( T1+, T2+ ):
        T1 is higher than T2.
*/
avl_higher( N1/H1, N2/H2 ) :-
    H1 > H2.
 
 
/*  avl_lower( T1+, T2+ ):
        T1 is lower than T2.
*/
avl_lower( N1/H1, N2/H2 ) :-
    H1 < H2.
 
 
:- endmodule.
