gcc/ada/libgnat/s-casuti.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                     S Y S T E M . C A S E _ U T I L                      --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 1995-2023, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  17 --                                                                          --
  18 -- As a special exception under Section 7 of GPL version 3, you are granted --
  19 -- additional permissions described in the GCC Runtime Library Exception,   --
  20 -- version 3.1, as published by the Free Software Foundation.               --
  21 --                                                                          --
  22 -- You should have received a copy of the GNU General Public License and    --
  23 -- a copy of the GCC Runtime Library Exception along with this program;     --
  24 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  25 -- <http://www.gnu.org/licenses/>.                                          --
  26 --                                                                          --
  27 -- GNAT was originally developed  by the GNAT team at  New York University. --
  28 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  29 --                                                                          --
  30 ------------------------------------------------------------------------------
  31
  32 --  Simple casing functions
  33
  34 --  This package provides simple casing functions that do not require the
  35 --  overhead of the full casing tables found in Ada.Characters.Handling.
  36
  37 --  Preconditions in this unit are meant for analysis only, not for run-time
  38 --  checking, so that the expected exceptions are raised. This is enforced by
  39 --  setting the corresponding assertion policy to Ignore. Postconditions and
  40 --  contract cases should not be executed at runtime as well, in order not to
  41 --  slow down the execution of these functions.
  42
  43 pragma Assertion_Policy (Pre            => Ignore,
  44                          Post           => Ignore,
  45                          Contract_Cases => Ignore,
  46                          Ghost          => Ignore);
  47
  48 package System.Case_Util
  49   with Pure, SPARK_Mode
  50 is
  51    --  Note: all the following functions handle the full Latin-1 set
  52
  53    function To_Upper (A : Character) return Character
  54    with
  55      Post => (declare
  56                 A_Val : constant Natural := Character'Pos (A);
  57               begin
  58                 (if A in 'a' .. 'z'
  59                    or else A_Val in 16#E0# .. 16#F6#
  60                    or else A_Val in 16#F8# .. 16#FE#
  61                  then
  62                    To_Upper'Result = Character'Val (A_Val - 16#20#)
  63                  else
  64                    To_Upper'Result = A));
  65    --  Converts A to upper case if it is a lower case letter, otherwise
  66    --  returns the input argument unchanged.
  67
  68    procedure To_Upper (A : in out String)
  69    with
  70      Post => (for all J in A'Range => A (J) = To_Upper (A'Old (J)));
  71
  72    function To_Upper (A : String) return String
  73    with
  74      Post => To_Upper'Result'First = A'First
  75        and then To_Upper'Result'Last = A'Last
  76        and then (for all J in A'Range =>
  77                    To_Upper'Result (J) = To_Upper (A (J)));
  78    --  Folds all characters of string A to upper case
  79
  80    function To_Lower (A : Character) return Character
  81    with
  82      Post => (declare
  83                 A_Val : constant Natural := Character'Pos (A);
  84               begin
  85                 (if A in 'A' .. 'Z'
  86                    or else A_Val in 16#C0# .. 16#D6#
  87                    or else A_Val in 16#D8# .. 16#DE#
  88                  then
  89                    To_Lower'Result = Character'Val (A_Val + 16#20#)
  90                  else
  91                    To_Lower'Result = A));
  92    --  Converts A to lower case if it is an upper case letter, otherwise
  93    --  returns the input argument unchanged.
  94
  95    procedure To_Lower (A : in out String)
  96    with
  97      Post => (for all J in A'Range => A (J) = To_Lower (A'Old (J)));
  98
  99    function To_Lower (A : String) return String
 100    with
 101      Post => To_Lower'Result'First = A'First
 102        and then To_Lower'Result'Last = A'Last
 103        and then (for all J in A'Range =>
 104                    To_Lower'Result (J) = To_Lower (A (J)));
 105    --  Folds all characters of string A to lower case
 106
 107    procedure To_Mixed (A : in out String)
 108    with
 109      Post =>
 110        (for all J in A'Range =>
 111           (if J = A'First
 112              or else A'Old (J - 1) = '_'
 113            then
 114              A (J) = To_Upper (A'Old (J))
 115            else
 116              A (J) = To_Lower (A'Old (J))));
 117
 118    function To_Mixed (A : String) return String
 119    with
 120      Post => To_Mixed'Result'First = A'First
 121        and then To_Mixed'Result'Last = A'Last
 122        and then (for all J in A'Range =>
 123                    (if J = A'First
 124                       or else A (J - 1) = '_'
 125                     then
 126                       To_Mixed'Result (J) = To_Upper (A (J))
 127                     else
 128                       To_Mixed'Result (J) = To_Lower (A (J))));
 129    --  Converts A to mixed case (i.e. lower case, except for initial
 130    --  character and any character after an underscore, which are
 131    --  converted to upper case.
 132
 133 end System.Case_Util;