--::::::::::
--lipoptcn.ads -- List_Pos_Pt_Cntl
--::::::::::
-- 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 zqklst is
--       a zqklst of n objects, then (h, zqklst) 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(zqklst)  The largest list contianing zqklst as a sublist
--  PL(zqklst)  If LF(zqklst) /= zqklst, then PL(zqklst) = (h, zqklst)
------------------------------------------------------------------
--  This package should be instantiated with an BOUND
--  List_Type made visible as UNBOUND MANAGED CONTROLLED
------------------------------------------------------------------
with List_Pos_LPBase, Ada.Finalization, Pt_To_Lpt;
use Ada.Finalization;
generic
   type Object_Type is private;
package List_Pos_Pt_Cntl is
   ------------------------------------------------
   -- DO NOT USE zqklst & ptl
      package ptl is new Pt_To_Lpt (Object_Type);
      package zqklst is new List_Pos_LPBase
         (Object_Type, ptl.Initialize, ptl.Finalize, ptl.Copy, ptl.Swap);
   ------------------------------------------------

   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;

   List_Underflow  : exception renames zqklst.List_Underflow;
   List_Overflow   : exception renames zqklst.List_Overflow;
   Undefined_position: exception renames zqklst.Undefined_Position;
   Invalid_Remove  : exception renames zqklst.Invalid_Remove;
   Invalid_Share   : exception renames zqklst.Invalid_Share;

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

procedure Move_To_Rear (List: in out List_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 List_Type);
   ------------------------------------------------
   -- Pre Cond : List = (i, ...), i /= 0
   -- Post Cond: List' = (i-1, ...),
   -- Exception: Undefined_Position, List_Underflow,
   ------------------------------------------------

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

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

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

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

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

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

procedure Append (List    : in out List_Type;
                  New_Tail: in out List_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 List_Type;
                  New_Tail: in     Object_Type);

procedure Insert_Before (Object: in     Object_Type;
                         List  : in out List_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
   ------------------------------------------------
procedure Insert_Before (Objects: in out List_Type;
                         List   : in out List_Type);

procedure Insert_After (Object: in     Object_Type;
                        List  : in out List_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
   ------------------------------------------------
procedure Insert_After (Objects: in out List_Type;
                        List   : in out List_Type);

procedure Process_Current (List   : in     List_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 List_Type;
                          Object:    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
   ------------------------------------------------

procedure Update_Current (List  : in     List_Type;
                          Object: in     Object_Type);
   ------------------------------------------------
   -- Pre Cond : List = (i, ...);
   -- Post Cond: List' = (i, a , a , ..., a   , Object, a   , ..., a )
   --                         1   2        i-1           i+1        n
   ------------------------------------------------

procedure Slice_Tail (Source: in out List_Type;
                      Target: in out List_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 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
         Actual: zqklst.LPList_Type;
      end record;
end List_Pos_Pt_Cntl;