with Ada.Numerics.Elementary_Functions;

package body Dnrm2_Pkg
  with SPARK_Mode => On
is

   function Selected_Value
     (X         : Vector_Element_Type_Vectors.Vector;
      N         : Integer;
      Increment : Stride_Type;
      I         : Positive) return Float
   is
      Idx : Natural;
   begin
      if Increment.Value >= 0 then
         Idx := (I - 1) * Increment.Value;
      else
         Idx := (N - I) * abs Increment.Value;
      end if;
      return Vector_Element_Type_Vectors.Element (X, Idx).Value;
   end Selected_Value;

   function Sum_Of_Squares
     (X         : Vector_Element_Type_Vectors.Vector;
      N         : Integer;
      Increment : Stride_Type;
      K         : Natural) return Float
   is
      Sum : Float := 0.0;
      V   : Float;
   begin
      if K = 0 then
         return 0.0;
      end if;

      for I in 1 .. K loop
         V := Selected_Value (X, N, Increment, I);
         Sum := Sum + V * V;
         pragma Loop_Invariant (Sum >= 0.0);
      end loop;

      return Sum;
   end Sum_Of_Squares;

   function Euclidean_Norm
     (N         : Integer;
      X         : Vector_Element_Type_Vectors.Vector;
      Increment : Stride_Type) return Vector_Element_Type
   is
      Sum    : Float := 0.0;
      V      : Float;
      Idx    : Natural;
      Result : Float;
   begin
      if N <= 0 then
         return (Value => 0.0);
      end if;

      for I in 1 .. N loop
         if Increment.Value >= 0 then
            Idx := (I - 1) * Increment.Value;
         else
            Idx := (N - I) * abs Increment.Value;
         end if;
         V := Vector_Element_Type_Vectors.Element (X, Idx).Value;
         Sum := Sum + V * V;
         pragma Loop_Invariant (Sum >= 0.0);
      end loop;

      if Sum <= 0.0 then
         Result := 0.0;
      else
         Result := Ada.Numerics.Elementary_Functions.Sqrt (Sum);
         if Result < 0.0 then
            Result := 0.0;
         end if;
      end if;

      return (Value => Result);
   end Euclidean_Norm;

end Dnrm2_Pkg;