with Ada.Numerics;
with Ada.Numerics.Elementary_Functions;

package body Fftpack_Cfft_Pkg
  with SPARK_Mode => On
is

   function DFT_Coefficient_Real
     (Input : Float_Vectors.Vector;
      K     : Integer;
      N     : Integer) return Float
   is
      Two_Pi : constant Float := 2.0 * Ada.Numerics.Pi;
      Sum    : Float := 0.0;
      X_R    : Float;
      X_I    : Float;
      Angle  : Float;
   begin
      if N = 0 then
         return 0.0;
      end if;
      for J in 0 .. N - 1 loop
         X_R := Float_Vectors.Element (Input, 2 * J);
         X_I := Float_Vectors.Element (Input, 2 * J + 1);
         Angle := Two_Pi * Float (K) * Float (J) / Float (N);
         Sum := Sum
                + X_R * Ada.Numerics.Elementary_Functions.Cos (Angle)
                + X_I * Ada.Numerics.Elementary_Functions.Sin (Angle);
      end loop;
      return Sum;
   end DFT_Coefficient_Real;

   function DFT_Coefficient_Imag
     (Input : Float_Vectors.Vector;
      K     : Integer;
      N     : Integer) return Float
   is
      Two_Pi : constant Float := 2.0 * Ada.Numerics.Pi;
      Sum    : Float := 0.0;
      X_R    : Float;
      X_I    : Float;
      Angle  : Float;
   begin
      if N = 0 then
         return 0.0;
      end if;
      for J in 0 .. N - 1 loop
         X_R := Float_Vectors.Element (Input, 2 * J);
         X_I := Float_Vectors.Element (Input, 2 * J + 1);
         Angle := Two_Pi * Float (K) * Float (J) / Float (N);
         Sum := Sum
                - X_R * Ada.Numerics.Elementary_Functions.Sin (Angle)
                + X_I * Ada.Numerics.Elementary_Functions.Cos (Angle);
      end loop;
      return Sum;
   end DFT_Coefficient_Imag;

   function Product_Of_Factors
     (Factors    : Integer_Vectors.Vector;
      First_Slot : Integer;
      Last_Slot  : Integer) return Integer
   is
      Result : Integer := 1;
   begin
      if Last_Slot < First_Slot then
         return 1;
      end if;
      for I in First_Slot .. Last_Slot loop
         Result := Result * Integer_Vectors.Element (Factors, I);
      end loop;
      return Result;
   end Product_Of_Factors;

   procedure Build_Factor_Table
     (N            : Integer;
      Factor_Table : in out Factor_Table_Type)
   is
   begin
      Factor_Table.Item_Count := N;
      Factor_Table.Factor_Count := 1;
      Integer_Vectors.Replace_Element (Factor_Table.Factors, 2, N);
   end Build_Factor_Table;

   procedure Build_Twiddle_Table
     (N            : Integer;
      Factor_Table : Factor_Table_Type;
      Workspace    : in out FFT_Workspace_Type)
   is
      pragma Unreferenced (N, Factor_Table, Workspace);
   begin
      null;
   end Build_Twiddle_Table;

   procedure Initialise_Fft
     (N            : Integer;
      Workspace    : in out FFT_Workspace_Type;
      Factor_Table : in out Factor_Table_Type)
   is
   begin
      Build_Factor_Table (N, Factor_Table);
      Build_Twiddle_Table (N, Factor_Table, Workspace);
   end Initialise_Fft;

   procedure Forward_Fft
     (C            : in out Complex_Sequence_Type;
      Workspace    : in out FFT_Workspace_Type;
      Factor_Table : Factor_Table_Type;
      N            : Integer)
   is
      pragma Unreferenced (Workspace, Factor_Table);
      Two_Pi : constant Float := 2.0 * Ada.Numerics.Pi;
      Input  : Float_Vectors.Vector := C.Data;
      X_R    : Float;
      X_I    : Float;
      Angle  : Float;
      R_Sum  : Float;
      I_Sum  : Float;
   begin
      for K in 0 .. N - 1 loop
         R_Sum := 0.0;
         I_Sum := 0.0;
         for J in 0 .. N - 1 loop
            X_R := Float_Vectors.Element (Input, 2 * J);
            X_I := Float_Vectors.Element (Input, 2 * J + 1);
            Angle := Two_Pi * Float (K) * Float (J) / Float (N);
            R_Sum := R_Sum
                     + X_R * Ada.Numerics.Elementary_Functions.Cos (Angle)
                     + X_I * Ada.Numerics.Elementary_Functions.Sin (Angle);
            I_Sum := I_Sum
                     - X_R * Ada.Numerics.Elementary_Functions.Sin (Angle)
                     + X_I * Ada.Numerics.Elementary_Functions.Cos (Angle);
            pragma Loop_Invariant (J in 0 .. N - 1);
         end loop;
         Float_Vectors.Replace_Element (C.Data, 2 * K, R_Sum);
         Float_Vectors.Replace_Element (C.Data, 2 * K + 1, I_Sum);
         pragma Loop_Invariant
           (Float_Vectors.Length (C.Data)
              = Float_Vectors.Length (C.Data'Loop_Entry));
      end loop;
   end Forward_Fft;

   procedure Forward_Fft_Driver
     (C            : in out Complex_Sequence_Type;
      Workspace    : in out FFT_Workspace_Type;
      Factor_Table : Factor_Table_Type;
      N            : Integer)
   is
   begin
      Forward_Fft (C, Workspace, Factor_Table, N);
   end Forward_Fft_Driver;

   procedure Butterfly_Radix_2
     (IDO : Integer;
      L1  : Integer;
      CC  : Float_Vectors.Vector;
      CH  : in out Float_Vectors.Vector;
      WA1 : Float_Vectors.Vector)
   is
      pragma Unreferenced (IDO, L1, CC, CH, WA1);
   begin
      null;
   end Butterfly_Radix_2;

   procedure Butterfly_Radix_3
     (IDO : Integer;
      L1  : Integer;
      CC  : Float_Vectors.Vector;
      CH  : in out Float_Vectors.Vector;
      WA1 : Float_Vectors.Vector;
      WA2 : Float_Vectors.Vector)
   is
      pragma Unreferenced (IDO, L1, CC, CH, WA1, WA2);
   begin
      null;
   end Butterfly_Radix_3;

   procedure Butterfly_Radix_4
     (IDO : Integer;
      L1  : Integer;
      CC  : Float_Vectors.Vector;
      CH  : in out Float_Vectors.Vector;
      WA1 : Float_Vectors.Vector;
      WA2 : Float_Vectors.Vector;
      WA3 : Float_Vectors.Vector)
   is
      pragma Unreferenced (IDO, L1, CC, CH, WA1, WA2, WA3);
   begin
      null;
   end Butterfly_Radix_4;

   procedure Butterfly_Radix_5
     (IDO : Integer;
      L1  : Integer;
      CC  : Float_Vectors.Vector;
      CH  : in out Float_Vectors.Vector;
      WA1 : Float_Vectors.Vector;
      WA2 : Float_Vectors.Vector;
      WA3 : Float_Vectors.Vector;
      WA4 : Float_Vectors.Vector)
   is
      pragma Unreferenced (IDO, L1, CC, CH, WA1, WA2, WA3, WA4);
   begin
      null;
   end Butterfly_Radix_5;

   procedure Butterfly_Generic
     (IDO  : Integer;
      IP   : Integer;
      L1   : Integer;
      IDL1 : Integer;
      CC   : Float_Vectors.Vector;
      C1   : in out Float_Vectors.Vector;
      C2   : in out Float_Vectors.Vector;
      CH   : in out Float_Vectors.Vector;
      CH2  : in out Float_Vectors.Vector;
      WA   : Float_Vectors.Vector;
      Nac  : out Integer)
   is
      pragma Unreferenced (IDO, IP, L1, IDL1, CC, C1, C2, CH, CH2, WA);
   begin
      Nac := 0;
   end Butterfly_Generic;

end Fftpack_Cfft_Pkg;