(*
 * Full equational specs for a binary search tree.  Note that none of the 440
 * equational specs will be this elaborate.  This example shows how more
 * advanced forms of objects can be defined equationally.
 *)


obj BinSearchTree
   components: integer*;
   operations:
      makeTree (integer, BinSearchTree, BinSearchTree) -> (BinSearchTree),
      root (BinSearchTree) -> (integer),
      find (BinSearchTree, integer) -> (BinSearchTree),
      del (BinSearchTree, integer) -> (BinSearchTree),
      reinsert (BinSearchTree, BinSearchTree) -> (BinSearchTree),
      enum (BinSearchTree) -> (List),
      emptyTree () -> (BinSearchTree),
      legalBinSearchTree (BinSearchTree) -> (boolean),    (* Optional *)
      insert (BinSearchTree, integer) -> (BinSearchTree); (* Optional *)

   equations:
      var b,b1,b2: BinSearchTree;
      var e,e1,e2: integer;

      (*
       * Equation for root simply extracts the first arg to makeTree.
       *)
      root(makeTree(e, b1, b2)) == e;


      (*
       * First equation for find is simple empty case.  Second equation uses
       * standard two-way recursion to search in left and right subtrees,
       * depending on whether search key e2 is less than or greater than key e1
       * at current subtree root.  The result of the find is the root of the
       * subtree containing the search key.  Note that find also enforces
       * search tree well-formedness (see well-formedness alternatives below).
       *)
      find(emptyTree(),e) == emptyTree();
      find(makeTree(e1,b1,b2),e2) ==
	 if legalBinSearchTree(makeTree(e1,b1,b2))
	 then if e1 = e2 then makeTree(e1,b1,b2)
	      else if e2 < e1 then find(b1,e2)
		   else find(b2,e2)
	 else
	    emptyTree();

      (*
       * Equations for del are similar to find, except that tree is remade down
       * to the point where the deletion occurs.  Result of del is the orignial
       * tree, less the node containing the key e.
       *)
      del(emptyTree(),e) == emptyTree();
      del(makeTree(e1,b1,b2),e2) ==
	 if e1 = e2 then reinsert(b1,b2)
	 else if e2 < e1 then makeTree(e1,del(b1,e2),b2) 
	      else makeTree(e1,b1,del(b2,e2));

      (*
       * Equations for reinsert define standard search tree insertion.
       * reinsert is an auxiliary operation used to make del equations easier
       * to read.
       *)
      reinsert(b,makeTree(e,b1,b2)) ==
         if b1 = emptyTree()
         then makeTree(e,b,b2) else makeTree(e,reinsert(b,b1),b2);
      reinsert(b,emptyTree()) == b;
      reinsert(emptyTree(),b) == b;

      (*
       * Equations for enum define a standard two-way recursive in-order
       * enumeration.  The result of the enumeration is an in-order list of
       * node values.
       *)
      enum(emptyTree()) == emptyList();
      enum(makeTree(e,b1,b2)) == consl(enum(b1), cons(e, enum(b2)));


      (*
       * ALTERNATIVES FOR OPTIONAL WELL-FORMEDNESS CHECKING
       * Eqns for legalBinSearchTree could be expanded to check search tree
       * well-formedness.
       *)
      legalBinSearchTree(makeTree(e,b1,b2)) == true;

      (*
       * Alternatively, eqns for an insert op could enforce well-formedness.
       *)
      insert(emptyTree(),e) == makeTree(e,emptyTree(),emptyTree());
      insert(makeTree(e1,b1,b2),e2) ==
	 if e1 = e2 then makeTree(e1,b1,b2)
	 else
	    if e2 < e1
	    then makeTree(e1,insert(b1,e2),b2)
	    else makeTree(e1,b1,insert(b2,e2));

end BinSearchTree;


obj List
   components: integer*;
   operations:
      car (List) -> (integer),
      cdr (List) -> (List),
      cons (integer, List) -> (List),
      consl (List, List) -> (List),
      emptyList () -> (List);

   equations:
      var e : integer;
      var l, l1, l2 : List;

      car(cons(e,l)) == e;
      cdr(cons(e,l)) == l;
      car(consl(l1,l2)) == car(l1);
      cdr(consl(l1,l2)) == consl(cdr(l1),l2);
      consl(emptyList(),l) == l;
      consl(l,emptyList()) == l;
   description: (*
      This is a fully equational definition of a Lisp/ML-style list.  It's used
      in the BinarySearchTree object to store the result of the enum operation.
   *);
end List;



(*** Here are some sample reductions:


 *** SAMPLE 1: ***

reduce del(
  makeTree(5,
    makeTree(2,
      makeTree(1,emptyTree,emptyTree),
	makeTree(3,emptyTree,emptyTree)),
    makeTree(10,
      makeTree(6,emptyTree,emptyTree),
      makeTree(12,emptyTree,emptyTree))),
  5);

 *** Result after 9 rewrites is:

 makeTree(10,
   makeTree(6,
        makeTree(2,
          makeTree(1,emptyTree,emptyTree),
          makeTree(3,emptyTree,emptyTree)),
        emptyTree),
      makeTree(12,emptyTree,emptyTree))

 ***
 *** The preceding reduction deletes node 5 from the following bin search tree:

		5
		|
	|-------|-------|
	|		|
	2		10
	|	        |
	|---|	    |---|---|
	    |	    |       |
	    3	    6	    12


 *** resulting in:

		10
		|
	|-------|-------|
	|		|
	6		12
	|
    |---|
    |
    2
    |
|---|---|
|       |
1       3




 *** SAMPLE 2: ***

reduce enum(
  makeTree(5,
    makeTree(2,
	 makeTree(1,emptyTree,emptyTree),
	 makeTree(3,emptyTree,emptyTree)),
    makeTree(10,
	 makeTree(6,emptyTree,emptyTree),
	 makeTree(12,emptyTree,emptyTree)))
  );

 *** Result after 19 rewrites is:
    consl(consl(cons(1,emptyList),cons(2,cons(3,emptyList))),
       cons(5,consl(cons(6,emptyList),cons(10,cons(12,emptyList)))))

 ***
 *** The preceding reduction enumerates the following tree:

		5
		|
	|-------|-------|
	|		|
	2		10
	|	        |
    |---|---|	    |---|---|
    |	    |	    |       |
    1	    3	    6	    12

 *** resulting in the list

	[ 1, 2, 3, 5, 6, 10, 12 ]



 *** SAMPLE 3: ***

reduce car(cdr(cdr(
 enum(
  makeTree(5,
    makeTree(2,
	 makeTree(1,emptyTree,emptyTree),
	 makeTree(3,emptyTree,emptyTree)),
    makeTree(10,
	 makeTree(6,emptyTree,emptyTree),
	 makeTree(12,emptyTree,emptyTree)))
  )))) .

*** Result after 27 rewrites is: 3

*** The preceding reduction selects the 3rd element of the enumerated list
*** using the lisp caddr function; i.e.,

	caddr([ 1, 2, 3, 5, 6, 10, 12 ])

*** which gets the 3.

***
***)