spark 2012.0.deb-11+b2 / usr / lib / spark / current / spark-ada-strings-unbounded.adb

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

with SPARK.Ada.Strings.Not_SPARK;
with SPARK.Ada.Strings.Maps.Not_SPARK;

package body SPARK.Ada.Strings.Unbounded is
   --# hide SPARK.Ada.Strings.Unbounded;

   pragma Warnings ("Y"); -- Turn off warnings for Ada 2005 features

   function Get_Length (Source : Unbounded_String) return Natural is
   begin
      return Standard.Ada.Strings.Unbounded.Length
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source));
   end Get_Length;

   function Get_Null_Unbounded_String return Unbounded_String is
   begin
      return Null_Unbounded_String;
   end Get_Null_Unbounded_String;

   function Get_Element
     (Source : Unbounded_String;
      Index  : Positive) return Character is
   begin
      return Standard.Ada.Strings.Unbounded.Element
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Index  => Index);
   end Get_Element;

   function String_To_Unbounded_String
     (Source : String) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded.To_Unbounded_String
           (Source => Source));
   end String_To_Unbounded_String;

   function Length_To_Unbounded_String
     (Length : Natural) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded."*" (Left  => Length,
                                             Right => ' '));
   end Length_To_Unbounded_String;

   --  Set_Unbounded_String is only defined in Ada 2005
   procedure Set_Unbounded_String
     (Target :    out Unbounded_String;
      Source : in     String) is
   begin
      Standard.Ada.Strings.Unbounded.Set_Unbounded_String
        (Target => Standard.Ada.Strings.Unbounded.Unbounded_String (Target),
         Source => Source);
   end Set_Unbounded_String;

   procedure Append_Unbounded_String
     (Source   : in out Unbounded_String;
      New_Item : in     Unbounded_String) is
   begin
      Standard.Ada.Strings.Unbounded.Append
        (Source   => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         New_Item => Standard.Ada.Strings.Unbounded.Unbounded_String
           (New_Item));
   end Append_Unbounded_String;

   procedure Append_String
     (Source   : in out Unbounded_String;
      New_Item : in     String) is
   begin
      Standard.Ada.Strings.Unbounded.Append
        (Source   => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         New_Item => New_Item);
   end Append_String;

   procedure Append_Char
     (Source   : in out Unbounded_String;
      New_Item : in     Character) is
   begin
      Standard.Ada.Strings.Unbounded.Append
        (Source   => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         New_Item => New_Item);
   end Append_Char;

   function Concat_Unbounded_String_Unbounded_String
     (Left  : Unbounded_String;
      Right : Unbounded_String) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded."&"
           (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
            Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right)));
   end Concat_Unbounded_String_Unbounded_String;

   function Concat_Unbounded_String_String
     (Left  : Unbounded_String;
      Right : String) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded."&"
           (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
            Right => Right));
   end Concat_Unbounded_String_String;

   function Concat_String_Unbounded_String
     (Left  : String;
      Right : Unbounded_String) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded."&"
           (Left  => Left,
            Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right)));
   end Concat_String_Unbounded_String;

   function Concat_Unbounded_String_Char
     (Left  : Unbounded_String;
      Right : Character) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded."&"
           (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
            Right => Right));
   end Concat_Unbounded_String_Char;

   function Concat_Char_Unbounded_String
     (Left  : Character;
      Right : Unbounded_String) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded."&"
           (Left  => Left,
            Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right)));
   end Concat_Char_Unbounded_String;

   procedure Replace_Element
     (Source : in out Unbounded_String;
      Index  : in     Positive;
      By     : in     Character) is
   begin
      Standard.Ada.Strings.Unbounded.Replace_Element
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Index  => Index,
         By     => By);
   end Replace_Element;

   --  Unbounded_Slice is only available in Ada 2005
   function Function_Unbounded_Slice
     (Source : Unbounded_String;
      Low    : Positive;
      High   : Natural) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded.Unbounded_Slice
           (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
            Low    => Low,
            High   => High));
   end Function_Unbounded_Slice;

   procedure Procedure_Unbounded_Slice
     (Source : in     Unbounded_String;
      Target :    out Unbounded_String;
      Low    : in     Positive;
      High   : in     Natural) is
   begin
      Standard.Ada.Strings.Unbounded.Unbounded_Slice
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Target => Standard.Ada.Strings.Unbounded.Unbounded_String (Target),
         Low    => Low,
         High   => High);
   end Procedure_Unbounded_Slice;

   function Equal_Unbounded_String_Unbounded_String
     (Left  : Unbounded_String;
      Right : Unbounded_String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded."="
        (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
         Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right));
   end Equal_Unbounded_String_Unbounded_String;

   function Equal_Unbounded_String_String
     (Left  : Unbounded_String;
      Right : String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded."="
        (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
         Right => Right);
   end Equal_Unbounded_String_String;

   function Equal_String_Unbounded_String
     (Left  : String;
      Right : Unbounded_String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded."="
        (Left  => Left,
         Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right));
   end Equal_String_Unbounded_String;

   function Less_Unbounded_String_Unbounded_String
     (Left  : Unbounded_String;
      Right : Unbounded_String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded."<"
        (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
         Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right));
   end Less_Unbounded_String_Unbounded_String;

   function Less_Unbounded_String_String
     (Left  : Unbounded_String;
      Right : String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded."<"
        (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
         Right => Right);
   end Less_Unbounded_String_String;

   function Less_String_Unbounded_String
     (Left  : String;
      Right : Unbounded_String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded."<"
        (Left  => Left,
         Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right));
   end Less_String_Unbounded_String;

   function Less_Equal_Unbounded_String_Unbounded_String
     (Left  : Unbounded_String;
      Right : Unbounded_String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded."<="
        (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
         Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right));
   end Less_Equal_Unbounded_String_Unbounded_String;

   function Less_Equal_Unbounded_String_String
     (Left  : Unbounded_String;
      Right : String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded."<="
        (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
         Right => Right);
   end Less_Equal_Unbounded_String_String;

   function Less_Equal_String_Unbounded_String
     (Left  : String;
      Right : Unbounded_String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded."<="
        (Left  => Left,
         Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right));
   end Less_Equal_String_Unbounded_String;

   function Greater_Unbounded_String_Unbounded_String
     (Left  : Unbounded_String;
      Right : Unbounded_String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded.">"
        (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
         Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right));
   end Greater_Unbounded_String_Unbounded_String;

   function Greater_Unbounded_String_String
     (Left  : Unbounded_String;
      Right : String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded.">"
        (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
         Right => Right);
   end Greater_Unbounded_String_String;

   function Greater_String_Unbounded_String
     (Left  : String;
      Right : Unbounded_String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded.">"
        (Left  => Left,
         Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right));
   end Greater_String_Unbounded_String;

   function Greater_Equal_Unbounded_String_Unbounded_String
     (Left  : Unbounded_String;
      Right : Unbounded_String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded.">="
        (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
         Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right));
   end Greater_Equal_Unbounded_String_Unbounded_String;

   function Greater_Equal_Unbounded_String_String
     (Left  : Unbounded_String;
      Right : String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded.">="
        (Left  => Standard.Ada.Strings.Unbounded.Unbounded_String (Left),
         Right => Right);
   end Greater_Equal_Unbounded_String_String;

   function Greater_Equal_String_Unbounded_String
     (Left  : String;
      Right : Unbounded_String) return Boolean is
   begin
      return Standard.Ada.Strings.Unbounded.">="
        (Left  => Left,
         Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right));
   end Greater_Equal_String_Unbounded_String;

   function Index_Pattern
     (Source  : Unbounded_String;
      Pattern : String;
      Going   : Strings.Direction;
      Mapping : Maps.Character_Mapping) return Natural is
   begin
      return Standard.Ada.Strings.Unbounded.Index
        (Source  => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Pattern => Pattern,
         Going   => SPARK.Ada.Strings.Not_SPARK.To_Direction (From => Going),
         Mapping => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Mapping
           (From => Mapping));
   end Index_Pattern;

   function Index_Set
     (Source  : Unbounded_String;
      Arg_Set : Maps.Character_Set;
      Test    : Strings.Membership;
      Going   : Strings.Direction) return Natural is
   begin
      return Standard.Ada.Strings.Unbounded.Index
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Set    => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Set
           (From => Arg_Set),
         Test   => SPARK.Ada.Strings.Not_SPARK.To_Membership (From => Test),
         Going  => SPARK.Ada.Strings.Not_SPARK.To_Direction (From => Going));
   end Index_Set;

   --  Index is only defined in Ada 2005
   function Index_Pattern_From
     (Source   : Unbounded_String;
      Pattern  : String;
      Arg_From : Positive;
      Going    : Strings.Direction;
      Mapping  : Maps.Character_Mapping) return Natural is
   begin
      return Standard.Ada.Strings.Unbounded.Index
        (Source  => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Pattern => Pattern,
         From    => Arg_From,
         Going   => SPARK.Ada.Strings.Not_SPARK.To_Direction (From => Going),
         Mapping => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Mapping
           (From => Mapping));
   end Index_Pattern_From;

   function Index_Set_From
     (Source   : Unbounded_String;
      Arg_Set  : Maps.Character_Set;
      Arg_From : Positive;
      Test     : Strings.Membership;
      Going    : Strings.Direction) return Natural is
   begin
      return Standard.Ada.Strings.Unbounded.Index
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Set    => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Set
           (From => Arg_Set),
         From   => Arg_From,
         Test   => SPARK.Ada.Strings.Not_SPARK.To_Membership (From => Test),
         Going  => SPARK.Ada.Strings.Not_SPARK.To_Direction (From => Going));
   end Index_Set_From;

   --  Index_Non_Blank is only defined in Ada 2005
   function Index_Non_Blank
     (Source : Unbounded_String;
      Going  : Strings.Direction) return Natural is
   begin
      return Standard.Ada.Strings.Unbounded.Index_Non_Blank
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Going  => SPARK.Ada.Strings.Not_SPARK.To_Direction (From => Going));
   end Index_Non_Blank;

   function Index_Non_Blank_From
     (Source   : Unbounded_String;
      Arg_From : Positive;
      Going    : Strings.Direction) return Natural is
   begin
      return Standard.Ada.Strings.Unbounded.Index_Non_Blank
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         From   => Arg_From,
         Going  => SPARK.Ada.Strings.Not_SPARK.To_Direction (From => Going));
   end Index_Non_Blank_From;

   function Count_Pattern
     (Source  : Unbounded_String;
      Pattern : String;
      Mapping : Maps.Character_Mapping) return Natural is
   begin
      return Standard.Ada.Strings.Unbounded.Count
        (Source  => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Pattern => Pattern,
         Mapping => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Mapping
           (From => Mapping));
   end Count_Pattern;

   function Count_Set
     (Source  : Unbounded_String;
      Arg_Set : Maps.Character_Set) return Natural is
   begin
      return Standard.Ada.Strings.Unbounded.Count
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Set    => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Set
           (From => Arg_Set));
   end Count_Set;

   procedure Find_Token
     (Source    : in     Unbounded_String;
      Arg_Set   : in     Maps.Character_Set;
      Test      : in     Strings.Membership;
      Arg_First :    out Positive;
      Arg_Last  :    out Natural) is
   begin
      Standard.Ada.Strings.Unbounded.Find_Token
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Set    => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Set
           (From => Arg_Set),
         Test   => SPARK.Ada.Strings.Not_SPARK.To_Membership (From => Test),
         First  => Arg_First,
         Last   => Arg_Last);
   end Find_Token;

   function Function_Translate
     (Source  : Unbounded_String;
      Mapping : Maps.Character_Mapping) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded.Translate
           (Source  => Standard.Ada.Strings.Unbounded.Unbounded_String
              (Source),
            Mapping => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Mapping
              (From => Mapping)));
   end Function_Translate;

   procedure Procedure_Translate
     (Source  : in out Unbounded_String;
      Mapping : in     Maps.Character_Mapping) is
   begin
      Standard.Ada.Strings.Unbounded.Translate
        (Source  => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Mapping => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Mapping
           (From => Mapping));
   end Procedure_Translate;

   function Function_Replace_Slice
     (Source : Unbounded_String;
      Low    : Positive;
      High   : Natural;
      By     : String) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded.Replace_Slice
           (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
            Low    => Low,
            High   => High,
            By     => By));
   end Function_Replace_Slice;

   procedure Procedure_Replace_Slice
     (Source : in out Unbounded_String;
      Low    : in     Positive;
      High   : in     Natural;
      By     : in     String) is
   begin
      Standard.Ada.Strings.Unbounded.Replace_Slice
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Low    => Low,
         High   => High,
         By     => By);
   end Procedure_Replace_Slice;

   function Function_Insert
     (Source   : Unbounded_String;
      Before   : Positive;
      New_Item : String) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded.Insert
           (Source   => Standard.Ada.Strings.Unbounded.Unbounded_String
              (Source),
            Before   => Before,
            New_Item => New_Item));
   end Function_Insert;

   procedure Procedure_Insert
     (Source   : in out Unbounded_String;
      Before   : in     Positive;
      New_Item : in     String) is
   begin
      Standard.Ada.Strings.Unbounded.Insert
        (Source   => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Before   => Before,
         New_Item => New_Item);
   end Procedure_Insert;

   function Function_Overwrite
     (Source   : Unbounded_String;
      Position : Positive;
      New_Item : String) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded.Overwrite
           (Source   => Standard.Ada.Strings.Unbounded.Unbounded_String
              (Source),
            Position => Position,
            New_Item => New_Item));
   end Function_Overwrite;

   procedure Procedure_Overwrite
     (Source   : in out Unbounded_String;
      Position : in     Positive;
      New_Item : in     String) is
   begin
      Standard.Ada.Strings.Unbounded.Overwrite
        (Source   => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Position => Position,
         New_Item => New_Item);
   end Procedure_Overwrite;

   function Function_Delete
     (Source   : Unbounded_String;
      Arg_From : Positive;
      Through  : Natural) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded.Delete
           (Source  => Standard.Ada.Strings.Unbounded.Unbounded_String
              (Source),
            From    => Arg_From,
            Through => Through));
   end Function_Delete;

   procedure Procedure_Delete
     (Source   : in out Unbounded_String;
      Arg_From : in     Positive;
      Through  : in     Natural) is
   begin
      Standard.Ada.Strings.Unbounded.Delete
        (Source  => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         From    => Arg_From,
         Through => Through);
   end Procedure_Delete;

   function Function_Trim_Side
     (Source : Unbounded_String;
      Side   : Trim_End) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded.Trim
           (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
            Side   => SPARK.Ada.Strings.Not_SPARK.To_Trim_End (From => Side)));
   end Function_Trim_Side;

   procedure Procedure_Trim_Side
     (Source : in out Unbounded_String;
      Side   : in     Trim_End) is
   begin
      Standard.Ada.Strings.Unbounded.Trim
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Side   => SPARK.Ada.Strings.Not_SPARK.To_Trim_End (From => Side));
   end Procedure_Trim_Side;

   function Function_Trim_Character_Set
     (Source : Unbounded_String;
      Left   : Maps.Character_Set;
      Right  : Maps.Character_Set) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded.Trim
           (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
            Left   => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Set
              (From => Left),
            Right  => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Set
              (From => Right)));
   end Function_Trim_Character_Set;

   procedure Procedure_Trim_Character_Set
     (Source : in out Unbounded_String;
      Left   : in     Maps.Character_Set;
      Right  : in     Maps.Character_Set) is
   begin
      Standard.Ada.Strings.Unbounded.Trim
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Left   => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Set
           (From => Left),
         Right  => SPARK.Ada.Strings.Maps.Not_SPARK.To_Character_Set
           (From => Right));
   end Procedure_Trim_Character_Set;

   function Function_Head
     (Source : Unbounded_String;
      Count  : Natural;
      Pad    : Character) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded.Head
           (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
            Count  => Count,
            Pad    => Pad));
   end Function_Head;

   procedure Procedure_Head
     (Source : in out Unbounded_String;
      Count  : in     Natural;
      Pad    : in     Character) is
   begin
      Standard.Ada.Strings.Unbounded.Head
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Count  => Count,
         Pad    => Pad);
   end Procedure_Head;

   function Function_Tail
     (Source : Unbounded_String;
      Count  : Natural;
      Pad    : Character) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded.Tail
           (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
            Count  => Count,
            Pad    => Pad));
   end Function_Tail;

   procedure Procedure_Tail
     (Source : in out Unbounded_String;
      Count  : in     Natural;
      Pad    : in     Character) is
   begin
      Standard.Ada.Strings.Unbounded.Tail
        (Source => Standard.Ada.Strings.Unbounded.Unbounded_String (Source),
         Count  => Count,
         Pad    => Pad);
   end Procedure_Tail;

   function Times_Char
     (Left  : Natural;
      Right : Character) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded."*" (Left  => Left,
                                             Right => Right));
   end Times_Char;

   function Times_String
     (Left  : Natural;
      Right : String) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded."*" (Left  => Left,
                                             Right => Right));
   end Times_String;

   function Times_Unbounded_String
     (Left  : Natural;
      Right : Unbounded_String) return Unbounded_String is
   begin
      return Unbounded_String
        (Standard.Ada.Strings.Unbounded."*"
           (Left  => Left,
            Right => Standard.Ada.Strings.Unbounded.Unbounded_String (Right)));
   end Times_Unbounded_String;

end SPARK.Ada.Strings.Unbounded;