| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT RUN-TIME COMPONENTS -- |
| -- -- |
| -- A D A . S T R I N G S . B O U N D E D -- |
| -- -- |
| -- S p e c -- |
| -- -- |
| -- Copyright (C) 1992-2022, Free Software Foundation, Inc. -- |
| -- -- |
| -- This specification is derived from the Ada Reference Manual for use with -- |
| -- GNAT. The copyright notice above, and the license provisions that follow -- |
| -- apply solely to the contents of the part following the private keyword. -- |
| -- -- |
| -- 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. -- |
| -- -- |
| ------------------------------------------------------------------------------ |
| |
| -- The language-defined package Strings.Bounded provides a generic package |
| -- each of whose instances yields a private type Bounded_String and a set |
| -- of operations. An object of a particular Bounded_String type represents |
| -- a String whose low bound is 1 and whose length can vary conceptually |
| -- between 0 and a maximum size established at the generic instantiation. The |
| -- subprograms for fixed-length string handling are either overloaded directly |
| -- for Bounded_String, or are modified as needed to reflect the variability in |
| -- length. Additionally, since the Bounded_String type is private, appropriate |
| -- constructor and selector operations are provided. |
| |
| with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; |
| with Ada.Strings.Superbounded; |
| with Ada.Strings.Search; |
| |
| package Ada.Strings.Bounded with SPARK_Mode is |
| pragma Preelaborate; |
| |
| generic |
| Max : Positive; |
| -- Maximum length of a Bounded_String |
| |
| package Generic_Bounded_Length with SPARK_Mode, |
| Initial_Condition => Length (Null_Bounded_String) = 0, |
| Abstract_State => null |
| is |
| -- 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 and contract cases 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); |
| |
| Max_Length : constant Positive := Max; |
| |
| type Bounded_String is private; |
| pragma Preelaborable_Initialization (Bounded_String); |
| |
| Null_Bounded_String : constant Bounded_String; |
| -- Null_Bounded_String represents the null string. If an object of type |
| -- Bounded_String is not otherwise initialized, it will be initialized |
| -- to the same value as Null_Bounded_String. |
| |
| subtype Length_Range is Natural range 0 .. Max_Length; |
| |
| function Length (Source : Bounded_String) return Length_Range with |
| Global => null; |
| -- The Length function returns the length of the string represented by |
| -- Source. |
| |
| -------------------------------------------------------- |
| -- Conversion, Concatenation, and Selection Functions -- |
| -------------------------------------------------------- |
| |
| function To_Bounded_String |
| (Source : String; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => (if Source'Length > Max_Length then Drop /= Error), |
| Contract_Cases => |
| (Source'Length <= Max_Length |
| => |
| To_String (To_Bounded_String'Result) = Source, |
| |
| Source'Length > Max_Length and then Drop = Left |
| => |
| To_String (To_Bounded_String'Result) = |
| Source (Source'Last - Max_Length + 1 .. Source'Last), |
| |
| others -- Drop = Right |
| => |
| To_String (To_Bounded_String'Result) = |
| Source (Source'First .. Source'First - 1 + Max_Length)); |
| -- If Source'Length <= Max_Length, then this function returns a |
| -- Bounded_String that represents Source. Otherwise, the effect |
| -- depends on the value of Drop: |
| -- |
| -- * If Drop=Left, then the result is a Bounded_String that represents |
| -- the string comprising the rightmost Max_Length characters of |
| -- Source. |
| -- |
| -- * If Drop=Right, then the result is a Bounded_String that represents |
| -- the string comprising the leftmost Max_Length characters of Source. |
| -- |
| -- * If Drop=Error, then Strings.Length_Error is propagated. |
| |
| function To_String (Source : Bounded_String) return String with |
| Global => null; |
| -- To_String returns the String value with lower bound 1 |
| -- represented by Source. If B is a Bounded_String, then |
| -- B = To_Bounded_String(To_String(B)). |
| |
| procedure Set_Bounded_String |
| (Target : out Bounded_String; |
| Source : String; |
| Drop : Truncation := Error) |
| with |
| Pre => (if Source'Length > Max_Length then Drop /= Error), |
| Contract_Cases => |
| (Source'Length <= Max_Length |
| => |
| To_String (Target) = Source, |
| |
| Source'Length > Max_Length and then Drop = Left |
| => |
| To_String (Target) = |
| Source (Source'Last - Max_Length + 1 .. Source'Last), |
| |
| others -- Drop = Right |
| => |
| To_String (Target) = |
| Source (Source'First .. Source'First - 1 + Max_Length)); |
| pragma Ada_05 (Set_Bounded_String); |
| -- Equivalent to Target := To_Bounded_String (Source, Drop); |
| |
| -- Each of the Append functions returns a Bounded_String obtained by |
| -- concatenating the string or character given or represented by one |
| -- of the parameters, with the string or character given or represented |
| -- by the other parameter, and applying To_Bounded_String to the |
| -- concatenation result string, with Drop as provided to the Append |
| -- function. |
| |
| function Append |
| (Left : Bounded_String; |
| Right : Bounded_String; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => |
| (if Length (Left) > Max_Length - Length (Right) |
| then Drop /= Error), |
| Contract_Cases => |
| (Length (Left) <= Max_Length - Length (Right) |
| => |
| Length (Append'Result) = Length (Left) + Length (Right) |
| and then |
| Slice (Append'Result, 1, Length (Left)) = To_String (Left) |
| and then |
| (if Length (Right) > 0 then |
| Slice (Append'Result, |
| Length (Left) + 1, Length (Append'Result)) = |
| To_String (Right)), |
| |
| Length (Left) > Max_Length - Length (Right) |
| and then Drop = Strings.Left |
| => |
| Length (Append'Result) = Max_Length |
| and then |
| (if Length (Right) < Max_Length then |
| Slice (Append'Result, 1, Max_Length - Length (Right)) = |
| Slice (Left, |
| Length (Left) - Max_Length + Length (Right) + 1, |
| Length (Left))) |
| and then |
| Slice (Append'Result, |
| Max_Length - Length (Right) + 1, Max_Length) = |
| To_String (Right), |
| |
| others -- Drop = Right |
| => |
| Length (Append'Result) = Max_Length |
| and then |
| Slice (Append'Result, 1, Length (Left)) = To_String (Left) |
| and then |
| (if Length (Left) < Max_Length then |
| Slice (Append'Result, Length (Left) + 1, Max_Length) = |
| Slice (Right, 1, Max_Length - Length (Left)))); |
| |
| function Append |
| (Left : Bounded_String; |
| Right : String; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => |
| (if Right'Length > Max_Length - Length (Left) |
| then Drop /= Error), |
| Contract_Cases => |
| (Length (Left) <= Max_Length - Right'Length |
| => |
| Length (Append'Result) = Length (Left) + Right'Length |
| and then |
| Slice (Append'Result, 1, Length (Left)) = To_String (Left) |
| and then |
| (if Right'Length > 0 then |
| Slice (Append'Result, |
| Length (Left) + 1, Length (Append'Result)) = |
| Right), |
| |
| Length (Left) > Max_Length - Right'Length |
| and then Drop = Strings.Left |
| => |
| Length (Append'Result) = Max_Length |
| and then |
| (if Right'Length < Max_Length then |
| |
| -- The result is the end of Left followed by Right |
| |
| Slice (Append'Result, 1, Max_Length - Right'Length) = |
| Slice (Left, |
| Length (Left) - Max_Length + Right'Length + 1, |
| Length (Left)) |
| and then |
| Slice (Append'Result, |
| Max_Length - Right'Length + 1, Max_Length) = |
| Right |
| else |
| -- The result is the last Max_Length characters of Right |
| |
| To_String (Append'Result) = |
| Right (Right'Last - Max_Length + 1 .. Right'Last)), |
| |
| others -- Drop = Right |
| => |
| Length (Append'Result) = Max_Length |
| and then |
| Slice (Append'Result, 1, Length (Left)) = To_String (Left) |
| and then |
| (if Length (Left) < Max_Length then |
| Slice (Append'Result, Length (Left) + 1, Max_Length) = |
| Right (Right'First |
| .. Max_Length - Length (Left) - 1 + Right'First))); |
| function Append |
| (Left : String; |
| Right : Bounded_String; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => |
| (if Left'Length > Max_Length - Length (Right) |
| then Drop /= Error), |
| Contract_Cases => |
| (Left'Length <= Max_Length - Length (Right) |
| => |
| Length (Append'Result) = Left'Length + Length (Right) |
| and then Slice (Append'Result, 1, Left'Length) = Left |
| and then |
| (if Length (Right) > 0 then |
| Slice (Append'Result, |
| Left'Length + 1, Length (Append'Result)) = |
| To_String (Right)), |
| |
| Left'Length > Max_Length - Length (Right) |
| and then Drop = Strings.Left |
| => |
| Length (Append'Result) = Max_Length |
| and then |
| (if Length (Right) < Max_Length then |
| Slice (Append'Result, 1, Max_Length - Length (Right)) = |
| Left (Left'Last - Max_Length + Length (Right) + 1 |
| .. Left'Last)) |
| and then |
| Slice (Append'Result, |
| Max_Length - Length (Right) + 1, Max_Length) = |
| To_String (Right), |
| |
| others -- Drop = Right |
| => |
| Length (Append'Result) = Max_Length |
| and then |
| (if Left'Length < Max_Length then |
| |
| -- The result is Left followed by the beginning of Right |
| |
| Slice (Append'Result, 1, Left'Length) = Left |
| and then |
| Slice (Append'Result, Left'Length + 1, Max_Length) = |
| Slice (Right, 1, Max_Length - Left'Length) |
| else |
| -- The result is the first Max_Length characters of Left |
| |
| To_String (Append'Result) = |
| Left (Left'First .. Max_Length - 1 + Left'First))); |
| |
| function Append |
| (Left : Bounded_String; |
| Right : Character; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => (if Length (Left) = Max_Length then Drop /= Error), |
| Contract_Cases => |
| (Length (Left) < Max_Length |
| => |
| Length (Append'Result) = Length (Left) + 1 |
| and then |
| Slice (Append'Result, 1, Length (Left)) = To_String (Left) |
| and then Element (Append'Result, Length (Left) + 1) = Right, |
| |
| Length (Left) = Max_Length and then Drop = Strings.Right |
| => |
| Length (Append'Result) = Max_Length |
| and then To_String (Append'Result) = To_String (Left), |
| |
| others -- Drop = Left |
| => |
| Length (Append'Result) = Max_Length |
| and then |
| Slice (Append'Result, 1, Max_Length - 1) = |
| Slice (Left, 2, Max_Length) |
| and then Element (Append'Result, Max_Length) = Right); |
| |
| function Append |
| (Left : Character; |
| Right : Bounded_String; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => (if Length (Right) = Max_Length then Drop /= Error), |
| Contract_Cases => |
| (Length (Right) < Max_Length |
| => |
| Length (Append'Result) = Length (Right) + 1 |
| and then |
| Slice (Append'Result, 2, Length (Right) + 1) = |
| To_String (Right) |
| and then Element (Append'Result, 1) = Left, |
| |
| Length (Right) = Max_Length and then Drop = Strings.Left |
| => |
| Length (Append'Result) = Max_Length |
| and then To_String (Append'Result) = To_String (Right), |
| |
| others -- Drop = Right |
| => |
| Length (Append'Result) = Max_Length |
| and then |
| Slice (Append'Result, 2, Max_Length) = |
| Slice (Right, 1, Max_Length - 1) |
| and then Element (Append'Result, 1) = Left); |
| |
| -- Each of the procedures Append(Source, New_Item, Drop) has the same |
| -- effect as the corresponding assignment |
| -- Source := Append(Source, New_Item, Drop). |
| |
| procedure Append |
| (Source : in out Bounded_String; |
| New_Item : Bounded_String; |
| Drop : Truncation := Error) |
| with |
| Pre => |
| (if Length (Source) > Max_Length - Length (New_Item) |
| then Drop /= Error), |
| Contract_Cases => |
| (Length (Source) <= Max_Length - Length (New_Item) |
| => |
| Length (Source) = Length (Source'Old) + Length (New_Item) |
| and then |
| Slice (Source, 1, Length (Source'Old)) = |
| To_String (Source'Old) |
| and then |
| (if Length (New_Item) > 0 then |
| Slice (Source, Length (Source'Old) + 1, Length (Source)) = |
| To_String (New_Item)), |
| |
| Length (Source) > Max_Length - Length (New_Item) |
| and then Drop = Left |
| => |
| Length (Source) = Max_Length |
| and then |
| (if Length (New_Item) < Max_Length then |
| Slice (Source, 1, Max_Length - Length (New_Item)) = |
| Slice (Source'Old, |
| Length (Source'Old) - Max_Length + Length (New_Item) |
| + 1, |
| Length (Source'Old))) |
| and then |
| Slice (Source, Max_Length - Length (New_Item) + 1, Max_Length) |
| = To_String (New_Item), |
| |
| others -- Drop = Right |
| => |
| Length (Source) = Max_Length |
| and then |
| Slice (Source, 1, Length (Source'Old)) = |
| To_String (Source'Old) |
| and then |
| (if Length (Source'Old) < Max_Length then |
| Slice (Source, Length (Source'Old) + 1, Max_Length) = |
| Slice (New_Item, 1, Max_Length - Length (Source'Old)))); |
| |
| procedure Append |
| (Source : in out Bounded_String; |
| New_Item : String; |
| Drop : Truncation := Error) |
| with |
| Pre => |
| (if New_Item'Length > Max_Length - Length (Source) |
| then Drop /= Error), |
| Contract_Cases => |
| (Length (Source) <= Max_Length - New_Item'Length |
| => |
| Length (Source) = Length (Source'Old) + New_Item'Length |
| and then |
| Slice (Source, 1, Length (Source'Old)) = |
| To_String (Source'Old) |
| and then |
| (if New_Item'Length > 0 then |
| Slice (Source, Length (Source'Old) + 1, Length (Source)) = |
| New_Item), |
| |
| Length (Source) > Max_Length - New_Item'Length |
| and then Drop = Left |
| => |
| Length (Source) = Max_Length |
| and then |
| (if New_Item'Length < Max_Length then |
| |
| -- The result is the end of Source followed by New_Item |
| |
| Slice (Source, 1, Max_Length - New_Item'Length) = |
| Slice (Source'Old, |
| Length (Source'Old) - Max_Length + New_Item'Length + 1, |
| Length (Source'Old)) |
| and then |
| Slice (Source, |
| Max_Length - New_Item'Length + 1, Max_Length) = |
| New_Item |
| else |
| -- The result is the last Max_Length characters of |
| -- New_Item. |
| |
| To_String (Source) = New_Item |
| (New_Item'Last - Max_Length + 1 .. New_Item'Last)), |
| |
| others -- Drop = Right |
| => |
| Length (Source) = Max_Length |
| and then |
| Slice (Source, 1, Length (Source'Old)) = |
| To_String (Source'Old) |
| and then |
| (if Length (Source'Old) < Max_Length then |
| Slice (Source, Length (Source'Old) + 1, Max_Length) = |
| New_Item (New_Item'First |
| .. Max_Length - Length (Source'Old) - 1 |
| + New_Item'First))); |
| |
| procedure Append |
| (Source : in out Bounded_String; |
| New_Item : Character; |
| Drop : Truncation := Error) |
| with |
| Pre => (if Length (Source) = Max_Length then Drop /= Error), |
| Contract_Cases => |
| (Length (Source) < Max_Length |
| => |
| Length (Source) = Length (Source'Old) + 1 |
| and then |
| Slice (Source, 1, Length (Source'Old)) = |
| To_String (Source'Old) |
| and then Element (Source, Length (Source'Old) + 1) = New_Item, |
| |
| Length (Source) = Max_Length and then Drop = Right |
| => |
| Length (Source) = Max_Length |
| and then To_String (Source) = To_String (Source'Old), |
| |
| others -- Drop = Left |
| => |
| Length (Source) = Max_Length |
| and then |
| Slice (Source, 1, Max_Length - 1) = |
| Slice (Source'Old, 2, Max_Length) |
| and then Element (Source, Max_Length) = New_Item); |
| |
| -- Each of the "&" functions has the same effect as the corresponding |
| -- Append function, with Error as the Drop parameter. |
| |
| function "&" |
| (Left : Bounded_String; |
| Right : Bounded_String) return Bounded_String |
| with |
| Pre => Length (Left) <= Max_Length - Length (Right), |
| Post => Length ("&"'Result) = Length (Left) + Length (Right) |
| and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left) |
| and then |
| (if Length (Right) > 0 then |
| Slice ("&"'Result, Length (Left) + 1, Length ("&"'Result)) = |
| To_String (Right)); |
| |
| function "&" |
| (Left : Bounded_String; |
| Right : String) return Bounded_String |
| with |
| Pre => Right'Length <= Max_Length - Length (Left), |
| Post => Length ("&"'Result) = Length (Left) + Right'Length |
| and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left) |
| and then |
| (if Right'Length > 0 then |
| Slice ("&"'Result, Length (Left) + 1, Length ("&"'Result)) = |
| Right); |
| |
| function "&" |
| (Left : String; |
| Right : Bounded_String) return Bounded_String |
| with |
| Pre => Left'Length <= Max_Length - Length (Right), |
| Post => Length ("&"'Result) = Left'Length + Length (Right) |
| and then Slice ("&"'Result, 1, Left'Length) = Left |
| and then |
| (if Length (Right) > 0 then |
| Slice ("&"'Result, Left'Length + 1, Length ("&"'Result)) = |
| To_String (Right)); |
| |
| function "&" |
| (Left : Bounded_String; |
| Right : Character) return Bounded_String |
| with |
| Pre => Length (Left) < Max_Length, |
| Post => Length ("&"'Result) = Length (Left) + 1 |
| and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left) |
| and then Element ("&"'Result, Length (Left) + 1) = Right; |
| |
| function "&" |
| (Left : Character; |
| Right : Bounded_String) return Bounded_String |
| with |
| Pre => Length (Right) < Max_Length, |
| Post => Length ("&"'Result) = 1 + Length (Right) |
| and then Element ("&"'Result, 1) = Left |
| and then |
| Slice ("&"'Result, 2, Length ("&"'Result)) = To_String (Right); |
| |
| function Element |
| (Source : Bounded_String; |
| Index : Positive) return Character |
| with |
| Pre => Index <= Length (Source), |
| Global => null; |
| -- Returns the character at position Index in the string represented by |
| -- Source; propagates Index_Error if Index > Length(Source). |
| |
| procedure Replace_Element |
| (Source : in out Bounded_String; |
| Index : Positive; |
| By : Character) |
| with |
| Pre => Index <= Length (Source), |
| Post => Length (Source) = Length (Source'Old) |
| and then (for all K in 1 .. Length (Source) => |
| Element (Source, K) = |
| (if K = Index then By else Element (Source'Old, K))), |
| Global => null; |
| -- Updates Source such that the character at position Index in the |
| -- string represented by Source is By; propagates Index_Error if |
| -- Index > Length(Source). |
| |
| function Slice |
| (Source : Bounded_String; |
| Low : Positive; |
| High : Natural) return String |
| with |
| Pre => Low - 1 <= Length (Source) and then High <= Length (Source), |
| Global => null; |
| -- Returns the slice at positions Low through High in the |
| -- string represented by Source; propagates Index_Error if |
| -- Low > Length(Source)+1 or High > Length(Source). |
| -- The bounds of the returned string are Low and High. |
| |
| function Bounded_Slice |
| (Source : Bounded_String; |
| Low : Positive; |
| High : Natural) return Bounded_String |
| with |
| Pre => Low - 1 <= Length (Source) and then High <= Length (Source), |
| Post => To_String (Bounded_Slice'Result) = Slice (Source, Low, High), |
| Global => null; |
| pragma Ada_05 (Bounded_Slice); |
| -- Returns the slice at positions Low through High in the string |
| -- represented by Source as a bounded string; propagates Index_Error |
| -- if Low > Length(Source)+1 or High > Length(Source). |
| |
| procedure Bounded_Slice |
| (Source : Bounded_String; |
| Target : out Bounded_String; |
| Low : Positive; |
| High : Natural) |
| with |
| Pre => Low - 1 <= Length (Source) and then High <= Length (Source), |
| Post => To_String (Target) = Slice (Source, Low, High), |
| Global => null; |
| pragma Ada_05 (Bounded_Slice); |
| -- Equivalent to Target := Bounded_Slice (Source, Low, High); |
| |
| -- Each of the functions "=", "<", ">", "<=", and ">=" returns the same |
| -- result as the corresponding String operation applied to the String |
| -- values given or represented by the two parameters. |
| |
| function "=" |
| (Left : Bounded_String; |
| Right : Bounded_String) return Boolean |
| with |
| Post => "="'Result = (To_String (Left) = To_String (Right)), |
| Global => null; |
| |
| function "=" |
| (Left : Bounded_String; |
| Right : String) return Boolean |
| with |
| Post => "="'Result = (To_String (Left) = Right), |
| Global => null; |
| |
| function "=" |
| (Left : String; |
| Right : Bounded_String) return Boolean |
| with |
| Post => "="'Result = (Left = To_String (Right)), |
| Global => null; |
| |
| function "<" |
| (Left : Bounded_String; |
| Right : Bounded_String) return Boolean |
| with |
| Post => "<"'Result = (To_String (Left) < To_String (Right)), |
| Global => null; |
| |
| function "<" |
| (Left : Bounded_String; |
| Right : String) return Boolean |
| with |
| Post => "<"'Result = (To_String (Left) < Right), |
| Global => null; |
| |
| function "<" |
| (Left : String; |
| Right : Bounded_String) return Boolean |
| with |
| Post => "<"'Result = (Left < To_String (Right)), |
| Global => null; |
| |
| function "<=" |
| (Left : Bounded_String; |
| Right : Bounded_String) return Boolean |
| with |
| Post => "<="'Result = (To_String (Left) <= To_String (Right)), |
| Global => null; |
| |
| function "<=" |
| (Left : Bounded_String; |
| Right : String) return Boolean |
| with |
| Post => "<="'Result = (To_String (Left) <= Right), |
| Global => null; |
| |
| function "<=" |
| (Left : String; |
| Right : Bounded_String) return Boolean |
| with |
| Post => "<="'Result = (Left <= To_String (Right)), |
| Global => null; |
| |
| function ">" |
| (Left : Bounded_String; |
| Right : Bounded_String) return Boolean |
| with |
| Post => ">"'Result = (To_String (Left) > To_String (Right)), |
| Global => null; |
| |
| function ">" |
| (Left : Bounded_String; |
| Right : String) return Boolean |
| with |
| Post => ">"'Result = (To_String (Left) > Right), |
| Global => null; |
| |
| function ">" |
| (Left : String; |
| Right : Bounded_String) return Boolean |
| with |
| Post => ">"'Result = (Left > To_String (Right)), |
| Global => null; |
| |
| function ">=" |
| (Left : Bounded_String; |
| Right : Bounded_String) return Boolean |
| with |
| Post => ">="'Result = (To_String (Left) >= To_String (Right)), |
| Global => null; |
| |
| function ">=" |
| (Left : Bounded_String; |
| Right : String) return Boolean |
| with |
| Post => ">="'Result = (To_String (Left) >= Right), |
| Global => null; |
| |
| function ">=" |
| (Left : String; |
| Right : Bounded_String) return Boolean |
| with |
| Post => ">="'Result = (Left >= To_String (Right)), |
| Global => null; |
| |
| ---------------------- |
| -- Search Functions -- |
| ---------------------- |
| |
| -- Each of the search subprograms (Index, Index_Non_Blank, Count, |
| -- Find_Token) has the same effect as the corresponding subprogram in |
| -- Strings.Fixed applied to the string represented by the Bounded_String |
| -- parameter. |
| |
| function Index |
| (Source : Bounded_String; |
| Pattern : String; |
| Going : Direction := Forward; |
| Mapping : Maps.Character_Mapping := Maps.Identity) return Natural |
| with |
| Pre => Pattern'Length > 0, |
| Post => Index'Result <= Length (Source), |
| Contract_Cases => |
| |
| -- If Source is the empty string, then 0 is returned |
| |
| (Length (Source) = 0 |
| => |
| Index'Result = 0, |
| |
| -- If some slice of Source matches Pattern, then a valid index is |
| -- returned. |
| |
| Length (Source) > 0 |
| and then |
| (for some J in 1 .. Length (Source) - (Pattern'Length - 1) => |
| Search.Match (To_String (Source), Pattern, Mapping, J)) |
| => |
| -- The result is in the considered range of Source |
| |
| Index'Result in 1 .. Length (Source) - (Pattern'Length - 1) |
| |
| -- The slice beginning at the returned index matches Pattern |
| |
| and then Search.Match |
| (To_String (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 1 .. Length (Source) => |
| (if (if Going = Forward |
| then J <= Index'Result - 1 |
| else J - 1 in Index'Result |
| .. Length (Source) - Pattern'Length) |
| then not (Search.Match |
| (To_String (Source), Pattern, Mapping, J)))), |
| |
| -- Otherwise, 0 is returned |
| |
| others |
| => |
| Index'Result = 0), |
| Global => null; |
| |
| function Index |
| (Source : Bounded_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 <= Length (Source), |
| Contract_Cases => |
| |
| -- If Source is the empty string, then 0 is returned |
| |
| (Length (Source) = 0 |
| => |
| Index'Result = 0, |
| |
| -- If some slice of Source matches Pattern, then a valid index is |
| -- returned. |
| |
| Length (Source) > 0 |
| and then |
| (for some J in 1 .. Length (Source) - (Pattern'Length - 1) => |
| Search.Match (To_String (Source), Pattern, Mapping, J)) |
| => |
| -- The result is in the considered range of Source |
| |
| Index'Result in 1 .. Length (Source) - (Pattern'Length - 1) |
| |
| -- The slice beginning at the returned index matches Pattern |
| |
| and then Search.Match |
| (To_String (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 1 .. Length (Source) => |
| (if (if Going = Forward |
| then J <= Index'Result - 1 |
| else J - 1 in Index'Result |
| .. Length (Source) - Pattern'Length) |
| then not (Search.Match |
| (To_String (Source), Pattern, Mapping, J)))), |
| |
| -- Otherwise, 0 is returned |
| |
| others |
| => |
| Index'Result = 0), |
| Global => null; |
| |
| function Index |
| (Source : Bounded_String; |
| Set : Maps.Character_Set; |
| Test : Membership := Inside; |
| Going : Direction := Forward) return Natural |
| with |
| Post => Index'Result <= Length (Source), |
| Contract_Cases => |
| |
| -- If no character of Source satisfies the property Test on Set, |
| -- then 0 is returned. |
| |
| ((for all C of To_String (Source) => |
| (Test = Inside) /= 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 1 .. Length (Source) |
| |
| -- The character at the returned index satisfies the property |
| -- Test on Set. |
| |
| and then |
| (Test = Inside) = |
| Maps.Is_In (Element (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 1 .. Length (Source) => |
| (if J /= Index'Result |
| and then (J < Index'Result) = (Going = Forward) |
| then (Test = Inside) |
| /= Maps.Is_In (Element (Source, J), Set)))), |
| Global => null; |
| |
| function Index |
| (Source : Bounded_String; |
| Pattern : String; |
| From : Positive; |
| Going : Direction := Forward; |
| Mapping : Maps.Character_Mapping := Maps.Identity) return Natural |
| with |
| Pre => |
| (if Length (Source) /= 0 then From <= Length (Source)) |
| and then Pattern'Length /= 0, |
| Post => Index'Result <= Length (Source), |
| Contract_Cases => |
| |
| -- If Source is the empty string, then 0 is returned |
| |
| (Length (Source) = 0 |
| => |
| Index'Result = 0, |
| |
| -- If some slice of Source matches Pattern, then a valid index is |
| -- returned. |
| |
| Length (Source) > 0 |
| and then |
| (for some J in |
| (if Going = Forward then From else 1) |
| .. (if Going = Forward then Length (Source) else From) |
| - (Pattern'Length - 1) => |
| Search.Match (To_String (Source), Pattern, Mapping, J)) |
| => |
| -- The result is in the considered range of Source |
| |
| Index'Result in |
| (if Going = Forward then From else 1) |
| .. (if Going = Forward then Length (Source) else From) |
| - (Pattern'Length - 1) |
| |
| -- The slice beginning at the returned index matches Pattern |
| |
| and then Search.Match |
| (To_String (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 1 .. Length (Source) => |
| (if (if Going = Forward |
| then J in From .. Index'Result - 1 |
| else J - 1 in Index'Result |
| .. From - Pattern'Length) |
| then not (Search.Match |
| (To_String (Source), Pattern, Mapping, J)))), |
| |
| -- Otherwise, 0 is returned |
| |
| others |
| => |
| Index'Result = 0), |
| Global => null; |
| pragma Ada_05 (Index); |
| |
| function Index |
| (Source : Bounded_String; |
| Pattern : String; |
| From : Positive; |
| Going : Direction := Forward; |
| Mapping : Maps.Character_Mapping_Function) return Natural |
| with |
| Pre => |
| (if Length (Source) /= 0 then From <= Length (Source)) |
| and then Pattern'Length /= 0 |
| and then Mapping /= null, |
| Post => Index'Result <= Length (Source), |
| Contract_Cases => |
| |
| -- If Source is the empty string, then 0 is returned |
| |
| (Length (Source) = 0 |
| => |
| Index'Result = 0, |
| |
| -- If some slice of Source matches Pattern, then a valid index is |
| -- returned. |
| |
| Length (Source) > 0 |
| and then |
| (for some J in |
| (if Going = Forward then From else 1) |
| .. (if Going = Forward then Length (Source) else From) |
| - (Pattern'Length - 1) => |
| Search.Match (To_String (Source), Pattern, Mapping, J)) |
| => |
| -- The result is in the considered range of Source |
| |
| Index'Result in |
| (if Going = Forward then From else 1) |
| .. (if Going = Forward then Length (Source) else From) |
| - (Pattern'Length - 1) |
| |
| -- The slice beginning at the returned index matches Pattern |
| |
| and then Search.Match |
| (To_String (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 1 .. Length (Source) => |
| (if (if Going = Forward |
| then J in From .. Index'Result - 1 |
| else J - 1 in Index'Result |
| .. From - Pattern'Length) |
| then not (Search.Match |
| (To_String (Source), Pattern, Mapping, J)))), |
| |
| -- Otherwise, 0 is returned |
| |
| others |
| => |
| Index'Result = 0), |
| Global => null; |
| pragma Ada_05 (Index); |
| |
| function Index |
| (Source : Bounded_String; |
| Set : Maps.Character_Set; |
| From : Positive; |
| Test : Membership := Inside; |
| Going : Direction := Forward) return Natural |
| with |
| Pre => |
| (if Length (Source) /= 0 then From <= Length (Source)), |
| Post => Index'Result <= Length (Source), |
| 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. |
| |
| (Length (Source) = 0 |
| or else |
| (for all J in 1 .. Length (Source) => |
| (if J = From or else (J > From) = (Going = Forward) then |
| (Test = Inside) /= Maps.Is_In (Element (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 1 .. Length (Source) |
| 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) = |
| Maps.Is_In (Element (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 1 .. Length (Source) => |
| (if J /= Index'Result |
| and then (J < Index'Result) = (Going = Forward) |
| and then (J = From |
| or else (J > From) = (Going = Forward)) |
| then (Test = Inside) |
| /= Maps.Is_In (Element (Source, J), Set)))), |
| Global => null; |
| pragma Ada_05 (Index); |
| |
| function Index_Non_Blank |
| (Source : Bounded_String; |
| Going : Direction := Forward) return Natural |
| with |
| Post => Index_Non_Blank'Result <= Length (Source), |
| Contract_Cases => |
| |
| -- If all characters of Source are Space characters, then 0 is |
| -- returned. |
| |
| ((for all C of To_String (Source) => C = ' ') |
| => |
| Index_Non_Blank'Result = 0, |
| |
| -- Otherwise, an index in the range of Source is returned |
| |
| others |
| => |
| -- The result is in the range of Source |
| |
| Index_Non_Blank'Result in 1 .. Length (Source) |
| |
| -- The character at the returned index is not a Space character |
| |
| and then Element (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 1 .. Length (Source) => |
| (if J /= Index_Non_Blank'Result |
| and then |
| (J < Index_Non_Blank'Result) = (Going = Forward) |
| then Element (Source, J) = ' '))), |
| Global => null; |
| |
| function Index_Non_Blank |
| (Source : Bounded_String; |
| From : Positive; |
| Going : Direction := Forward) return Natural |
| with |
| Pre => |
| (if Length (Source) /= 0 then From <= Length (Source)), |
| Post => Index_Non_Blank'Result <= Length (Source), |
| Contract_Cases => |
| |
| -- If Source is the empty string, or all characters of the |
| -- considered slice of Source are Space characters, then 0 |
| -- is returned. |
| |
| (Length (Source) = 0 |
| or else |
| (for all J in 1 .. Length (Source) => |
| (if J = From or else (J > From) = (Going = Forward) then |
| Element (Source, J) = ' ')) |
| => |
| Index_Non_Blank'Result = 0, |
| |
| -- Otherwise, an index in the considered range of Source is |
| -- returned. |
| |
| others |
| => |
| -- The result is in the considered range of Source |
| |
| Index_Non_Blank'Result in 1 .. Length (Source) |
| 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 Element (Source, Index_Non_Blank'Result) /= ' ' |
| |
| -- The result is the smallest or largest index which isn't a |
| -- Space character, respectively when Going = Forward and Going |
| -- = Backward. |
| |
| and then |
| (for all J in 1 .. Length (Source) => |
| (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 Element (Source, J) = ' '))), |
| Global => null; |
| pragma Ada_05 (Index_Non_Blank); |
| |
| function Count |
| (Source : Bounded_String; |
| Pattern : String; |
| Mapping : Maps.Character_Mapping := Maps.Identity) return Natural |
| with |
| Pre => Pattern'Length /= 0, |
| Global => null; |
| |
| function Count |
| (Source : Bounded_String; |
| Pattern : String; |
| Mapping : Maps.Character_Mapping_Function) return Natural |
| with |
| Pre => Pattern'Length /= 0 and then Mapping /= null, |
| Global => null; |
| |
| function Count |
| (Source : Bounded_String; |
| Set : Maps.Character_Set) return Natural |
| with |
| Global => null; |
| |
| procedure Find_Token |
| (Source : Bounded_String; |
| Set : Maps.Character_Set; |
| From : Positive; |
| Test : Membership; |
| First : out Positive; |
| Last : out Natural) |
| with |
| Pre => |
| (if Length (Source) /= 0 then From <= Length (Source)), |
| 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. |
| |
| (Length (Source) = 0 |
| or else |
| (for all J in From .. Length (Source) => |
| (Test = Inside) /= Maps.Is_In (Element (Source, J), 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 .. Length (Source) |
| and then Last in First .. Length (Source) |
| |
| -- No character between From and First satisfies the property |
| -- Test on Set. |
| |
| and then |
| (for all J in From .. First - 1 => |
| (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)) |
| |
| -- All characters between First and Last satisfy the property |
| -- Test on Set. |
| |
| and then |
| (for all J in First .. Last => |
| (Test = Inside) = Maps.Is_In (Element (Source, J), 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 < Length (Source) |
| then |
| (Test = Inside) |
| /= Maps.Is_In (Element (Source, Last + 1), Set))), |
| Global => null; |
| pragma Ada_2012 (Find_Token); |
| |
| procedure Find_Token |
| (Source : Bounded_String; |
| Set : Maps.Character_Set; |
| Test : Membership; |
| First : out Positive; |
| Last : out Natural) |
| with |
| 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 1 and Last is set to 0. |
| |
| (Length (Source) = 0 |
| or else |
| (for all J in 1 .. Length (Source) => |
| (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)) |
| => |
| First = 1 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 1 .. Length (Source) |
| and then Last in First .. Length (Source) |
| |
| -- No character between 1 and First satisfies the property Test |
| -- on Set. |
| |
| and then |
| (for all J in 1 .. First - 1 => |
| (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)) |
| |
| -- All characters between First and Last satisfy the property |
| -- Test on Set. |
| |
| and then |
| (for all J in First .. Last => |
| (Test = Inside) = Maps.Is_In (Element (Source, J), 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 < Length (Source) |
| then |
| (Test = Inside) |
| /= Maps.Is_In (Element (Source, Last + 1), Set))), |
| Global => null; |
| |
| ------------------------------------ |
| -- String Translation Subprograms -- |
| ------------------------------------ |
| |
| -- Each of the Translate subprograms, when applied to a Bounded_String, |
| -- has an analogous effect to the corresponding subprogram in |
| -- Strings.Fixed. For the Translate function, the translation is applied |
| -- to the string represented by the Bounded_String parameter, and the |
| -- result is converted (via To_Bounded_String) to a Bounded_String. For |
| -- the Translate procedure, the string represented by the Bounded_String |
| -- parameter after the translation is given by the Translate function |
| -- for fixed-length strings applied to the string represented by the |
| -- original value of the parameter. |
| |
| function Translate |
| (Source : Bounded_String; |
| Mapping : Maps.Character_Mapping) return Bounded_String |
| with |
| Post => Length (Translate'Result) = Length (Source) |
| and then |
| (for all K in 1 .. Length (Source) => |
| Element (Translate'Result, K) = |
| Ada.Strings.Maps.Value (Mapping, Element (Source, K))), |
| Global => null; |
| |
| procedure Translate |
| (Source : in out Bounded_String; |
| Mapping : Maps.Character_Mapping) |
| with |
| Post => Length (Source) = Length (Source'Old) |
| and then |
| (for all K in 1 .. Length (Source) => |
| Element (Source, K) = |
| Ada.Strings.Maps.Value (Mapping, Element (Source'Old, K))), |
| Global => null; |
| |
| function Translate |
| (Source : Bounded_String; |
| Mapping : Maps.Character_Mapping_Function) return Bounded_String |
| with |
| Pre => Mapping /= null, |
| Post => Length (Translate'Result) = Length (Source) |
| and then |
| (for all K in 1 .. Length (Source) => |
| Element (Translate'Result, K) = Mapping (Element (Source, K))), |
| Global => null; |
| |
| procedure Translate |
| (Source : in out Bounded_String; |
| Mapping : Maps.Character_Mapping_Function) |
| with |
| Pre => Mapping /= null, |
| Post => Length (Source) = Length (Source'Old) |
| and then |
| (for all K in 1 .. Length (Source) => |
| Element (Source, K) = Mapping (Element (Source'Old, K))), |
| Global => null; |
| |
| --------------------------------------- |
| -- String Transformation Subprograms -- |
| --------------------------------------- |
| |
| -- Each of the transformation subprograms (Replace_Slice, Insert, |
| -- Overwrite, Delete), selector subprograms (Trim, Head, Tail), and |
| -- constructor functions ("*") has an effect based on its corresponding |
| -- subprogram in Strings.Fixed, and Replicate is based on Fixed."*". |
| -- In the case of a function, the corresponding fixed-length string |
| -- subprogram is applied to the string represented by the Bounded_String |
| -- parameter. To_Bounded_String is applied the result string, with Drop |
| -- (or Error in the case of Generic_Bounded_Length."*") determining |
| -- the effect when the string length exceeds Max_Length. In |
| -- the case of a procedure, the corresponding function in |
| -- Strings.Bounded.Generic_Bounded_Length is applied, with the |
| -- result assigned into the Source parameter. |
| |
| function Replace_Slice |
| (Source : Bounded_String; |
| Low : Positive; |
| High : Natural; |
| By : String; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => |
| Low - 1 <= Length (Source) |
| and then |
| (if Drop = Error |
| then (if High >= Low |
| then Low - 1 |
| <= Max_Length - By'Length |
| - Integer'Max (Length (Source) - High, 0) |
| else Length (Source) <= Max_Length - By'Length)), |
| Contract_Cases => |
| (Low - 1 <= Max_Length - By'Length |
| - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0) |
| => |
| -- Total length is lower than Max_Length: nothing is dropped |
| |
| -- Note that if High < Low, the insertion is done before Low, |
| -- so in all cases the starting position of the slice of Source |
| -- remaining after the replaced Slice is Integer'Max (High + 1, |
| -- Low). |
| |
| Length (Replace_Slice'Result) = Low - 1 + By'Length |
| + Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0) |
| and then |
| Slice (Replace_Slice'Result, 1, Low - 1) = |
| Slice (Source, 1, Low - 1) |
| and then |
| Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By |
| and then |
| (if Integer'Max (High, Low - 1) < Length (Source) then |
| Slice (Replace_Slice'Result, |
| Low + By'Length, Length (Replace_Slice'Result)) = |
| Slice (Source, |
| Integer'Max (High + 1, Low), Length (Source))), |
| |
| Low - 1 > Max_Length - By'Length |
| - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0) |
| and then Drop = Left |
| => |
| -- Final_Slice is the length of the slice of Source remaining |
| -- after the replaced part. |
| (declare |
| Final_Slice : constant Natural := |
| Integer'Max |
| (Length (Source) - Integer'Max (High, Low - 1), 0); |
| begin |
| -- The result is of maximal length and ends by the last |
| -- Final_Slice characters of Source. |
| |
| Length (Replace_Slice'Result) = Max_Length |
| and then |
| (if Final_Slice > 0 then |
| Slice (Replace_Slice'Result, |
| Max_Length - Final_Slice + 1, Max_Length) = |
| Slice (Source, |
| Integer'Max (High + 1, Low), Length (Source))) |
| |
| -- Depending on when we reach Max_Length, either the first |
| -- part of Source is fully dropped and By is partly dropped, |
| -- or By is fully added and the first part of Source is |
| -- partly dropped. |
| |
| and then |
| (if Max_Length - Final_Slice - By'Length <= 0 then |
| |
| -- The first (possibly zero) characters of By are |
| -- dropped. |
| |
| (if Final_Slice < Max_Length then |
| Slice (Replace_Slice'Result, |
| 1, Max_Length - Final_Slice) = |
| By (By'Last - Max_Length + Final_Slice + 1 |
| .. By'Last)) |
| |
| else -- By is added to the result |
| |
| Slice (Replace_Slice'Result, |
| Max_Length - Final_Slice - By'Length + 1, |
| Max_Length - Final_Slice) = |
| By |
| |
| -- The first characters of Source (1 .. Low - 1) are |
| -- dropped. |
| |
| and then Slice (Replace_Slice'Result, 1, |
| Max_Length - Final_Slice - By'Length) = |
| Slice (Source, |
| Low - Max_Length + Final_Slice + By'Length, |
| Low - 1))), |
| |
| others -- Drop = Right |
| => |
| -- The result is of maximal length and starts by the first Low - |
| -- 1 characters of Source. |
| |
| Length (Replace_Slice'Result) = Max_Length |
| and then |
| Slice (Replace_Slice'Result, 1, Low - 1) = |
| Slice (Source, 1, Low - 1) |
| |
| -- Depending on when we reach Max_Length, either the last part |
| -- of Source is fully dropped and By is partly dropped, or By |
| -- is fully added and the last part of Source is partly |
| -- dropped. |
| |
| and then |
| (if Low - 1 >= Max_Length - By'Length then |
| |
| -- The last characters of By are dropped |
| |
| Slice (Replace_Slice'Result, Low, Max_Length) = |
| By (By'First .. Max_Length - Low + By'First) |
| |
| else -- By is fully added |
| |
| Slice (Replace_Slice'Result, Low, Low + By'Length - 1) = By |
| |
| -- Then Source starting from Integer'Max (High + 1, Low) |
| -- is added but the last characters are dropped. |
| |
| and then Slice (Replace_Slice'Result, |
| Low + By'Length, Max_Length) = |
| Slice (Source, Integer'Max (High + 1, Low), |
| Integer'Max (High + 1, Low) + |
| (Max_Length - Low - By'Length)))); |
| |
| procedure Replace_Slice |
| (Source : in out Bounded_String; |
| Low : Positive; |
| High : Natural; |
| By : String; |
| Drop : Truncation := Error) |
| with |
| Pre => |
| Low - 1 <= Length (Source) |
| and then |
| (if Drop = Error |
| then (if High >= Low |
| then Low - 1 |
| <= Max_Length - By'Length |
| - Natural'Max (Length (Source) - High, 0) |
| else Length (Source) <= Max_Length - By'Length)), |
| Contract_Cases => |
| (Low - 1 <= Max_Length - By'Length |
| - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0) |
| => |
| -- Total length is lower than Max_Length: nothing is dropped |
| |
| -- Note that if High < Low, the insertion is done before Low, |
| -- so in all cases the starting position of the slice of Source |
| -- remaining after the replaced Slice is Integer'Max (High + 1, |
| -- Low). |
| |
| Length (Source) = Low - 1 + By'Length + Integer'Max |
| (Length (Source'Old) - Integer'Max (High, Low - 1), 0) |
| and then |
| Slice (Source, 1, Low - 1) = Slice (Source'Old, 1, Low - 1) |
| and then Slice (Source, Low, Low - 1 + By'Length) = By |
| and then |
| (if Integer'Max (High, Low - 1) < Length (Source'Old) then |
| Slice (Source, Low + By'Length, Length (Source)) = |
| Slice (Source'Old, |
| Integer'Max (High + 1, Low), Length (Source'Old))), |
| |
| Low - 1 > Max_Length - By'Length |
| - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0) |
| and then Drop = Left |
| => |
| -- Final_Slice is the length of the slice of Source remaining |
| -- after the replaced part. |
| (declare |
| Final_Slice : constant Integer := |
| Integer'Max (0, |
| Length (Source'Old) - Integer'Max (High, Low - 1)); |
| begin |
| -- The result is of maximal length and ends by the last |
| -- Final_Slice characters of Source. |
| |
| Length (Source) = Max_Length |
| and then |
| (if Final_Slice > 0 then |
| Slice (Source, |
| Max_Length - Final_Slice + 1, Max_Length) = |
| Slice (Source'Old, |
| Integer'Max (High + 1, Low), Length (Source'Old))) |
| |
| -- Depending on when we reach Max_Length, either the first |
| -- part of Source is fully dropped and By is partly dropped, |
| -- or By is fully added and the first part of Source is |
| -- partly dropped. |
| |
| and then |
| (if Max_Length - Final_Slice - By'Length <= 0 then |
| |
| -- The first characters of By are dropped |
| |
| (if Final_Slice < Max_Length then |
| Slice (Source, 1, Max_Length - Final_Slice) = |
| By (By'Last - Max_Length + Final_Slice + 1 |
| .. By'Last)) |
| |
| else -- By is added to the result |
| |
| Slice (Source, |
| Max_Length - Final_Slice - By'Length + 1, |
| Max_Length - Final_Slice) = By |
| |
| -- The first characters of Source (1 .. Low - 1) are |
| -- dropped. |
| |
| and then Slice (Source, 1, |
| Max_Length - Final_Slice - By'Length) = |
| Slice (Source'Old, |
| Low - Max_Length + Final_Slice + By'Length, |
| Low - 1))), |
| |
| others -- Drop = Right |
| => |
| -- The result is of maximal length and starts by the first Low - |
| -- 1 characters of Source. |
| |
| Length (Source) = Max_Length |
| and then |
| Slice (Source, 1, Low - 1) = Slice (Source'Old, 1, Low - 1) |
| |
| -- Depending on when we reach Max_Length, either the last part |
| -- of Source is fully dropped and By is partly dropped, or By |
| -- is fully added and the last part of Source is partly |
| -- dropped. |
| |
| and then |
| (if Low - 1 >= Max_Length - By'Length then |
| |
| -- The last characters of By are dropped |
| |
| Slice (Source, Low, Max_Length) = |
| By (By'First .. Max_Length - Low + By'First) |
| |
| else -- By is fully added |
| |
| Slice (Source, Low, Low + By'Length - 1) = By |
| |
| -- Then Source starting from Natural'Max (High + 1, Low) |
| -- is added but the last characters are dropped. |
| |
| and then Slice (Source, Low + By'Length, Max_Length) = |
| Slice (Source'Old, Integer'Max (High + 1, Low), |
| Integer'Max (High + 1, Low) + |
| (Max_Length - Low - By'Length)))); |
| |
| function Insert |
| (Source : Bounded_String; |
| Before : Positive; |
| New_Item : String; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => |
| Before - 1 <= Length (Source) |
| and then (if New_Item'Length > Max_Length - Length (Source) |
| then Drop /= Error), |
| Contract_Cases => |
| (Length (Source) <= Max_Length - New_Item'Length |
| => |
| -- Total length is lower than Max_Length: nothing is dropped |
| |
| Length (Insert'Result) = Length (Source) + New_Item'Length |
| and then |
| Slice (Insert'Result, 1, Before - 1) = |
| Slice (Source, 1, Before - 1) |
| and then |
| Slice (Insert'Result, Before, Before - 1 + New_Item'Length) = |
| New_Item |
| and then |
| (if Before <= Length (Source) then |
| Slice (Insert'Result, |
| Before + New_Item'Length, Length (Insert'Result)) = |
| Slice (Source, Before, Length (Source))), |
| |
| Length (Source) > Max_Length - New_Item'Length and then Drop = Left |
| => |
| -- The result is of maximal length and ends by the last |
| -- characters of Source. |
| |
| Length (Insert'Result) = Max_Length |
| and then |
| (if Before <= Length (Source) then |
| Slice (Insert'Result, |
| Max_Length - Length (Source) + Before, Max_Length) = |
| Slice (Source, Before, Length (Source))) |
| |
| -- Depending on when we reach Max_Length, either the first part |
| -- of Source is fully dropped and New_Item is partly dropped, |
| -- or New_Item is fully added and the first part of Source is |
| -- partly dropped. |
| |
| and then |
| (if Max_Length - Length (Source) - 1 + Before |
| < New_Item'Length |
| then |
| -- The first characters of New_Item are dropped |
| |
| (if Length (Source) - Before + 1 < Max_Length then |
| Slice (Insert'Result, |
| 1, Max_Length - Length (Source) - 1 + Before) = |
| New_Item |
| (New_Item'Last - Max_Length + Length (Source) |
| - Before + 2 |
| .. New_Item'Last)) |
| |
| else -- New_Item is added to the result |
| |
| Slice (Insert'Result, |
| Max_Length - Length (Source) - New_Item'Length + Before, |
| Max_Length - Length (Source) - 1 + Before) = New_Item |
| |
| -- The first characters of Source (1 .. Before - 1) are |
| -- dropped. |
| |
| and then Slice (Insert'Result, |
| 1, Max_Length - Length (Source) - New_Item'Length |
| - 1 + Before) = |
| Slice (Source, |
| Length (Source) - Max_Length + New_Item'Length |
| + 1, |
| Before - 1)), |
| |
| others -- Drop = Right |
| => |
| -- The result is of maximal length and starts by the first |
| -- characters of Source. |
| |
| Length (Insert'Result) = Max_Length |
| and then |
| Slice (Insert'Result, 1, Before - 1) = |
| Slice (Source, 1, Before - 1) |
| |
| -- Depending on when we reach Max_Length, either the last part |
| -- of Source is fully dropped and New_Item is partly dropped, |
| -- or New_Item is fully added and the last part of Source is |
| -- partly dropped. |
| |
| and then |
| (if Before - 1 >= Max_Length - New_Item'Length then |
| |
| -- The last characters of New_Item are dropped |
| |
| Slice (Insert'Result, Before, Max_Length) = |
| New_Item (New_Item'First |
| .. Max_Length - Before + New_Item'First) |
| |
| else -- New_Item is fully added |
| |
| Slice (Insert'Result, |
| Before, Before + New_Item'Length - 1) = |
| New_Item |
| |
| -- Then Source starting from Before is added but the |
| -- last characters are dropped. |
| |
| and then Slice (Insert'Result, |
| Before + New_Item'Length, Max_Length) = |
| Slice (Source, |
| Before, Max_Length - New_Item'Length))); |
| |
| procedure Insert |
| (Source : in out Bounded_String; |
| Before : Positive; |
| New_Item : String; |
| Drop : Truncation := Error) |
| with |
| Pre => |
| Before - 1 <= Length (Source) |
| and then (if New_Item'Length > Max_Length - Length (Source) |
| then Drop /= Error), |
| Contract_Cases => |
| (Length (Source) <= Max_Length - New_Item'Length |
| => |
| -- Total length is lower than Max_Length: nothing is dropped |
| |
| Length (Source) = Length (Source'Old) + New_Item'Length |
| and then |
| Slice (Source, 1, Before - 1) = |
| Slice (Source'Old, 1, Before - 1) |
| and then |
| Slice (Source, Before, Before - 1 + New_Item'Length) = |
| New_Item |
| and then |
| (if Before <= Length (Source'Old) then |
| Slice (Source, Before + New_Item'Length, Length (Source)) = |
| Slice (Source'Old, Before, Length (Source'Old))), |
| |
| Length (Source) > Max_Length - New_Item'Length and then Drop = Left |
| => |
| -- The result is of maximal length and ends by the last |
| -- characters of Source. |
| |
| Length (Source) = Max_Length |
| and then |
| (if Before <= Length (Source'Old) then |
| Slice (Source, |
| Max_Length - Length (Source'Old) + Before, Max_Length) = |
| Slice (Source'Old, Before, Length (Source'Old))) |
| |
| -- Depending on when we reach Max_Length, either the first part |
| -- of Source is fully dropped and New_Item is partly dropped, |
| -- or New_Item is fully added and the first part of Source is |
| -- partly dropped. |
| |
| and then |
| (if Max_Length - Length (Source'Old) - 1 + Before |
| < New_Item'Length |
| then |
| -- The first characters of New_Item are dropped |
| |
| (if Length (Source'Old) - Before + 1 < Max_Length then |
| Slice (Source, |
| 1, Max_Length - Length (Source'Old) - 1 + Before) = |
| New_Item |
| (New_Item'Last - Max_Length + Length (Source'Old) |
| - Before + 2 |
| .. New_Item'Last)) |
| |
| else -- New_Item is added to the result |
| |
| Slice (Source, |
| Max_Length - Length (Source'Old) - New_Item'Length |
| + Before, |
| Max_Length - Length (Source'Old) - 1 + Before) = New_Item |
| |
| -- The first characters of Source (1 .. Before - 1) are |
| -- dropped. |
| |
| and then Slice (Source, 1, |
| Max_Length - Length (Source'Old) - New_Item'Length |
| - 1 + Before) = |
| Slice (Source'Old, |
| Length (Source'Old) |
| - Max_Length + New_Item'Length + 1, |
| Before - 1)), |
| |
| others -- Drop = Right |
| => |
| -- The result is of maximal length and starts by the first |
| -- characters of Source. |
| |
| Length (Source) = Max_Length |
| and then |
| Slice (Source, 1, Before - 1) = |
| Slice (Source'Old, 1, Before - 1) |
| |
| -- Depending on when we reach Max_Length, either the last part |
| -- of Source is fully dropped and New_Item is partly dropped, |
| -- or New_Item is fully added and the last part of Source is |
| -- partly dropped. |
| |
| and then |
| (if Before - 1 >= Max_Length - New_Item'Length then |
| |
| -- The last characters of New_Item are dropped |
| |
| Slice (Source, Before, Max_Length) = |
| New_Item (New_Item'First |
| .. Max_Length - Before + New_Item'First) |
| |
| else -- New_Item is fully added |
| |
| Slice (Source, Before, Before + New_Item'Length - 1) = |
| New_Item |
| |
| -- Then Source starting from Before is added but the |
| -- last characters are dropped. |
| |
| and then |
| Slice (Source, Before + New_Item'Length, Max_Length) = |
| Slice (Source'Old, |
| Before, Max_Length - New_Item'Length))); |
| |
| function Overwrite |
| (Source : Bounded_String; |
| Position : Positive; |
| New_Item : String; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => |
| Position - 1 <= Length (Source) |
| and then (if New_Item'Length > Max_Length - (Position - 1) |
| then Drop /= Error), |
| Contract_Cases => |
| (Position - 1 <= Max_Length - New_Item'Length |
| => |
| -- The length is unchanged, unless New_Item overwrites further |
| -- than the end of Source. In this contract case, we suppose |
| -- New_Item doesn't overwrite further than Max_Length. |
| |
| Length (Overwrite'Result) = |
| Integer'Max (Length (Source), Position - 1 + New_Item'Length) |
| and then |
| Slice (Overwrite'Result, 1, Position - 1) = |
| Slice (Source, 1, Position - 1) |
| and then Slice (Overwrite'Result, |
| Position, Position - 1 + New_Item'Length) = |
| New_Item |
| and then |
| (if Position - 1 + New_Item'Length < Length (Source) then |
| |
| -- There are some unchanged characters of Source remaining |
| -- after New_Item. |
| |
| Slice (Overwrite'Result, |
| Position + New_Item'Length, Length (Source)) = |
| Slice (Source, |
| Position + New_Item'Length, Length (Source))), |
| |
| Position - 1 > Max_Length - New_Item'Length and then Drop = Left |
| => |
| Length (Overwrite'Result) = Max_Length |
| |
| -- If a part of the result has to be dropped, it means New_Item |
| -- is overwriting further than the end of Source. Thus the |
| -- result is necessarily ending by New_Item. However, we don't |
| -- know whether New_Item covers all Max_Length characters or |
| -- some characters of Source are remaining at the left. |
| |
| and then |
| (if New_Item'Length > Max_Length then |
| |
| -- New_Item covers all Max_Length characters |
| |
| To_String (Overwrite'Result) = |
| New_Item |
| (New_Item'Last - Max_Length + 1 .. New_Item'Last) |
| else |
| -- New_Item fully appears at the end |
| |
| Slice (Overwrite'Result, |
| Max_Length - New_Item'Length + 1, Max_Length) = |
| New_Item |
| |
| -- The left of Source is cut |
| |
| and then |
| Slice (Overwrite'Result, |
| 1, Max_Length - New_Item'Length) = |
| Slice (Source, |
| Position - Max_Length + New_Item'Length, |
| Position - 1)), |
| |
| others -- Drop = Right |
| => |
| -- The result is of maximal length and starts by the first |
| -- characters of Source. |
| |
| Length (Overwrite'Result) = Max_Length |
| and then |
| Slice (Overwrite'Result, 1, Position - 1) = |
| Slice (Source, 1, Position - 1) |
| |
| -- Then New_Item is written until Max_Length |
| |
| and then Slice (Overwrite'Result, Position, Max_Length) = |
| New_Item |
| (New_Item'First .. Max_Length - Position + New_Item'First)); |
| |
| procedure Overwrite |
| (Source : in out Bounded_String; |
| Position : Positive; |
| New_Item : String; |
| Drop : Truncation := Error) |
| with |
| Pre => |
| Position - 1 <= Length (Source) |
| and then (if New_Item'Length > Max_Length - (Position - 1) |
| then Drop /= Error), |
| Contract_Cases => |
| (Position - 1 <= Max_Length - New_Item'Length |
| => |
| -- The length of Source is unchanged, unless New_Item overwrites |
| -- further than the end of Source. In this contract case, we |
| -- suppose New_Item doesn't overwrite further than Max_Length. |
| |
| Length (Source) = Integer'Max |
| (Length (Source'Old), Position - 1 + New_Item'Length) |
| and then |
| Slice (Source, 1, Position - 1) = |
| Slice (Source'Old, 1, Position - 1) |
| and then Slice (Source, |
| Position, Position - 1 + New_Item'Length) = |
| New_Item |
| and then |
| (if Position - 1 + New_Item'Length < Length (Source'Old) then |
| |
| -- There are some unchanged characters of Source remaining |
| -- after New_Item. |
| |
| Slice (Source, |
| Position + New_Item'Length, Length (Source'Old)) = |
| Slice (Source'Old, |
| Position + New_Item'Length, Length (Source'Old))), |
| |
| Position - 1 > Max_Length - New_Item'Length and then Drop = Left |
| => |
| Length (Source) = Max_Length |
| |
| -- If a part of the result has to be dropped, it means New_Item |
| -- is overwriting further than the end of Source. Thus the |
| -- result is necessarily ending by New_Item. However, we don't |
| -- know whether New_Item covers all Max_Length characters or |
| -- some characters of Source are remaining at the left. |
| |
| and then |
| (if New_Item'Length > Max_Length then |
| |
| -- New_Item covers all Max_Length characters |
| |
| To_String (Source) = |
| New_Item |
| (New_Item'Last - Max_Length + 1 .. New_Item'Last) |
| else |
| -- New_Item fully appears at the end |
| |
| Slice (Source, |
| Max_Length - New_Item'Length + 1, Max_Length) = |
| New_Item |
| |
| -- The left of Source is cut |
| |
| and then |
| Slice (Source, 1, Max_Length - New_Item'Length) = |
| Slice (Source'Old, |
| Position - Max_Length + New_Item'Length, |
| Position - 1)), |
| |
| others -- Drop = Right |
| => |
| -- The result is of maximal length and starts by the first |
| -- characters of Source. |
| |
| Length (Source) = Max_Length |
| and then |
| Slice (Source, 1, Position - 1) = |
| Slice (Source'Old, 1, Position - 1) |
| |
| -- New_Item is written until Max_Length |
| |
| and then Slice (Source, Position, Max_Length) = |
| New_Item |
| (New_Item'First .. Max_Length - Position + New_Item'First)); |
| |
| function Delete |
| (Source : Bounded_String; |
| From : Positive; |
| Through : Natural) return Bounded_String |
| with |
| Pre => |
| (if Through >= From then From - 1 <= Length (Source)), |
| Contract_Cases => |
| (Through >= From => |
| Length (Delete'Result) = |
| From - 1 + Natural'Max (Length (Source) - Through, 0) |
| and then |
| Slice (Delete'Result, 1, From - 1) = |
| Slice (Source, 1, From - 1) |
| and then |
| (if Through < Length (Source) then |
| Slice (Delete'Result, From, Length (Delete'Result)) = |
| Slice (Source, Through + 1, Length (Source))), |
| others => |
| Delete'Result = Source), |
| Global => null; |
| |
| procedure Delete |
| (Source : in out Bounded_String; |
| From : Positive; |
| Through : Natural) |
| with |
| Pre => |
| (if Through >= From then From - 1 <= Length (Source)), |
| Contract_Cases => |
| (Through >= From => |
| Length (Source) = |
| From - 1 + Natural'Max (Length (Source'Old) - Through, 0) |
| and then |
| Slice (Source, 1, From - 1) = Slice (Source'Old, 1, From - 1) |
| and then |
| (if Through < Length (Source) then |
| Slice (Source, From, Length (Source)) = |
| Slice (Source'Old, Through + 1, Length (Source'Old))), |
| others => |
| Source = Source'Old), |
| Global => null; |
| |
| --------------------------------- |
| -- String Selector Subprograms -- |
| --------------------------------- |
| |
| function Trim |
| (Source : Bounded_String; |
| Side : Trim_End) return Bounded_String |
| with |
| Contract_Cases => |
| -- If all characters in Source are Space, the returned string is |
| -- empty. |
| |
| ((for all C of To_String (Source) => C = ' ') |
| => |
| Length (Trim'Result) = 0, |
| |
| -- Otherwise, the returned string is a slice of Source |
| |
| others |
| => |
| (declare |
| Low : constant Positive := |
| (if Side = Right then 1 |
| else Index_Non_Blank (Source, Forward)); |
| High : constant Positive := |
| (if Side = Left then Length (Source) |
| else Index_Non_Blank (Source, Backward)); |
| begin |
| To_String (Trim'Result) = Slice (Source, Low, High))), |
| Global => null; |
| |
| procedure Trim |
| (Source : in out Bounded_String; |
| Side : Trim_End) |
| with |
| Contract_Cases => |
| -- If all characters in Source are Space, the returned string is |
| -- empty. |
| |
| ((for all C of To_String (Source) => C = ' ') |
| => |
| Length (Source) = 0, |
| |
| -- Otherwise, the returned string is a slice of Source |
| |
| others |
| => |
| (declare |
| Low : constant Positive := |
| (if Side = Right then 1 |
| else Index_Non_Blank (Source'Old, Forward)); |
| High : constant Positive := |
| (if Side = Left then Length (Source'Old) |
| else Index_Non_Blank (Source'Old, Backward)); |
| begin |
| To_String (Source) = Slice (Source'Old, Low, High))), |
| Global => null; |
| |
| function Trim |
| (Source : Bounded_String; |
| Left : Maps.Character_Set; |
| Right : Maps.Character_Set) return Bounded_String |
| with |
| Contract_Cases => |
| -- If all characters in Source are contained in one of the sets Left |
| -- or Right, then the returned string is empty. |
| |
| ((for all C of To_String (Source) => Maps.Is_In (C, Left)) |
| or else |
| (for all C of To_String (Source) => Maps.Is_In (C, Right)) |
| => |
| Length (Trim'Result) = 0, |
| |
| -- Otherwise, the returned string is a slice of Source |
| |
| others |
| => |
| (declare |
| Low : constant Positive := |
| Index (Source, Left, Outside, Forward); |
| High : constant Positive := |
| Index (Source, Right, Outside, Backward); |
| begin |
| To_String (Trim'Result) = Slice (Source, Low, High))), |
| Global => null; |
| |
| procedure Trim |
| (Source : in out Bounded_String; |
| Left : Maps.Character_Set; |
| Right : Maps.Character_Set) |
| with |
| Contract_Cases => |
| -- If all characters in Source are contained in one of the sets Left |
| -- or Right, then the returned string is empty. |
| |
| ((for all C of To_String (Source) => Maps.Is_In (C, Left)) |
| or else |
| (for all C of To_String (Source) => Maps.Is_In (C, Right)) |
| => |
| Length (Source) = 0, |
| |
| -- Otherwise, the returned string is a slice of Source |
| |
| others |
| => |
| (declare |
| Low : constant Positive := |
| Index (Source'Old, Left, Outside, Forward); |
| High : constant Positive := |
| Index (Source'Old, Right, Outside, Backward); |
| begin |
| To_String (Source) = Slice (Source'Old, Low, High))), |
| Global => null; |
| |
| function Head |
| (Source : Bounded_String; |
| Count : Natural; |
| Pad : Character := Space; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => (if Count > Max_Length then Drop /= Error), |
| Contract_Cases => |
| (Count <= Length (Source) |
| => |
| -- Source is cut |
| |
| To_String (Head'Result) = Slice (Source, 1, Count), |
| |
| Count > Length (Source) and then Count <= Max_Length |
| => |
| -- Source is followed by Pad characters |
| |
| Length (Head'Result) = Count |
| and then |
| Slice (Head'Result, 1, Length (Source)) = To_String (Source) |
| and then |
| Slice (Head'Result, Length (Source) + 1, Count) = |
| [1 .. Count - Length (Source) => Pad], |
| |
| Count > Max_Length and then Drop = Right |
| => |
| -- Source is followed by Pad characters |
| |
| Length (Head'Result) = Max_Length |
| and then |
| Slice (Head'Result, 1, Length (Source)) = To_String (Source) |
| and then |
| Slice (Head'Result, Length (Source) + 1, Max_Length) = |
| [1 .. Max_Length - Length (Source) => Pad], |
| |
| Count - Length (Source) > Max_Length and then Drop = Left |
| => |
| -- Source is fully dropped at the left |
| |
| To_String (Head'Result) = [1 .. Max_Length => Pad], |
| |
| others |
| => |
| -- Source is partly dropped at the left |
| |
| Length (Head'Result) = Max_Length |
| and then |
| Slice (Head'Result, 1, Max_Length - Count + Length (Source)) = |
| Slice (Source, Count - Max_Length + 1, Length (Source)) |
| and then |
| Slice (Head'Result, |
| Max_Length - Count + Length (Source) + 1, Max_Length) = |
| [1 .. Count - Length (Source) => Pad]); |
| |
| procedure Head |
| (Source : in out Bounded_String; |
| Count : Natural; |
| Pad : Character := Space; |
| Drop : Truncation := Error) |
| with |
| Pre => (if Count > Max_Length then Drop /= Error), |
| Contract_Cases => |
| (Count <= Length (Source) |
| => |
| -- Source is cut |
| |
| To_String (Source) = Slice (Source'Old, 1, Count), |
| |
| Count > Length (Source) and then Count <= Max_Length |
| => |
| -- Source is followed by Pad characters |
| |
| Length (Source) = Count |
| and then |
| Slice (Source, 1, Length (Source'Old)) = |
| To_String (Source'Old) |
| and then |
| Slice (Source, Length (Source'Old) + 1, Count) = |
| [1 .. Count - Length (Source'Old) => Pad], |
| |
| Count > Max_Length and then Drop = Right |
| => |
| -- Source is followed by Pad characters |
| |
| Length (Source) = Max_Length |
| and then |
| Slice (Source, 1, Length (Source'Old)) = |
| To_String (Source'Old) |
| and then |
| Slice (Source, Length (Source'Old) + 1, Max_Length) = |
| [1 .. Max_Length - Length (Source'Old) => Pad], |
| |
| Count - Length (Source) > Max_Length and then Drop = Left |
| => |
| -- Source is fully dropped on the left |
| |
| To_String (Source) = [1 .. Max_Length => Pad], |
| |
| others |
| => |
| -- Source is partly dropped on the left |
| |
| Length (Source) = Max_Length |
| and then |
| Slice (Source, 1, Max_Length - Count + Length (Source'Old)) = |
| Slice (Source'Old, |
| Count - Max_Length + 1, Length (Source'Old)) |
| and then |
| Slice (Source, |
| Max_Length - Count + Length (Source'Old) + 1, Max_Length) = |
| [1 .. Count - Length (Source'Old) => Pad]); |
| |
| function Tail |
| (Source : Bounded_String; |
| Count : Natural; |
| Pad : Character := Space; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => (if Count > Max_Length then Drop /= Error), |
| Contract_Cases => |
| (Count < Length (Source) |
| => |
| -- Source is cut |
| |
| (if Count > 0 then |
| To_String (Tail'Result) = |
| Slice (Source, Length (Source) - Count + 1, Length (Source)) |
| else Length (Tail'Result) = 0), |
| |
| Count >= Length (Source) and then Count < Max_Length |
| => |
| -- Source is preceded by Pad characters |
| |
| Length (Tail'Result) = Count |
| and then |
| Slice (Tail'Result, 1, Count - Length (Source)) = |
| [1 .. Count - Length (Source) => Pad] |
| and then |
| Slice (Tail'Result, Count - Length (Source) + 1, Count) = |
| To_String (Source), |
| |
| Count >= Max_Length and then Drop = Left |
| => |
| -- Source is preceded by Pad characters |
| |
| Length (Tail'Result) = Max_Length |
| and then |
| Slice (Tail'Result, 1, Max_Length - Length (Source)) = |
| [1 .. Max_Length - Length (Source) => Pad] |
| and then |
| (if Length (Source) > 0 then |
| Slice (Tail'Result, |
| Max_Length - Length (Source) + 1, Max_Length) = |
| To_String (Source)), |
| |
| Count - Length (Source) >= Max_Length and then Drop /= Left |
| => |
| -- Source is fully dropped on the right |
| |
| To_String (Tail'Result) = [1 .. Max_Length => Pad], |
| |
| others |
| => |
| -- Source is partly dropped on the right |
| |
| Length (Tail'Result) = Max_Length |
| and then |
| Slice (Tail'Result, 1, Count - Length (Source)) = |
| [1 .. Count - Length (Source) => Pad] |
| and then |
| Slice (Tail'Result, Count - Length (Source) + 1, Max_Length) = |
| Slice (Source, 1, Max_Length - Count + Length (Source))); |
| |
| procedure Tail |
| (Source : in out Bounded_String; |
| Count : Natural; |
| Pad : Character := Space; |
| Drop : Truncation := Error) |
| with |
| Pre => (if Count > Max_Length then Drop /= Error), |
| Contract_Cases => |
| (Count < Length (Source) |
| => |
| -- Source is cut |
| |
| (if Count > 0 then |
| To_String (Source) = |
| Slice (Source'Old, |
| Length (Source'Old) - Count + 1, Length (Source'Old)) |
| else Length (Source) = 0), |
| |
| Count >= Length (Source) and then Count < Max_Length |
| => |
| -- Source is preceded by Pad characters |
| |
| Length (Source) = Count |
| and then |
| Slice (Source, 1, Count - Length (Source'Old)) = |
| [1 .. Count - Length (Source'Old) => Pad] |
| and then |
| Slice (Source, Count - Length (Source'Old) + 1, Count) = |
| To_String (Source'Old), |
| |
| Count >= Max_Length and then Drop = Left |
| => |
| -- Source is preceded by Pad characters |
| |
| Length (Source) = Max_Length |
| and then |
| Slice (Source, 1, Max_Length - Length (Source'Old)) = |
| [1 .. Max_Length - Length (Source'Old) => Pad] |
| and then |
| (if Length (Source'Old) > 0 then |
| Slice (Source, |
| Max_Length - Length (Source'Old) + 1, Max_Length) = |
| To_String (Source'Old)), |
| |
| Count - Length (Source) >= Max_Length and then Drop /= Left |
| => |
| -- Source is fully dropped at the right |
| |
| To_String (Source) = [1 .. Max_Length => Pad], |
| |
| others |
| => |
| -- Source is partly dropped at the right |
| |
| Length (Source) = Max_Length |
| and then |
| Slice (Source, 1, Count - Length (Source'Old)) = |
| [1 .. Count - Length (Source'Old) => Pad] |
| and then |
| Slice (Source, Count - Length (Source'Old) + 1, Max_Length) = |
| Slice (Source'Old, |
| 1, Max_Length - Count + Length (Source'Old))); |
| |
| ------------------------------------ |
| -- String Constructor Subprograms -- |
| ------------------------------------ |
| |
| function "*" |
| (Left : Natural; |
| Right : Character) return Bounded_String |
| with |
| Pre => Left <= Max_Length, |
| Post => To_String ("*"'Result) = [1 .. Left => Right]; |
| |
| function "*" |
| (Left : Natural; |
| Right : String) return Bounded_String |
| with |
| Pre => (if Left /= 0 then Right'Length <= Max_Length / Left), |
| Post => |
| Length ("*"'Result) = Left * Right'Length |
| and then |
| (if Right'Length > 0 then |
| (for all K in 1 .. Left * Right'Length => |
| Element ("*"'Result, K) = |
| Right (Right'First + (K - 1) mod Right'Length))); |
| |
| function "*" |
| (Left : Natural; |
| Right : Bounded_String) return Bounded_String |
| with |
| Pre => (if Left /= 0 then Length (Right) <= Max_Length / Left), |
| Post => |
| Length ("*"'Result) = Left * Length (Right) |
| and then |
| (if Length (Right) > 0 then |
| (for all K in 1 .. Left * Length (Right) => |
| Element ("*"'Result, K) = |
| Element (Right, 1 + (K - 1) mod Length (Right)))); |
| |
| function Replicate |
| (Count : Natural; |
| Item : Character; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => (if Count > Max_Length then Drop /= Error), |
| Post => |
| To_String (Replicate'Result) = |
| [1 .. Natural'Min (Max_Length, Count) => Item]; |
| |
| function Replicate |
| (Count : Natural; |
| Item : String; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => |
| (if Count /= 0 and then Item'Length > Max_Length / Count |
| then Drop /= Error), |
| Contract_Cases => |
| (Count = 0 or else Item'Length <= Max_Length / Count |
| => |
| Length (Replicate'Result) = Count * Item'Length |
| and then |
| (if Item'Length > 0 then |
| (for all K in 1 .. Count * Item'Length => |
| Element (Replicate'Result, K) = |
| Item (Item'First + (K - 1) mod Item'Length))), |
| Count /= 0 |
| and then Item'Length > Max_Length / Count |
| and then Drop = Right |
| => |
| Length (Replicate'Result) = Max_Length |
| and then |
| (for all K in 1 .. Max_Length => |
| Element (Replicate'Result, K) = |
| Item (Item'First + (K - 1) mod Item'Length)), |
| others -- Drop = Left |
| => |
| Length (Replicate'Result) = Max_Length |
| and then |
| (for all K in 1 .. Max_Length => |
| Element (Replicate'Result, K) = |
| Item (Item'Last - (Max_Length - K) mod Item'Length))); |
| |
| function Replicate |
| (Count : Natural; |
| Item : Bounded_String; |
| Drop : Truncation := Error) return Bounded_String |
| with |
| Pre => |
| (if Count /= 0 and then Length (Item) > Max_Length / Count |
| then Drop /= Error), |
| Contract_Cases => |
| ((if Count /= 0 then Length (Item) <= Max_Length / Count) |
| => |
| Length (Replicate'Result) = Count * Length (Item) |
| and then |
| (if Length (Item) > 0 then |
| (for all K in 1 .. Count * Length (Item) => |
| Element (Replicate'Result, K) = |
| Element (Item, 1 + (K - 1) mod Length (Item)))), |
| Count /= 0 |
| and then Length (Item) > Max_Length / Count |
| and then Drop = Right |
| => |
| Length (Replicate'Result) = Max_Length |
| and then |
| (for all K in 1 .. Max_Length => |
| Element (Replicate'Result, K) = |
| Element (Item, 1 + (K - 1) mod Length (Item))), |
| others -- Drop = Left |
| => |
| Length (Replicate'Result) = Max_Length |
| and then |
| (for all K in 1 .. Max_Length => |
| Element (Replicate'Result, K) = |
| Element (Item, |
| Length (Item) - (Max_Length - K) mod Length (Item)))); |
| |
| private |
| -- Most of the implementation is in the separate non generic package |
| -- Ada.Strings.Superbounded. Type Bounded_String is derived from type |
| -- Superbounded.Super_String with the maximum length constraint. In |
| -- almost all cases, the routines in Superbounded can be called with |
| -- no requirement to pass the maximum length explicitly, since there |
| -- is at least one Bounded_String argument from which the maximum |
| -- length can be obtained. For all such routines, the implementation |
| -- in this private part is simply a renaming of the corresponding |
| -- routine in the superbounded package. |
| |
| -- The five exceptions are the * and Replicate routines operating on |
| -- character values. For these cases, we have a routine in the body |
| -- that calls the superbounded routine passing the maximum length |
| -- explicitly as an extra parameter. |
| |
| type Bounded_String is new Superbounded.Super_String (Max_Length); |
| -- Deriving Bounded_String from Superbounded.Super_String is the |
| -- real trick, it ensures that the type Bounded_String declared in |
| -- the generic instantiation is compatible with the Super_String |
| -- type declared in the Superbounded package. |
| |
| function From_String (Source : String) return Bounded_String |
| with Pre => Source'Length <= Max_Length; |
| -- Private routine used only by Stream_Convert |
| |
| pragma Stream_Convert (Bounded_String, From_String, To_String); |
| -- Provide stream routines without dragging in Ada.Streams |
| |
| Null_Bounded_String : constant Bounded_String := |
| (Max_Length => Max_Length, |
| Current_Length => 0, |
| Data => |
| [1 .. Max_Length => ASCII.NUL]); |
| |
| pragma Inline (To_Bounded_String); |
| |
| procedure Set_Bounded_String |
| (Target : out Bounded_String; |
| Source : String; |
| Drop : Truncation := Error) |
| renames Set_Super_String; |
| |
| function Length |
| (Source : Bounded_String) return Length_Range |
| renames Super_Length; |
| |
| function To_String |
| (Source : Bounded_String) return String |
| renames Super_To_String; |
| |
| function Append |
| (Left : Bounded_String; |
| Right : Bounded_String; |
| Drop : Truncation := Error) return Bounded_String |
| renames Super_Append; |
| |
| function Append |
| (Left : Bounded_String; |
| Right : String; |
| Drop : Truncation := Error) return Bounded_String |
| renames Super_Append; |
| |
| function Append |
| (Left : String; |
| Right : Bounded_String; |
| Drop : Truncation := Error) return Bounded_String |
| renames Super_Append; |
| |
| function Append |
| (Left : Bounded_String; |
| Right : Character; |
| Drop : Truncation := Error) return Bounded_String |
| renames Super_Append; |
| |
| function Append |
| (Left : Character; |
| Right : Bounded_String; |
| Drop : Truncation := Error) return Bounded_String |
| renames Super_Append; |
| |
| procedure Append |
| (Source : in out Bounded_String; |
| New_Item : Bounded_String; |
| Drop : Truncation := Error) |
| renames Super_Append; |
| |
| procedure Append |
| (Source : in out Bounded_String; |
| New_Item : String; |
| Drop : Truncation := Error) |
| renames Super_Append; |
| |
| procedure Append |
| (Source : in out Bounded_String; |
| New_Item : Character; |
| Drop : Truncation := Error) |
| renames Super_Append; |
| |
| function "&" |
| (Left : Bounded_String; |
| Right : Bounded_String) return Bounded_String |
| renames Concat; |
| |
| function "&" |
| (Left : Bounded_String; |
| Right : String) return Bounded_String |
| renames Concat; |
| |
| function "&" |
| (Left : String; |
| Right : Bounded_String) return Bounded_String |
| renames Concat; |
| |
| function "&" |
| (Left : Bounded_String; |
| Right : Character) return Bounded_String |
| renames Concat; |
| |
| function "&" |
| (Left : Character; |
| Right : Bounded_String) return Bounded_String |
| renames Concat; |
| |
| function Element |
| (Source : Bounded_String; |
| Index : Positive) return Character |
| renames Super_Element; |
| |
| procedure Replace_Element |
| (Source : in out Bounded_String; |
| Index : Positive; |
| By : Character) |
| renames Super_Replace_Element; |
| |
| function Slice |
| (Source : Bounded_String; |
| Low : Positive; |
| High : Natural) return String |
| renames Super_Slice; |
| |
| function Bounded_Slice |
| (Source : Bounded_String; |
| Low : Positive; |
| High : Natural) return Bounded_String |
| renames Super_Slice; |
| |
| procedure Bounded_Slice |
| (Source : Bounded_String; |
| Target : out Bounded_String; |
| Low : Positive; |
| High : Natural) |
| renames Super_Slice; |
| |
| overriding function "=" |
| (Left : Bounded_String; |
| Right : Bounded_String) return Boolean |
| renames Equal; |
| |
| function "=" |
| (Left : Bounded_String; |
| Right : String) return Boolean |
| renames Equal; |
| |
| function "=" |
| (Left : String; |
| Right : Bounded_String) return Boolean |
| renames Equal; |
| |
| function "<" |
| (Left : Bounded_String; |
| Right : Bounded_String) return Boolean |
| renames Less; |
| |
| function "<" |
| (Left : Bounded_String; |
| Right : String) return Boolean |
| renames Less; |
| |
| function "<" |
| (Left : String; |
| Right : Bounded_String) return Boolean |
| renames Less; |
| |
| function "<=" |
| (Left : Bounded_String; |
| Right : Bounded_String) return Boolean |
| renames Less_Or_Equal; |
| |
| function "<=" |
| (Left : Bounded_String; |
| Right : String) return Boolean |
| renames Less_Or_Equal; |
| |
| function "<=" |
| (Left : String; |
| Right : Bounded_String) return Boolean |
| renames Less_Or_Equal; |
| |
| function ">" |
| (Left : Bounded_String; |
| Right : Bounded_String) return Boolean |
| renames Greater; |
| |
| function ">" |
| (Left : Bounded_String; |
| Right : String) return Boolean |
| renames Greater; |
| |
| function ">" |
| (Left : String; |
| Right : Bounded_String) return Boolean |
| renames Greater; |
| |
| function ">=" |
| (Left : Bounded_String; |
| Right : Bounded_String) return Boolean |
| renames Greater_Or_Equal; |
| |
| function ">=" |
| (Left : Bounded_String; |
| Right : String) return Boolean |
| renames Greater_Or_Equal; |
| |
| function ">=" |
| (Left : String; |
| Right : Bounded_String) return Boolean |
| renames Greater_Or_Equal; |
| |
| function Index |
| (Source : Bounded_String; |
| Pattern : String; |
| Going : Direction := Forward; |
| Mapping : Maps.Character_Mapping := Maps.Identity) return Natural |
| renames Super_Index; |
| |
| function Index |
| (Source : Bounded_String; |
| Pattern : String; |
| Going : Direction := Forward; |
| Mapping : Maps.Character_Mapping_Function) return Natural |
| renames Super_Index; |
| |
| function Index |
| (Source : Bounded_String; |
| Set : Maps.Character_Set; |
| Test : Membership := Inside; |
| Going : Direction := Forward) return Natural |
| renames Super_Index; |
| |
| function Index |
| (Source : Bounded_String; |
| Pattern : String; |
| From : Positive; |
| Going : Direction := Forward; |
| Mapping : Maps.Character_Mapping := Maps.Identity) return Natural |
| renames Super_Index; |
| |
| function Index |
| (Source : Bounded_String; |
| Pattern : String; |
| From : Positive; |
| Going : Direction := Forward; |
| Mapping : Maps.Character_Mapping_Function) return Natural |
| renames Super_Index; |
| |
| function Index |
| (Source : Bounded_String; |
| Set : Maps.Character_Set; |
| From : Positive; |
| Test : Membership := Inside; |
| Going : Direction := Forward) return Natural |
| renames Super_Index; |
| |
| function Index_Non_Blank |
| (Source : Bounded_String; |
| Going : Direction := Forward) return Natural |
| renames Super_Index_Non_Blank; |
| |
| function Index_Non_Blank |
| (Source : Bounded_String; |
| From : Positive; |
| Going : Direction := Forward) return Natural |
| renames Super_Index_Non_Blank; |
| |
| function Count |
| (Source : Bounded_String; |
| Pattern : String; |
| Mapping : Maps.Character_Mapping := Maps.Identity) return Natural |
| renames Super_Count; |
| |
| function Count |
| (Source : Bounded_String; |
| Pattern : String; |
| Mapping : Maps.Character_Mapping_Function) return Natural |
| renames Super_Count; |
| |
| function Count |
| (Source : Bounded_String; |
| Set : Maps.Character_Set) return Natural |
| renames Super_Count; |
| |
| procedure Find_Token |
| (Source : Bounded_String; |
| Set : Maps.Character_Set; |
| From : Positive; |
| Test : Membership; |
| First : out Positive; |
| Last : out Natural) |
| renames Super_Find_Token; |
| |
| procedure Find_Token |
| (Source : Bounded_String; |
| Set : Maps.Character_Set; |
| Test : Membership; |
| First : out Positive; |
| Last : out Natural) |
| renames Super_Find_Token; |
| |
| function Translate |
| (Source : Bounded_String; |
| Mapping : Maps.Character_Mapping) return Bounded_String |
| renames Super_Translate; |
| |
| procedure Translate |
| (Source : in out Bounded_String; |
| Mapping : Maps.Character_Mapping) |
| renames Super_Translate; |
| |
| function Translate |
| (Source : Bounded_String; |
| Mapping : Maps.Character_Mapping_Function) return Bounded_String |
| renames Super_Translate; |
| |
| procedure Translate |
| (Source : in out Bounded_String; |
| Mapping : Maps.Character_Mapping_Function) |
| renames Super_Translate; |
| |
| function Replace_Slice |
| (Source : Bounded_String; |
| Low : Positive; |
| High : Natural; |
| By : String; |
| Drop : Truncation := Error) return Bounded_String |
| renames Super_Replace_Slice; |
| |
| procedure Replace_Slice |
| (Source : in out Bounded_String; |
| Low : Positive; |
| High : Natural; |
| By : String; |
| Drop : Truncation := Error) |
| renames Super_Replace_Slice; |
| |
| function Insert |
| (Source : Bounded_String; |
| Before : Positive; |
| New_Item : String; |
| Drop : Truncation := Error) return Bounded_String |
| renames Super_Insert; |
| |
| procedure Insert |
| (Source : in out Bounded_String; |
| Before : Positive; |
| New_Item : String; |
| Drop : Truncation := Error) |
| renames Super_Insert; |
| |
| function Overwrite |
| (Source : Bounded_String; |
| Position : Positive; |
| New_Item : String; |
| Drop : Truncation := Error) return Bounded_String |
| renames Super_Overwrite; |
| |
| procedure Overwrite |
| (Source : in out Bounded_String; |
| Position : Positive; |
| New_Item : String; |
| Drop : Truncation := Error) |
| renames Super_Overwrite; |
| |
| function Delete |
| (Source : Bounded_String; |
| From : Positive; |
| Through : Natural) return Bounded_String |
| renames Super_Delete; |
| |
| procedure Delete |
| (Source : in out Bounded_String; |
| From : Positive; |
| Through : Natural) |
| renames Super_Delete; |
| |
| function Trim |
| (Source : Bounded_String; |
| Side : Trim_End) return Bounded_String |
| renames Super_Trim; |
| |
| procedure Trim |
| (Source : in out Bounded_String; |
| Side : Trim_End) |
| renames Super_Trim; |
| |
| function Trim |
| (Source : Bounded_String; |
| Left : Maps.Character_Set; |
| Right : Maps.Character_Set) return Bounded_String |
| renames Super_Trim; |
| |
| procedure Trim |
| (Source : in out Bounded_String; |
| Left : Maps.Character_Set; |
| Right : Maps.Character_Set) |
| renames Super_Trim; |
| |
| function Head |
| (Source : Bounded_String; |
| Count : Natural; |
| Pad : Character := Space; |
| Drop : Truncation := Error) return Bounded_String |
| renames Super_Head; |
| |
| procedure Head |
| (Source : in out Bounded_String; |
| Count : Natural; |
| Pad : Character := Space; |
| Drop : Truncation := Error) |
| renames Super_Head; |
| |
| function Tail |
| (Source : Bounded_String; |
| Count : Natural; |
| Pad : Character
|