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