with SPARK.Containers.Formal.Unbounded_Vectors;
with Ada;
with Ada.Containers;

use type Ada.Containers.Count_Type;

package Fftpack_Cfft_Pkg
  with SPARK_Mode => On
is

   package Float_Vectors is new SPARK.Containers.Formal.Unbounded_Vectors
      (Index_Type   => Natural,
       Element_Type => Float);

   type Complex_Sequence_Type is record
      Data                           : Float_Vectors.Vector;
   end record;

   package Complex_Sequence_Type_Vectors is new SPARK.Containers.Formal.Unbounded_Vectors
      (Index_Type   => Natural,
       Element_Type => Complex_Sequence_Type);

   type FFT_Workspace_Type is record
      Data                           : Float_Vectors.Vector;
   end record;

   package FFT_Workspace_Type_Vectors is new SPARK.Containers.Formal.Unbounded_Vectors
      (Index_Type   => Natural,
       Element_Type => FFT_Workspace_Type);

   package Integer_Vectors is new SPARK.Containers.Formal.Unbounded_Vectors
      (Index_Type   => Natural,
       Element_Type => Integer);

   type Factor_Table_Type is record
      Item_Count                     : Integer;
      Factor_Count                   : Integer;
      Factors                        : Integer_Vectors.Vector;
   end record;

   package Factor_Table_Type_Vectors is new SPARK.Containers.Formal.Unbounded_Vectors
      (Index_Type   => Natural,
       Element_Type => Factor_Table_Type);

   function DFT_Coefficient_Real
     (Input : Float_Vectors.Vector;
   K     : Integer;
   N     : Integer) return Float
   with Ghost,
     Pre  => N >= 1
             and then K in 0 .. N - 1
             and then Float_Vectors.Length (Input) >= Ada.Containers.Count_Type (2 * N);

   function DFT_Coefficient_Imag
     (Input : Float_Vectors.Vector;
   K     : Integer;
   N     : Integer) return Float
   with Ghost,
     Pre  => N >= 1
             and then K in 0 .. N - 1
             and then Float_Vectors.Length (Input) >= Ada.Containers.Count_Type (2 * N);

   function Product_Of_Factors
     (Factors    : Integer_Vectors.Vector;
   First_Slot : Integer;
   Last_Slot  : Integer) return Integer
   with Ghost,
     Pre  => First_Slot >= 0
             and then Last_Slot >= First_Slot - 1
             and then Integer_Vectors.Length (Factors)
                       >= Ada.Containers.Count_Type (Last_Slot + 1);

   procedure Initialise_Fft
     (N            : Integer;
   Workspace    : in out FFT_Workspace_Type;
   Factor_Table : in out Factor_Table_Type)
   with Pre  => N >= 1
             and then Float_Vectors.Length (Workspace.Data)
                       >= Ada.Containers.Count_Type (4 * N + 15)
             and then Integer_Vectors.Length (Factor_Table.Factors)
                       >= Ada.Containers.Count_Type (32),
     Post => Factor_Table.Item_Count = N
             and then Factor_Table.Factor_Count >= 1
             and then Integer_Vectors.Length (Factor_Table.Factors)
                       >= Ada.Containers.Count_Type
                            (Factor_Table.Factor_Count + 2)
             and then Product_Of_Factors
                        (Factor_Table.Factors,
                         2,
                         Factor_Table.Factor_Count + 1) = N
             and then Float_Vectors.Length (Workspace.Data)
                       = Float_Vectors.Length (Workspace.Data'Old);

   procedure Forward_Fft
     (C            : in out Complex_Sequence_Type;
   Workspace    : in out FFT_Workspace_Type;
   Factor_Table : Factor_Table_Type;
   N            : Integer)
   with Pre  => N >= 1
             and then Factor_Table.Item_Count = N
             and then Factor_Table.Factor_Count >= 1
             and then Integer_Vectors.Length (Factor_Table.Factors)
                       >= Ada.Containers.Count_Type
                            (Factor_Table.Factor_Count + 2)
             and then Product_Of_Factors
                        (Factor_Table.Factors,
                         2,
                         Factor_Table.Factor_Count + 1) = N
             and then Float_Vectors.Length (C.Data)
                       >= Ada.Containers.Count_Type (2 * N)
             and then Float_Vectors.Length (Workspace.Data)
                       >= Ada.Containers.Count_Type (4 * N + 15),
     Post => Float_Vectors.Length (C.Data)
              = Float_Vectors.Length (C.Data'Old)
             and then Float_Vectors.Length (Workspace.Data)
                       = Float_Vectors.Length (Workspace.Data'Old)
             and then (for all K in 0 .. N - 1 =>
                         Float_Vectors.Element (C.Data, 2 * K)
                            = DFT_Coefficient_Real (C.Data'Old, K, N)
                         and then Float_Vectors.Element
                                    (C.Data, 2 * K + 1)
                            = DFT_Coefficient_Imag (C.Data'Old, K, N));

   procedure Forward_Fft_Driver
     (C            : in out Complex_Sequence_Type;
   Workspace    : in out FFT_Workspace_Type;
   Factor_Table : Factor_Table_Type;
   N            : Integer)
   with Pre  => N >= 1
             and then Factor_Table.Item_Count = N
             and then Factor_Table.Factor_Count >= 1
             and then Integer_Vectors.Length (Factor_Table.Factors)
                       >= Ada.Containers.Count_Type
                            (Factor_Table.Factor_Count + 2)
             and then Product_Of_Factors
                        (Factor_Table.Factors,
                         2,
                         Factor_Table.Factor_Count + 1) = N
             and then Float_Vectors.Length (C.Data)
                       >= Ada.Containers.Count_Type (2 * N)
             and then Float_Vectors.Length (Workspace.Data)
                       >= Ada.Containers.Count_Type (4 * N + 15),
     Post => Float_Vectors.Length (C.Data)
              = Float_Vectors.Length (C.Data'Old)
             and then (for all K in 0 .. N - 1 =>
                         Float_Vectors.Element (C.Data, 2 * K)
                            = DFT_Coefficient_Real (C.Data'Old, K, N)
                         and then Float_Vectors.Element
                                    (C.Data, 2 * K + 1)
                            = DFT_Coefficient_Imag (C.Data'Old, K, N));

   procedure Build_Factor_Table
     (N            : Integer;
   Factor_Table : in out Factor_Table_Type)
   with Pre  => N >= 1
             and then Integer_Vectors.Length (Factor_Table.Factors)
                       >= Ada.Containers.Count_Type (32),
     Post => Factor_Table.Item_Count = N
             and then Factor_Table.Factor_Count >= 1
             and then Integer_Vectors.Length (Factor_Table.Factors)
                       >= Ada.Containers.Count_Type
                            (Factor_Table.Factor_Count + 2)
             and then Product_Of_Factors
                        (Factor_Table.Factors,
                         2,
                         Factor_Table.Factor_Count + 1) = N;

   procedure Build_Twiddle_Table
     (N            : Integer;
   Factor_Table : Factor_Table_Type;
   Workspace    : in out FFT_Workspace_Type)
   with Pre  => N >= 1
             and then Factor_Table.Item_Count = N
             and then Factor_Table.Factor_Count >= 1
             and then Integer_Vectors.Length (Factor_Table.Factors)
                       >= Ada.Containers.Count_Type
                            (Factor_Table.Factor_Count + 2)
             and then Float_Vectors.Length (Workspace.Data)
                       >= Ada.Containers.Count_Type (4 * N + 15),
     Post => Float_Vectors.Length (Workspace.Data)
              = Float_Vectors.Length (Workspace.Data'Old);

   procedure Butterfly_Radix_2
     (IDO : Integer;
   L1  : Integer;
   CC  : Float_Vectors.Vector;
   CH  : in out Float_Vectors.Vector;
   WA1 : Float_Vectors.Vector)
   with Pre  => IDO >= 2
             and then IDO mod 2 = 0
             and then L1 >= 1
             and then Float_Vectors.Length (CC)
                       >= Ada.Containers.Count_Type (2 * IDO * L1)
             and then Float_Vectors.Length (CH)
                       >= Ada.Containers.Count_Type (2 * IDO * L1)
             and then Float_Vectors.Length (WA1)
                       >= Ada.Containers.Count_Type (IDO),
     Post => Float_Vectors.Length (CH)
              = Float_Vectors.Length (CH'Old);

   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)
   with Pre  => IDO >= 2
             and then IDO mod 2 = 0
             and then L1 >= 1
             and then Float_Vectors.Length (CC)
                       >= Ada.Containers.Count_Type (3 * IDO * L1)
             and then Float_Vectors.Length (CH)
                       >= Ada.Containers.Count_Type (3 * IDO * L1)
             and then Float_Vectors.Length (WA1)
                       >= Ada.Containers.Count_Type (IDO)
             and then Float_Vectors.Length (WA2)
                       >= Ada.Containers.Count_Type (IDO),
     Post => Float_Vectors.Length (CH)
              = Float_Vectors.Length (CH'Old);

   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)
   with Pre  => IDO >= 2
             and then IDO mod 2 = 0
             and then L1 >= 1
             and then Float_Vectors.Length (CC)
                       >= Ada.Containers.Count_Type (4 * IDO * L1)
             and then Float_Vectors.Length (CH)
                       >= Ada.Containers.Count_Type (4 * IDO * L1)
             and then Float_Vectors.Length (WA1)
                       >= Ada.Containers.Count_Type (IDO)
             and then Float_Vectors.Length (WA2)
                       >= Ada.Containers.Count_Type (IDO)
             and then Float_Vectors.Length (WA3)
                       >= Ada.Containers.Count_Type (IDO),
     Post => Float_Vectors.Length (CH)
              = Float_Vectors.Length (CH'Old);

   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)
   with Pre  => IDO >= 2
             and then IDO mod 2 = 0
             and then L1 >= 1
             and then Float_Vectors.Length (CC)
                       >= Ada.Containers.Count_Type (5 * IDO * L1)
             and then Float_Vectors.Length (CH)
                       >= Ada.Containers.Count_Type (5 * IDO * L1)
             and then Float_Vectors.Length (WA1)
                       >= Ada.Containers.Count_Type (IDO)
             and then Float_Vectors.Length (WA2)
                       >= Ada.Containers.Count_Type (IDO)
             and then Float_Vectors.Length (WA3)
                       >= Ada.Containers.Count_Type (IDO)
             and then Float_Vectors.Length (WA4)
                       >= Ada.Containers.Count_Type (IDO),
     Post => Float_Vectors.Length (CH)
              = Float_Vectors.Length (CH'Old);

   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)
   with Pre  => IDO >= 2
             and then IDO mod 2 = 0
             and then IP >= 2
             and then L1 >= 1
             and then IDL1 >= IDO
             and then Float_Vectors.Length (CC)
                       >= Ada.Containers.Count_Type (IP * IDO * L1)
             and then Float_Vectors.Length (C1)
                       >= Ada.Containers.Count_Type (IP * IDO * L1)
             and then Float_Vectors.Length (C2)
                       >= Ada.Containers.Count_Type (IP * IDL1)
             and then Float_Vectors.Length (CH)
                       >= Ada.Containers.Count_Type (IP * IDO * L1)
             and then Float_Vectors.Length (CH2)
                       >= Ada.Containers.Count_Type (IP * IDL1)
             and then Float_Vectors.Length (WA)
                       >= Ada.Containers.Count_Type (IDO),
     Post => Nac in 0 | 1
             and then Float_Vectors.Length (CH)
                       = Float_Vectors.Length (CH'Old)
             and then Float_Vectors.Length (C1)
                       = Float_Vectors.Length (C1'Old);

end Fftpack_Cfft_Pkg;