int_list_pkg

int_list_pkg.adb

package Int_List_Pkg is
   type Int_List (Max_Length : Natural) is private
     with Type_Invariant => Is_Sorted (Int_List);

   function Is_Sorted (List : Int_List) return Boolean;

   type Int_array is array (Positive range <>) of Integer;

   function To_Int_List (Ints : Int_Array) return Int_List;

   function To_Int_Array (List : Int_List) return Int_Array;

   function "&" (Left, Right : Int_List) return Int_List;

   ... -- other subprograms
private

   type int_List (Max_Length : Natural) is record
      Length : Natural;
      Data   : Int_Array (1..Max_Length);
   end record;

   function Is_Sorted (List : Int_List) return Boolean is
      (for all I in List.Data'First .. List.Length-1 =>
         List.Data (I) <= List.Data (I+1));

end Int_List_Pkg;

package body Int_List_Pkg is
   procedure Sort (Ints : in out Int_Array) is
   begin
     ... -- Your favourite sorting algorithm
   end Sort;

   function To_Int_List (Ints : Int_Array) return Int_List is
      List : Int_List :=
        (Max_Length => Ints'Length,
         Length     => Ints'Length,
         Data       => Ints);
   begin
     Sort (List.Data);
     return List;
   end To_Int_List;

   function To_Int_Array (List : Int_List) return Int_Array is
   begin
      return List.Data;
   end To_Int_Array;

   function "&" (Left, Right : Int_List) return Int_List is
      Ints : Int_array := Left.Data & Right.Data;
   begin
      Sort (Ints);
      return To_int_list (Ints);
   end "&"

   ... -- Other subprograms
end Int_List_Pkg;