1pragma Spark_Mode (On);
2
3package body Predicate8_Pkg is
4   function Empty
5     (Buffer : in Ring_Buffer_Type) return Boolean
6   is (Size (Buffer) = 0);
7
8   function Full
9     (Buffer : in Ring_Buffer_Type) return Boolean
10   is (Size (Buffer) = Buffer.Max_Size);
11
12   function Size
13     (Buffer : in Ring_Buffer_Type) return Natural
14   is (Buffer.Count);
15
16   function Free
17     (Buffer : in Ring_Buffer_Type) return Natural
18   is (Buffer.Max_Size - Size (Buffer));
19
20   function First
21     (Buffer : in Ring_Buffer_Type) return Element_Type
22   is (Buffer.Items (Buffer.Head));
23
24   function Last
25     (Buffer : in Ring_Buffer_Type) return Element_Type
26   is (Buffer.Items (Buffer.Tail));
27
28   procedure Get
29     (Buffer   : in out Ring_Buffer_Type;
30      Element  :    out Element_Type)
31   is
32   begin
33      Element := Buffer.Items (Buffer.Head);
34      Buffer  :=
35        Buffer'Update
36          (Head  =>
37            (if Buffer.Head = Buffer.Max_Size then 1 else Buffer.Head + 1),
38           Count => Buffer.Count - 1);
39   end Get;
40
41   procedure Put
42     (Buffer   : in out Ring_Buffer_Type;
43      Element  : in     Element_Type)
44   is
45    begin
46      if Buffer.Tail = Buffer.Max_Size then
47         Buffer.Tail := 1;
48      else
49         Buffer.Tail := Buffer.Tail + 1;
50      end if;
51
52      Buffer.Items (Buffer.Tail) := Element;
53      Buffer.Count := Buffer.Count + 1;
54   end Put;
55
56   procedure Clear
57     (Buffer : in out Ring_Buffer_Type)
58   is
59   begin
60      Buffer.Head  := 1;
61      Buffer.Tail  := Buffer.Max_Size;
62      Buffer.Count := 0;
63   end Clear;
64end Predicate8_Pkg;
65