/* searchtree.q: An example showing the use of algebraic data types with
   inheritance. */

/* We first define a generic search tree type (we call this an "abstract" type
   since it doesn't have any constructors of its own). This type is used as
   the supertype for two concrete subtypes BinTree and AVLTree below. NB: The
   `public' keyword causes the type to be exported so that it can be used in
   other modules which import this script. */

public type Tree;

/* Interface operations to be provided by all subtypes of the Tree type:
   insert/delete elements, compute the list of members (in ascending order),
   test membership. In this example we allow multiple instances of the same
   element in a tree. This means that the resulting trees will represent
   multisets. */

public insert T X, delete T X, members T, member T X;

/* Generic tree operations implemented in terms of the interface functions:
   size, union, difference, intersection, subset comparison. */

#T:Tree				= #members T;

T1:Tree + T2:Tree		= foldl insert T1 (members T2);
T1:Tree - T2:Tree		= foldl delete T1 (members T2);
T1:Tree * T2:Tree		= T1 - (T1 - T2);

T1:Tree <= T2:Tree		= all (member T2) (members T1);
T1:Tree >= T2:Tree		= all (member T1) (members T2);

T1:Tree < T2:Tree		= (T1<=T2) and then not (T2<=T1);
T1:Tree > T2:Tree		= (T1>=T2) and then not (T2>=T1);

(T1:Tree = T2:Tree)		= (T1<=T2) and then (T2<=T1);
T1:Tree <> T2:Tree		= not (T1=T2);

/* The binary tree and AVL tree subtypes, along with corresponding virtual
   constructor functions which create a tree from a list of its members. The
   real constructors are private so that they cannot be (ab)used outside this
   module. */

public type BinTree : Tree = virtual bintree Xs
			   | private const nil, bin X T1 T2;
public type AVLTree : Tree = virtual avltree Xs
			   | private const anil, abin H X T1 T2;

/* Define the corresponding views in terms of the virtual constructors. */

view T:BinTree			= '(bintree ~(members T));
view T:AVLTree			= '(avltree ~(members T));

/* Note that the above definitions of the generic tree operations apply to
   _all_ subtypes of Tree (provided that they implement the required interface
   operations). Examples: */

def T1 = avltree [17,5,26,5], T2 = bintree [8,17], S = T1+T2, T = T1-T2;

/* Also note that the views for BinTree and AVLTree objects we defined above
   let us use the virtual constructors in pattern-matching definitions just as
   if they were real constructors. The virtual representations of these
   objects will be constructed on the fly, as they are required during pattern
   matching. Since the virtual constructors are public, this will even work
   outside this module. Examples: */

def avltree Xs = S, avltree Ys = T;

mymembers (bintree Xs)		= Xs;
mymembers (avltree Xs)		= Xs;

/* Implementation of the BinTree operations. */

bintree Xs			= foldl insert nil Xs;

members nil			= [];
members (bin X T1 T2)		= members T1 ++ [X] ++ members T2;

member nil Y			= false;
member (bin X T1 T2) Y		= member T1 Y if X>Y;
				= member T2 Y if X<Y;
				= true otherwise;

insert nil Y			= bin Y nil nil;
insert (bin X T1 T2) Y		= bin X (insert T1 Y) T2 if X>Y;
				= bin X T1 (insert T2 Y) otherwise;

delete nil Y			= nil;
delete (bin X T1 T2) Y		= bin X (delete T1 Y) T2 if X>Y;
				= bin X T1 (delete T2 Y) if X<Y;
				= join T1 T2 otherwise;

join nil T2			= T2;
join T1:BinTree T2		= bin (last T1) (init T1) T2 otherwise;

init (bin X T1 nil)		= T1;
init (bin X T1 T2)		= bin X T1 (init T2) otherwise;

last (bin X T1 nil)		= X;
last (bin X T1 T2)		= last T2 otherwise;

/* Implementation of the AVLTree operations (after Bird/Wadler). */

avltree Xs			= foldl insert anil Xs;

members anil			= [];
members (abin H X T1 T2)
				= members T1 ++ [X|members T2];

member anil Y			= false;
member (abin H X T1 T2) Y
				= member T1 Y if X>Y;
				= member T2 Y if X<Y;
				= true otherwise;

insert anil Y			= abin 1 Y anil anil;
insert (abin H X T1 T2) Y	= rebal (mknode X (insert T1 Y) T2) if X>Y;
				= rebal (mknode X T1 (insert T2 Y)) otherwise;

delete anil Y			= anil;
delete (abin H X T1 T2) Y	= rebal (mknode X (delete T1 Y) T2) if X>Y;
				= rebal (mknode X T1 (delete T2 Y)) if X<Y;
				= join T1 T2 if X=Y;

join anil T2			= T2;
join T1:AVLTree T2		= rebal (mknode (last T1) (init T1) T2)
				    otherwise;

init (abin H X T1 anil)		= T1;
init (abin H X T1 T2)		= rebal (mknode X T1 (init T2)) otherwise;

last (abin H X T1 anil)		= X;
last (abin H X T1 T2)		= last T2 otherwise;

/* mknode constructs an AVL tree node, computing the height value */

mknode X T1 T2			= abin (max (height T1) (height T2) +1)
				  X T1 T2;

/* height and slope compute the height and slope (difference between heights
   of the left and the right subtree), respectively */

height anil			= 0;
height (abin H X T1 T2)		= H;

slope anil			= 0;
slope (abin H X T1 T2)		= height T1 - height T2;

/* rebal rebalances after single insertions and deletions */

rebal T				= shl T if slope T = -2;
				= shr T if slope T = 2;
				= T otherwise;

/* rotation operations */

rol (abin H X1 T1 (abin H2 X2 T2 T3))
				= mknode X2 (mknode X1 T1 T2) T3;

ror (abin H1 X1 (abin H2 X2 T1 T2) T3)
				= mknode X2 T1 (mknode X1 T2 T3);

shl (abin H X T1 T2)		= rol (mknode X T1 (ror T2)) if slope T2 =1;
				= rol (abin H X T1 T2) otherwise;

shr (abin H X T1 T2)		= ror (mknode X T1 (ror T2)) if slope T2 = -1;
				= ror (abin H X T1 T2) otherwise;