pragma SPARK_Mode (On);

package body Dger_Pkg is

   procedure Rank_One_Update
     (Number_Of_Rows    : in     Matrix_Dimension_Type;
      Number_Of_Columns : in     Matrix_Dimension_Type;
      Alpha             : in     Long_Float;
      X                 : in     Long_Float_Vectors.Vector;
      Incx              : in     Stride_Type;
      Y                 : in     Long_Float_Vectors.Vector;
      Incy              : in     Stride_Type;
      Leading_Dimension : in     Matrix_Dimension_Type;
      A                 : in out Long_Float_Vectors.Vector)
   is
      M   : constant Integer := Number_Of_Rows.Value;
      N   : constant Integer := Number_Of_Columns.Value;
      LDA : constant Integer := Leading_Dimension.Value;
      IX  : constant Integer := Incx.Value;
      IY  : constant Integer := Incy.Value;

      function X_Index (Logical_I : Positive) return Natural is
        (if IX > 0
         then (Logical_I - 1) * IX
         else (M - Logical_I) * (-IX));

      function Y_Index (Logical_J : Positive) return Natural is
        (if IY > 0
         then (Logical_J - 1) * IY
         else (N - Logical_J) * (-IY));

      function A_Index (Row_I, Column_J : Positive) return Natural is
        ((Column_J - 1) * LDA + (Row_I - 1));

   begin
      if M = 0 or else N = 0 or else Alpha = 0.0 then
         return;
      end if;

      for J in 1 .. N loop
         declare
            Y_Val  : constant Long_Float :=
              Long_Float_Vectors.Element (Y, Y_Index (Positive (J)));
            Temp_Y : constant Long_Float := Alpha * Y_Val;
         begin
            for I in 1 .. M loop
               declare
                  X_Val   : constant Long_Float :=
                    Long_Float_Vectors.Element (X, X_Index (Positive (I)));
                  A_Pos   : constant Natural :=
                    A_Index (Positive (I), Positive (J));
                  Old_Val : constant Long_Float :=
                    Long_Float_Vectors.Element (A, A_Pos);
               begin
                  Long_Float_Vectors.Replace_Element
                    (A, A_Pos, Old_Val + Temp_Y * X_Val);
               end;
            end loop;
         end;
      end loop;
   end Rank_One_Update;

   procedure Report_Invalid_Argument
     (Argument_Index : in Positive)
   is
      pragma Unreferenced (Argument_Index);
   begin
      null;
   end Report_Invalid_Argument;

end Dger_Pkg;