with Ada.Text_IO; use Ada.Text_IO;

with System.Storage_Elements; use System.Storage_Elements;
with BBqueue;
with BBqueue.Buffers.framed;
with System; use System;

procedure Main_Framed
with SPARK_Mode
is
   use type BBqueue.Result_Kind;

   Q : aliased BBqueue.Buffers.framed.Framed_Buffer (60);

   procedure Fill_With_CB (Request, Actual : BBqueue.Count;
                           Val : Storage_Element);
   procedure Print_Content_With_CB;

   ------------------
   -- Fill_With_CB --
   ------------------

   procedure Fill_With_CB (Request, Actual : BBqueue.Count;
                           Val             : Storage_Element)
   is
      pragma SPARK_Mode (Off);

      procedure Process_Write (Data      : out Storage_Array;
                               To_Commit : out BBqueue.Count);

      procedure Process_Write (Data      : out Storage_Array;
                               To_Commit : out BBqueue.Count)
      is
      begin
         Put_Line ("Fill" & Actual'Img & " bytes.");
         Data (Data'First .. Data'First + Actual - 1) := (others => Val);
         To_Commit := Actual;
      end Process_Write;

      procedure Write is new BBqueue.Buffers.framed.Write_CB (Process_Write);
      Result : BBqueue.Result_Kind;
   begin
      Write (Q, Request, Result);
      if Result /= BBqueue.Valid then
         Put_Line ("Write failed: " & Result'Img);
      end if;
   end Fill_With_CB;

   ---------------------------
   -- Print_Content_With_CB --
   ---------------------------

   procedure Print_Content_With_CB is
      procedure Process_Read (Data : Storage_Array);

      procedure Process_Read (Data : Storage_Array) is
      begin
         Put ("Print" & Data'Length'Img & " bytes -> ");
         for Elt of Data loop
            Put (Elt'Img);
         end loop;
         New_Line;
      end Process_Read;

      procedure Read is new BBqueue.Buffers.framed.Read_CB (Process_Read);
      Result : BBqueue.Result_Kind;
   begin
      Read (Q, Result);
      if Result /= BBqueue.Valid then
         Put_Line ("Read failed: " & Result'Img);
      end if;
   end Print_Content_With_CB;

   V : Storage_Element := 1;
begin

   Put_Line ("Count'Object_Size:" & BBqueue.Count'Object_Size'Img);

   for X in BBqueue.Count range 1 .. 4 loop
      Put_Line ("-- Loop" & X'Img & " --");
      Fill_With_CB (10, X, V);
      Fill_With_CB (20, X * 2, V * 2);
      V := V + 1;
      Print_Content_With_CB;
      Print_Content_With_CB;
   end loop;
end Main_Framed;