-- Copyright (c) 1995/6    John Beidler
--                         Computing Sciences Dept.
--                         Univ. of Scranton, Scranton, PA 18510
--
--                         (717) 941-7446 voice
--                         (717) 941-4250 FAX
--                         beidler@cs.uofs.edu
--
--  For use by non-profit educational institutions only.
--  This software is GUARANTEED.  Please report any errors.  All
--  corrections will be made as soon as possible (normally within
--  one working day).
------------------------------------------------------------------
--  Assertion notation:
--   /=  not equal
--   ()  empty list
--   ,   and
--   |   or
--   '   If x passed as argument then x' is result after subprog executes
-- () or (h,T) A list is either empty of an ordered, (h,T), where h is an.
--       object called the head of the list, and T is a list, called the
--       tail of the list being represented by the ordered pair.
------------------------------------------------------------------
with Ada.Finalization; use Ada.Finalization;
package List_Polymorphic_Cntl is

type Place_Holder is new controlled with private;
   procedure Initialize (Object: in out Place_Holder);
   procedure Finalize (Object: in out Place_Holder);
   procedure Adjust (Object: in out Place_Holder);
   -------------------------------------------------------------
   -- When extending Place_Holder type the client must provide
   -- Initialize, Finalize, and Adjust procedures for the extended
   -- type UNLESS the extension is bound AND an aggregate is used
   -- to initialize the components in the extension
   -------------------------------------------------------------

type Holder_Class_Ptr is access Place_Holder'Class;
   procedure Recycle (Point: in out Holder_Class_Ptr);

type List_Type is new controlled with private;
   procedure Initialize (List: in out List_Type);
   procedure Finalize (List: in out List_Type);
   procedure Adjust (List: in out List_Type);

   List_Underflow  : exception;
   List_Overflow   : exception;

function Tail_Of (List: List_Type) return List_Type;
   ------------------------------------------------------------------
   -- Pre Cond : List /= {}, List = (head, tail) head is
   --            an Place_Holder and tail is a List_Type
   -- Post Cond: Returns tail
   -- Exception: Invalid_Position, List_Underflow.
   ------------------------------------------------------------------

generic
   type Extended_Type is new Place_Holder with private;
function g_Head_Of (List: List_Type) return Extended_Type;

function Head_Of (List: List_Type) return Holder_Class_Ptr;
   ------------------------------------------------------------------
   -- Pre Cond : List = (h, tail), i.e. not empty
   -- Post Cond: returns copy of h
   -- Exception: List_Underflow or Invalid_Position
   ------------------------------------------------------------------

function Empty (List: in     List_Type) return boolean;
   ------------------------------------------------------------------
   -- Pre Cond : None
   -- Post Cond: returns (List /= {})
   -- Exception: None
   ------------------------------------------------------------------

function Empty_List return List_Type;
   ------------------------------------------------------------------
   -- PostCond: returns ()
   ------------------------------------------------------------------

procedure New_Head (Object: in     Place_Holder'Class;
                    List  : in     List_Type);
   ------------------------------------------------------------------
   -- Pre Cond : List is a (possibly empty) list
   -- Post Cond: List' = (Object, List)
   -- Exception: Invalid_Position, List_Overflow
   -- NOTE:   Swap used to exchange value of Place_Holder
   ----------------------------------------------------------

generic
   type Extended_Type is new Place_Holder with private;
procedure g_Remove_Head (List  : in     List_Type;
                         Object: in out Extended_Type);
procedure Remove_Head (List  : in     List_Type;
                       Object: in out Holder_Class_Ptr);
   ------------------------------------------------------------------
   -- Pre Cond : List = (head, Tail)
   -- Post Cond: List' = Tail
   -- Exception: Invalid_Position, List_Overflow
   -- NOTE:   Swap used to exchange value of Place_Holder
   ----------------------------------------------------------

procedure Swap_Tail (Source: in     List_Type;
                     Target: in     List_Type);
   ---------------------------------------------------------------
   -- Pre-cond : Source = (s, Stail) or (), Target = (t, Ttail) or ()
   --            where Stail and/or Ttail may be ().
   -- Post-cond: Source' = (s, Ttail) or (Ttail),
   --            Target' = (t, Stail) or (Stail)
   -- Exception: Invalid_Share
   ---------------------------------------------------------------

procedure Append (List    : in     List_Type;
                  New_Tail: in out List_Type);
   ------------------------------------------------------------------
   -- Pre Cond : None
   -- Post Cond: List' = List==New_Tail (Net_Tail attached to the end
   --             New_Tail' = {}
   -- Exception: List_Underflow
   ------------------------------------------------------------------
procedure Append (List    : in     List_Type;
                  New_Tail: in     Place_Holder'Class);
   ------------------------------------------------------------------
   -- NOTE:   Swap used to exchange value of Place_Holder
   ------------------------------------------------------------------

procedure Update_Head (List  : in     List_Type;
                       Object: in     Place_Holder'Class);
   ---------------------------------------------------------
   -- Pre Cond : List = (x, tail)
   -- Post Cond: List' = (Object, tail)
   -- Exception: Invalid_Position
   -- NOTE:   Swap used to exchange value of Place_Holder
   ----------------------------------------------------------

procedure Swap (Source: in out List_Type;
                Target: in out List_Type);
   ---------------------------------------------------------
   -- Pre-Cond : None
   -- Post-Cond: Target' = Source, Source' = Target
   -- Exception: None
   ---------------------------------------------------------

private

type Place_Holder is new controlled with
   record
      Next: aliased Holder_Class_Ptr:= null;
   end record;
   ----------------------------------------
type List_Anchor is access all Holder_Class_Ptr;

type List_Type is new controlled with
   record
      Actual: List_Anchor:= null;
      Base  : boolean := true;
   end record;

end List_Polymorphic_Cntl;