chests/src/chests-stacks.ads at master · JeremyGrosser/chests · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
--
--  Copyright (C) 2022 Jeremy Grosser <jeremy@synack.me>
--
--  SPDX-License-Identifier: BSD-3-Clause
--
generic
   type Element_Type is private;
   Capacity : Positive := 1;
package Chests.Stacks
   with Preelaborate
is
   type Stack is private;

   function Is_Full
      (S : Stack)
      return Boolean;

   function Is_Empty
      (S : Stack)
      return Boolean;

   function Length
      (S : Stack)
      return Natural;

   procedure Push
      (S    : in out Stack;
       Item : Element_Type)
   with Pre  => not Is_Full (S),
        Post => Length (S) = Length (S'Old) + 1;

   procedure Pop
      (S    : in out Stack;
       Item : out Element_Type)
   with Pre  => not Is_Empty (S),
        Post => Length (S) = Length (S'Old) - 1;
   --  Last In, First Out (LIFO)

   function Pop
      (S : in out Stack)
      return Element_Type
   with Pre  => not Is_Empty (S),
        Post => Length (S) = Length (S'Old) - 1;

   procedure Clear
      (S : in out Stack);

private

   type Element_Array is array (1 .. Capacity) of Element_Type
      with Pack;

   type Stack is record
      Items : Element_Array;
      Last  : Natural := 0;
   end record;

end Chests.Stacks;