--::::::::::
--liposlpb.ads  -- List_Pos_LPBase
--::::::::::
-- Copyright (c) 1994      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
--  (...)  A list of n objects may be viewed as an n-tuple.  If Lst is
--       a Lst of n objects, then (h, Lst) is a list of n+1 objects.
--  *    Currently viewed object.  (..., x*, ...) indicates that x is the
--       currently viewed object in the list
--  #(L) No. of objects in the list L
--  L(i) The i-th object in the list L, L(1) is front, L(#(L)) is rear
--  FL(Lst)  The largest list contianing Lst as a sublist
--  PL(Lst)  If LF(Lst) /= Lst, then PL(Lst) = (h, Lst)
------------------------------------------------------------------
--  This is a base package, from which other packages will be
--  derived, DO NOT MAKE DIRECT USE OF THIS PACKAGE
------------------------------------------------------------------

generic
   type Object_Type is limited private;
   with procedure Initialize (Object: in out Object_Type);
   with procedure Finalize (Object: in out Object_Type);
   with procedure Copy (Source: in     Object_Type;
                        Target: in out Object_Type);
   with procedure Swap (Source, Target: in out Object_Type);
package List_Pos_LPBase is

   type LPList_Type is private;

   List_Underflow  : exception;
   List_Overflow   : exception;
   Undefined_position: exception;
   Invalid_Remove  : exception;
   Invalid_Share   : exception;

procedure Initialize (List: in out LPList_Type);
   ------------------------------------------------------------------
   -- Pre Cond : List not initialized
   -- Post Cond: List = (0)
   -- Exception: None
   ------------------------------------------------------------------

procedure Finalize (List: in out LPList_Type);
   ------------------------------------------------------------------
   -- Pre Cond : List is initialized
   -- Post Cond: List not initialized
   -- Exception: None
   ------------------------------------------------------------------

procedure Move_To_Front (List: in out LPList_Type);
   ------------------------------------------------------------------
   -- Pre Cond : List = (i, ...), List /= (0)
   -- Post Cond: List' = (1, ...)
   -- Exception: List_Underflow
   ------------------------------------------------------------------

procedure Move_To_Rear (List: in out LPList_Type);
   ------------------------------------------------------------------
   -- Pre Cond : List /= (0), List = (i, ...)
   -- Post Cond: List' = (n, ...) where n is the number of objects in
   --            the list
   -- Exception: List_Underflow
   ------------------------------------------------------------------

procedure Move_Towards_Front (List: in out LPList_Type);
   ------------------------------------------------------------------
   -- Pre Cond : List = (i, ...), i /= 0
   -- Post Cond: List' = (i-1, ...),
   -- Exception: Undefined_Position, List_Underflow,
   ------------------------------------------------------------------

procedure Move_Towards_Rear (List: in out LPList_Type);
   ------------------------------------------------------------------
   -- Pre Cond : List /= {}, List = (..., x*, y, ...)
   -- Post Cond: List' = ((i+1) mod (n+1), ...),
   -- Exception: Undefined_Position, List_Underflow
   ------------------------------------------------------------------

function Current_Object (List: LPList_Type) return Object_Type;
   ------------------------------------------------------------------
   -- Pre Cond : List = (i, ...)
   -- Post Cond: returns a
   --                     i
   -- Exception: List_Underflow or Undefined_Position
   ------------------------------------------------------------------

function Current_Defined (List: LPList_Type) return boolean;
   ------------------------------------------------------------------
   -- Pre Cond : List = (i, ...)
   -- Post Cond: returns i /= 0
   -- Exception: List_Underflow or Undefined_Position
   ------------------------------------------------------------------

function Empty (List: LPList_Type) return boolean;
   ------------------------------------------------------------------
   -- Pre Cond : None
   -- Post Cond: returns (List = (0))
   -- Exception: None
   ------------------------------------------------------------------

function At_Rear (List : LPList_Type) return boolean;
   ------------------------------------------------------------------
   -- Pre Cond : List = (i, ...)
   -- Post Cond: returns (i = n)
   -- Exception: Undefined_Position
   ------------------------------------------------------------------

function At_Front (List: LPList_Type) return boolean;
   ------------------------------------------------------------------
   -- Pre Cond : List = (i, ...)
   -- Post Cond: returns (i = 1)
   -- Exception: Undefined_Position
   ------------------------------------------------------------------

procedure Append (List    : in out LPList_Type;
                  New_Tail: in out LPList_Type);
   ------------------------------------------------------------------
   -- Pre Cond : List = (i, ...), New_Tail = (j, ...)
   -- Post Cond: List' = (List, New_Tail)
   --            New_Tail' = (0)
   -- Exception: List_Underflow
   ------------------------------------------------------------------
procedure Append (List    : in out LPList_Type;
                  New_Tail: in out Object_Type);
   -- NOTE:   Swap used to exchange value of Object_Type

procedure Insert_Before (Object: in out Object_Type;
                         List  : in out LPList_Type);
   ------------------------------------------------------------------
   -- Pre Cond : List = (i, ...)
   -- Post Cond: List' = (i+1, a , a , ... a   , Object, a , ..., a )
   --                           1   2       i-1           i        n
   -- Exception: Undefined_Position, List_Overflow
   -- NOTE:   Swap used to exchange value of Object_Type
   ----------------------------------------------------------
procedure Insert_Before (Objects: in out LPList_Type;
                         List   : in out LPList_Type);

procedure Insert_After (Object: in out Object_Type;
                        List  : in out LPList_Type  );
   ---------------------------------------------------------
   -- Pre Cond : List = (i, ...)
   -- Post Cond: List' = (i, a , a , ... a , Object, a   , ..., a )
   --                         1   2       i           i+1        n
   -- Exception: Undefined_Position, List_Overflow
   -- NOTE:   Swap used to exchange value of Object_Type
   ---------------------------------------------------------
procedure Insert_After (Objects: in out LPList_Type;
                        List   : in out LPList_Type);

type In_Place_Process_Type is access
   procedure (Object: in out Object_Type);

procedure Process_Current (List   : in     LPList_Type;
                           Process:        In_Place_Process_Type);
   ----------------------------------------------------------------
   -- Pre Cond : List = (i, ...)
   -- Post Cond: Calls Process (a ) performed
   --                            i
   -- Exception: Depends upon Process
   ------------------------------------------------------------------

procedure Remove_Current (List  : in out LPList_Type;
                          Object: in out Object_Type);
   ---------------------------------------------------------
   -- Pre Cond : List = (i, ...)
   -- Post Cond: Object' = a , List' = (i, a , a , ..., a   , a   , ..., a )
   --                       i               1   2        i-1   i+1        n
   --            If i = n, then List' = (n-1, ...)
   -- Exception: Invalid_Remove
   -- NOTE:   Swap used to exchange value of Object_Type
   ----------------------------------------------------------

procedure Update_Current (List  : in     LPList_Type;
                          Object: in out Object_Type);
   ---------------------------------------------------------
   -- Pre Cond : List = (i, ...);
   -- Post Cond: List' = (i, a , a , ..., a   , Object, a   , ..., a )
   --                         1   2        i-1           i+1        n
   -- NOTE:   Swap used to exchange value of Object_Type
   ----------------------------------------------------------

procedure Slice_Tail (Source: in out LPList_Type;
                      Target: in out LPList_Type);
   ---------------------------------------------------------------
   -- Pre-cond : Source = (i, ...)
   -- Post-cond: Source' = (i, a , a , ..., a ), Target' = (1, a   , ..., a )
   --                           1   2        i                  i+1        n
   -- Exception: Invalid_Share
   ---------------------------------------------------------------

procedure Copy (Source: in     LPList_Type;
                Target: in out LPList_Type);
   ------------------------------------------------------------------
   -- Pre Cond : None
   -- Post Cond: Target' = Source
   -- Exception: None
   ------------------------------------------------------------------

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

private
   function Size (List: LPList_Type) return natural;

   type Object_Holder;
   type List_Ptr is access Object_Holder;
   type Object_Holder is
      record
         Object  : Object_Type; -- Generic data type
         Previous: List_Ptr:= null;
         Next    : List_Ptr:= null;
      end record;

   type List_Descriptor;
   type Desc_Ptr is access List_Descriptor;

   type List_Descriptor is
      record
         Size  : integer := 0;
         First : List_Ptr:= null;
         Last  : List_Ptr:= null;
         Shared: positive:= 1;
      end record;

   type LPList_Type is
      record
         Current: List_Ptr:= null;
         Actual : Desc_Ptr:= null;
      end record;

end List_Pos_LPBase;