--::::::::::
--lipocnen.ads -- List_Pos_Cntl_En 
--::::::::::
-- 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 CONTROLLED
------------------------------------------------------------------
with List_Pos_Cntl_Cntl;
generic
   type Object_Type is private;
   with procedure Swap (Source, Target: in out Object_Type);
package List_Pos_Cntl_En is
   ------------------------------------------------
   -- DO NOT USE zqklst
      package zqklst is new List_Pos_Cntl_Cntl (Object_Type, Swap);
   ------------------------------------------------

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

   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;
   ------------------------------------------------
   -- Pre Cond : List = (i, ...), List /= (0)
   -- Post Cond: List' = (1, ...)
   -- Exception: List_Underflow
   ------------------------------------------------

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

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

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

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

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

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

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

procedure Append (New_Tail: in out Object_Type);
   ------------------------------------------------
   -- Pre Cond : List = (i, ...), New_Tail = (j, ...)
   -- Post Cond: List' = (List, New_Tail)
   --            New_Tail' = (0)
   -- Exception: List_Underflow
   -- NOTE: Swap is used to transfer the Object_Type
   --       value into the structure
   ------------------------------------------------

procedure Insert_Before (Object: in out Object_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 is used to transfer the Object_Type
   --       value into the structure
   ------------------------------------------------

procedure Insert_After (Object: in out Object_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 is used to transfer the Object_Type
   --       value into the structure
   ------------------------------------------------

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

procedure Remove_Current (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 is used to transfer the Object_Type
   --       value into the structure
   ------------------------------------------------

procedure Update_Current (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 is used to transfer the Object_Type
   --       value into the structure
   ------------------------------------------------

private
   List: zqklst.List_Type;

end List_Pos_Cntl_En;