------------------------------------------------------------------------------
--                                                                          --
--                         GNAT RUN-TIME COMPONENTS                         --
--                                                                          --
--                   A D A . S T R I N G S . S E A R C H                    --
--                                                                          --
--                                 S p e c                                  --
--                                                                          --
--          Copyright (C) 1992-2021, Free Software Foundation, Inc.         --
--                                                                          --
-- GNAT is free software;  you can  redistribute it  and/or modify it under --
-- terms of the  GNU General Public License as published  by the Free Soft- --
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
--                                                                          --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception,   --
-- version 3.1, as published by the Free Software Foundation.               --
--                                                                          --
-- You should have received a copy of the GNU General Public License and    --
-- a copy of the GCC Runtime Library Exception along with this program;     --
-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
-- <http://www.gnu.org/licenses/>.                                          --
--                                                                          --
-- GNAT was originally developed  by the GNAT team at  New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc.      --
--                                                                          --
------------------------------------------------------------------------------

--  This package contains the search functions from Ada.Strings.Fixed. They
--  are separated out because they are shared by Ada.Strings.Bounded and
--  Ada.Strings.Unbounded, and we don't want to drag in other irrelevant stuff
--  from Ada.Strings.Fixed when using the other two packages. Although user
--  programs should access these subprograms via one of the standard string
--  packages, we do not make this a private package, since ghost function
--  Match is used in the contracts of the standard string packages.

--  Preconditions in this unit are meant for analysis only, not for run-time
--  checking, so that the expected exceptions are raised. This is enforced
--  by setting the corresponding assertion policy to Ignore. Postconditions,
--  contract cases and ghost code should not be executed at runtime as well,
--  in order not to slow down the execution of these functions.

pragma Assertion_Policy (Pre            => Ignore,
                         Post           => Ignore,
                         Contract_Cases => Ignore,
                         Ghost          => Ignore);

with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;

package Ada.Strings.Search with SPARK_Mode is
   pragma Preelaborate;

   --  The ghost function Match tells whether the slice of Source starting at
   --  From and of length Pattern'Length matches with Pattern with respect to
   --  Mapping. Pattern should be non-empty and the considered slice should be
   --  fully included in Source'Range.

   function Match
     (Source  : String;
      Pattern : String;
      Mapping : Maps.Character_Mapping_Function;
      From    : Integer) return Boolean
   is
      (for all K in Pattern'Range =>
         Pattern (K) = Mapping (Source (From + (K - Pattern'First))))
   with
     Ghost,
     Pre    => Mapping /= null
       and then Pattern'Length > 0
       and then Source'Length > 0
       and then From in Source'First .. Source'Last - (Pattern'Length - 1),
     Global => null;

   function Match
     (Source  : String;
      Pattern : String;
      Mapping : Maps.Character_Mapping;
      From    : Integer) return Boolean
   is
      (for all K in Pattern'Range =>
         Pattern (K) =
           Ada.Strings.Maps.Value
             (Mapping, Source (From + (K - Pattern'First))))
   with
     Ghost,
     Pre    => Pattern'Length > 0
       and then Source'Length > 0
       and then From in Source'First .. Source'Last - (Pattern'Length - 1),
     Global => null;

   function Is_Identity
     (Mapping : Maps.Character_Mapping) return Boolean
   with
     Post   => (if Is_Identity'Result then
                (for all K in Character =>
                   Ada.Strings.Maps.Value (Mapping, K) = K)),
     Global => null;

   function Index
     (Source  : String;
      Pattern : String;
      Going   : Direction := Forward;
      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
   with
     Pre            => Pattern'Length > 0,

     Post           => Index'Result in 0 | Source'Range,
     Contract_Cases =>

       --  If Source is the empty string, then 0 is returned

       (Source'Length = 0 => Index'Result = 0,

        --  If some slice of Source matches Pattern, then a valid index is
        --  returned.

        Source'Length > 0
          and then
            (for some J in
               Source'First .. Source'Last - (Pattern'Length - 1) =>
                 Match (Source, Pattern, Mapping, J))
        =>

          --  The result is in the considered range of Source

          Index'Result in Source'First .. Source'Last - (Pattern'Length - 1)

            --  The slice beginning at the returned index matches Pattern

            and then Match (Source, Pattern, Mapping, Index'Result)

            --  The result is the smallest or largest index which satisfies
            --  the matching, respectively when Going = Forward and Going =
            --  Backward.

            and then
              (for all J in Source'Range =>
                 (if (if Going = Forward
                      then J <= Index'Result - 1
                      else J - 1 in Index'Result
                                    .. Source'Last - Pattern'Length)
                  then not (Match (Source, Pattern, Mapping, J)))),

        --  Otherwise, 0 is returned

        others => Index'Result = 0),
     Global         => null;

   function Index
     (Source  : String;
      Pattern : String;
      Going   : Direction := Forward;
      Mapping : Maps.Character_Mapping_Function) return Natural
   with
     Pre            => Pattern'Length > 0 and then Mapping /= null,
     Post           => Index'Result in 0 | Source'Range,
     Contract_Cases =>

       --  If Source is the null string, then 0 is returned

       (Source'Length = 0 => Index'Result = 0,

        --  If some slice of Source matches Pattern, then a valid index is
        --  returned.

        Source'Length > 0 and then
        (for some J in Source'First .. Source'Last - (Pattern'Length - 1) =>
             Match (Source, Pattern, Mapping, J))
        =>

          --  The result is in the considered range of Source

          Index'Result in Source'First .. Source'Last - (Pattern'Length - 1)

            --  The slice beginning at the returned index matches Pattern

            and then Match (Source, Pattern, Mapping, Index'Result)

            --  The result is the smallest or largest index which satisfies
            --  the matching, respectively when Going = Forward and Going =
            --  Backward.

            and then
              (for all J in Source'Range =>
                 (if (if Going = Forward
                      then J <= Index'Result - 1
                      else J - 1 in Index'Result
                                    .. Source'Last - Pattern'Length)
                  then not (Match (Source, Pattern, Mapping, J)))),

        --  Otherwise, 0 is returned

        others => Index'Result = 0),
     Global         => null;

   function Index
     (Source : String;
      Set    : Maps.Character_Set;
      Test   : Membership := Inside;
      Going  : Direction  := Forward) return Natural
   with
     Post           => Index'Result in 0 | Source'Range,
     Contract_Cases =>

        --  If no character of Source satisfies the property Test on Set, then
        --  0 is returned.

       ((for all C of Source =>
           (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))
        =>
          Index'Result = 0,

        --  Otherwise, an index in the range of Source is returned

        others =>

          --  The result is in the range of Source

          Index'Result in Source'Range

            --  The character at the returned index satisfies the property
            --  Test on Set.

            and then (Test = Inside)
              = Ada.Strings.Maps.Is_In (Source (Index'Result), Set)

            --  The result is the smallest or largest index which satisfies
            --  the property, respectively when Going = Forward and Going =
            --  Backward.

            and then
              (for all J in Source'Range =>
                 (if J /= Index'Result
                       and then (J < Index'Result) = (Going = Forward)
                  then (Test = Inside)
                       /= Ada.Strings.Maps.Is_In (Source (J), Set)))),
     Global         => null;

   function Index
     (Source  : String;
      Pattern : String;
      From    : Positive;
      Going   : Direction := Forward;
      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
   with
     Pre            => Pattern'Length > 0
       and then (if Source'Length > 0 then From in Source'Range),

     Post           => Index'Result in 0 | Source'Range,
     Contract_Cases =>

       --  If Source is the empty string, then 0 is returned

       (Source'Length = 0 => Index'Result = 0,

        --  If some slice of Source matches Pattern, then a valid index is
        --  returned.

        Source'Length > 0
          and then
            (for some J in
              (if Going = Forward then From else Source'First)
              .. (if Going = Forward then Source'Last else From)
               - (Pattern'Length - 1) =>
              Match (Source, Pattern, Mapping, J))
        =>

          --  The result is in the considered range of Source

          Index'Result in
            (if Going = Forward then From else Source'First)
            .. (if Going = Forward then Source'Last else From)
              - (Pattern'Length - 1)

            --  The slice beginning at the returned index matches Pattern

            and then Match (Source, Pattern, Mapping, Index'Result)

            --  The result is the smallest or largest index which satisfies
            --  the matching, respectively when Going = Forward and Going =
            --  Backward.

            and then
              (for all J in Source'Range =>
                 (if (if Going = Forward
                      then J in From .. Index'Result - 1
                      else J - 1 in Index'Result
                                    .. From - Pattern'Length)
                  then not (Match (Source, Pattern, Mapping, J)))),

        --  Otherwise, 0 is returned

        others => Index'Result = 0),
     Global         => null;

   function Index
     (Source  : String;
      Pattern : String;
      From    : Positive;
      Going   : Direction := Forward;
      Mapping : Maps.Character_Mapping_Function) return Natural
   with
     Pre            => Pattern'Length > 0
       and then Mapping /= null
       and then (if Source'Length > 0 then From in Source'Range),

     Post           => Index'Result in 0 | Source'Range,
     Contract_Cases =>

       --  If Source is the empty string, then 0 is returned

       (Source'Length = 0 => Index'Result = 0,

        --  If some slice of Source matches Pattern, then a valid index is
        --  returned.

        Source'Length > 0
          and then
            (for some J in
              (if Going = Forward then From else Source'First)
              .. (if Going = Forward then Source'Last else From)
               - (Pattern'Length - 1) =>
              Match (Source, Pattern, Mapping, J))
        =>

          --  The result is in the considered range of Source

          Index'Result in
            (if Going = Forward then From else Source'First)
            .. (if Going = Forward then Source'Last else From)
              - (Pattern'Length - 1)

            --  The slice beginning at the returned index matches Pattern

            and then Match (Source, Pattern, Mapping, Index'Result)

            --  The result is the smallest or largest index which satisfies
            --  the matching, respectively when Going = Forward and Going =
            --  Backwards.

            and then
              (for all J in Source'Range =>
                 (if (if Going = Forward
                      then J in From .. Index'Result - 1
                      else J - 1 in Index'Result
                                    .. From - Pattern'Length)
                  then not (Match (Source, Pattern, Mapping, J)))),

        --  Otherwise, 0 is returned

        others => Index'Result = 0),
     Global         => null;

   function Index
     (Source  : String;
      Set     : Maps.Character_Set;
      From    : Positive;
      Test    : Membership := Inside;
      Going   : Direction := Forward) return Natural
   with
     Pre            => (if Source'Length > 0 then From in Source'Range),
     Post           => Index'Result in 0 | Source'Range,
     Contract_Cases =>

        --  If Source is the empty string, or no character of the considered
        --  slice of Source satisfies the property Test on Set, then 0 is
        --  returned.

        (Source'Length = 0
          or else
            (for all J in Source'Range =>
               (if J = From or else (J > From) = (Going = Forward) then
                  (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (J), Set)))
        =>
          Index'Result = 0,

        --  Otherwise, an index in the considered range of Source is returned

        others =>

          --  The result is in the considered range of Source

          Index'Result in Source'Range
            and then (Index'Result = From
                       or else
                         (Index'Result > From) = (Going = Forward))

            --  The character at the returned index satisfies the property
            --  Test on Set

            and then
              (Test = Inside)
              = Ada.Strings.Maps.Is_In (Source (Index'Result), Set)

            --  The result is the smallest or largest index which satisfies
            --  the property, respectively when Going = Forward and Going =
            --  Backward.

            and then
              (for all J in Source'Range =>
                 (if J /= Index'Result
                    and then (J < Index'Result) = (Going = Forward)
                    and then (J = From
                                or else (J > From) = (Going = Forward))
                  then (Test = Inside)
                       /= Ada.Strings.Maps.Is_In (Source (J), Set)))),
     Global         => null;

   function Index_Non_Blank
     (Source : String;
      Going  : Direction := Forward) return Natural
   with
     Post           => Index_Non_Blank'Result in 0 | Source'Range,
     Contract_Cases =>

        --  If all characters of Source are Space characters, then 0 is
        --  returned.

       ((for all C of Source => C = ' ') => Index_Non_Blank'Result = 0,

        --  Otherwise, a valid index is returned

        others                           =>

          --  The result is in the range of Source

          Index_Non_Blank'Result in Source'Range

            --  The character at the returned index is not a Space character

            and then Source (Index_Non_Blank'Result) /= ' '

            --  The result is the smallest or largest index which is not a
            --  Space character, respectively when Going = Forward and
            --  Going = Backward.

            and then
              (for all J in Source'Range =>
                 (if J /= Index_Non_Blank'Result
                       and then (J < Index_Non_Blank'Result)
                              = (Going = Forward)
                  then Source (J) = ' '))),
     Global         => null;

   function Index_Non_Blank
     (Source : String;
      From   : Positive;
      Going  : Direction := Forward) return Natural
   with
     Pre            => (if Source'Length /= 0 then From in Source'Range),
     Post           => Index_Non_Blank'Result in 0 | Source'Range,
     Contract_Cases =>

        --  If Source is the null string, or all characters in the considered
        --  slice of Source are Space characters, then 0 is returned.

        (Source'Length = 0
          or else
            (for all J in Source'Range =>
               (if J = From or else (J > From) = (Going = Forward) then
                  Source (J) = ' '))
        =>
          Index_Non_Blank'Result = 0,

        --  Otherwise, a valid index is returned

        others =>

          --  The result is in the considered range of Source

          Index_Non_Blank'Result in Source'Range
            and then (Index_Non_Blank'Result = From
                        or else (Index_Non_Blank'Result > From)
                                = (Going = Forward))

            --  The character at the returned index is not a Space character

            and then Source (Index_Non_Blank'Result) /= ' '

            --  The result is the smallest or largest index which is not a
            --  Space character, respectively when Going = Forward and
            --  Going = Backward.

            and then
              (for all J in Source'Range =>
                 (if J /= Index_Non_Blank'Result
                       and then (J < Index_Non_Blank'Result)
                                = (Going = Forward)
                       and then (J = From or else (J > From)
                                = (Going = Forward))
                  then Source (J) = ' '))),
     Global         => null;

   function Count
     (Source  : String;
      Pattern : String;
      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
   with
     Pre    => Pattern'Length > 0,
     Global => null;

   function Count
     (Source  : String;
      Pattern : String;
      Mapping : Maps.Character_Mapping_Function) return Natural
   with
     Pre    => Pattern'Length > 0 and then Mapping /= null,
     Global => null;

   function Count
     (Source : String;
      Set    : Maps.Character_Set) return Natural
   with
     Global => null;

   procedure Find_Token
     (Source : String;
      Set    : Maps.Character_Set;
      From   : Positive;
      Test   : Membership;
      First  : out Positive;
      Last   : out Natural)
   with
     Pre            => (if Source'Length /= 0 then From in Source'Range),
     Contract_Cases =>

        --  If Source is the empty string, or if no character of the considered
        --  slice of Source satisfies the property Test on Set, then First is
        --  set to From and Last is set to 0.

       (Source'Length = 0
         or else
           (for all C of Source (From .. Source'Last) =>
              (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))
        =>
          First = From and then Last = 0,

        --  Otherwise, First and Last are set to valid indexes

        others =>

          --  First and Last are in the considered range of Source

          First in From .. Source'Last
            and then Last in First .. Source'Last

            --  No character between From and First satisfies the property Test
            --  on Set.

            and then
              (for all C of Source (From .. First - 1) =>
                 (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))

            --  All characters between First and Last satisfy the property Test
            --  on Set.

            and then
              (for all C of Source (First .. Last) =>
                 (Test = Inside) = Ada.Strings.Maps.Is_In (C, Set))

            --  If Last is not Source'Last, then the character at position
            --  Last + 1 does not satify the property Test on Set.

            and then
              (if Last < Source'Last
               then (Test = Inside)
                 /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))),
     Global         => null;

   procedure Find_Token
     (Source : String;
      Set    : Maps.Character_Set;
      Test   : Membership;
      First  : out Positive;
      Last   : out Natural)
   with
     Pre            => Source'First > 0,
     Contract_Cases =>

        --  If Source is the empty string, or if no character of Source
        --  satisfies the property Test on Set, then First is set to From
        --  and Last is set to 0.

       (Source'Length = 0
         or else
           (for all C of Source =>
              (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))
        =>
          First = Source'First and then Last = 0,

        --  Otherwise, First and Last are set to valid indexes

        others =>

          --  First and Last are in the considered range of Source

          First in Source'Range
            and then Last in First .. Source'Last

            --  No character before First satisfies the property Test on Set

            and then
              (for all C of Source (Source'First .. First - 1) =>
                 (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))

            --  All characters between First and Last satisfy the property Test
            --  on Set.

            and then
              (for all C of Source (First .. Last) =>
                 (Test = Inside) = Ada.Strings.Maps.Is_In (C, Set))

            --  If Last is not Source'Last, then the character at position
            --  Last + 1 does not satify the property Test on Set.

            and then
              (if Last < Source'Last
               then (Test = Inside)
                 /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))),
     Global => null;

end Ada.Strings.Search;