------------------------------------------------------------------------------
-- --
-- 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-2023, 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;
pragma Annotate (GNATprove, Always_Return, Bounded);
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);
pragma Annotate (GNATprove, Always_Return, Generic_Bounded_Length);
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 := Space;
Drop : Truncation := Error) return Bounded_String
renames Super_Tail;
procedure Tail
(Source : in out Bounded_String;
Count : Natural;
Pad : Character := Space;
Drop : Truncation := Error)
renames Super_Tail;
function "*"
(Left : Natural;
Right : Bounded_String) return Bounded_String
renames Times;
function Replicate
(Count : Natural;
Item : Bounded_String;
Drop : Truncation := Error) return Bounded_String
renames Super_Replicate;
end Generic_Bounded_Length;
end Ada.Strings.Bounded;