-- Copyright (c) 1995      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.
------------------------------------------------------------------
--  For safe use of this package
--  Object_Type is BOUND NONPOLYMORPHIC
--  List_Type is UNBOUND CONTROLLED
------------------------------------------------------------------
with List_LPBase, Ada.Finalization, Pt_To_Lpt;
use Ada.Finalization;
generic
   type Object_Type is private;
package List_Pt_Cntl is
   ---------------------------------------------
   --  WARNING: DO NOT USE zqklst & ptl
       package ptl is new Pt_To_Lpt (Object_Type);
       package zqklst is new List_LPBase
          (Object_Type, ptl.Initialize, ptl.Finalize, ptl.Copy, ptl.Swap);
   ---------------------------------------------

   List_Underflow  : exception renames zqklst.List_Underflow;
   List_Overflow   : exception renames zqklst.List_Overflow;

   subtype In_Place_Process_Type is zqklst.In_Place_Process_Type;
   -- access procedure (Object: in out Object_Type);

type List_Type is new controlled with private;

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

function Head_Of (List: List_Type) return Object_Type;
   ------------------------------------------------------------------
   -- Pre Cond : List /= ()
   -- Post Cond: returns copy of a
   --                             1
   -- Exception: List_Underflow or Invalid_Position
   ------------------------------------------------------------------

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

procedure New_Head (Object: in     Object_Type;
                    List  : in     List_Type);
   ------------------------------------------------------------------
   -- Pre Cond : none
   -- Post Cond: List' = (Object, List)
   -- Exception: Invalid_Position, List_Overflow
   ----------------------------------------------------------

procedure Remove_Head (List  : in     List_Type;
                       Object:    out Object_Type);
   ------------------------------------------------------------------
   -- Pre Cond : none
   -- Post Cond: List = (Object, List')
   -- Exception: Invalid_Position, List_Overflow
   ----------------------------------------------------------

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     List_Type);
   ------------------------------------------------------------------
   -- Pre Cond : None
   -- Post Cond: List' = (List, New_Tail)
   --             New_Tail' = {}
   -- Exception: List_Underflow
   ------------------------------------------------------------------
procedure Append (List    : in     List_Type;
                  New_Tail: in     Object_Type);

procedure Process_Head (List   : in     List_Type;
                        Process:        In_Place_Process_Type);
   ----------------------------------------------------------------
   -- Pre Cond : List = (x, tail)
   -- Post Cond: Process (x) performed
   -- Exception: Depends upon Process
   ------------------------------------------------------------------

procedure Update_Head (List  : in     List_Type;
                       Object: in     Object_Type);
   ---------------------------------------------------------
   -- Pre Cond : List = (x, tail)
   -- Post Cond: List' = (Object, tail)
   -- Exception: Invalid_Position
   ----------------------------------------------------------

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

private
   procedure Initialize (List: in out List_Type);
   procedure Finalize (List: in out List_Type);
   procedure Adjust (List: in out List_Type);

   type List_Type is new controlled with
      record
         Base: boolean := true;
         List: zqklst.LPList_Type;
      end record;

end List_Pt_Cntl;