Having a hard time indexing an array

Question

I was trying to write a generic Heap_Sort procedure with similar specification to Ada.Containers.Generic_Array_Sort (that is, with type Index_Type is (<>)) but I'm not sure if there's a good way of dealing with this type of index. If I constrain the Index_Type to Positive, it's not that big of a deal:

generic
   type Element is private;
procedure Generic_Swap (Left, Right : in out Element);

procedure Generic_Swap (Left, Right : in out Element) is
   Buffer : constant Element := Left;
begin
   Left := Right;
   Right := Buffer;
end Generic_Swap;

generic
   type Element_Type is private;
   type Array_Type is array (Positive range <>) of Element_Type;
   with function ">" (Left, Right : Element_Type) return Boolean is <>;
procedure Generic_Heap_Sort (Data : in out Array_Type);

procedure Generic_Heap_Sort (Data : in out Array_Type) is
   function Left_Heap_Index (Root : Positive) return Positive is
      (Root * 2 - Data'First + 1);

   function Right_Heap_Index (Root : Positive) return Positive is
      (Root * 2 - Data'First + 2);

   procedure Swap is new Generic_Swap (Element_Type);

   procedure Heap_Insert (Index, Heap_Last : in Positive) is
      Left  : constant Positive := Left_Heap_Index (Index);
      Right : constant Positive := Right_Heap_Index (Index);
      Swap_Index : Positive := Index;
   begin
      if Left <= Heap_Last and then Data (Left) > Data (Swap_Index) then
         Swap_Index := Left;
      end if;
      if Right <= Heap_Last and then Data (Right) > Data (Swap_Index) then
         Swap_Index := Right;
      end if;
      if Swap_Index /= Index then
         Swap (Data (Swap_Index), Data (Index));
         Heap_Insert (Swap_Index, Heap_Last);
      end if;
   end Heap_Insert;
begin
   for Index in reverse Data'First .. (Data'Last - Data'First) / 2 loop
      Heap_Insert (Index, Data'Last);
   end loop;
   for Index in reverse Data'First + 1 .. Data'Last loop
      Swap (Data (Data'First), Data (Index));
      Heap_Insert (Data'First, Index - 1);
   end loop;
end Generic_Heap_Sort;

But even then I have to take into account that not all arrays in Positive range <> start at 1 in Left_Heap_Index and Right_Heap_Index functions. Ideally I would like to treat any array parameter Data as a sequence of elements in range 1 .. Data'Length instead of -5 .. -3 or JAN, FEB, MAR, even if the array type is indexed by values of some discrete formal type (<>). Is it possible without defining a To_Index function that translates a System.Min_Int .. System.Max_Int integer representing a 1-based index to Index_Type, similar to the one used in GNAT implementation of Ada.Containers.Generic_Constrained_Array_Sort?

Just to clarify, the code below works but all the calls to Convert are exactly the stuff I'm trying to avoid.

generic
   type Element_Type is private;
procedure Generic_Swap (Left, Right : in out Element_Type);

procedure Generic_Swap (Left, Right : in out Element_Type) is
   Buffer : constant Element_Type := Left;
begin
   Left := Right;
   Right := Buffer;
end Generic_Swap;

generic
   type Index_Type is (<>);
   type Element_Type is private;
   type Array_Type is array (Index_Type range <>) of Element_Type;
   with function ">" (Left, Right : Element_Type) return Boolean is <>;
procedure Heap_Sort (Data : in out Array_Type);

procedure Heap_Sort (Data : in out Array_Type) is
   subtype Integer_Index is Positive;

   function Convert (Index : Index_Type) return Integer_Index is
      (Integer_Index'First + Index_Type'Pos (Index) - Index_Type'Pos (Data'First));

   function Convert (Index : Integer_Index) return Index_Type is
      (Index_Type'Val (Index_Type'Pos (Data'First) + Index - Integer_Index'First));

   procedure Swap is new Generic_Swap (Element_Type);

   procedure Heap_Insert (Index, Heap_Last : in Integer_Index) is
      Left_Heap  : constant Integer_Index := Index * 2 - Convert (Data'First) + 1;
      Right_Heap : constant Integer_Index := Index * 2 - Convert (Data'First) + 2;
      Swap_Index : Integer_Index := Index;
   begin
      if Left_Heap <= Heap_Last and then Data (Convert (Left_Heap)) > Data (Convert (Swap_Index)) then
         Swap_Index := Left_Heap;
      end if;
      if Right_Heap <= Heap_Last and then Data (Convert (Right_Heap)) > Data (Convert (Swap_Index)) then
         Swap_Index := Right_Heap;
      end if;
      if Swap_Index /= Index then
         Swap (Data (Convert (Swap_Index)), Data (Convert (Index)));
         Heap_Insert (Swap_Index, Heap_Last);
      end if;
   end Heap_Insert;
begin
   for Index in reverse Convert (Data'First) .. (Convert (Data'Last) - Convert (Data'First)) / 2 loop
      Heap_Insert (Index, Convert (Data'Last));
   end loop;
   for Index in reverse Index_Type'Succ (Data'First) .. Data'Last loop
      Swap (Data (Data'First), Data (Index));
      Heap_Insert (Convert (Data'First), Convert (Index_Type'Pred (Index)));
   end loop;
end Heap_Sort;

user_9604966 · Answer

You might check out the attributes Pos and Val for discrete types. You can transform indexes to and from a 0 based integer position so you can do your math as you see fit and then convert back to an index_type value. Note that they are 0 indexed relative to the Index_Type as a whole, not the first element of the array, so you would still need to use 'First and 'Last to handle arrays that can start at any index, but you can also encapsulate this calculation into a function where you supply the numeric indexes you want your logic to use and convert using the Val aspect inside the function.

For example, if you wanted 1-indexed based indices for math, you could make a Swap procedure that is declared inside the Generic_Heap_Sort procedure like this:

   procedure Swap(L,R : Positive) is
        -- Use a -1 to adjust from 1-indexed indices to 0-indexed indices
        L_Index : constant Index_Type   := Index_Type'Val(L-1 + Index_Type'Pos(Data'First));
        R_Index : constant Index_Type   := Index_Type'Val(R-1 + Index_Type'Pos(Data'First));
        Buffer  : constant Element_Type := Data(L_Index);
   begin
        Data(L_Index) := Data(R_Index);
        Data(R_Index) := Buffer;
   end Swap;

And do yall your outside math in positives.

You can also check out 'Succ and 'Pred attributes to shortcuts to do +1 and -1 to your indexes without needing to convert inbetween.

See also:

http://www.ada-auth.org/standards/2xrm/html/RM-3-5-5.html#I1764

http://www.ada-auth.org/standards/2xrm/html/RM-3-5.html#I1632

user_40851 · Answer

This is a fairly straightforward translation of your algorithm, translating

Root * 2 - Data'First + 1

into

Index_Type'Val
  (Index_Type'Pos (Root) * 2 - Index_Type'Pos (Data'First) + 1)

(’Pos returns a zero-based integer corresponding to the input’s position in the enumeration, ’Val does the reverse).

with Ada.Text_IO; use Ada.Text_IO;
procedure Gdi512
with SPARK_Mode
is

   generic
      type Element_Type is private;
      type Index_Type is (<>);
      type Array_Type is array (Index_Type range <>) of Element_Type;
      with function ">" (Left, Right : Element_Type) return Boolean is <>;
   procedure Generic_Heap_Sort (Data : in out Array_Type);

   procedure Generic_Heap_Sort (Data : in out Array_Type) is

      subtype Data_Range is Index_Type range Data'Range;

      function Left_Heap_Index (Root : Data_Range) return Natural
      is (Index_Type'Pos (Root) * 2 - Index_Type'Pos (Data'First) + 1);

      function Right_Heap_Index (Root : Data_Range) return Natural
      is (Index_Type'Pos (Root) * 2 - Index_Type'Pos (Data'First) + 2);

      procedure Heap_Insert (Index, Heap_Last : in Data_Range) is
         Left  : constant Natural := Left_Heap_Index (Index);
         Right : constant Natural := Right_Heap_Index (Index);
         Swap_Index : Index_Type := Index;
      begin
         if Left <= Index_Type'Pos (Heap_Last)
           and then Data (Index_Type'Val (Left)) > Data (Swap_Index)
         then
            Swap_Index := Index_Type'Val (Left);
         end if;
         if Right <= Index_Type'Pos (Heap_Last)
           and then Data (Index_Type'Val (Right)) > Data (Swap_Index)
         then
            Swap_Index := Index_Type'Val (Right);
         end if;
         if Swap_Index /= Index then
            --  Using Swap here gives a 'might be aliased' warning
            --  with Gnatprove CE 2019.
            declare
               Buffer : constant Element_Type := Data (Swap_Index);
            begin
               Data (Swap_Index) := Data (Index);
               Data (Index) := Buffer;
            end;
            Heap_Insert (Swap_Index, Heap_Last);
         end if;
      end Heap_Insert;

   begin
      if Data'Length >= 2 then
         for Index in reverse Data'First ..
           Index_Type'Val
             ((Index_Type'Pos (Data'Last) + Index_Type'Pos (Data'First)) / 2)
         loop
            Heap_Insert (Index, Data'Last);
         end loop;
         for Index in reverse Index_Type'Succ (Data'First) .. Data'Last loop
            --  Using Swap here gives a 'might be aliased' warning
            --  with Gnatprove CE 2019.
            declare
               Buffer : constant Element_Type := Data (Data'First);
            begin
               Data (Data'First) := Data (Index);
               Data (Index) := Buffer;
            end;
            Heap_Insert (Data'First, Index_Type'Pred (Index));
         end loop;
      end if;
   end Generic_Heap_Sort;

   type Alpha is
     (A, B, C, D, E, F, G, H, I, J, K, L, M,
      N, O, P, Q, R, S, T, U, V, W, X, Y, Z);

   type Arry is array (Alpha range <>) of Integer;

   procedure Sort_Up is new Generic_Heap_Sort (Element_Type => Integer,
                                               Index_Type => Alpha,
                                               Array_Type => Arry);
   procedure Sort_Down is new Generic_Heap_Sort (Element_Type => Integer,
                                                 Index_Type => Alpha,
                                                 Array_Type => Arry,
                                                 ">" => "<");

   Data : Arry := (D => 9,
                   E => 8,
                   F => 7,
                   G => 6,
                   H => 5,
                   I => 4,
                   J => 3,
                   K => 2);

   End_Data : Arry := (W => 5,
                       X => 4,
                       Y => 3,
                       Z => 2);
begin
   Sort_Up (Data);
   for J in Data'Range loop
      Put_Line (J'Image & " " & Data (J)'Image);
   end loop;
   New_Line;
   Sort_Down (Data);
   for J in Data'Range loop
      Put_Line (J'Image & " " & Data (J)'Image);
   end loop;
   New_Line;
   Sort_Up (End_Data);
   for J in End_Data'Range loop
      Put_Line (J'Image & " " & End_Data (J)'Image);
   end loop;
   New_Line;
   Sort_Down (End_Data);
   for J in End_Data'Range loop
      Put_Line (J'Image & " " & End_Data (J)'Image);
   end loop;
end Gdi512;

The output:

$ ./gdi512
D  2
E  3
F  4
G  5
H  6
I  7
J  8
K  9

D  9
E  8
F  7
G  6
H  5
I  4
J  3
K  2

W  2
X  3
Y  4
Z  5

W  5
X  4
Y  3
Z  2

Note 1: I've removed Generic_Swap, it caused problems with gnatprove (parmeters might be aliased).

Note 2: there was an issue with the check if Data'Length > 1 when the generic parameter ">" was set to "<". I think there might be a compiler error lurking here somewhere.

Note 3: compiler bug reported.

Having a hard time indexing an array

2 Answers