with Ada.Command_Line; use Ada.Command_Line;
with Ada.Containers.Vectors; use Ada.Containers;
with Ada.Numerics.Discrete_Random; use Ada.Numerics;
with Ada.Numerics.Elementary_Functions; use Ada.Numerics.Elementary_Functions;
with Ada.Text_IO; use Ada.Text_IO;
procedure Pipelined_Mergesort is
No_Of_Elements : constant Positive := Positive'Value (Argument (1));
subtype Element is Natural;
package Random_Elements is new Discrete_Random (Result_Subtype => Element);
use Random_Elements;
Random_Generator : Generator;
type Index is new Natural;
type Element_Array is array (Index range <>) of Element;
begin
Reset (Random_Generator);
declare
Data : constant Element_Array (1 .. Index (No_Of_Elements)) := (others => Random (Random_Generator));
function Is_Sorted (D : Element_Array) return Boolean is
(for all i in D'First .. D'Last - 1 => D (i) <= D (i + 1));
function Is_Permutation (Field_A, Field_B : Element_Array) return Boolean is
package Element_Vectors is new Vectors (Positive, Element); use Element_Vectors;
package Sorting is new Generic_Sorting; use Sorting;
Vector_A, Vector_B : Vector := Empty_Vector;
begin
for A of Field_A loop
Append (Vector_A, A);
end loop;
for B of Field_B loop
Append (Vector_B, B);
end loop;
Sort (Vector_A);
Sort (Vector_B);
return Vector_A = Vector_B;
end Is_Permutation;
No_Of_Stages : constant Positive := Positive (Float'Ceiling (Log (Float (No_Of_Elements), 2.0)));
function Merge (A, B : Element_Array) return Element_Array is
(if A'Length = 0 then B
elsif B'Length = 0 then A
elsif A (A'First) < B (B'First)
then A (A'First) & Merge (A (Index'Succ (A'First) .. A'Last), B)
else B (B'First) & Merge (A, B (Index'Succ (B'First) .. B'Last)))
with Pre => Is_Sorted (A) and then Is_Sorted (B),
Post => Is_Sorted (Merge'Result) and then Is_Permutation (Merge'Result, A & B);
function Merge_Imperative (A, B : Element_Array) return Element_Array
with Pre => Is_Sorted (A) and then Is_Sorted (B),
Post => Is_Sorted (Merge_Imperative'Result) and then Is_Permutation (Merge_Imperative'Result, A & B);
function Merge_Imperative (A, B : Element_Array) return Element_Array is
begin
if A'Length = 0 then
return B;
elsif B'Length = 0 then
return A;
else
declare
Merged : Element_Array (A'First .. A'Last + B'Length);
A_Index : Index range A'Range := A'First;
B_Index : Index range B'Range := B'First;
begin
for M_Index in Merged'Range loop
declare
Merge_Element : Element renames Merged (M_Index);
Merge_Tail : Element_Array renames Merged (Index'Succ (M_Index) .. Merged'Last);
A_Element : constant Element := A (A_Index);
B_Element : constant Element := B (B_Index);
begin
if A_Element < B_Element then
Merge_Element := A_Element;
if A_Index = A'Last then
Merge_Tail := B (B_Index .. B'Last); return Merged;
else
A_Index := Index'Succ (A_Index);
end if;
else
Merge_Element := B_Element;
if B_Index = B'Last then
Merge_Tail := A (A_Index .. A'Last); return Merged;
else
B_Index := Index'Succ (B_Index);
end if;
end if;
end;
end loop;
raise Program_Error with "Merge for-loop should never complete";
end;
end if;
end Merge_Imperative;
begin
Put_Line ("Original data is " & (if Is_Sorted (Data) then "sorted" else "not sorted"));
end;
end Pipelined_Mergesort;