-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================

--------------------------------------------------------------------------------
--  E_Strings
--
--  Purpose:
--
--  In addition to the basic constructors and operations, simple I/O
--  procedure are prodived to Put and Read such strings to/from a
--  SPARK_IO file.
--
--  Clients:
--   Used throughout the Examiner and other tools.
--
--  Use:
--   Declare an E_Strings.T
--
--  Initialization via the constant Empty_String or via constructors
--  Copy_String
--
--  Extension:
--   None planned.
--------------------------------------------------------------------------------

with SPARK.Ada.Strings.Unbounded;
with SPARK_IO;

--# inherit Ada.Characters.Handling,
--#         Ada.Characters.Latin_1,
--#         SPARK.Ada.Strings.Maps,
--#         SPARK.Ada.Strings.Unbounded,
--#         SPARK_IO;

package E_Strings is

   subtype Lengths is Natural;

   subtype Positions is Positive;

   subtype Valid_Base is Positive range 2 .. 16;

   type T is private;

   --  First_One_First  : first parameter is lexigraphicaly less
   --  Second_One_First : second parameter is lexigraphicaly less
   --  Neither_First    : 2 parameters are equal
   type Order_Types is (First_One_First, Second_One_First, Neither_First);

   -----------------------------------------------------------------------------
   -- Constants
   -----------------------------------------------------------------------------

   Empty_String : constant T;

   -----------------------------------------------------------------------------
   -- Operations
   -----------------------------------------------------------------------------

   --  Conversion
   function To_Unbounded_String (E_Str : T) return SPARK.Ada.Strings.Unbounded.Unbounded_String;

   --  Equality operators

   -- Case INsensitive comparison.
   function Eq_String (E_Str1, E_Str2 : T) return Boolean;

   -- Case INsensitive comparison.
   function Eq1_String (E_Str : T;
                        Str   : String) return Boolean;

   --  Case sensitive comparison.
   function Eq_CS_String (E_Str1, E_Str2 : T) return Boolean;

   function Is_Empty (E_Str : T) return Boolean;

   function Get_Length (E_Str : T) return Lengths;

   function Get_Empty_String return T;
   --# return S => Get_Length (S) = 0 and S = Empty_String;

   function Get_Element (E_Str : T;
                         Pos   : Positions) return Character;

   function Copy_String (Str : String) return T;

   --  Append Str to E_Str
   procedure Append_String (E_Str : in out T;
                            Str   : in     String);
   --# derives E_Str from *,
   --#                    Str;

   --  Append E_Str2 to E_Str1
   procedure Append_Examiner_String (E_Str1 : in out T;
                                     E_Str2 : in     T);
   --# derives E_Str1 from *,
   --#                     E_Str2;

   function Lower_Case (E_Str : T) return T;

   function Upper_Case (E_Str : T) return T;

   function Lower_Case_Char (E_Str : T;
                             Pos   : Positions) return T;

   function Upper_Case_Char (E_Str : T;
                             Pos   : Positions) return T;

   --  Replace all the From_Char by To_Char
   function Translate
     (E_Str     : T;
      From_Char : Character;
      To_Char   : Character)
     return      T;

   procedure Append_Char (E_Str : in out T;
                          Ch    : in     Character);
   --# derives E_Str from *,
   --#                    Ch;
   --# post Get_Length (E_Str) = Get_Length (E_Str~) + 1;

   --  Find_Sub_String_After : find the specified Search_String,
   --  starting at the specified position in the given T
   procedure Find_Sub_String_After
     (E_Str         : in     T;
      Search_Start  : in     Positions;
      Search_String : in     String;
      String_Found  :    out Boolean;
      String_Start  :    out Positions);
   --# derives String_Found,
   --#         String_Start from E_Str,
   --#                           Search_Start,
   --#                           Search_String;

   --  Find_Sub_String : find specified Search_String in the given T
   procedure Find_Sub_String
     (E_Str         : in     T;
      Search_String : in     String;
      String_Found  :    out Boolean;
      String_Start  :    out Positions);
   --# derives String_Found,
   --#         String_Start from E_Str,
   --#                           Search_String;

   procedure Find_Examiner_Sub_String
     (E_Str         : in     T;
      Search_String : in     T;
      String_Found  :    out Boolean;
      String_Start  :    out Positions);
   --# derives String_Found,
   --#         String_Start from E_Str,
   --#                           Search_String;

   --  Pop_Char takes as input a T.  It removes the first character
   --  from the string and returns it in the Char output parameter.
   --  If the empty string is passed in then the outputs are:
   --     E_Str = EmptyString
   --     Char  = ' '
   procedure Pop_Char (E_Str : in out T;
                       Char  :    out Character);
   --# derives Char,
   --#         E_Str from E_Str;

   --  Find_Char_After : find specified character in E_Str, starting
   --  at specified position
   procedure Find_Char_After
     (E_Str        : in     T;
      Search_Start : in     Positions;
      Search_Char  : in     Character;
      Char_Found   :    out Boolean;
      Char_Pos     :    out Positions);
   --# derives Char_Found,
   --#         Char_Pos   from E_Str,
   --#                         Search_Char,
   --#                         Search_Start;

   -- Find_Char : find first occurrence of specified character in E_Str
   procedure Find_Char
     (E_Str       : in     T;
      Search_Char : in     Character;
      Char_Found  :    out Boolean;
      Char_Pos    :    out Positions);
   --# derives Char_Found,
   --#         Char_Pos   from E_Str,
   --#                         Search_Char;

   --  See Order_Types above
   function Lex_Order (First_Name, Second_Name : T) return Order_Types;

   --  Section returns the specified subsection of the string if the
   --  subsection lies outside the string, empty string returned
   function Section
     (E_Str     : T;
      Start_Pos : Positions;
      Length    : Lengths)
     return      T;

   --  Trim removes ' ', Latin_1.HT, Latin_1.LF, Latin_1.CR from both
   --  ends of the string
   function Trim (E_Str : T) return T;

   procedure Get_Int_From_String
     (Source   : in     T;
      Item     :    out Integer;
      Start_Pt : in     Positions;
      Stop     :    out Natural);
   --# derives Item,
   --#         Stop from Source,
   --#                   Start_Pt;

   --  This procedure generates a string, optionally space-padded with
   --  Start_Pt - 1 spaces, representing the given integer Item. You
   --  can specify a Base other than ten.
   --
   --  The precondition requires some explanation: The maximum string
   --  length cannot exceed Lengths'Last. To show that the generated
   --  string will fit into that the padding + the maximum string
   --  length may not exceed Lengths'Last. The maximum string length
   --  that can be generated is either Integer'First or Integer'Last
   --  in base 2. This means you will at most need 4 + 1 + 31 extra
   --  characters, 3 for the base prefix (bb#<number>#), 1 for the
   --  sign, and up to 31 (i.e. max(ln2(Integer'First),
   --  ln2(Integer'Last))). The latter is enforced by comparing 2 **
   --  31 to Integer'First and Integer'Last.
   Put_Int_To_String_Max_Int_Size : constant Integer := 31;
   procedure Put_Int_To_String
     (Dest     :    out T;
      Item     : in     Integer;
      Start_Pt : in     Positions;
      Base     : in     Valid_Base);
   --# derives Dest from Base,
   --#                   Item,
   --#                   Start_Pt;
   --# pre Start_Pt < Lengths'Last - (4 + 1 + Put_Int_To_String_Max_Int_Size) and
   --#   -(2 ** Put_Int_To_String_Max_Int_Size) = Integer'First and
   --#   (2 ** Put_Int_To_String_Max_Int_Size) - 1 = Integer'Last;

   -- Given two strings, A and B, return the length of their
   -- common prefix (if any), limited to '.' and string
   -- boundaries. So, for example:
   --
   -- E_Str_A   E_Str_B   Prefix
   -- -----------------------------
   -- Foo.B1  | Foo.B2  | 3 (Foo)
   -- Foo     | Foo.B2  | 3 (Foo)
   -- Foo     | Foobar  | 0 ()
   -- A.B.C   | A.B.X   | 3 (A.B)
   function Get_Dotted_Common_Prefix_Length (E_Str_A, E_Str_B : T) return Lengths;

   --  This function returns true if the given E_Str starts with Str.
   function Starts_With (E_Str : T;
                         Str   : String) return Boolean;
   --# return X => X -> Get_Length (E_Str) >= Str'Length;

   -----------------------------------------------------------------------------
   -- I/O procedures
   -----------------------------------------------------------------------------
   --  See Ada.Text_IO for the Form_Of_File parameters

   procedure Create
     (File         : in out SPARK_IO.File_Type;
      Name_Of_File : in     T;
      Form_Of_File : in     String;
      Status       :    out SPARK_IO.File_Status);
   --# global in out SPARK_IO.File_Sys;
   --# derives File,
   --#         SPARK_IO.File_Sys,
   --#         Status            from File,
   --#                                Form_Of_File,
   --#                                Name_Of_File,
   --#                                SPARK_IO.File_Sys;

   procedure Open
     (File         : in out SPARK_IO.File_Type;
      Mode_Of_File : in     SPARK_IO.File_Mode;
      Name_Of_File : in     T;
      Form_Of_File : in     String;
      Status       :    out SPARK_IO.File_Status);
   --# global in out SPARK_IO.File_Sys;
   --# derives File,
   --#         SPARK_IO.File_Sys,
   --#         Status            from File,
   --#                                Form_Of_File,
   --#                                Mode_Of_File,
   --#                                Name_Of_File,
   --#                                SPARK_IO.File_Sys;

   procedure Put_String (File  : in SPARK_IO.File_Type;
                         E_Str : in T);
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                E_Str,
   --#                                File;

   procedure Put_Line (File  : in SPARK_IO.File_Type;
                       E_Str : in T);
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                E_Str,
   --#                                File;

   procedure Get_Line (File  : in     SPARK_IO.File_Type;
                       E_Str :    out T);
   --# global in out SPARK_IO.File_Sys;
   --# derives E_Str,
   --#         SPARK_IO.File_Sys from File,
   --#                                SPARK_IO.File_Sys;

private

   type T is record
      Content : SPARK.Ada.Strings.Unbounded.Unbounded_String;
   end record;

   Empty_String : constant T := T'(Content => SPARK.Ada.Strings.Unbounded.Null_Unbounded_String);

end E_Strings;