with Ada.Numerics.Discrete_Random;
package body Bingo_Basket_Original with SPARK_Mode => On is

   type Number_Array is array (Callable_Number) of Callable_Number;
   The_Basket : Number_Array; -- A sequence of numbers in the basket
   The_Count  : Bingo_Number; -- The count of numbers in the basket

   package Random_Bingo is new Ada.Numerics.Discrete_Random
                               (Result_Subtype => Callable_Number);
   use Random_Bingo;
   -- The following object holds the state of a random Bingo number generator
   Bingo_Gen : Random_Bingo.Generator;

   procedure Swap (X : in out Callable_Number;
                   Y : in out Callable_Number) is
      Temp : Callable_Number;
   begin
      Temp := X;  X := Y;  Y := Temp;
   end Swap;

   function Empty return Boolean is
   begin
      return The_Count = 0;
   end Empty;

   procedure Load is
      Random_Index : Callable_Number;
   begin
      -- Put all numbers into the basket (in order)
      for Number in Callable_Number loop
         The_Basket (Number) := Number;
      end loop;
      -- Randomize the array of numbers
      Reset (Bingo_Gen);  -- Seed random generator from clock
      for Index in Callable_Number loop
         Random_Index := Random (Bingo_Gen);
         Swap (X => The_Basket (Index),
               Y => The_Basket (Random_Index));
      end loop;
      The_Count := Callable_Number'Last;  -- all numbers now in the basket
   end Load;

   procedure Draw (Letter : out Bingo_Letter;
                   Number : out Callable_Number) is
   begin
      Number := The_Basket (The_Count);
      The_Count := The_Count - 1;

      -- Determine the letter using the subtypes in Bingo_Definitions
      case Number is
         when B_Range =>  Letter := B;
         when I_Range =>  Letter := I;
         when N_Range =>  Letter := N;
         when G_Range =>  Letter := G;
         when O_Range =>  Letter := O;
      end case;
   end Draw;
end Bingo_Basket_Original;