--::::::::::
--sttagcnt.ads   -- Stack_Tag_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 is an object, then x' is the value of x after the
--       the subprogram or statement sequence in question executes
------------------------------------------------------------------
--  For safe use of this package
--  Object_Type is Tagged (polymorphic)
--  Stack_Type is unbound managed controlled
------------------------------------------------------------------
with tag_to_lpt, Stack_LPBase, Ada.Finalization;
use Ada.Finalization;
generic
   type Object_Type is tagged private;
package Stack_Tag_Cntl is

type Object_Ptr  is access Object_Type'Class;
   ---------------------------------------------------------------------
   -- DO NOT USE Stk
      package ttl is new tag_to_lpt (Object_Type, Object_Ptr);
      package Stk is new
         Stack_LPBase (Object_Ptr, ttl.Initialize, ttl.Finalize,
                       ttl.Copy, ttl.Swap);
   ---------------------------------------------------------------------

type Stack_Type  is new controlled with private;

Stack_Underflow: exception renames Stk.Stack_Underflow;
Stack_Overflow : exception renames stk.Stack_Overflow;

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

procedure Pop (Stack : in out Stack_Type;
               Object: in out Object_Ptr);
   ---------------------------------------------------------------------
   -- Pre  Cond  : Stack /= {}
   -- Post Cond  : if Stack = (obj, substack) then
   --              Stack' = substack, Object.all' = obj
   -- Exceptions : Stack_Empty
   ---------------------------------------------------------------------
procedure Pop (Stack : in out Stack_Type;
               Object:    out Object_Type'Class);
   ---------------------------------------------------------------------
   -- Pre  Cond  : Stack /= {}
   -- Post Cond  : if Stack = (obj, substack) then
   --              Stack' = substack, Object.all' = obj
   -- Exceptions : Stack_Empty
   ---------------------------------------------------------------------

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

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

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

end Stack_Tag_Cntl;