-- Copyright (c) 1995/6    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
------------------------------------------------------------------
with Ada.Finalization; use Ada.Finalization;

package Stack_Polymorphic_Cntl is

type Place_Holder is new controlled with private;
   procedure Initialize (Source: in out Place_Holder);
   procedure Finalize (Source: in out Place_Holder);
   procedure Adjust (Source: in out Place_Holder);
   -------------------------------------------------------------
   -- When extending Place_Holder type the client must provide
   -- Initialize, Finalize, and Adjust procedures for the extended
   -- type UNLESS the extension is bound AND an aggregate is used
   -- to initialize the components in the extension
   -------------------------------------------------------------

type Holder_Class_Ptr is access Place_Holder'Class;
   procedure Recycle (Point: in out Holder_Class_Ptr);

type Stack_Type is new controlled with private;
   procedure Initialize (Stack: in out Stack_Type);
   procedure Finalize (Stack: in out Stack_Type);
   procedure Adjust (Stack: in out Stack_Type);

   Stack_Underflow: exception;
   Stack_Overflow : exception;

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

function Empty_Stack return Stack_Type;
   ---------------------------------------------------
   -- PostCond: Stack' = ()
   ---------------------------------------------------

generic
   type Extended_Type is new Place_Holder with private;
function g_Top_Of (Stack: Stack_Type) return Extended_Type;

function Top_Of (Stack: Stack_Type) return Holder_Class_Ptr;
   ---------------------------------------------------
   -- PreCond: Stack = (Obj, rest)
   -- PostCond: return Obj
   ---------------------------------------------------

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

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

generic
   type Extended_Type is new Place_Holder with private;
procedure g_Pop (Stack : in out Stack_Type;
                 Object: in out Extended_Type);

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

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

private

type Place_Holder is new controlled with
   record
      Next  : Holder_Class_Ptr := null;
   end record;

type Stack_Type is new controlled with
   record
      Top : Holder_Class_Ptr := null;
      Size: natural := 0;
   end record;

end Stack_Polymorphic_Cntl;