| blob | 339cb17f5dfda998fdd949f7b1e0d10e022a172e |
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT RUN-TIME COMPONENTS --
4 -- --
5 -- A D A . S T R I N G S . S U P E R B O U N D E D --
6 -- --
7 -- S p e c --
8 -- --
9 -- Copyright (C) 2003-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 ------------------------------------------------------------------------------
32 -- This non generic package contains most of the implementation of the
33 -- generic package Ada.Strings.Bounded.Generic_Bounded_Length.
35 -- It defines type Super_String as a discriminated record with the maximum
36 -- length as the discriminant. Individual instantiations of Strings.Bounded
37 -- use this type with an appropriate discriminant value set.
39 -- Preconditions in this unit are meant for analysis only, not for run-time
40 -- checking, so that the expected exceptions are raised. This is enforced by
41 -- setting the corresponding assertion policy to Ignore. Postconditions and
42 -- contract cases should not be executed at runtime as well, in order not to
43 -- slow down the execution of these functions.
55 SPARK_Mode,
56 Always_Terminates
57 is
60 -- Type Bounded_String in Ada.Strings.Bounded.Generic_Bounded_Length is
61 -- derived from Super_String, with the constraint of the maximum length.
68 -- A previous version had a default initial value for Data, which is
69 -- no longer necessary, because we now special-case this type in the
70 -- compiler, so "=" composes properly for descendants of this type.
71 -- Leaving it out is more efficient.
72 end record
73 with
74 Ghost_Predicate =>
75 Current_Length <= Max_Length
79 -- The subprograms defined for Super_String are similar to those
80 -- defined for Bounded_String, except that they have different names, so
81 -- that they can be renamed in Ada.Strings.Bounded.Generic_Bounded_Length.
87 --------------------------------------------------------
88 -- Conversion, Concatenation, and Selection Functions --
89 --------------------------------------------------------
91 function To_Super_String
95 with
98 Contract_Cases =>
100 =>
104 =>
109 =>
113 -- Note the additional parameter Max_Length, which specifies the maximum
114 -- length setting of the resulting Super_String value.
116 -- The following procedures have declarations (and semantics) that are
117 -- exactly analogous to those declared in Ada.Strings.Bounded.
122 procedure Set_Super_String
126 with
127 Pre =>
129 Contract_Cases =>
131 =>
135 =>
140 =>
145 function Super_Append
149 with
150 Pre =>
152 and then
156 Contract_Cases =>
158 =>
161 and then
164 and then
173 =>
175 and then
178 1, Left.Max_Length - Super_Length (Right))) =
179 Super_Slice (Left,
180 Super_Length (Left) - Left.Max_Length
181 + Super_Length (Right) + 1,
182 Super_Length (Left)))
183 and then
184 Super_Slice (Super_Append'Result,
185 Left.Max_Length - Super_Length (Right) + 1, Left.Max_Length) =
186 Super_To_String (Right),
188 others -- Drop = Right
189 =>
190 Super_Length (Super_Append'Result) = Left.Max_Length
191 and then
192 Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
193 Super_To_String (Left)
194 and then
195 (if Super_Length (Left) < Left.Max_Length then
202 function Super_Append
206 with
207 Pre =>
211 Contract_Cases =>
213 =>
216 and then
219 and then
224 Right),
228 =>
230 and then
233 -- The result is the end of Left followed by Right
236 1, Left.Max_Length - Right'Length)) =
237 Super_Slice (Left,
238 Super_Length (Left) - Left.Max_Length + Right'Length
239 + 1,
240 Super_Length (Left))
241 and then
242 Super_Slice (Super_Append'Result,
243 Left.Max_Length - Right'Length + 1, Left.Max_Length) =
244 Right
245 else
246 -- The result is the last Max_Length characters of Right
248 Super_To_String (Super_Append'Result) =
249 Right (Right'Last - Left.Max_Length + 1 .. Right'Last)),
251 others -- Drop = Right
252 =>
253 Super_Length (Super_Append'Result) = Left.Max_Length
254 and then
255 Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
256 Super_To_String (Left)
257 and then
258 (if Super_Length (Left) < Left.Max_Length then
259 Super_Slice (Super_Append'Result,
260 Super_Length (Left) + 1, Left.Max_Length) =
261 Right (Right'First
262 .. Left.Max_Length - Super_Length (Left)
263 - 1 + Right'First))),
264 Global => null;
266 function Super_Append
267 (Left : String;
268 Right : Super_String;
269 Drop : Truncation := Error) return Super_String
270 with
271 Pre =>
272 (if Left'Length > Right.Max_Length - Super_Length (Right)
273 then Drop /= Error),
274 Post => Super_Append'Result.Max_Length = Right.Max_Length,
275 Contract_Cases =>
276 (Left'Length <= Right.Max_Length - Super_Length (Right)
277 =>
278 Super_Length (Super_Append'Result) =
279 Left'Length + Super_Length (Right)
280 and then Super_Slice (Super_Append'Result, 1, Left'Length) = Left
281 and then
282 (if Super_Length (Right) > 0 then
283 Super_Slice (Super_Append'Result,
284 Left'Length + 1, Super_Length (Super_Append'Result)) =
285 Super_To_String (Right)),
287 Left'Length > Right.Max_Length - Super_Length (Right)
288 and then Drop = Strings.Left
289 =>
290 Super_Length (Super_Append'Result) = Right.Max_Length
291 and then
292 (if Super_Length (Right) < Right.Max_Length then
293 Super_Slice (Super_Append'Result,
294 1, Right.Max_Length - Super_Length (Right)) =
295 Left
296 (Left'Last - Right.Max_Length + Super_Length (Right) + 1
297 .. Left'Last))
298 and then
299 Super_Slice (Super_Append'Result,
300 Right.Max_Length - Super_Length (Right) + 1,
301 Right.Max_Length) =
302 Super_To_String (Right),
304 others -- Drop = Right
305 =>
306 Super_Length (Super_Append'Result) = Right.Max_Length
307 and then
308 (if Left'Length < Right.Max_Length then
310 -- The result is Left followed by the beginning of Right
312 Super_Slice (Super_Append'Result, 1, Left'Length) = Left
313 and then
317 else
318 -- The result is the first Max_Length characters of Left
324 function Super_Append
328 with
329 Pre =>
332 Contract_Cases =>
334 =>
336 and then
339 and then
341 Right,
344 =>
346 and then
350 =>
352 and then
354 1, Left.Max_Length - 1)) =
355 Super_Slice (Left, 2, Left.Max_Length)
356 and then
357 Super_Element (Super_Append'Result, Left.Max_Length) = Right),
358 Global => null;
360 function Super_Append
361 (Left : Character;
362 Right : Super_String;
363 Drop : Truncation := Error) return Super_String
364 with
365 Pre =>
366 (if Super_Length (Right) = Right.Max_Length then Drop /= Error),
367 Post => Super_Append'Result.Max_Length = Right.Max_Length,
368 Contract_Cases =>
369 (Super_Length (Right) < Right.Max_Length
370 =>
371 Super_Length (Super_Append'Result) = Super_Length (Right) + 1
372 and then
373 Super_Slice (Super_Append'Result, 2, Super_Length (Right) + 1) =
374 Super_To_String (Right)
375 and then Super_Element (Super_Append'Result, 1) = Left,
377 Super_Length (Right) = Right.Max_Length and then Drop = Strings.Left
378 =>
379 Super_Length (Super_Append'Result) = Right.Max_Length
380 and then
381 Super_To_String (Super_Append'Result) = Super_To_String (Right),
383 others -- Drop = Right
384 =>
385 Super_Length (Super_Append'Result) = Right.Max_Length
386 and then
392 procedure Super_Append
396 with
397 Pre =>
399 and then
403 Contract_Cases =>
405 =>
408 and then
411 and then
419 =>
421 and then
424 1, Source.Max_Length - Super_Length (New_Item))) =
425 Super_Slice (Source'Old,
426 Super_Length (Source'Old) - Source.Max_Length
427 + Super_Length (New_Item) + 1,
428 Super_Length (Source'Old)))
429 and then
430 Super_Slice (Source,
431 Source.Max_Length - Super_Length (New_Item) + 1,
432 Source.Max_Length) =
433 Super_To_String (New_Item),
435 others -- Drop = Right
436 =>
437 Super_Length (Source) = Source.Max_Length
438 and then
439 Super_Slice (Source, 1, Super_Length (Source'Old)) =
440 Super_To_String (Source'Old)
441 and then
442 (if Super_Length (Source'Old) < Source.Max_Length then
449 procedure Super_Append
453 with
454 Pre =>
457 Contract_Cases =>
459 =>
461 and then
464 and then
468 New_Item),
472 =>
474 and then
477 -- The result is the end of Source followed by New_Item
480 1, Source.Max_Length - New_Item'Length)) =
481 Super_Slice (Source'Old,
482 Super_Length (Source'Old) - Source.Max_Length
483 + New_Item'Length + 1,
484 Super_Length (Source'Old))
485 and then
486 Super_Slice (Source,
487 Source.Max_Length - New_Item'Length + 1,
488 Source.Max_Length) =
489 New_Item
490 else
491 -- The result is the last Max_Length characters of
492 -- New_Item.
494 Super_To_String (Source) = New_Item
495 (New_Item'Last - Source.Max_Length + 1 .. New_Item'Last)),
497 others -- Drop = Right
498 =>
499 Super_Length (Source) = Source.Max_Length
500 and then
501 Super_Slice (Source, 1, Super_Length (Source'Old)) =
502 Super_To_String (Source'Old)
503 and then
504 (if Super_Length (Source'Old) < Source.Max_Length then
505 Super_Slice (Source,
506 Super_Length (Source'Old) + 1, Source.Max_Length) =
507 New_Item (New_Item'First
508 .. Source.Max_Length - Super_Length (Source'Old) - 1
509 + New_Item'First))),
510 Global => null;
512 procedure Super_Append
513 (Source : in out Super_String;
514 New_Item : Character;
515 Drop : Truncation := Error)
516 with
517 Pre =>
518 (if Super_Length (Source) = Source.Max_Length then Drop /= Error),
519 Contract_Cases =>
520 (Super_Length (Source) < Source.Max_Length
521 =>
522 Super_Length (Source) = Super_Length (Source'Old) + 1
523 and then
524 Super_Slice (Source, 1, Super_Length (Source'Old)) =
525 Super_To_String (Source'Old)
526 and then
527 Super_Element (Source, Super_Length (Source'Old) + 1) = New_Item,
529 Super_Length (Source) = Source.Max_Length and then Drop = Right
530 =>
531 Super_Length (Source) = Source.Max_Length
532 and then Super_To_String (Source) = Super_To_String (Source'Old),
534 others -- Drop = Left
535 =>
536 Super_Length (Source) = Source.Max_Length
537 and then
543 function Concat
546 with
550 and then
553 and then
556 and then
563 function Concat
566 with
569 and then
571 and then
574 and then
578 Right),
581 function Concat
584 with
587 and then
590 and then
597 function Concat
600 with
604 and then
610 function Concat
613 with
618 and then
623 function Super_Element
632 procedure Super_Replace_Element
636 with
639 and then
645 function Super_Slice
651 -- Note: test of High > Length is in accordance with AI95-00128
653 then raise Index_Error
654 else
655 -- Note: in this case, superflat bounds are not a problem, we just
656 -- get the null string in accordance with normal Ada slice rules.
663 function Super_Slice
667 with
668 Pre =>
671 and then
676 procedure Super_Slice
681 with
691 with
694 Global => null;
696 function Equal
697 (Left : Super_String;
698 Right : Super_String) return Boolean renames "=";
700 function Equal
701 (Left : Super_String;
702 Right : String) return Boolean
703 with
704 Post => Equal'Result = (Super_To_String (Left) = Right),
705 Global => null;
707 function Equal
708 (Left : String;
709 Right : Super_String) return Boolean
710 with
711 Post => Equal'Result = (Left = Super_To_String (Right)),
712 Global => null;
714 function Less
715 (Left : Super_String;
716 Right : Super_String) return Boolean
717 with
718 Pre => Left.Max_Length = Right.Max_Length,
719 Post =>
720 Less'Result = (Super_To_String (Left) < Super_To_String (Right)),
721 Global => null;
723 function Less
724 (Left : Super_String;
725 Right : String) return Boolean
726 with
727 Post => Less'Result = (Super_To_String (Left) < Right),
728 Global => null;
730 function Less
731 (Left : String;
732 Right : Super_String) return Boolean
733 with
734 Post => Less'Result = (Left < Super_To_String (Right)),
735 Global => null;
737 function Less_Or_Equal
738 (Left : Super_String;
739 Right : Super_String) return Boolean
740 with
741 Pre => Left.Max_Length = Right.Max_Length,
742 Post =>
743 Less_Or_Equal'Result =
744 (Super_To_String (Left) <= Super_To_String (Right)),
745 Global => null;
747 function Less_Or_Equal
748 (Left : Super_String;
749 Right : String) return Boolean
750 with
751 Post => Less_Or_Equal'Result = (Super_To_String (Left) <= Right),
752 Global => null;
754 function Less_Or_Equal
755 (Left : String;
756 Right : Super_String) return Boolean
757 with
758 Post => Less_Or_Equal'Result = (Left <= Super_To_String (Right)),
759 Global => null;
761 function Greater
762 (Left : Super_String;
763 Right : Super_String) return Boolean
764 with
765 Pre => Left.Max_Length = Right.Max_Length,
766 Post =>
767 Greater'Result = (Super_To_String (Left) > Super_To_String (Right)),
768 Global => null;
770 function Greater
771 (Left : Super_String;
772 Right : String) return Boolean
773 with
774 Post => Greater'Result = (Super_To_String (Left) > Right),
775 Global => null;
777 function Greater
778 (Left : String;
779 Right : Super_String) return Boolean
780 with
781 Post => Greater'Result = (Left > Super_To_String (Right)),
782 Global => null;
784 function Greater_Or_Equal
785 (Left : Super_String;
786 Right : Super_String) return Boolean
787 with
788 Pre => Left.Max_Length = Right.Max_Length,
789 Post =>
790 Greater_Or_Equal'Result =
791 (Super_To_String (Left) >= Super_To_String (Right)),
792 Global => null;
794 function Greater_Or_Equal
795 (Left : Super_String;
796 Right : String) return Boolean
797 with
798 Post => Greater_Or_Equal'Result = (Super_To_String (Left) >= Right),
799 Global => null;
801 function Greater_Or_Equal
802 (Left : String;
803 Right : Super_String) return Boolean
804 with
805 Post => Greater_Or_Equal'Result = (Left >= Super_To_String (Right)),
806 Global => null;
808 ----------------------
809 -- Search Functions --
810 ----------------------
812 function Super_Index
813 (Source : Super_String;
814 Pattern : String;
815 Going : Direction := Forward;
816 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
817 with
818 Pre => Pattern'Length > 0,
819 Post => Super_Index'Result <= Super_Length (Source),
820 Contract_Cases =>
822 -- If Source is the empty string, then 0 is returned
824 (Super_Length (Source) = 0
825 =>
826 Super_Index'Result = 0,
828 -- If some slice of Source matches Pattern, then a valid index is
829 -- returned.
831 Super_Length (Source) > 0
832 and then
833 (for some J in 1 .. Super_Length (Source) - (Pattern'Length - 1) =>
834 Search.Match (Super_To_String (Source), Pattern, Mapping, J))
835 =>
836 -- The result is in the considered range of Source
838 Super_Index'Result in
839 1 .. Super_Length (Source) - (Pattern'Length - 1)
841 -- The slice beginning at the returned index matches Pattern
843 and then Search.Match
844 (Super_To_String (Source), Pattern, Mapping, Super_Index'Result)
846 -- The result is the smallest or largest index which satisfies
847 -- the matching, respectively when Going = Forward and Going =
848 -- Backward.
850 and then
851 (for all J in 1 .. Super_Length (Source) =>
852 (if (if Going = Forward
853 then J <= Super_Index'Result - 1
854 else J - 1 in Super_Index'Result
855 .. Super_Length (Source) - Pattern'Length)
856 then not (Search.Match
857 (Super_To_String (Source), Pattern, Mapping, J)))),
859 -- Otherwise, 0 is returned
861 others
862 =>
863 Super_Index'Result = 0),
864 Global => null;
866 function Super_Index
867 (Source : Super_String;
868 Pattern : String;
869 Going : Direction := Forward;
870 Mapping : Maps.Character_Mapping_Function) return Natural
871 with
872 Pre => Pattern'Length /= 0 and then Mapping /= null,
873 Post => Super_Index'Result <= Super_Length (Source),
874 Contract_Cases =>
876 -- If Source is the empty string, then 0 is returned
878 (Super_Length (Source) = 0
879 =>
880 Super_Index'Result = 0,
882 -- If some slice of Source matches Pattern, then a valid index is
883 -- returned.
885 Super_Length (Source) > 0
886 and then
887 (for some J in 1 .. Super_Length (Source) - (Pattern'Length - 1) =>
888 Search.Match (Super_To_String (Source), Pattern, Mapping, J))
889 =>
890 -- The result is in the considered range of Source
892 Super_Index'Result in
893 1 .. Super_Length (Source) - (Pattern'Length - 1)
895 -- The slice beginning at the returned index matches Pattern
897 and then Search.Match
898 (Super_To_String (Source), Pattern, Mapping, Super_Index'Result)
900 -- The result is the smallest or largest index which satisfies
901 -- the matching, respectively when Going = Forward and Going =
902 -- Backward.
904 and then
905 (for all J in 1 .. Super_Length (Source) =>
906 (if (if Going = Forward
907 then J <= Super_Index'Result - 1
908 else J - 1 in Super_Index'Result
909 .. Super_Length (Source) - Pattern'Length)
910 then not (Search.Match
911 (Super_To_String (Source), Pattern, Mapping, J)))),
913 -- Otherwise, 0 is returned
915 others
916 =>
917 Super_Index'Result = 0),
918 Global => null;
920 function Super_Index
921 (Source : Super_String;
922 Set : Maps.Character_Set;
923 Test : Membership := Inside;
924 Going : Direction := Forward) return Natural
925 with
926 Post => Super_Index'Result <= Super_Length (Source),
927 Contract_Cases =>
929 -- If no character of Source satisfies the property Test on Set,
930 -- then 0 is returned.
932 ((for all C of Super_To_String (Source) =>
933 (Test = Inside) /= Maps.Is_In (C, Set))
934 =>
935 Super_Index'Result = 0,
937 -- Otherwise, an index in the range of Source is returned
939 others
940 =>
941 -- The result is in the range of Source
943 Super_Index'Result in 1 .. Super_Length (Source)
945 -- The character at the returned index satisfies the property
946 -- Test on Set.
948 and then
949 (Test = Inside) =
950 Maps.Is_In (Super_Element (Source, Super_Index'Result), Set)
952 -- The result is the smallest or largest index which satisfies
953 -- the property, respectively when Going = Forward and Going =
954 -- Backward.
956 and then
957 (for all J in 1 .. Super_Length (Source) =>
958 (if J /= Super_Index'Result
959 and then (J < Super_Index'Result) = (Going = Forward)
960 then (Test = Inside)
961 /= Maps.Is_In (Super_Element (Source, J), Set)))),
962 Global => null;
964 function Super_Index
965 (Source : Super_String;
966 Pattern : String;
967 From : Positive;
968 Going : Direction := Forward;
969 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
970 with
971 Pre =>
972 (if Super_Length (Source) /= 0 then From <= Super_Length (Source))
973 and then Pattern'Length /= 0,
974 Post => Super_Index'Result <= Super_Length (Source),
975 Contract_Cases =>
977 -- If Source is the empty string, then 0 is returned
979 (Super_Length (Source) = 0
980 =>
981 Super_Index'Result = 0,
983 -- If some slice of Source matches Pattern, then a valid index is
984 -- returned.
986 Super_Length (Source) > 0
987 and then
988 (for some J in
989 (if Going = Forward then From else 1)
990 .. (if Going = Forward then Super_Length (Source) else From)
991 - (Pattern'Length - 1) =>
992 Search.Match (Super_To_String (Source), Pattern, Mapping, J))
993 =>
994 -- The result is in the considered range of Source
996 Super_Index'Result in
997 (if Going = Forward then From else 1)
998 .. (if Going = Forward then Super_Length (Source) else From)
999 - (Pattern'Length - 1)
1001 -- The slice beginning at the returned index matches Pattern
1003 and then Search.Match
1004 (Super_To_String (Source), Pattern, Mapping, Super_Index'Result)
1006 -- The result is the smallest or largest index which satisfies
1007 -- the matching, respectively when Going = Forward and Going =
1008 -- Backward.
1010 and then
1011 (for all J in 1 .. Super_Length (Source) =>
1012 (if (if Going = Forward
1013 then J in From .. Super_Index'Result - 1
1014 else J - 1 in Super_Index'Result
1015 .. From - Pattern'Length)
1016 then not (Search.Match
1017 (Super_To_String (Source), Pattern, Mapping, J)))),
1019 -- Otherwise, 0 is returned
1021 others
1022 =>
1023 Super_Index'Result = 0),
1024 Global => null;
1026 function Super_Index
1027 (Source : Super_String;
1028 Pattern : String;
1029 From : Positive;
1030 Going : Direction := Forward;
1031 Mapping : Maps.Character_Mapping_Function) return Natural
1032 with
1033 Pre =>
1034 (if Super_Length (Source) /= 0 then From <= Super_Length (Source))
1035 and then Pattern'Length /= 0
1036 and then Mapping /= null,
1037 Post => Super_Index'Result <= Super_Length (Source),
1038 Contract_Cases =>
1040 -- If Source is the empty string, then 0 is returned
1042 (Super_Length (Source) = 0
1043 =>
1044 Super_Index'Result = 0,
1046 -- If some slice of Source matches Pattern, then a valid index is
1047 -- returned.
1049 Super_Length (Source) > 0
1050 and then
1051 (for some J in
1052 (if Going = Forward then From else 1)
1053 .. (if Going = Forward then Super_Length (Source) else From)
1054 - (Pattern'Length - 1) =>
1055 Search.Match (Super_To_String (Source), Pattern, Mapping, J))
1056 =>
1057 -- The result is in the considered range of Source
1059 Super_Index'Result in
1060 (if Going = Forward then From else 1)
1061 .. (if Going = Forward then Super_Length (Source) else From)
1062 - (Pattern'Length - 1)
1064 -- The slice beginning at the returned index matches Pattern
1066 and then Search.Match
1067 (Super_To_String (Source), Pattern, Mapping, Super_Index'Result)
1069 -- The result is the smallest or largest index which satisfies
1070 -- the matching, respectively when Going = Forward and Going =
1071 -- Backward.
1073 and then
1074 (for all J in 1 .. Super_Length (Source) =>
1075 (if (if Going = Forward
1076 then J in From .. Super_Index'Result - 1
1077 else J - 1 in Super_Index'Result
1078 .. From - Pattern'Length)
1079 then not (Search.Match
1080 (Super_To_String (Source), Pattern, Mapping, J)))),
1082 -- Otherwise, 0 is returned
1084 others
1085 =>
1086 Super_Index'Result = 0),
1087 Global => null;
1089 function Super_Index
1090 (Source : Super_String;
1091 Set : Maps.Character_Set;
1092 From : Positive;
1093 Test : Membership := Inside;
1094 Going : Direction := Forward) return Natural
1095 with
1096 Pre =>
1097 (if Super_Length (Source) /= 0 then From <= Super_Length (Source)),
1098 Post => Super_Index'Result <= Super_Length (Source),
1099 Contract_Cases =>
1101 -- If Source is the empty string, or no character of the considered
1102 -- slice of Source satisfies the property Test on Set, then 0 is
1103 -- returned.
1105 (Super_Length (Source) = 0
1106 or else
1107 (for all J in 1 .. Super_Length (Source) =>
1108 (if J = From or else (J > From) = (Going = Forward) then
1109 (Test = Inside) /=
1110 Maps.Is_In (Super_Element (Source, J), Set)))
1111 =>
1112 Super_Index'Result = 0,
1114 -- Otherwise, an index in the considered range of Source is returned
1116 others
1117 =>
1118 -- The result is in the considered range of Source
1120 Super_Index'Result in 1 .. Super_Length (Source)
1121 and then
1122 (Super_Index'Result = From
1123 or else (Super_Index'Result > From) = (Going = Forward))
1125 -- The character at the returned index satisfies the property
1126 -- Test on Set.
1128 and then
1129 (Test = Inside) =
1130 Maps.Is_In (Super_Element (Source, Super_Index'Result), Set)
1132 -- The result is the smallest or largest index which satisfies
1133 -- the property, respectively when Going = Forward and Going =
1134 -- Backward.
1136 and then
1137 (for all J in 1 .. Super_Length (Source) =>
1138 (if J /= Super_Index'Result
1139 and then (J < Super_Index'Result) = (Going = Forward)
1140 and then (J = From
1141 or else (J > From) = (Going = Forward))
1142 then (Test = Inside)
1143 /= Maps.Is_In (Super_Element (Source, J), Set)))),
1144 Global => null;
1146 function Super_Index_Non_Blank
1147 (Source : Super_String;
1148 Going : Direction := Forward) return Natural
1149 with
1150 Post => Super_Index_Non_Blank'Result <= Super_Length (Source),
1151 Contract_Cases =>
1153 -- If all characters of Source are Space characters, then 0 is
1154 -- returned.
1157 =>
1158 Super_Index_Non_Blank'Result = 0,
1160 -- Otherwise, an index in the range of Source is returned
1162 others
1163 =>
1164 -- The result is in the range of Source
1166 Super_Index_Non_Blank'Result in 1 .. Super_Length (Source)
1168 -- The character at the returned index is not a Space character
1170 and then
1173 -- The result is the smallest or largest index which is not a
1174 -- Space character, respectively when Going = Forward and Going
1175 -- = Backward.
1177 and then
1178 (for all J in 1 .. Super_Length (Source) =>
1179 (if J /= Super_Index_Non_Blank'Result
1180 and then
1181 (J < Super_Index_Non_Blank'Result) = (Going = Forward)
1183 Global => null;
1185 function Super_Index_Non_Blank
1186 (Source : Super_String;
1187 From : Positive;
1188 Going : Direction := Forward) return Natural
1189 with
1190 Pre =>
1191 (if Super_Length (Source) /= 0 then From <= Super_Length (Source)),
1192 Post => Super_Index_Non_Blank'Result <= Super_Length (Source),
1193 Contract_Cases =>
1195 -- If Source is the empty string, or all characters of the
1196 -- considered slice of Source are Space characters, then 0
1197 -- is returned.
1199 (Super_Length (Source) = 0
1200 or else
1201 (for all J in 1 .. Super_Length (Source) =>
1202 (if J = From or else (J > From) = (Going = Forward) then
1204 =>
1205 Super_Index_Non_Blank'Result = 0,
1207 -- Otherwise, an index in the considered range of Source is returned
1209 others
1210 =>
1211 -- The result is in the considered range of Source
1213 Super_Index_Non_Blank'Result in 1 .. Super_Length (Source)
1214 and then
1215 (Super_Index_Non_Blank'Result = From
1216 or else
1217 (Super_Index_Non_Blank'Result > From) = (Going = Forward))
1219 -- The character at the returned index is not a Space character
1221 and then
1224 -- The result is the smallest or largest index which isn't a
1225 -- Space character, respectively when Going = Forward and Going
1226 -- = Backward.
1228 and then
1229 (for all J in 1 .. Super_Length (Source) =>
1230 (if J /= Super_Index_Non_Blank'Result
1231 and then
1232 (J < Super_Index_Non_Blank'Result) = (Going = Forward)
1233 and then (J = From
1234 or else (J > From) = (Going = Forward))
1236 Global => null;
1238 function Super_Count
1239 (Source : Super_String;
1240 Pattern : String;
1241 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
1242 with
1243 Pre => Pattern'Length /= 0,
1244 Global => null;
1246 function Super_Count
1247 (Source : Super_String;
1248 Pattern : String;
1249 Mapping : Maps.Character_Mapping_Function) return Natural
1250 with
1251 Pre => Pattern'Length /= 0 and then Mapping /= null,
1252 Global => null;
1254 function Super_Count
1255 (Source : Super_String;
1256 Set : Maps.Character_Set) return Natural
1257 with
1258 Global => null;
1260 procedure Super_Find_Token
1261 (Source : Super_String;
1262 Set : Maps.Character_Set;
1263 From : Positive;
1264 Test : Membership;
1265 First : out Positive;
1266 Last : out Natural)
1267 with
1268 Pre =>
1269 (if Super_Length (Source) /= 0 then From <= Super_Length (Source)),
1270 Contract_Cases =>
1272 -- If Source is the empty string, or if no character of the
1273 -- considered slice of Source satisfies the property Test on
1274 -- Set, then First is set to From and Last is set to 0.
1276 (Super_Length (Source) = 0
1277 or else
1278 (for all J in From .. Super_Length (Source) =>
1279 (Test = Inside) /= Maps.Is_In (Super_Element (Source, J), Set))
1280 =>
1281 First = From and then Last = 0,
1283 -- Otherwise, First and Last are set to valid indexes
1285 others
1286 =>
1287 -- First and Last are in the considered range of Source
1289 First in From .. Super_Length (Source)
1290 and then Last in First .. Super_Length (Source)
1292 -- No character between From and First satisfies the property
1293 -- Test on Set.
1295 and then
1296 (for all J in From .. First - 1 =>
1297 (Test = Inside) /=
1298 Maps.Is_In (Super_Element (Source, J), Set))
1300 -- All characters between First and Last satisfy the property
1301 -- Test on Set.
1303 and then
1304 (for all J in First .. Last =>
1305 (Test = Inside) =
1306 Maps.Is_In (Super_Element (Source, J), Set))
1308 -- If Last is not Source'Last, then the character at position
1309 -- Last + 1 does not satify the property Test on Set.
1311 and then
1312 (if Last < Super_Length (Source)
1313 then
1314 (Test = Inside) /=
1315 Maps.Is_In (Super_Element (Source, Last + 1), Set))),
1316 Global => null;
1318 procedure Super_Find_Token
1319 (Source : Super_String;
1320 Set : Maps.Character_Set;
1321 Test : Membership;
1322 First : out Positive;
1323 Last : out Natural)
1324 with
1325 Contract_Cases =>
1327 -- If Source is the empty string, or if no character of the considered
1328 -- slice of Source satisfies the property Test on Set, then First is
1329 -- set to 1 and Last is set to 0.
1331 (Super_Length (Source) = 0
1332 or else
1333 (for all J in 1 .. Super_Length (Source) =>
1334 (Test = Inside) /= Maps.Is_In (Super_Element (Source, J), Set))
1335 =>
1336 First = 1 and then Last = 0,
1338 -- Otherwise, First and Last are set to valid indexes
1340 others
1341 =>
1342 -- First and Last are in the considered range of Source
1344 First in 1 .. Super_Length (Source)
1345 and then Last in First .. Super_Length (Source)
1347 -- No character between 1 and First satisfies the property Test on
1348 -- Set.
1350 and then
1351 (for all J in 1 .. First - 1 =>
1352 (Test = Inside) /=
1353 Maps.Is_In (Super_Element (Source, J), Set))
1355 -- All characters between First and Last satisfy the property
1356 -- Test on Set.
1358 and then
1359 (for all J in First .. Last =>
1360 (Test = Inside) =
1361 Maps.Is_In (Super_Element (Source, J), Set))
1363 -- If Last is not Source'Last, then the character at position
1364 -- Last + 1 does not satify the property Test on Set.
1366 and then
1367 (if Last < Super_Length (Source)
1368 then
1369 (Test = Inside) /=
1370 Maps.Is_In (Super_Element (Source, Last + 1), Set))),
1371 Global => null;
1373 ------------------------------------
1374 -- String Translation Subprograms --
1375 ------------------------------------
1377 function Super_Translate
1378 (Source : Super_String;
1379 Mapping : Maps.Character_Mapping) return Super_String
1380 with
1381 Post => Super_Translate'Result.Max_Length = Source.Max_Length
1382 and then Super_Length (Super_Translate'Result) = Super_Length (Source)
1383 and then
1384 (for all K in 1 .. Super_Length (Source) =>
1385 Super_Element (Super_Translate'Result, K) =
1386 Ada.Strings.Maps.Value (Mapping, Super_Element (Source, K))),
1387 Global => null;
1389 procedure Super_Translate
1390 (Source : in out Super_String;
1391 Mapping : Maps.Character_Mapping)
1392 with
1393 Post => Super_Length (Source) = Super_Length (Source'Old)
1394 and then
1395 (for all K in 1 .. Super_Length (Source) =>
1396 Super_Element (Source, K) =
1397 Ada.Strings.Maps.Value (Mapping, Super_Element (Source'Old, K))),
1398 Global => null;
1400 function Super_Translate
1401 (Source : Super_String;
1402 Mapping : Maps.Character_Mapping_Function) return Super_String
1403 with
1404 Pre => Mapping /= null,
1405 Post => Super_Translate'Result.Max_Length = Source.Max_Length
1406 and then Super_Length (Super_Translate'Result) = Super_Length (Source)
1407 and then
1408 (for all K in 1 .. Super_Length (Source) =>
1409 Super_Element (Super_Translate'Result, K) =
1410 Mapping (Super_Element (Source, K))),
1411 Global => null;
1412 pragma Annotate (GNATprove, False_Positive,
1413 "call via access-to-subprogram",
1414 "function Mapping must always terminate");
1416 procedure Super_Translate
1417 (Source : in out Super_String;
1418 Mapping : Maps.Character_Mapping_Function)
1419 with
1420 Pre => Mapping /= null,
1421 Post => Super_Length (Source) = Super_Length (Source'Old)
1422 and then
1423 (for all K in 1 .. Super_Length (Source) =>
1424 Super_Element (Source, K) =
1425 Mapping (Super_Element (Source'Old, K))),
1426 Global => null;
1427 pragma Annotate (GNATprove, False_Positive,
1428 "call via access-to-subprogram",
1429 "function Mapping must always terminate");
1431 ---------------------------------------
1432 -- String Transformation Subprograms --
1433 ---------------------------------------
1435 function Super_Replace_Slice
1436 (Source : Super_String;
1437 Low : Positive;
1438 High : Natural;
1439 By : String;
1440 Drop : Truncation := Error) return Super_String
1441 with
1442 Pre =>
1443 Low - 1 <= Super_Length (Source)
1444 and then
1445 (if Drop = Error
1446 then (if High >= Low
1447 then Low - 1
1448 <= Source.Max_Length - By'Length
1449 - Integer'Max (Super_Length (Source) - High, 0)
1450 else Super_Length (Source) <=
1451 Source.Max_Length - By'Length)),
1452 Post =>
1453 Super_Replace_Slice'Result.Max_Length = Source.Max_Length,
1454 Contract_Cases =>
1455 (Low - 1 <= Source.Max_Length - By'Length - Integer'Max
1456 (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
1457 =>
1458 -- Total length is lower than Max_Length: nothing is dropped
1460 -- Note that if High < Low, the insertion is done before Low, so in
1461 -- all cases the starting position of the slice of Source remaining
1462 -- after the replaced Slice is Integer'Max (High + 1, Low).
1464 Super_Length (Super_Replace_Slice'Result) =
1465 Low - 1 + By'Length + Integer'Max
1466 (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
1467 and then
1470 and then
1473 and then
1476 Low + By'Length,
1477 Super_Length (Super_Replace_Slice'Result))) =
1478 Super_Slice (Source,
1479 Integer'Max (High + 1, Low), Super_Length (Source))),
1481 Low - 1 > Source.Max_Length - By'Length - Integer'Max
1482 (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
1483 and then Drop = Left
1484 =>
1485 -- Final_Super_Slice is the length of the slice of Source remaining
1486 -- after the replaced part.
1487 (declare
1488 Final_Super_Slice : constant Natural :=
1489 Integer'Max
1490 (Super_Length (Source) - Integer'Max (High, Low - 1), 0);
1491 begin
1492 -- The result is of maximal length and ends by the last
1493 -- Final_Super_Slice characters of Source.
1495 Super_Length (Super_Replace_Slice'Result) = Source.Max_Length
1496 and then
1497 (if Final_Super_Slice > 0 then
1504 -- Depending on when we reach Max_Length, either the first
1505 -- part of Source is fully dropped and By is partly dropped,
1506 -- or By is fully added and the first part of Source is partly
1507 -- dropped.
1509 and then
1512 -- The first (possibly zero) characters of By are dropped
1526 By
1528 -- The first characters of Source (1 .. Low - 1) are
1529 -- dropped.
1531 and then
1533 Source.Max_Length - Final_Super_Slice - By'Length)) =
1534 Super_Slice (Source,
1535 Low - Source.Max_Length
1536 + Final_Super_Slice + By'Length,
1537 Low - 1))),
1539 others -- Drop = Right
1540 =>
1541 -- The result is of maximal length and starts by the first Low - 1
1542 -- characters of Source.
1544 Super_Length (Super_Replace_Slice'Result) = Source.Max_Length
1545 and then
1549 -- Depending on when we reach Max_Length, either the last part
1550 -- of Source is fully dropped and By is partly dropped, or By
1551 -- is fully added and the last part of Source is partly dropped.
1553 and then
1556 -- The last characters of By are dropped
1567 -- Then Source starting from Natural'Max (High + 1, Low)
1568 -- is added but the last characters are dropped.
1570 and then
1572 Low + By'Length, Source.Max_Length)) =
1573 Super_Slice (Source, Integer'Max (High + 1, Low),
1574 Integer'Max (High + 1, Low) +
1575 (Source.Max_Length - Low - By'Length)))),
1576 Global => null;
1578 procedure Super_Replace_Slice
1579 (Source : in out Super_String;
1580 Low : Positive;
1581 High : Natural;
1582 By : String;
1583 Drop : Truncation := Error)
1584 with
1585 Pre =>
1586 Low - 1 <= Super_Length (Source)
1587 and then
1588 (if Drop = Error
1589 then (if High >= Low
1590 then Low - 1
1591 <= Source.Max_Length - By'Length
1592 - Natural'Max (Super_Length (Source) - High, 0)
1593 else Super_Length (Source) <=
1594 Source.Max_Length - By'Length)),
1595 Contract_Cases =>
1596 (Low - 1 <= Source.Max_Length - By'Length - Integer'Max
1597 (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
1598 =>
1599 -- Total length is lower than Max_Length: nothing is dropped
1601 -- Note that if High < Low, the insertion is done before Low, so in
1602 -- all cases the starting position of the slice of Source remaining
1603 -- after the replaced Slice is Integer'Max (High + 1, Low).
1605 Super_Length (Source) = Low - 1 + By'Length + Integer'Max
1606 (Super_Length (Source'Old) - Integer'Max (High, Low - 1), 0)
1607 and then
1611 and then
1614 Low + By'Length, Super_Length (Source))) =
1615 Super_Slice (Source'Old,
1616 Integer'Max (High + 1, Low),
1617 Super_Length (Source'Old))),
1619 Low - 1 > Source.Max_Length - By'Length - Integer'Max
1620 (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
1621 and then Drop = Left
1622 =>
1623 -- Final_Super_Slice is the length of the slice of Source remaining
1624 -- after the replaced part.
1625 (declare
1626 Final_Super_Slice : constant Natural :=
1627 Integer'Max (0,
1628 Super_Length (Source'Old) - Integer'Max (High, Low - 1));
1629 begin
1630 -- The result is of maximal length and ends by the last
1631 -- Final_Super_Slice characters of Source.
1633 Super_Length (Source) = Source.Max_Length
1634 and then
1635 (if Final_Super_Slice > 0 then
1643 -- Depending on when we reach Max_Length, either the first
1644 -- part of Source is fully dropped and By is partly dropped,
1645 -- or By is fully added and the first part of Source is partly
1646 -- dropped.
1648 and then
1650 then
1651 -- The first characters of By are dropped
1666 -- The first characters of Source (1 .. Low - 1) are
1667 -- dropped.
1669 and then
1671 Source.Max_Length - Final_Super_Slice - By'Length)) =
1672 Super_Slice (Source'Old,
1673 Low - Source.Max_Length + Final_Super_Slice
1674 + By'Length,
1675 Low - 1))),
1677 others -- Drop = Right
1678 =>
1679 -- The result is of maximal length and starts by the first Low - 1
1680 -- characters of Source.
1682 Super_Length (Source) = Source.Max_Length
1683 and then
1687 -- Depending on when we reach Max_Length, either the last part
1688 -- of Source is fully dropped and By is partly dropped, or By
1689 -- is fully added and the last part of Source is partly dropped.
1691 and then
1694 -- The last characters of By are dropped
1703 -- Then Source starting from Natural'Max (High + 1, Low)
1704 -- is added but the last characters are dropped.
1706 and then
1708 Low + By'Length, Source.Max_Length)) =
1709 Super_Slice (Source'Old, Integer'Max (High + 1, Low),
1710 Integer'Max (High + 1, Low) +
1711 (Source.Max_Length - Low - By'Length)))),
1712 Global => null;
1714 function Super_Insert
1715 (Source : Super_String;
1716 Before : Positive;
1717 New_Item : String;
1718 Drop : Truncation := Error) return Super_String
1719 with
1720 Pre =>
1721 Before - 1 <= Super_Length (Source)
1722 and then
1723 (if New_Item'Length > Source.Max_Length - Super_Length (Source)
1724 then Drop /= Error),
1725 Post => Super_Insert'Result.Max_Length = Source.Max_Length,
1726 Contract_Cases =>
1727 (Super_Length (Source) <= Source.Max_Length - New_Item'Length
1728 =>
1729 -- Total length is lower than Max_Length: nothing is dropped
1731 Super_Length (Super_Insert'Result) =
1732 Super_Length (Source) + New_Item'Length
1733 and then
1736 and then
1739 New_Item
1740 and then
1743 Before + New_Item'Length,
1744 Super_Length (Super_Insert'Result))) =
1745 Super_Slice (Source, Before, Super_Length (Source))),
1747 Super_Length (Source) > Source.Max_Length - New_Item'Length
1748 and then Drop = Left
1749 =>
1750 -- The result is of maximal length and ends by the last characters
1751 -- of Source.
1753 Super_Length (Super_Insert'Result) = Source.Max_Length
1754 and then
1755 (if Before <= Super_Length (Source) then
1761 -- Depending on when we reach Max_Length, either the first part
1762 -- of Source is fully dropped and New_Item is partly dropped, or
1763 -- New_Item is fully added and the first part of Source is partly
1764 -- dropped.
1766 and then
1769 then
1770 -- The first characters of New_Item are dropped
1773 then
1776 New_Item
1787 New_Item
1789 -- The first characters of Source (1 .. Before - 1) are
1790 -- dropped.
1792 and then
1794 1, Source.Max_Length - Super_Length (Source)
1795 - New_Item'Length - 1 + Before)) =
1796 Super_Slice (Source,
1797 Super_Length (Source) - Source.Max_Length
1798 + New_Item'Length + 1,
1799 Before - 1)),
1801 others -- Drop = Right
1802 =>
1803 -- The result is of maximal length and starts by the first
1804 -- characters of Source.
1806 Super_Length (Super_Insert'Result) = Source.Max_Length
1807 and then
1811 -- Depending on when we reach Max_Length, either the last part
1812 -- of Source is fully dropped and New_Item is partly dropped, or
1813 -- New_Item is fully added and the last part of Source is partly
1814 -- dropped.
1816 and then
1819 -- The last characters of New_Item are dropped
1829 New_Item
1831 -- Then Source starting from Before is added but the
1832 -- last characters are dropped.
1834 and then
1836 Before + New_Item'Length, Source.Max_Length)) =
1837 Super_Slice (Source,
1838 Before, Source.Max_Length - New_Item'Length))),
1839 Global => null;
1841 procedure Super_Insert
1842 (Source : in out Super_String;
1843 Before : Positive;
1844 New_Item : String;
1845 Drop : Truncation := Error)
1846 with
1847 Pre =>
1848 Before - 1 <= Super_Length (Source)
1849 and then
1850 (if New_Item'Length > Source.Max_Length - Super_Length (Source)
1851 then Drop /= Error),
1852 Contract_Cases =>
1853 (Super_Length (Source) <= Source.Max_Length - New_Item'Length
1854 =>
1855 -- Total length is lower than Max_Length: nothing is dropped
1857 Super_Length (Source) = Super_Length (Source'Old) + New_Item'Length
1858 and then
1861 and then
1863 New_Item
1864 and then
1867 Before + New_Item'Length, Super_Length (Source))) =
1868 Super_Slice (Source'Old,
1869 Before, Super_Length (Source'Old))),
1871 Super_Length (Source) > Source.Max_Length - New_Item'Length
1872 and then Drop = Left
1873 =>
1874 -- The result is of maximal length and ends by the last characters
1875 -- of Source.
1877 Super_Length (Source) = Source.Max_Length
1878 and then
1879 (if Before <= Super_Length (Source'Old) then
1886 -- Depending on when we reach Max_Length, either the first part
1887 -- of Source is fully dropped and New_Item is partly dropped, or
1888 -- New_Item is fully added and the first part of Source is partly
1889 -- dropped.
1891 and then
1894 then
1895 -- The first characters of New_Item are dropped
1898 then
1902 New_Item
1913 = New_Item
1915 -- The first characters of Source (1 .. Before - 1) are
1916 -- dropped.
1918 and then
1920 Source.Max_Length - Super_Length (Source'Old)
1921 - New_Item'Length - 1 + Before)) =
1922 Super_Slice (Source'Old,
1923 Super_Length (Source'Old)
1924 - Source.Max_Length + New_Item'Length + 1,
1925 Before - 1)),
1927 others -- Drop = Right
1928 =>
1929 -- The result is of maximal length and starts by the first
1930 -- characters of Source.
1932 Super_Length (Source) = Source.Max_Length
1933 and then
1937 -- Depending on when we reach Max_Length, either the last part
1938 -- of Source is fully dropped and New_Item is partly dropped, or
1939 -- New_Item is fully added and the last part of Source is partly
1940 -- dropped.
1942 and then
1945 -- The last characters of New_Item are dropped
1954 New_Item
1956 -- Then Source starting from Before is added but the
1957 -- last characters are dropped.
1959 and then
1961 Before + New_Item'Length, Source.Max_Length)) =
1962 Super_Slice (Source'Old,
1963 Before, Source.Max_Length - New_Item'Length))),
1964 Global => null;
1966 function Super_Overwrite
1967 (Source : Super_String;
1968 Position : Positive;
1969 New_Item : String;
1970 Drop : Truncation := Error) return Super_String
1971 with
1972 Pre =>
1973 Position - 1 <= Super_Length (Source)
1974 and then (if New_Item'Length > Source.Max_Length - (Position - 1)
1975 then Drop /= Error),
1976 Post => Super_Overwrite'Result.Max_Length = Source.Max_Length,
1977 Contract_Cases =>
1978 (Position - 1 <= Source.Max_Length - New_Item'Length
1979 =>
1980 -- The length is unchanged, unless New_Item overwrites further than
1981 -- the end of Source. In this contract case, we suppose New_Item
1982 -- doesn't overwrite further than Max_Length.
1984 Super_Length (Super_Overwrite'Result) =
1985 Integer'Max (Super_Length (Source), Position - 1 + New_Item'Length)
1986 and then
1991 New_Item
1992 and then
1995 -- There are some unchanged characters of Source remaining
1996 -- after New_Item.
1999 Position + New_Item'Length, Super_Length (Source))) =
2000 Super_Slice (Source,
2001 Position + New_Item'Length, Super_Length (Source))),
2003 Position - 1 > Source.Max_Length - New_Item'Length and then Drop = Left
2004 =>
2005 Super_Length (Super_Overwrite'Result) = Source.Max_Length
2007 -- If a part of the result has to be dropped, it means New_Item is
2008 -- overwriting further than the end of Source. Thus the result is
2009 -- necessarily ending by New_Item. However, we don't know whether
2010 -- New_Item covers all Max_Length characters or some characters of
2011 -- Source are remaining at the left.
2013 and then
2014 (if New_Item'Length >= Source.Max_Length then
2016 -- New_Item covers all Max_Length characters
2018 Super_To_String (Super_Overwrite'Result) =
2019 New_Item
2020 (New_Item'Last - Source.Max_Length + 1 .. New_Item'Last)
2021 else
2022 -- New_Item fully appears at the end
2024 Super_Slice (Super_Overwrite'Result,
2025 Source.Max_Length - New_Item'Length + 1,
2026 Source.Max_Length) =
2027 New_Item
2029 -- The left of Source is cut
2031 and then
2039 =>
2040 -- The result is of maximal length and starts by the first
2041 -- characters of Source.
2044 and then
2046 Super_Slice (Source, 1, Position - 1)
2048 -- Then New_Item is written until Max_Length
2050 and then Super_Slice (Super_Overwrite'Result,
2051 Position, Source.Max_Length) =
2052 New_Item (New_Item'First
2053 .. Source.Max_Length - Position + New_Item'First)),
2054 Global => null;
2056 procedure Super_Overwrite
2057 (Source : in out Super_String;
2058 Position : Positive;
2059 New_Item : String;
2060 Drop : Truncation := Error)
2061 with
2062 Pre =>
2063 Position - 1 <= Super_Length (Source)
2064 and then (if New_Item'Length > Source.Max_Length - (Position - 1)
2065 then Drop /= Error),
2066 Contract_Cases =>
2067 (Position - 1 <= Source.Max_Length - New_Item'Length
2068 =>
2069 -- The length is unchanged, unless New_Item overwrites further than
2070 -- the end of Source. In this contract case, we suppose New_Item
2071 -- doesn't overwrite further than Max_Length.
2073 Super_Length (Source) = Integer'Max
2074 (Super_Length (Source'Old), Position - 1 + New_Item'Length)
2075 and then
2080 New_Item
2081 and then
2083 then
2084 -- There are some unchanged characters of Source remaining
2085 -- after New_Item.
2088 Position + New_Item'Length, Super_Length (Source'Old))) =
2089 Super_Slice (Source'Old,
2090 Position + New_Item'Length, Super_Length (Source'Old))),
2092 Position - 1 > Source.Max_Length - New_Item'Length and then Drop = Left
2093 =>
2094 Super_Length (Source) = Source.Max_Length
2096 -- If a part of the result has to be dropped, it means New_Item is
2097 -- overwriting further than the end of Source. Thus the result is
2098 -- necessarily ending by New_Item. However, we don't know whether
2099 -- New_Item covers all Max_Length characters or some characters of
2100 -- Source are remaining at the left.
2102 and then
2103 (if New_Item'Length >= Source.Max_Length then
2105 -- New_Item covers all Max_Length characters
2107 Super_To_String (Source) =
2108 New_Item
2109 (New_Item'Last - Source.Max_Length + 1 .. New_Item'Last)
2110 else
2111 -- New_Item fully appears at the end
2113 Super_Slice (Source,
2114 Source.Max_Length - New_Item'Length + 1,
2115 Source.Max_Length) =
2116 New_Item
2118 -- The left of Source is cut
2120 and then
2128 =>
2129 -- The result is of maximal length and starts by the first
2130 -- characters of Source.
2133 and then
2135 Super_Slice (Source'Old, 1, Position - 1)
2137 -- New_Item is written until Max_Length
2139 and then Super_Slice (Source, Position, Source.Max_Length) =
2140 New_Item (New_Item'First
2141 .. Source.Max_Length - Position + New_Item'First)),
2142 Global => null;
2144 function Super_Delete
2145 (Source : Super_String;
2146 From : Positive;
2147 Through : Natural) return Super_String
2148 with
2149 Pre =>
2150 (if Through >= From then From - 1 <= Super_Length (Source)),
2151 Post => Super_Delete'Result.Max_Length = Source.Max_Length,
2152 Contract_Cases =>
2153 (Through >= From =>
2154 Super_Length (Super_Delete'Result) =
2155 From - 1 + Natural'Max (Super_Length (Source) - Through, 0)
2156 and then
2159 and then
2162 From, Super_Length (Super_Delete'Result))) =
2163 Super_Slice (Source, Through + 1, Super_Length (Source))),
2164 others =>
2165 Super_Delete'Result = Source),
2166 Global => null;
2168 procedure Super_Delete
2169 (Source : in out Super_String;
2170 From : Positive;
2171 Through : Natural)
2172 with
2173 Pre =>
2174 (if Through >= From then From - 1 <= Super_Length (Source)),
2175 Contract_Cases =>
2176 (Through >= From =>
2177 Super_Length (Source) =
2178 From - 1 + Natural'Max (Super_Length (Source'Old) - Through, 0)
2179 and then
2182 and then
2185 Super_Slice (Source'Old,
2186 Through + 1, Super_Length (Source'Old))),
2187 others =>
2188 Source = Source'Old),
2189 Global => null;
2191 ---------------------------------
2192 -- String Selector Subprograms --
2193 ---------------------------------
2195 function Super_Trim
2196 (Source : Super_String;
2197 Side : Trim_End) return Super_String
2198 with
2199 Post => Super_Trim'Result.Max_Length = Source.Max_Length,
2200 Contract_Cases =>
2202 -- If all characters in Source are Space, the returned string is empty
2205 =>
2206 Super_Length (Super_Trim'Result) = 0,
2208 -- Otherwise, the returned string is a slice of Source
2210 others
2211 =>
2212 (declare
2213 Low : constant Positive :=
2214 (if Side = Right then 1
2215 else Super_Index_Non_Blank (Source, Forward));
2216 High : constant Positive :=
2217 (if Side = Left then Super_Length (Source)
2218 else Super_Index_Non_Blank (Source, Backward));
2219 begin
2220 Super_To_String (Super_Trim'Result) =
2221 Super_Slice (Source, Low, High))),
2222 Global => null;
2224 procedure Super_Trim
2225 (Source : in out Super_String;
2226 Side : Trim_End)
2227 with
2228 Contract_Cases =>
2230 -- If all characters in Source are Space, the returned string is empty
2233 =>
2234 Super_Length (Source) = 0,
2236 -- Otherwise, the returned string is a slice of Source
2238 others
2239 =>
2240 (declare
2241 Low : constant Positive :=
2242 (if Side = Right then 1
2243 else Super_Index_Non_Blank (Source'Old, Forward));
2244 High : constant Positive :=
2245 (if Side = Left then Super_Length (Source'Old)
2246 else Super_Index_Non_Blank (Source'Old, Backward));
2247 begin
2248 Super_To_String (Source) = Super_Slice (Source'Old, Low, High))),
2249 Global => null;
2251 function Super_Trim
2252 (Source : Super_String;
2253 Left : Maps.Character_Set;
2254 Right : Maps.Character_Set) return Super_String
2255 with
2256 Post => Super_Trim'Result.Max_Length = Source.Max_Length,
2257 Contract_Cases =>
2259 -- If all characters in Source are contained in one of the sets Left or
2260 -- Right, then the returned string is empty.
2262 ((for all C of Super_To_String (Source) => Maps.Is_In (C, Left))
2263 or else
2264 (for all C of Super_To_String (Source) => Maps.Is_In (C, Right))
2265 =>
2266 Super_Length (Super_Trim'Result) = 0,
2268 -- Otherwise, the returned string is a slice of Source
2270 others
2271 =>
2272 (declare
2273 Low : constant Positive :=
2274 Super_Index (Source, Left, Outside, Forward);
2275 High : constant Positive :=
2276 Super_Index (Source, Right, Outside, Backward);
2277 begin
2278 Super_To_String (Super_Trim'Result) =
2279 Super_Slice (Source, Low, High))),
2280 Global => null;
2282 procedure Super_Trim
2283 (Source : in out Super_String;
2284 Left : Maps.Character_Set;
2285 Right : Maps.Character_Set)
2286 with
2287 Contract_Cases =>
2289 -- If all characters in Source are contained in one of the sets Left or
2290 -- Right, then the returned string is empty.
2292 ((for all C of Super_To_String (Source) => Maps.Is_In (C, Left))
2293 or else
2294 (for all C of Super_To_String (Source) => Maps.Is_In (C, Right))
2295 =>
2296 Super_Length (Source) = 0,
2298 -- Otherwise, the returned string is a slice of Source
2300 others
2301 =>
2302 (declare
2303 Low : constant Positive :=
2304 Super_Index (Source'Old, Left, Outside, Forward);
2305 High : constant Positive :=
2306 Super_Index (Source'Old, Right, Outside, Backward);
2307 begin
2308 Super_To_String (Source) = Super_Slice (Source'Old, Low, High))),
2309 Global => null;
2311 function Super_Head
2312 (Source : Super_String;
2313 Count : Natural;
2314 Pad : Character := Space;
2315 Drop : Truncation := Error) return Super_String
2316 with
2317 Pre => (if Count > Source.Max_Length then Drop /= Error),
2318 Post => Super_Head'Result.Max_Length = Source.Max_Length,
2319 Contract_Cases =>
2320 (Count <= Super_Length (Source)
2321 =>
2322 -- Source is cut
2324 Super_To_String (Super_Head'Result) = Super_Slice (Source, 1, Count),
2325 Count > Super_Length (Source) and then Count <= Source.Max_Length
2326 =>
2327 -- Source is followed by Pad characters
2329 Super_Length (Super_Head'Result) = Count
2330 and then
2331 Super_Slice (Super_Head'Result, 1, Super_Length (Source)) =
2332 Super_To_String (Source)
2333 and then
2338 =>
2339 -- Source is followed by Pad characters
2342 and then
2345 and then
2347 Super_Length (Source) + 1, Source.Max_Length)) =
2348 [1 .. Source.Max_Length - Super_Length (Source) => Pad],
2349 Count - Super_Length (Source) > Source.Max_Length and then Drop = Left
2350 =>
2351 -- Source is fully dropped on the left
2353 Super_To_String (Super_Head'Result) =
2354 [1 .. Source.Max_Length => Pad],
2355 others
2356 =>
2357 -- Source is partly dropped on the left
2359 Super_Length (Super_Head'Result) = Source.Max_Length
2360 and then
2365 and then
2367 Source.Max_Length - Count + Super_Length (Source) + 1,
2368 Source.Max_Length)) =
2369 [1 .. Count - Super_Length (Source) => Pad]),
2370 Global => null;
2372 procedure Super_Head
2373 (Source : in out Super_String;
2374 Count : Natural;
2375 Pad : Character := Space;
2376 Drop : Truncation := Error)
2377 with
2378 Pre => (if Count > Source.Max_Length then Drop /= Error),
2379 Contract_Cases =>
2380 (Count <= Super_Length (Source)
2381 =>
2382 -- Source is cut
2384 Super_To_String (Source) = Super_Slice (Source'Old, 1, Count),
2385 Count > Super_Length (Source) and then Count <= Source.Max_Length
2386 =>
2387 -- Source is followed by Pad characters
2389 Super_Length (Source) = Count
2390 and then
2391 Super_Slice (Source, 1, Super_Length (Source'Old)) =
2392 Super_To_String (Source'Old)
2393 and then
2398 =>
2399 -- Source is followed by Pad characters
2402 and then
2405 and then
2407 Super_Length (Source'Old) + 1, Source.Max_Length)) =
2408 [1 .. Source.Max_Length - Super_Length (Source'Old) => Pad],
2409 Count - Super_Length (Source) > Source.Max_Length and then Drop = Left
2410 =>
2411 -- Source is fully dropped on the left
2413 Super_To_String (Source) = [1 .. Source.Max_Length => Pad],
2414 others
2415 =>
2416 -- Source is partly dropped on the left
2418 Super_Length (Source) = Source.Max_Length
2419 and then
2424 and then
2426 Source.Max_Length - Count + Super_Length (Source'Old) + 1,
2427 Source.Max_Length)) =
2428 [1 .. Count - Super_Length (Source'Old) => Pad]),
2429 Global => null;
2431 function Super_Tail
2432 (Source : Super_String;
2433 Count : Natural;
2434 Pad : Character := Space;
2435 Drop : Truncation := Error) return Super_String
2436 with
2437 Pre => (if Count > Source.Max_Length then Drop /= Error),
2438 Post => Super_Tail'Result.Max_Length = Source.Max_Length,
2439 Contract_Cases =>
2440 (Count < Super_Length (Source)
2441 =>
2442 -- Source is cut
2444 (if Count > 0 then
2445 Super_To_String (Super_Tail'Result) =
2446 Super_Slice (Source,
2447 Super_Length (Source) - Count + 1, Super_Length (Source))
2448 else Super_Length (Super_Tail'Result) = 0),
2449 Count >= Super_Length (Source) and then Count < Source.Max_Length
2450 =>
2451 -- Source is preceded by Pad characters
2453 Super_Length (Super_Tail'Result) = Count
2454 and then
2458 and then
2463 =>
2464 -- Source is preceded by Pad characters
2467 and then
2469 1, Source.Max_Length - Super_Length (Source))) =
2470 [1 .. Source.Max_Length - Super_Length (Source) => Pad]
2471 and then
2472 (if Super_Length (Source) > 0 then
2473 Super_Slice (Super_Tail'Result,
2474 Source.Max_Length - Super_Length (Source) + 1,
2475 Source.Max_Length) =
2476 Super_To_String (Source)),
2477 Count - Super_Length (Source) >= Source.Max_Length
2478 and then Drop /= Left
2479 =>
2480 -- Source is fully dropped on the right
2482 Super_To_String (Super_Tail'Result) =
2483 [1 .. Source.Max_Length => Pad],
2484 others
2485 =>
2486 -- Source is partly dropped on the right
2488 Super_Length (Super_Tail'Result) = Source.Max_Length
2489 and then
2493 and then
2495 Count - Super_Length (Source) + 1, Source.Max_Length)) =
2496 Super_Slice (Source,
2497 1, Source.Max_Length - Count + Super_Length (Source))),
2498 Global => null;
2500 procedure Super_Tail
2501 (Source : in out Super_String;
2502 Count : Natural;
2503 Pad : Character := Space;
2504 Drop : Truncation := Error)
2505 with
2506 Pre => (if Count > Source.Max_Length then Drop /= Error),
2507 Contract_Cases =>
2508 (Count < Super_Length (Source)
2509 =>
2510 -- Source is cut
2512 (if Count > 0 then
2513 Super_To_String (Source) =
2514 Super_Slice (Source'Old,
2515 Super_Length (Source'Old) - Count + 1,
2516 Super_Length (Source'Old))
2517 else Super_Length (Source) = 0),
2518 Count >= Super_Length (Source) and then Count < Source.Max_Length
2519 =>
2520 -- Source is preceded by Pad characters
2522 Super_Length (Source) = Count
2523 and then
2527 and then
2532 =>
2533 -- Source is preceded by Pad characters
2536 and then
2538 1, Source.Max_Length - Super_Length (Source'Old))) =
2539 [1 .. Source.Max_Length - Super_Length (Source'Old) => Pad]
2540 and then
2541 (if Super_Length (Source'Old) > 0 then
2542 Super_Slice (Source,
2543 Source.Max_Length - Super_Length (Source'Old) + 1,
2544 Source.Max_Length) =
2545 Super_To_String (Source'Old)),
2546 Count - Super_Length (Source) >= Source.Max_Length
2547 and then Drop /= Left
2548 =>
2549 -- Source is fully dropped on the right
2551 Super_To_String (Source) = [1 .. Source.Max_Length => Pad],
2552 others
2553 =>
2554 -- Source is partly dropped on the right
2556 Super_Length (Source) = Source.Max_Length
2557 and then
2561 and then
2563 Count - Super_Length (Source'Old) + 1, Source.Max_Length)) =
2564 Super_Slice (Source'Old,
2565 1, Source.Max_Length - Count + Super_Length (Source'Old))),
2566 Global => null;
2568 ------------------------------------
2569 -- String Constructor Subprograms --
2570 ------------------------------------
2572 -- Note: in some of the following routines, there is an extra parameter
2573 -- Max_Length which specifies the value of the maximum length for the
2574 -- resulting Super_String value.
2576 function Times
2577 (Left : Natural;
2578 Right : Character;
2579 Max_Length : Positive) return Super_String
2580 with
2581 Pre => Left <= Max_Length,
2582 Post => Times'Result.Max_Length = Max_Length
2583 and then Super_To_String (Times'Result) = [1 .. Left => Right],
2584 Global => null;
2585 -- Note the additional parameter Max_Length
2587 function Times
2588 (Left : Natural;
2589 Right : String;
2590 Max_Length : Positive) return Super_String
2591 with
2592 Pre => (if Left /= 0 then Right'Length <= Max_Length / Left),
2593 Post => Times'Result.Max_Length = Max_Length
2594 and then Super_Length (Times'Result) = Left * Right'Length
2595 and then
2596 (if Right'Length > 0 then
2597 (for all K in 1 .. Left * Right'Length =>
2598 Super_Element (Times'Result, K) =
2599 Right (Right'First + (K - 1) mod Right'Length))),
2600 Global => null;
2601 -- Note the additional parameter Max_Length
2603 function Times
2604 (Left : Natural;
2605 Right : Super_String) return Super_String
2606 with
2607 Pre =>
2608 (if Left /= 0 then Super_Length (Right) <= Right.Max_Length / Left),
2609 Post => Times'Result.Max_Length = Right.Max_Length
2610 and then Super_Length (Times'Result) = Left * Super_Length (Right)
2611 and then
2612 (if Super_Length (Right) > 0 then
2613 (for all K in 1 .. Left * Super_Length (Right) =>
2614 Super_Element (Times'Result, K) =
2615 Super_Element (Right, 1 + (K - 1) mod Super_Length (Right)))),
2616 Global => null;
2618 function Super_Replicate
2619 (Count : Natural;
2620 Item : Character;
2621 Drop : Truncation := Error;
2622 Max_Length : Positive) return Super_String
2623 with
2624 Pre => (if Count > Max_Length then Drop /= Error),
2625 Post => Super_Replicate'Result.Max_Length = Max_Length
2626 and then Super_To_String (Super_Replicate'Result) =
2627 [1 .. Natural'Min (Max_Length, Count) => Item],
2628 Global => null;
2629 -- Note the additional parameter Max_Length
2631 function Super_Replicate
2632 (Count : Natural;
2633 Item : String;
2634 Drop : Truncation := Error;
2635 Max_Length : Positive) return Super_String
2636 with
2637 Pre =>
2638 (if Count /= 0 and then Item'Length > Max_Length / Count
2639 then Drop /= Error),
2640 Post => Super_Replicate'Result.Max_Length = Max_Length,
2641 Contract_Cases =>
2642 (Count = 0 or else Item'Length <= Max_Length / Count
2643 =>
2644 Super_Length (Super_Replicate'Result) = Count * Item'Length
2645 and then
2646 (if Item'Length > 0 then
2647 (for all K in 1 .. Count * Item'Length =>
2648 Super_Element (Super_Replicate'Result, K) =
2649 Item (Item'First + (K - 1) mod Item'Length))),
2650 Count /= 0
2651 and then Item'Length > Max_Length / Count
2652 and then Drop = Right
2653 =>
2654 Super_Length (Super_Replicate'Result) = Max_Length
2655 and then
2656 (for all K in 1 .. Max_Length =>
2657 Super_Element (Super_Replicate'Result, K) =
2658 Item (Item'First + (K - 1) mod Item'Length)),
2659 others -- Drop = Left
2660 =>
2661 Super_Length (Super_Replicate'Result) = Max_Length
2662 and then
2663 (for all K in 1 .. Max_Length =>
2664 Super_Element (Super_Replicate'Result, K) =
2665 Item (Item'Last - (Max_Length - K) mod Item'Length))),
2666 Global => null;
2667 -- Note the additional parameter Max_Length
2669 function Super_Replicate
2670 (Count : Natural;
2671 Item : Super_String;
2672 Drop : Truncation := Error) return Super_String
2673 with
2674 Pre =>
2675 (if Count /= 0
2676 and then Super_Length (Item) > Item.Max_Length / Count
2677 then Drop /= Error),
2678 Post => Super_Replicate'Result.Max_Length = Item.Max_Length,
2679 Contract_Cases =>
2680 ((if Count /= 0 then Super_Length (Item) <= Item.Max_Length / Count)
2681 =>
2682 Super_Length (Super_Replicate'Result) = Count * Super_Length (Item)
2683 and then
2684 (if Super_Length (Item) > 0 then
2685 (for all K in 1 .. Count * Super_Length (Item) =>
2686 Super_Element (Super_Replicate'Result, K) =
2687 Super_Element (Item,
2688 1 + (K - 1) mod Super_Length (Item)))),
2689 Count /= 0
2690 and then Super_Length (Item) > Item.Max_Length / Count
2691 and then Drop = Right
2692 =>
2693 Super_Length (Super_Replicate'Result) = Item.Max_Length
2694 and then
2695 (for all K in 1 .. Item.Max_Length =>
2696 Super_Element (Super_Replicate'Result, K) =
2697 Super_Element (Item, 1 + (K - 1) mod Super_Length (Item))),
2698 others -- Drop = Left
2699 =>
2700 Super_Length (Super_Replicate'Result) = Item.Max_Length
2701 and then
2702 (for all K in 1 .. Item.Max_Length =>
2703 Super_Element (Super_Replicate'Result, K) =
2704 Super_Element (Item,
2705 Super_Length (Item)
2706 - (Item.Max_Length - K) mod Super_Length (Item)))),
2707 Global => null;
2709 procedure Put_Image
2710 (S : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class;
2711 Source : Super_String);
2713 private
2714 -- Pragma Inline declarations
2716 pragma Inline ("=");
2717 pragma Inline (Less);
2718 pragma Inline (Less_Or_Equal);
2719 pragma Inline (Greater);
2720 pragma Inline (Greater_Or_Equal);
2721 pragma Inline (Concat);
2722 pragma Inline (Super_Count);
2723 pragma Inline (Super_Element);
2724 pragma Inline (Super_Find_Token);
2725 pragma Inline (Super_Index);
2726 pragma Inline (Super_Index_Non_Blank);
2727 pragma Inline (Super_Length);
2728 pragma Inline (Super_Replace_Element);
2729 pragma Inline (Super_Slice);
2730 pragma Inline (Super_To_String);
2732 end Ada.Strings.Superbounded;