--::::::::::
--stacnten.ads   -- Stack_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 stack
--   ,   and
--   |   or
--  (a,...) a stack may be represented as an n-tuple, the first
--       object, a, is the top of the stack
--   '   If x passed as argument then x' is result after subprog executes
------------------------------------------------------------------
--  For safe use of this package
--  The instantiating object should be CONTROLLED
--  Stack_Type is CONTROLLED
------------------------------------------------------------------
with Stack_Cntl_Cntl;
generic
   type Object_Type is private;
   with procedure Swap (Source, Target: in out Object_Type);
package Stack_Cntl_En is
   ---------------------------------------------------
   -- WARNING:  Do not use PPS
      package PPS is new Stack_Cntl_Cntl (Object_Type, Swap);
   ---------------------------------------------------

   Stack_Underflow: exception renames PPS.Stack_Underflow;
   Stack_Overflow : exception renames PPS.Stack_Overflow;

function Empty return boolean;
   ---------------------------------------------------
   -- Pre  Cond  : None
   -- Post Cond  : Return (Stack = {})
   -- Exceptions : None
   ---------------------------------------------------

function Top_Of return Object_Type;
   ---------------------------------------------------
   -- Pre  Cond  : Stack /= {}
   -- Post Cond  : Returns Stack(1)
   -- Exceptions : Stack_Underflow
   ---------------------------------------------------

procedure Pop (Object: in out Object_Type);
   ---------------------------------------------------
   -- Pre  Cond  : Stack /= {}
   -- Post Cond  : Stack = (Object', Stack')
   -- Exceptions : Stack_Underflow
   -- NOTE:   Swap used to exchange value of Object_Type
   ---------------------------------------------------

procedure Pop;
   ---------------------------------------------------
   -- Pre  Cond  : Stack = (obj, rest);
   -- Post Cond  : Stack' = rest
   -- Exceptions : Stack_Underflow
   ---------------------------------------------------

procedure Push (Object: in out Object_Type);
   ---------------------------------------------------
   -- Pre  Cond  : None
   -- Post Cond  : Stack' = (Object, Stack)
   -- Exceptions : Stack_Overflow
   -- NOTE:   Swap used to exchange value of Object_Type
   ---------------------------------------------------

private
   Stack: PPS.Stack_Type;
end Stack_Cntl_En;