--::::::::::
--staptcnt.ads   -- stack_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 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 BOUND NONPOLYMORPHIC
--  Stack_Type is UNBOUND MANAGED CONTROLLED
------------------------------------------------------------------
with Ada.Finalization, Stack_LPBase, Pt_To_Lpt;
use Ada.Finalization;
generic
   type Object_Type is private;
package Stack_Pt_Cntl is
   ---------------------------------------------------
   -- WARNING:  Do not use PPS
      package lpt is new Pt_To_Lpt (Object_Type);
      package PPS is new Stack_LPBase
         (Object_Type, lpt.Initialize, lpt.Finalize, lpt.Copy, lpt.Swap);
   ---------------------------------------------------

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

   type Stack_Type is new controlled with private;

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

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

procedure Pop (Stack : in out Stack_Type;
               Object:    out Object_Type);
   ---------------------------------------------------
   -- Pre  Cond  : Stack /= {}
   -- Post Cond  : Stack = (Object', Stack')
   -- Exceptions : Stack_Underflow
   ---------------------------------------------------

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

procedure Push (Object: in     Object_Type;
                Stack : in out Stack_Type);
   ---------------------------------------------------
   -- Pre  Cond  : None
   -- Post Cond  : Stack' = (Object, Stack)
   -- Exceptions : Stack_Overflow
   ---------------------------------------------------

procedure Swap (Source: in out Stack_Type;
                Target: in out Stack_Type);
   ---------------------------------------------------
   -- Pre  Cond  :
   -- Post Cond  : Source' = Target, Target' = Source
   -- Exceptions :
   ---------------------------------------------------

private
   procedure Initialize (Stack: in out Stack_Type);
   procedure Adjust (Stack: in out Stack_Type);
   procedure Finalize (Stack: in out Stack_Type);

   type Stack_Type is new controlled with
      record
         Stack: PPS.LPStack_Type;
      end record;

end Stack_Pt_Cntl;