| blob | 6c360f1982be0bd8d5f3ae6255e632c580a7c032 |
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-2024, 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
693 Global => null;
695 function Equal
696 (Left : Super_String;
697 Right : Super_String) return Boolean renames "=";
699 function Equal
700 (Left : Super_String;
701 Right : String) return Boolean
702 with
703 Post => Equal'Result = (Super_To_String (Left) = Right),
704 Global => null;
706 function Equal
707 (Left : String;
708 Right : Super_String) return Boolean
709 with
710 Post => Equal'Result = (Left = Super_To_String (Right)),
711 Global => null;
713 function Less
714 (Left : Super_String;
715 Right : Super_String) return Boolean
716 with
717 Pre => Left.Max_Length = Right.Max_Length,
718 Post =>
719 Less'Result = (Super_To_String (Left) < Super_To_String (Right)),
720 Global => null;
722 function Less
723 (Left : Super_String;
724 Right : String) return Boolean
725 with
726 Post => Less'Result = (Super_To_String (Left) < Right),
727 Global => null;
729 function Less
730 (Left : String;
731 Right : Super_String) return Boolean
732 with
733 Post => Less'Result = (Left < Super_To_String (Right)),
734 Global => null;
736 function Less_Or_Equal
737 (Left : Super_String;
738 Right : Super_String) return Boolean
739 with
740 Pre => Left.Max_Length = Right.Max_Length,
741 Post =>
742 Less_Or_Equal'Result =
743 (Super_To_String (Left) <= Super_To_String (Right)),
744 Global => null;
746 function Less_Or_Equal
747 (Left : Super_String;
748 Right : String) return Boolean
749 with
750 Post => Less_Or_Equal'Result = (Super_To_String (Left) <= Right),
751 Global => null;
753 function Less_Or_Equal
754 (Left : String;
755 Right : Super_String) return Boolean
756 with
757 Post => Less_Or_Equal'Result = (Left <= Super_To_String (Right)),
758 Global => null;
760 function Greater
761 (Left : Super_String;
762 Right : Super_String) return Boolean
763 with
764 Pre => Left.Max_Length = Right.Max_Length,
765 Post =>
766 Greater'Result = (Super_To_String (Left) > Super_To_String (Right)),
767 Global => null;
769 function Greater
770 (Left : Super_String;
771 Right : String) return Boolean
772 with
773 Post => Greater'Result = (Super_To_String (Left) > Right),
774 Global => null;
776 function Greater
777 (Left : String;
778 Right : Super_String) return Boolean
779 with
780 Post => Greater'Result = (Left > Super_To_String (Right)),
781 Global => null;
783 function Greater_Or_Equal
784 (Left : Super_String;
785 Right : Super_String) return Boolean
786 with
787 Pre => Left.Max_Length = Right.Max_Length,
788 Post =>
789 Greater_Or_Equal'Result =
790 (Super_To_String (Left) >= Super_To_String (Right)),
791 Global => null;
793 function Greater_Or_Equal
794 (Left : Super_String;
795 Right : String) return Boolean
796 with
797 Post => Greater_Or_Equal'Result = (Super_To_String (Left) >= Right),
798 Global => null;
800 function Greater_Or_Equal
801 (Left : String;
802 Right : Super_String) return Boolean
803 with
804 Post => Greater_Or_Equal'Result = (Left >= Super_To_String (Right)),
805 Global => null;
807 ----------------------
808 -- Search Functions --
809 ----------------------
811 function Super_Index
812 (Source : Super_String;
813 Pattern : String;
814 Going : Direction := Forward;
815 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
816 with
817 Pre => Pattern'Length > 0,
818 Post => Super_Index'Result <= Super_Length (Source),
819 Contract_Cases =>
821 -- If Source is the empty string, then 0 is returned
823 (Super_Length (Source) = 0
824 =>
825 Super_Index'Result = 0,
827 -- If some slice of Source matches Pattern, then a valid index is
828 -- returned.
830 Super_Length (Source) > 0
831 and then
832 (for some J in 1 .. Super_Length (Source) - (Pattern'Length - 1) =>
833 Search.Match (Super_To_String (Source), Pattern, Mapping, J))
834 =>
835 -- The result is in the considered range of Source
837 Super_Index'Result in
838 1 .. Super_Length (Source) - (Pattern'Length - 1)
840 -- The slice beginning at the returned index matches Pattern
842 and then Search.Match
843 (Super_To_String (Source), Pattern, Mapping, Super_Index'Result)
845 -- The result is the smallest or largest index which satisfies
846 -- the matching, respectively when Going = Forward and Going =
847 -- Backward.
849 and then
850 (for all J in 1 .. Super_Length (Source) =>
851 (if (if Going = Forward
852 then J <= Super_Index'Result - 1
853 else J - 1 in Super_Index'Result
854 .. Super_Length (Source) - Pattern'Length)
855 then not (Search.Match
856 (Super_To_String (Source), Pattern, Mapping, J)))),
858 -- Otherwise, 0 is returned
860 others
861 =>
862 Super_Index'Result = 0),
863 Global => null;
865 function Super_Index
866 (Source : Super_String;
867 Pattern : String;
868 Going : Direction := Forward;
869 Mapping : Maps.Character_Mapping_Function) return Natural
870 with
871 Pre => Pattern'Length /= 0 and then Mapping /= null,
872 Post => Super_Index'Result <= Super_Length (Source),
873 Contract_Cases =>
875 -- If Source is the empty string, then 0 is returned
877 (Super_Length (Source) = 0
878 =>
879 Super_Index'Result = 0,
881 -- If some slice of Source matches Pattern, then a valid index is
882 -- returned.
884 Super_Length (Source) > 0
885 and then
886 (for some J in 1 .. Super_Length (Source) - (Pattern'Length - 1) =>
887 Search.Match (Super_To_String (Source), Pattern, Mapping, J))
888 =>
889 -- The result is in the considered range of Source
891 Super_Index'Result in
892 1 .. Super_Length (Source) - (Pattern'Length - 1)
894 -- The slice beginning at the returned index matches Pattern
896 and then Search.Match
897 (Super_To_String (Source), Pattern, Mapping, Super_Index'Result)
899 -- The result is the smallest or largest index which satisfies
900 -- the matching, respectively when Going = Forward and Going =
901 -- Backward.
903 and then
904 (for all J in 1 .. Super_Length (Source) =>
905 (if (if Going = Forward
906 then J <= Super_Index'Result - 1
907 else J - 1 in Super_Index'Result
908 .. Super_Length (Source) - Pattern'Length)
909 then not (Search.Match
910 (Super_To_String (Source), Pattern, Mapping, J)))),
912 -- Otherwise, 0 is returned
914 others
915 =>
916 Super_Index'Result = 0),
917 Global => null;
919 function Super_Index
920 (Source : Super_String;
921 Set : Maps.Character_Set;
922 Test : Membership := Inside;
923 Going : Direction := Forward) return Natural
924 with
925 Post => Super_Index'Result <= Super_Length (Source),
926 Contract_Cases =>
928 -- If no character of Source satisfies the property Test on Set,
929 -- then 0 is returned.
931 ((for all C of Super_To_String (Source) =>
932 (Test = Inside) /= Maps.Is_In (C, Set))
933 =>
934 Super_Index'Result = 0,
936 -- Otherwise, an index in the range of Source is returned
938 others
939 =>
940 -- The result is in the range of Source
942 Super_Index'Result in 1 .. Super_Length (Source)
944 -- The character at the returned index satisfies the property
945 -- Test on Set.
947 and then
948 (Test = Inside) =
949 Maps.Is_In (Super_Element (Source, Super_Index'Result), Set)
951 -- The result is the smallest or largest index which satisfies
952 -- the property, respectively when Going = Forward and Going =
953 -- Backward.
955 and then
956 (for all J in 1 .. Super_Length (Source) =>
957 (if J /= Super_Index'Result
958 and then (J < Super_Index'Result) = (Going = Forward)
959 then (Test = Inside)
960 /= Maps.Is_In (Super_Element (Source, J), Set)))),
961 Global => null;
963 function Super_Index
964 (Source : Super_String;
965 Pattern : String;
966 From : Positive;
967 Going : Direction := Forward;
968 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
969 with
970 Pre =>
971 (if Super_Length (Source) /= 0 then From <= Super_Length (Source))
972 and then Pattern'Length /= 0,
973 Post => Super_Index'Result <= Super_Length (Source),
974 Contract_Cases =>
976 -- If Source is the empty string, then 0 is returned
978 (Super_Length (Source) = 0
979 =>
980 Super_Index'Result = 0,
982 -- If some slice of Source matches Pattern, then a valid index is
983 -- returned.
985 Super_Length (Source) > 0
986 and then
987 (for some J in
988 (if Going = Forward then From else 1)
989 .. (if Going = Forward then Super_Length (Source) else From)
990 - (Pattern'Length - 1) =>
991 Search.Match (Super_To_String (Source), Pattern, Mapping, J))
992 =>
993 -- The result is in the considered range of Source
995 Super_Index'Result in
996 (if Going = Forward then From else 1)
997 .. (if Going = Forward then Super_Length (Source) else From)
998 - (Pattern'Length - 1)
1000 -- The slice beginning at the returned index matches Pattern
1002 and then Search.Match
1003 (Super_To_String (Source), Pattern, Mapping, Super_Index'Result)
1005 -- The result is the smallest or largest index which satisfies
1006 -- the matching, respectively when Going = Forward and Going =
1007 -- Backward.
1009 and then
1010 (for all J in 1 .. Super_Length (Source) =>
1011 (if (if Going = Forward
1012 then J in From .. Super_Index'Result - 1
1013 else J - 1 in Super_Index'Result
1014 .. From - Pattern'Length)
1015 then not (Search.Match
1016 (Super_To_String (Source), Pattern, Mapping, J)))),
1018 -- Otherwise, 0 is returned
1020 others
1021 =>
1022 Super_Index'Result = 0),
1023 Global => null;
1025 function Super_Index
1026 (Source : Super_String;
1027 Pattern : String;
1028 From : Positive;
1029 Going : Direction := Forward;
1030 Mapping : Maps.Character_Mapping_Function) return Natural
1031 with
1032 Pre =>
1033 (if Super_Length (Source) /= 0 then From <= Super_Length (Source))
1034 and then Pattern'Length /= 0
1035 and then Mapping /= null,
1036 Post => Super_Index'Result <= Super_Length (Source),
1037 Contract_Cases =>
1039 -- If Source is the empty string, then 0 is returned
1041 (Super_Length (Source) = 0
1042 =>
1043 Super_Index'Result = 0,
1045 -- If some slice of Source matches Pattern, then a valid index is
1046 -- returned.
1048 Super_Length (Source) > 0
1049 and then
1050 (for some J in
1051 (if Going = Forward then From else 1)
1052 .. (if Going = Forward then Super_Length (Source) else From)
1053 - (Pattern'Length - 1) =>
1054 Search.Match (Super_To_String (Source), Pattern, Mapping, J))
1055 =>
1056 -- The result is in the considered range of Source
1058 Super_Index'Result in
1059 (if Going = Forward then From else 1)
1060 .. (if Going = Forward then Super_Length (Source) else From)
1061 - (Pattern'Length - 1)
1063 -- The slice beginning at the returned index matches Pattern
1065 and then Search.Match
1066 (Super_To_String (Source), Pattern, Mapping, Super_Index'Result)
1068 -- The result is the smallest or largest index which satisfies
1069 -- the matching, respectively when Going = Forward and Going =
1070 -- Backward.
1072 and then
1073 (for all J in 1 .. Super_Length (Source) =>
1074 (if (if Going = Forward
1075 then J in From .. Super_Index'Result - 1
1076 else J - 1 in Super_Index'Result
1077 .. From - Pattern'Length)
1078 then not (Search.Match
1079 (Super_To_String (Source), Pattern, Mapping, J)))),
1081 -- Otherwise, 0 is returned
1083 others
1084 =>
1085 Super_Index'Result = 0),
1086 Global => null;
1088 function Super_Index
1089 (Source : Super_String;
1090 Set : Maps.Character_Set;
1091 From : Positive;
1092 Test : Membership := Inside;
1093 Going : Direction := Forward) return Natural
1094 with
1095 Pre =>
1096 (if Super_Length (Source) /= 0 then From <= Super_Length (Source)),
1097 Post => Super_Index'Result <= Super_Length (Source),
1098 Contract_Cases =>
1100 -- If Source is the empty string, or no character of the considered
1101 -- slice of Source satisfies the property Test on Set, then 0 is
1102 -- returned.
1104 (Super_Length (Source) = 0
1105 or else
1106 (for all J in 1 .. Super_Length (Source) =>
1107 (if J = From or else (J > From) = (Going = Forward) then
1108 (Test = Inside) /=
1109 Maps.Is_In (Super_Element (Source, J), Set)))
1110 =>
1111 Super_Index'Result = 0,
1113 -- Otherwise, an index in the considered range of Source is returned
1115 others
1116 =>
1117 -- The result is in the considered range of Source
1119 Super_Index'Result in 1 .. Super_Length (Source)
1120 and then
1121 (Super_Index'Result = From
1122 or else (Super_Index'Result > From) = (Going = Forward))
1124 -- The character at the returned index satisfies the property
1125 -- Test on Set.
1127 and then
1128 (Test = Inside) =
1129 Maps.Is_In (Super_Element (Source, Super_Index'Result), Set)
1131 -- The result is the smallest or largest index which satisfies
1132 -- the property, respectively when Going = Forward and Going =
1133 -- Backward.
1135 and then
1136 (for all J in 1 .. Super_Length (Source) =>
1137 (if J /= Super_Index'Result
1138 and then (J < Super_Index'Result) = (Going = Forward)
1139 and then (J = From
1140 or else (J > From) = (Going = Forward))
1141 then (Test = Inside)
1142 /= Maps.Is_In (Super_Element (Source, J), Set)))),
1143 Global => null;
1145 function Super_Index_Non_Blank
1146 (Source : Super_String;
1147 Going : Direction := Forward) return Natural
1148 with
1149 Post => Super_Index_Non_Blank'Result <= Super_Length (Source),
1150 Contract_Cases =>
1152 -- If all characters of Source are Space characters, then 0 is
1153 -- returned.
1156 =>
1157 Super_Index_Non_Blank'Result = 0,
1159 -- Otherwise, an index in the range of Source is returned
1161 others
1162 =>
1163 -- The result is in the range of Source
1165 Super_Index_Non_Blank'Result in 1 .. Super_Length (Source)
1167 -- The character at the returned index is not a Space character
1169 and then
1172 -- The result is the smallest or largest index which is not a
1173 -- Space character, respectively when Going = Forward and Going
1174 -- = Backward.
1176 and then
1177 (for all J in 1 .. Super_Length (Source) =>
1178 (if J /= Super_Index_Non_Blank'Result
1179 and then
1180 (J < Super_Index_Non_Blank'Result) = (Going = Forward)
1182 Global => null;
1184 function Super_Index_Non_Blank
1185 (Source : Super_String;
1186 From : Positive;
1187 Going : Direction := Forward) return Natural
1188 with
1189 Pre =>
1190 (if Super_Length (Source) /= 0 then From <= Super_Length (Source)),
1191 Post => Super_Index_Non_Blank'Result <= Super_Length (Source),
1192 Contract_Cases =>
1194 -- If Source is the empty string, or all characters of the
1195 -- considered slice of Source are Space characters, then 0
1196 -- is returned.
1198 (Super_Length (Source) = 0
1199 or else
1200 (for all J in 1 .. Super_Length (Source) =>
1201 (if J = From or else (J > From) = (Going = Forward) then
1203 =>
1204 Super_Index_Non_Blank'Result = 0,
1206 -- Otherwise, an index in the considered range of Source is returned
1208 others
1209 =>
1210 -- The result is in the considered range of Source
1212 Super_Index_Non_Blank'Result in 1 .. Super_Length (Source)
1213 and then
1214 (Super_Index_Non_Blank'Result = From
1215 or else
1216 (Super_Index_Non_Blank'Result > From) = (Going = Forward))
1218 -- The character at the returned index is not a Space character
1220 and then
1223 -- The result is the smallest or largest index which isn't a
1224 -- Space character, respectively when Going = Forward and Going
1225 -- = Backward.
1227 and then
1228 (for all J in 1 .. Super_Length (Source) =>
1229 (if J /= Super_Index_Non_Blank'Result
1230 and then
1231 (J < Super_Index_Non_Blank'Result) = (Going = Forward)
1232 and then (J = From
1233 or else (J > From) = (Going = Forward))
1235 Global => null;
1237 function Super_Count
1238 (Source : Super_String;
1239 Pattern : String;
1240 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
1241 with
1242 Pre => Pattern'Length /= 0,
1243 Global => null;
1245 function Super_Count
1246 (Source : Super_String;
1247 Pattern : String;
1248 Mapping : Maps.Character_Mapping_Function) return Natural
1249 with
1250 Pre => Pattern'Length /= 0 and then Mapping /= null,
1251 Global => null;
1253 function Super_Count
1254 (Source : Super_String;
1255 Set : Maps.Character_Set) return Natural
1256 with
1257 Global => null;
1259 procedure Super_Find_Token
1260 (Source : Super_String;
1261 Set : Maps.Character_Set;
1262 From : Positive;
1263 Test : Membership;
1264 First : out Positive;
1265 Last : out Natural)
1266 with
1267 Pre =>
1268 (if Super_Length (Source) /= 0 then From <= Super_Length (Source)),
1269 Contract_Cases =>
1271 -- If Source is the empty string, or if no character of the
1272 -- considered slice of Source satisfies the property Test on
1273 -- Set, then First is set to From and Last is set to 0.
1275 (Super_Length (Source) = 0
1276 or else
1277 (for all J in From .. Super_Length (Source) =>
1278 (Test = Inside) /= Maps.Is_In (Super_Element (Source, J), Set))
1279 =>
1280 First = From and then Last = 0,
1282 -- Otherwise, First and Last are set to valid indexes
1284 others
1285 =>
1286 -- First and Last are in the considered range of Source
1288 First in From .. Super_Length (Source)
1289 and then Last in First .. Super_Length (Source)
1291 -- No character between From and First satisfies the property
1292 -- Test on Set.
1294 and then
1295 (for all J in From .. First - 1 =>
1296 (Test = Inside) /=
1297 Maps.Is_In (Super_Element (Source, J), Set))
1299 -- All characters between First and Last satisfy the property
1300 -- Test on Set.
1302 and then
1303 (for all J in First .. Last =>
1304 (Test = Inside) =
1305 Maps.Is_In (Super_Element (Source, J), Set))
1307 -- If Last is not Source'Last, then the character at position
1308 -- Last + 1 does not satify the property Test on Set.
1310 and then
1311 (if Last < Super_Length (Source)
1312 then
1313 (Test = Inside) /=
1314 Maps.Is_In (Super_Element (Source, Last + 1), Set))),
1315 Global => null;
1317 procedure Super_Find_Token
1318 (Source : Super_String;
1319 Set : Maps.Character_Set;
1320 Test : Membership;
1321 First : out Positive;
1322 Last : out Natural)
1323 with
1324 Contract_Cases =>
1326 -- If Source is the empty string, or if no character of the considered
1327 -- slice of Source satisfies the property Test on Set, then First is
1328 -- set to 1 and Last is set to 0.
1330 (Super_Length (Source) = 0
1331 or else
1332 (for all J in 1 .. Super_Length (Source) =>
1333 (Test = Inside) /= Maps.Is_In (Super_Element (Source, J), Set))
1334 =>
1335 First = 1 and then Last = 0,
1337 -- Otherwise, First and Last are set to valid indexes
1339 others
1340 =>
1341 -- First and Last are in the considered range of Source
1343 First in 1 .. Super_Length (Source)
1344 and then Last in First .. Super_Length (Source)
1346 -- No character between 1 and First satisfies the property Test on
1347 -- Set.
1349 and then
1350 (for all J in 1 .. First - 1 =>
1351 (Test = Inside) /=
1352 Maps.Is_In (Super_Element (Source, J), Set))
1354 -- All characters between First and Last satisfy the property
1355 -- Test on Set.
1357 and then
1358 (for all J in First .. Last =>
1359 (Test = Inside) =
1360 Maps.Is_In (Super_Element (Source, J), Set))
1362 -- If Last is not Source'Last, then the character at position
1363 -- Last + 1 does not satify the property Test on Set.
1365 and then
1366 (if Last < Super_Length (Source)
1367 then
1368 (Test = Inside) /=
1369 Maps.Is_In (Super_Element (Source, Last + 1), Set))),
1370 Global => null;
1372 ------------------------------------
1373 -- String Translation Subprograms --
1374 ------------------------------------
1376 function Super_Translate
1377 (Source : Super_String;
1378 Mapping : Maps.Character_Mapping) return Super_String
1379 with
1380 Post => Super_Translate'Result.Max_Length = Source.Max_Length
1381 and then Super_Length (Super_Translate'Result) = Super_Length (Source)
1382 and then
1383 (for all K in 1 .. Super_Length (Source) =>
1384 Super_Element (Super_Translate'Result, K) =
1385 Ada.Strings.Maps.Value (Mapping, Super_Element (Source, K))),
1386 Global => null;
1388 procedure Super_Translate
1389 (Source : in out Super_String;
1390 Mapping : Maps.Character_Mapping)
1391 with
1392 Post => Super_Length (Source) = Super_Length (Source'Old)
1393 and then
1394 (for all K in 1 .. Super_Length (Source) =>
1395 Super_Element (Source, K) =
1396 Ada.Strings.Maps.Value (Mapping, Super_Element (Source'Old, K))),
1397 Global => null;
1399 function Super_Translate
1400 (Source : Super_String;
1401 Mapping : Maps.Character_Mapping_Function) return Super_String
1402 with
1403 Pre => Mapping /= null,
1404 Post => Super_Translate'Result.Max_Length = Source.Max_Length
1405 and then Super_Length (Super_Translate'Result) = Super_Length (Source)
1406 and then
1407 (for all K in 1 .. Super_Length (Source) =>
1408 Super_Element (Super_Translate'Result, K) =
1409 Mapping (Super_Element (Source, K))),
1410 Global => null;
1411 pragma Annotate (GNATprove, False_Positive,
1412 "call via access-to-subprogram",
1413 "function Mapping must always terminate");
1415 procedure Super_Translate
1416 (Source : in out Super_String;
1417 Mapping : Maps.Character_Mapping_Function)
1418 with
1419 Pre => Mapping /= null,
1420 Post => Super_Length (Source) = Super_Length (Source'Old)
1421 and then
1422 (for all K in 1 .. Super_Length (Source) =>
1423 Super_Element (Source, K) =
1424 Mapping (Super_Element (Source'Old, K))),
1425 Global => null;
1426 pragma Annotate (GNATprove, False_Positive,
1427 "call via access-to-subprogram",
1428 "function Mapping must always terminate");
1430 ---------------------------------------
1431 -- String Transformation Subprograms --
1432 ---------------------------------------
1434 function Super_Replace_Slice
1435 (Source : Super_String;
1436 Low : Positive;
1437 High : Natural;
1438 By : String;
1439 Drop : Truncation := Error) return Super_String
1440 with
1441 Pre =>
1442 Low - 1 <= Super_Length (Source)
1443 and then
1444 (if Drop = Error
1445 then (if High >= Low
1446 then Low - 1
1447 <= Source.Max_Length - By'Length
1448 - Integer'Max (Super_Length (Source) - High, 0)
1449 else Super_Length (Source) <=
1450 Source.Max_Length - By'Length)),
1451 Post =>
1452 Super_Replace_Slice'Result.Max_Length = Source.Max_Length,
1453 Contract_Cases =>
1454 (Low - 1 <= Source.Max_Length - By'Length - Integer'Max
1455 (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
1456 =>
1457 -- Total length is lower than Max_Length: nothing is dropped
1459 -- Note that if High < Low, the insertion is done before Low, so in
1460 -- all cases the starting position of the slice of Source remaining
1461 -- after the replaced Slice is Integer'Max (High + 1, Low).
1463 Super_Length (Super_Replace_Slice'Result) =
1464 Low - 1 + By'Length + Integer'Max
1465 (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
1466 and then
1469 and then
1472 and then
1475 Low + By'Length,
1476 Super_Length (Super_Replace_Slice'Result))) =
1477 Super_Slice (Source,
1478 Integer'Max (High + 1, Low), Super_Length (Source))),
1480 Low - 1 > Source.Max_Length - By'Length - Integer'Max
1481 (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
1482 and then Drop = Left
1483 =>
1484 -- Final_Super_Slice is the length of the slice of Source remaining
1485 -- after the replaced part.
1486 (declare
1487 Final_Super_Slice : constant Natural :=
1488 Integer'Max
1489 (Super_Length (Source) - Integer'Max (High, Low - 1), 0);
1490 begin
1491 -- The result is of maximal length and ends by the last
1492 -- Final_Super_Slice characters of Source.
1494 Super_Length (Super_Replace_Slice'Result) = Source.Max_Length
1495 and then
1496 (if Final_Super_Slice > 0 then
1503 -- Depending on when we reach Max_Length, either the first
1504 -- part of Source is fully dropped and By is partly dropped,
1505 -- or By is fully added and the first part of Source is partly
1506 -- dropped.
1508 and then
1511 -- The first (possibly zero) characters of By are dropped
1525 By
1527 -- The first characters of Source (1 .. Low - 1) are
1528 -- dropped.
1530 and then
1532 Source.Max_Length - Final_Super_Slice - By'Length)) =
1533 Super_Slice (Source,
1534 Low - Source.Max_Length
1535 + Final_Super_Slice + By'Length,
1536 Low - 1))),
1538 others -- Drop = Right
1539 =>
1540 -- The result is of maximal length and starts by the first Low - 1
1541 -- characters of Source.
1543 Super_Length (Super_Replace_Slice'Result) = Source.Max_Length
1544 and then
1548 -- Depending on when we reach Max_Length, either the last part
1549 -- of Source is fully dropped and By is partly dropped, or By
1550 -- is fully added and the last part of Source is partly dropped.
1552 and then
1555 -- The last characters of By are dropped
1566 -- Then Source starting from Natural'Max (High + 1, Low)
1567 -- is added but the last characters are dropped.
1569 and then
1571 Low + By'Length, Source.Max_Length)) =
1572 Super_Slice (Source, Integer'Max (High + 1, Low),
1573 Integer'Max (High + 1, Low) +
1574 (Source.Max_Length - Low - By'Length)))),
1575 Global => null;
1577 procedure Super_Replace_Slice
1578 (Source : in out Super_String;
1579 Low : Positive;
1580 High : Natural;
1581 By : String;
1582 Drop : Truncation := Error)
1583 with
1584 Pre =>
1585 Low - 1 <= Super_Length (Source)
1586 and then
1587 (if Drop = Error
1588 then (if High >= Low
1589 then Low - 1
1590 <= Source.Max_Length - By'Length
1591 - Natural'Max (Super_Length (Source) - High, 0)
1592 else Super_Length (Source) <=
1593 Source.Max_Length - By'Length)),
1594 Contract_Cases =>
1595 (Low - 1 <= Source.Max_Length - By'Length - Integer'Max
1596 (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
1597 =>
1598 -- Total length is lower than Max_Length: nothing is dropped
1600 -- Note that if High < Low, the insertion is done before Low, so in
1601 -- all cases the starting position of the slice of Source remaining
1602 -- after the replaced Slice is Integer'Max (High + 1, Low).
1604 Super_Length (Source) = Low - 1 + By'Length + Integer'Max
1605 (Super_Length (Source'Old) - Integer'Max (High, Low - 1), 0)
1606 and then
1610 and then
1613 Low + By'Length, Super_Length (Source))) =
1614 Super_Slice (Source'Old,
1615 Integer'Max (High + 1, Low),
1616 Super_Length (Source'Old))),
1618 Low - 1 > Source.Max_Length - By'Length - Integer'Max
1619 (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
1620 and then Drop = Left
1621 =>
1622 -- Final_Super_Slice is the length of the slice of Source remaining
1623 -- after the replaced part.
1624 (declare
1625 Final_Super_Slice : constant Natural :=
1626 Integer'Max (0,
1627 Super_Length (Source'Old) - Integer'Max (High, Low - 1));
1628 begin
1629 -- The result is of maximal length and ends by the last
1630 -- Final_Super_Slice characters of Source.
1632 Super_Length (Source) = Source.Max_Length
1633 and then
1634 (if Final_Super_Slice > 0 then
1642 -- Depending on when we reach Max_Length, either the first
1643 -- part of Source is fully dropped and By is partly dropped,
1644 -- or By is fully added and the first part of Source is partly
1645 -- dropped.
1647 and then
1649 then
1650 -- The first characters of By are dropped
1665 -- The first characters of Source (1 .. Low - 1) are
1666 -- dropped.
1668 and then
1670 Source.Max_Length - Final_Super_Slice - By'Length)) =
1671 Super_Slice (Source'Old,
1672 Low - Source.Max_Length + Final_Super_Slice
1673 + By'Length,
1674 Low - 1))),
1676 others -- Drop = Right
1677 =>
1678 -- The result is of maximal length and starts by the first Low - 1
1679 -- characters of Source.
1681 Super_Length (Source) = Source.Max_Length
1682 and then
1686 -- Depending on when we reach Max_Length, either the last part
1687 -- of Source is fully dropped and By is partly dropped, or By
1688 -- is fully added and the last part of Source is partly dropped.
1690 and then
1693 -- The last characters of By are dropped
1702 -- Then Source starting from Natural'Max (High + 1, Low)
1703 -- is added but the last characters are dropped.
1705 and then
1707 Low + By'Length, Source.Max_Length)) =
1708 Super_Slice (Source'Old, Integer'Max (High + 1, Low),
1709 Integer'Max (High + 1, Low) +
1710 (Source.Max_Length - Low - By'Length)))),
1711 Global => null;
1713 function Super_Insert
1714 (Source : Super_String;
1715 Before : Positive;
1716 New_Item : String;
1717 Drop : Truncation := Error) return Super_String
1718 with
1719 Pre =>
1720 Before - 1 <= Super_Length (Source)
1721 and then
1722 (if New_Item'Length > Source.Max_Length - Super_Length (Source)
1723 then Drop /= Error),
1724 Post => Super_Insert'Result.Max_Length = Source.Max_Length,
1725 Contract_Cases =>
1726 (Super_Length (Source) <= Source.Max_Length - New_Item'Length
1727 =>
1728 -- Total length is lower than Max_Length: nothing is dropped
1730 Super_Length (Super_Insert'Result) =
1731 Super_Length (Source) + New_Item'Length
1732 and then
1735 and then
1738 New_Item
1739 and then
1742 Before + New_Item'Length,
1743 Super_Length (Super_Insert'Result))) =
1744 Super_Slice (Source, Before, Super_Length (Source))),
1746 Super_Length (Source) > Source.Max_Length - New_Item'Length
1747 and then Drop = Left
1748 =>
1749 -- The result is of maximal length and ends by the last characters
1750 -- of Source.
1752 Super_Length (Super_Insert'Result) = Source.Max_Length
1753 and then
1754 (if Before <= Super_Length (Source) then
1760 -- Depending on when we reach Max_Length, either the first part
1761 -- of Source is fully dropped and New_Item is partly dropped, or
1762 -- New_Item is fully added and the first part of Source is partly
1763 -- dropped.
1765 and then
1768 then
1769 -- The first characters of New_Item are dropped
1772 then
1775 New_Item
1786 New_Item
1788 -- The first characters of Source (1 .. Before - 1) are
1789 -- dropped.
1791 and then
1793 1, Source.Max_Length - Super_Length (Source)
1794 - New_Item'Length - 1 + Before)) =
1795 Super_Slice (Source,
1796 Super_Length (Source) - Source.Max_Length
1797 + New_Item'Length + 1,
1798 Before - 1)),
1800 others -- Drop = Right
1801 =>
1802 -- The result is of maximal length and starts by the first
1803 -- characters of Source.
1805 Super_Length (Super_Insert'Result) = Source.Max_Length
1806 and then
1810 -- Depending on when we reach Max_Length, either the last part
1811 -- of Source is fully dropped and New_Item is partly dropped, or
1812 -- New_Item is fully added and the last part of Source is partly
1813 -- dropped.
1815 and then
1818 -- The last characters of New_Item are dropped
1828 New_Item
1830 -- Then Source starting from Before is added but the
1831 -- last characters are dropped.
1833 and then
1835 Before + New_Item'Length, Source.Max_Length)) =
1836 Super_Slice (Source,
1837 Before, Source.Max_Length - New_Item'Length))),
1838 Global => null;
1840 procedure Super_Insert
1841 (Source : in out Super_String;
1842 Before : Positive;
1843 New_Item : String;
1844 Drop : Truncation := Error)
1845 with
1846 Pre =>
1847 Before - 1 <= Super_Length (Source)
1848 and then
1849 (if New_Item'Length > Source.Max_Length - Super_Length (Source)
1850 then Drop /= Error),
1851 Contract_Cases =>
1852 (Super_Length (Source) <= Source.Max_Length - New_Item'Length
1853 =>
1854 -- Total length is lower than Max_Length: nothing is dropped
1856 Super_Length (Source) = Super_Length (Source'Old) + New_Item'Length
1857 and then
1860 and then
1862 New_Item
1863 and then
1866 Before + New_Item'Length, Super_Length (Source))) =
1867 Super_Slice (Source'Old,
1868 Before, Super_Length (Source'Old))),
1870 Super_Length (Source) > Source.Max_Length - New_Item'Length
1871 and then Drop = Left
1872 =>
1873 -- The result is of maximal length and ends by the last characters
1874 -- of Source.
1876 Super_Length (Source) = Source.Max_Length
1877 and then
1878 (if Before <= Super_Length (Source'Old) then
1885 -- Depending on when we reach Max_Length, either the first part
1886 -- of Source is fully dropped and New_Item is partly dropped, or
1887 -- New_Item is fully added and the first part of Source is partly
1888 -- dropped.
1890 and then
1893 then
1894 -- The first characters of New_Item are dropped
1897 then
1901 New_Item
1912 = New_Item
1914 -- The first characters of Source (1 .. Before - 1) are
1915 -- dropped.
1917 and then
1919 Source.Max_Length - Super_Length (Source'Old)
1920 - New_Item'Length - 1 + Before)) =
1921 Super_Slice (Source'Old,
1922 Super_Length (Source'Old)
1923 - Source.Max_Length + New_Item'Length + 1,
1924 Before - 1)),
1926 others -- Drop = Right
1927 =>
1928 -- The result is of maximal length and starts by the first
1929 -- characters of Source.
1931 Super_Length (Source) = Source.Max_Length
1932 and then
1936 -- Depending on when we reach Max_Length, either the last part
1937 -- of Source is fully dropped and New_Item is partly dropped, or
1938 -- New_Item is fully added and the last part of Source is partly
1939 -- dropped.
1941 and then
1944 -- The last characters of New_Item are dropped
1953 New_Item
1955 -- Then Source starting from Before is added but the
1956 -- last characters are dropped.
1958 and then
1960 Before + New_Item'Length, Source.Max_Length)) =
1961 Super_Slice (Source'Old,
1962 Before, Source.Max_Length - New_Item'Length))),
1963 Global => null;
1965 function Super_Overwrite
1966 (Source : Super_String;
1967 Position : Positive;
1968 New_Item : String;
1969 Drop : Truncation := Error) return Super_String
1970 with
1971 Pre =>
1972 Position - 1 <= Super_Length (Source)
1973 and then (if New_Item'Length > Source.Max_Length - (Position - 1)
1974 then Drop /= Error),
1975 Post => Super_Overwrite'Result.Max_Length = Source.Max_Length,
1976 Contract_Cases =>
1977 (Position - 1 <= Source.Max_Length - New_Item'Length
1978 =>
1979 -- The length is unchanged, unless New_Item overwrites further than
1980 -- the end of Source. In this contract case, we suppose New_Item
1981 -- doesn't overwrite further than Max_Length.
1983 Super_Length (Super_Overwrite'Result) =
1984 Integer'Max (Super_Length (Source), Position - 1 + New_Item'Length)
1985 and then
1990 New_Item
1991 and then
1994 -- There are some unchanged characters of Source remaining
1995 -- after New_Item.
1998 Position + New_Item'Length, Super_Length (Source))) =
1999 Super_Slice (Source,
2000 Position + New_Item'Length, Super_Length (Source))),
2002 Position - 1 > Source.Max_Length - New_Item'Length and then Drop = Left
2003 =>
2004 Super_Length (Super_Overwrite'Result) = Source.Max_Length
2006 -- If a part of the result has to be dropped, it means New_Item is
2007 -- overwriting further than the end of Source. Thus the result is
2008 -- necessarily ending by New_Item. However, we don't know whether
2009 -- New_Item covers all Max_Length characters or some characters of
2010 -- Source are remaining at the left.
2012 and then
2013 (if New_Item'Length >= Source.Max_Length then
2015 -- New_Item covers all Max_Length characters
2017 Super_To_String (Super_Overwrite'Result) =
2018 New_Item
2019 (New_Item'Last - Source.Max_Length + 1 .. New_Item'Last)
2020 else
2021 -- New_Item fully appears at the end
2023 Super_Slice (Super_Overwrite'Result,
2024 Source.Max_Length - New_Item'Length + 1,
2025 Source.Max_Length) =
2026 New_Item
2028 -- The left of Source is cut
2030 and then
2038 =>
2039 -- The result is of maximal length and starts by the first
2040 -- characters of Source.
2043 and then
2045 Super_Slice (Source, 1, Position - 1)
2047 -- Then New_Item is written until Max_Length
2049 and then Super_Slice (Super_Overwrite'Result,
2050 Position, Source.Max_Length) =
2051 New_Item (New_Item'First
2052 .. Source.Max_Length - Position + New_Item'First)),
2053 Global => null;
2055 procedure Super_Overwrite
2056 (Source : in out Super_String;
2057 Position : Positive;
2058 New_Item : String;
2059 Drop : Truncation := Error)
2060 with
2061 Pre =>
2062 Position - 1 <= Super_Length (Source)
2063 and then (if New_Item'Length > Source.Max_Length - (Position - 1)
2064 then Drop /= Error),
2065 Contract_Cases =>
2066 (Position - 1 <= Source.Max_Length - New_Item'Length
2067 =>
2068 -- The length is unchanged, unless New_Item overwrites further than
2069 -- the end of Source. In this contract case, we suppose New_Item
2070 -- doesn't overwrite further than Max_Length.
2072 Super_Length (Source) = Integer'Max
2073 (Super_Length (Source'Old), Position - 1 + New_Item'Length)
2074 and then
2079 New_Item
2080 and then
2082 then
2083 -- There are some unchanged characters of Source remaining
2084 -- after New_Item.
2087 Position + New_Item'Length, Super_Length (Source'Old))) =
2088 Super_Slice (Source'Old,
2089 Position + New_Item'Length, Super_Length (Source'Old))),
2091 Position - 1 > Source.Max_Length - New_Item'Length and then Drop = Left
2092 =>
2093 Super_Length (Source) = Source.Max_Length
2095 -- If a part of the result has to be dropped, it means New_Item is
2096 -- overwriting further than the end of Source. Thus the result is
2097 -- necessarily ending by New_Item. However, we don't know whether
2098 -- New_Item covers all Max_Length characters or some characters of
2099 -- Source are remaining at the left.
2101 and then
2102 (if New_Item'Length >= Source.Max_Length then
2104 -- New_Item covers all Max_Length characters
2106 Super_To_String (Source) =
2107 New_Item
2108 (New_Item'Last - Source.Max_Length + 1 .. New_Item'Last)
2109 else
2110 -- New_Item fully appears at the end
2112 Super_Slice (Source,
2113 Source.Max_Length - New_Item'Length + 1,
2114 Source.Max_Length) =
2115 New_Item
2117 -- The left of Source is cut
2119 and then
2127 =>
2128 -- The result is of maximal length and starts by the first
2129 -- characters of Source.
2132 and then
2134 Super_Slice (Source'Old, 1, Position - 1)
2136 -- New_Item is written until Max_Length
2138 and then Super_Slice (Source, Position, Source.Max_Length) =
2139 New_Item (New_Item'First
2140 .. Source.Max_Length - Position + New_Item'First)),
2141 Global => null;
2143 function Super_Delete
2144 (Source : Super_String;
2145 From : Positive;
2146 Through : Natural) return Super_String
2147 with
2148 Pre =>
2149 (if Through >= From then From - 1 <= Super_Length (Source)),
2150 Post => Super_Delete'Result.Max_Length = Source.Max_Length,
2151 Contract_Cases =>
2152 (Through >= From =>
2153 Super_Length (Super_Delete'Result) =
2154 From - 1 + Natural'Max (Super_Length (Source) - Through, 0)
2155 and then
2158 and then
2161 From, Super_Length (Super_Delete'Result))) =
2162 Super_Slice (Source, Through + 1, Super_Length (Source))),
2163 others =>
2164 Super_Delete'Result = Source),
2165 Global => null;
2167 procedure Super_Delete
2168 (Source : in out Super_String;
2169 From : Positive;
2170 Through : Natural)
2171 with
2172 Pre =>
2173 (if Through >= From then From - 1 <= Super_Length (Source)),
2174 Contract_Cases =>
2175 (Through >= From =>
2176 Super_Length (Source) =
2177 From - 1 + Natural'Max (Super_Length (Source'Old) - Through, 0)
2178 and then
2181 and then
2184 Super_Slice (Source'Old,
2185 Through + 1, Super_Length (Source'Old))),
2186 others =>
2187 Source = Source'Old),
2188 Global => null;
2190 ---------------------------------
2191 -- String Selector Subprograms --
2192 ---------------------------------
2194 function Super_Trim
2195 (Source : Super_String;
2196 Side : Trim_End) return Super_String
2197 with
2198 Post => Super_Trim'Result.Max_Length = Source.Max_Length,
2199 Contract_Cases =>
2201 -- If all characters in Source are Space, the returned string is empty
2204 =>
2205 Super_Length (Super_Trim'Result) = 0,
2207 -- Otherwise, the returned string is a slice of Source
2209 others
2210 =>
2211 (declare
2212 Low : constant Positive :=
2213 (if Side = Right then 1
2214 else Super_Index_Non_Blank (Source, Forward));
2215 High : constant Positive :=
2216 (if Side = Left then Super_Length (Source)
2217 else Super_Index_Non_Blank (Source, Backward));
2218 begin
2219 Super_To_String (Super_Trim'Result) =
2220 Super_Slice (Source, Low, High))),
2221 Global => null;
2223 procedure Super_Trim
2224 (Source : in out Super_String;
2225 Side : Trim_End)
2226 with
2227 Contract_Cases =>
2229 -- If all characters in Source are Space, the returned string is empty
2232 =>
2233 Super_Length (Source) = 0,
2235 -- Otherwise, the returned string is a slice of Source
2237 others
2238 =>
2239 (declare
2240 Low : constant Positive :=
2241 (if Side = Right then 1
2242 else Super_Index_Non_Blank (Source'Old, Forward));
2243 High : constant Positive :=
2244 (if Side = Left then Super_Length (Source'Old)
2245 else Super_Index_Non_Blank (Source'Old, Backward));
2246 begin
2247 Super_To_String (Source) = Super_Slice (Source'Old, Low, High))),
2248 Global => null;
2250 function Super_Trim
2251 (Source : Super_String;
2252 Left : Maps.Character_Set;
2253 Right : Maps.Character_Set) return Super_String
2254 with
2255 Post => Super_Trim'Result.Max_Length = Source.Max_Length,
2256 Contract_Cases =>
2258 -- If all characters in Source are contained in one of the sets Left or
2259 -- Right, then the returned string is empty.
2261 ((for all C of Super_To_String (Source) => Maps.Is_In (C, Left))
2262 or else
2263 (for all C of Super_To_String (Source) => Maps.Is_In (C, Right))
2264 =>
2265 Super_Length (Super_Trim'Result) = 0,
2267 -- Otherwise, the returned string is a slice of Source
2269 others
2270 =>
2271 (declare
2272 Low : constant Positive :=
2273 Super_Index (Source, Left, Outside, Forward);
2274 High : constant Positive :=
2275 Super_Index (Source, Right, Outside, Backward);
2276 begin
2277 Super_To_String (Super_Trim'Result) =
2278 Super_Slice (Source, Low, High))),
2279 Global => null;
2281 procedure Super_Trim
2282 (Source : in out Super_String;
2283 Left : Maps.Character_Set;
2284 Right : Maps.Character_Set)
2285 with
2286 Contract_Cases =>
2288 -- If all characters in Source are contained in one of the sets Left or
2289 -- Right, then the returned string is empty.
2291 ((for all C of Super_To_String (Source) => Maps.Is_In (C, Left))
2292 or else
2293 (for all C of Super_To_String (Source) => Maps.Is_In (C, Right))
2294 =>
2295 Super_Length (Source) = 0,
2297 -- Otherwise, the returned string is a slice of Source
2299 others
2300 =>
2301 (declare
2302 Low : constant Positive :=
2303 Super_Index (Source'Old, Left, Outside, Forward);
2304 High : constant Positive :=
2305 Super_Index (Source'Old, Right, Outside, Backward);
2306 begin
2307 Super_To_String (Source) = Super_Slice (Source'Old, Low, High))),
2308 Global => null;
2310 function Super_Head
2311 (Source : Super_String;
2312 Count : Natural;
2313 Pad : Character := Space;
2314 Drop : Truncation := Error) return Super_String
2315 with
2316 Pre => (if Count > Source.Max_Length then Drop /= Error),
2317 Post => Super_Head'Result.Max_Length = Source.Max_Length,
2318 Contract_Cases =>
2319 (Count <= Super_Length (Source)
2320 =>
2321 -- Source is cut
2323 Super_To_String (Super_Head'Result) = Super_Slice (Source, 1, Count),
2324 Count > Super_Length (Source) and then Count <= Source.Max_Length
2325 =>
2326 -- Source is followed by Pad characters
2328 Super_Length (Super_Head'Result) = Count
2329 and then
2330 Super_Slice (Super_Head'Result, 1, Super_Length (Source)) =
2331 Super_To_String (Source)
2332 and then
2337 =>
2338 -- Source is followed by Pad characters
2341 and then
2344 and then
2346 Super_Length (Source) + 1, Source.Max_Length)) =
2347 [1 .. Source.Max_Length - Super_Length (Source) => Pad],
2348 Count - Super_Length (Source) > Source.Max_Length and then Drop = Left
2349 =>
2350 -- Source is fully dropped on the left
2352 Super_To_String (Super_Head'Result) =
2353 [1 .. Source.Max_Length => Pad],
2354 others
2355 =>
2356 -- Source is partly dropped on the left
2358 Super_Length (Super_Head'Result) = Source.Max_Length
2359 and then
2364 and then
2366 Source.Max_Length - Count + Super_Length (Source) + 1,
2367 Source.Max_Length)) =
2368 [1 .. Count - Super_Length (Source) => Pad]),
2369 Global => null;
2371 procedure Super_Head
2372 (Source : in out Super_String;
2373 Count : Natural;
2374 Pad : Character := Space;
2375 Drop : Truncation := Error)
2376 with
2377 Pre => (if Count > Source.Max_Length then Drop /= Error),
2378 Contract_Cases =>
2379 (Count <= Super_Length (Source)
2380 =>
2381 -- Source is cut
2383 Super_To_String (Source) = Super_Slice (Source'Old, 1, Count),
2384 Count > Super_Length (Source) and then Count <= Source.Max_Length
2385 =>
2386 -- Source is followed by Pad characters
2388 Super_Length (Source) = Count
2389 and then
2390 Super_Slice (Source, 1, Super_Length (Source'Old)) =
2391 Super_To_String (Source'Old)
2392 and then
2397 =>
2398 -- Source is followed by Pad characters
2401 and then
2404 and then
2406 Super_Length (Source'Old) + 1, Source.Max_Length)) =
2407 [1 .. Source.Max_Length - Super_Length (Source'Old) => Pad],
2408 Count - Super_Length (Source) > Source.Max_Length and then Drop = Left
2409 =>
2410 -- Source is fully dropped on the left
2412 Super_To_String (Source) = [1 .. Source.Max_Length => Pad],
2413 others
2414 =>
2415 -- Source is partly dropped on the left
2417 Super_Length (Source) = Source.Max_Length
2418 and then
2423 and then
2425 Source.Max_Length - Count + Super_Length (Source'Old) + 1,
2426 Source.Max_Length)) =
2427 [1 .. Count - Super_Length (Source'Old) => Pad]),
2428 Global => null;
2430 function Super_Tail
2431 (Source : Super_String;
2432 Count : Natural;
2433 Pad : Character := Space;
2434 Drop : Truncation := Error) return Super_String
2435 with
2436 Pre => (if Count > Source.Max_Length then Drop /= Error),
2437 Post => Super_Tail'Result.Max_Length = Source.Max_Length,
2438 Contract_Cases =>
2439 (Count < Super_Length (Source)
2440 =>
2441 -- Source is cut
2443 (if Count > 0 then
2444 Super_To_String (Super_Tail'Result) =
2445 Super_Slice (Source,
2446 Super_Length (Source) - Count + 1, Super_Length (Source))
2447 else Super_Length (Super_Tail'Result) = 0),
2448 Count >= Super_Length (Source) and then Count < Source.Max_Length
2449 =>
2450 -- Source is preceded by Pad characters
2452 Super_Length (Super_Tail'Result) = Count
2453 and then
2457 and then
2462 =>
2463 -- Source is preceded by Pad characters
2466 and then
2468 1, Source.Max_Length - Super_Length (Source))) =
2469 [1 .. Source.Max_Length - Super_Length (Source) => Pad]
2470 and then
2471 (if Super_Length (Source) > 0 then
2472 Super_Slice (Super_Tail'Result,
2473 Source.Max_Length - Super_Length (Source) + 1,
2474 Source.Max_Length) =
2475 Super_To_String (Source)),
2476 Count - Super_Length (Source) >= Source.Max_Length
2477 and then Drop /= Left
2478 =>
2479 -- Source is fully dropped on the right
2481 Super_To_String (Super_Tail'Result) =
2482 [1 .. Source.Max_Length => Pad],
2483 others
2484 =>
2485 -- Source is partly dropped on the right
2487 Super_Length (Super_Tail'Result) = Source.Max_Length
2488 and then
2492 and then
2494 Count - Super_Length (Source) + 1, Source.Max_Length)) =
2495 Super_Slice (Source,
2496 1, Source.Max_Length - Count + Super_Length (Source))),
2497 Global => null;
2499 procedure Super_Tail
2500 (Source : in out Super_String;
2501 Count : Natural;
2502 Pad : Character := Space;
2503 Drop : Truncation := Error)
2504 with
2505 Pre => (if Count > Source.Max_Length then Drop /= Error),
2506 Contract_Cases =>
2507 (Count < Super_Length (Source)
2508 =>
2509 -- Source is cut
2511 (if Count > 0 then
2512 Super_To_String (Source) =
2513 Super_Slice (Source'Old,
2514 Super_Length (Source'Old) - Count + 1,
2515 Super_Length (Source'Old))
2516 else Super_Length (Source) = 0),
2517 Count >= Super_Length (Source) and then Count < Source.Max_Length
2518 =>
2519 -- Source is preceded by Pad characters
2521 Super_Length (Source) = Count
2522 and then
2526 and then
2531 =>
2532 -- Source is preceded by Pad characters
2535 and then
2537 1, Source.Max_Length - Super_Length (Source'Old))) =
2538 [1 .. Source.Max_Length - Super_Length (Source'Old) => Pad]
2539 and then
2540 (if Super_Length (Source'Old) > 0 then
2541 Super_Slice (Source,
2542 Source.Max_Length - Super_Length (Source'Old) + 1,
2543 Source.Max_Length) =
2544 Super_To_String (Source'Old)),
2545 Count - Super_Length (Source) >= Source.Max_Length
2546 and then Drop /= Left
2547 =>
2548 -- Source is fully dropped on the right
2550 Super_To_String (Source) = [1 .. Source.Max_Length => Pad],
2551 others
2552 =>
2553 -- Source is partly dropped on the right
2555 Super_Length (Source) = Source.Max_Length
2556 and then
2560 and then
2562 Count - Super_Length (Source'Old) + 1, Source.Max_Length)) =
2563 Super_Slice (Source'Old,
2564 1, Source.Max_Length - Count + Super_Length (Source'Old))),
2565 Global => null;
2567 ------------------------------------
2568 -- String Constructor Subprograms --
2569 ------------------------------------
2571 -- Note: in some of the following routines, there is an extra parameter
2572 -- Max_Length which specifies the value of the maximum length for the
2573 -- resulting Super_String value.
2575 function Times
2576 (Left : Natural;
2577 Right : Character;
2578 Max_Length : Positive) return Super_String
2579 with
2580 Pre => Left <= Max_Length,
2581 Post => Times'Result.Max_Length = Max_Length
2582 and then Super_To_String (Times'Result) = [1 .. Left => Right],
2583 Global => null;
2584 -- Note the additional parameter Max_Length
2586 function Times
2587 (Left : Natural;
2588 Right : String;
2589 Max_Length : Positive) return Super_String
2590 with
2591 Pre => (if Left /= 0 then Right'Length <= Max_Length / Left),
2592 Post => Times'Result.Max_Length = Max_Length
2593 and then Super_Length (Times'Result) = Left * Right'Length
2594 and then
2595 (if Right'Length > 0 then
2596 (for all K in 1 .. Left * Right'Length =>
2597 Super_Element (Times'Result, K) =
2598 Right (Right'First + (K - 1) mod Right'Length))),
2599 Global => null;
2600 -- Note the additional parameter Max_Length
2602 function Times
2603 (Left : Natural;
2604 Right : Super_String) return Super_String
2605 with
2606 Pre =>
2607 (if Left /= 0 then Super_Length (Right) <= Right.Max_Length / Left),
2608 Post => Times'Result.Max_Length = Right.Max_Length
2609 and then Super_Length (Times'Result) = Left * Super_Length (Right)
2610 and then
2611 (if Super_Length (Right) > 0 then
2612 (for all K in 1 .. Left * Super_Length (Right) =>
2613 Super_Element (Times'Result, K) =
2614 Super_Element (Right, 1 + (K - 1) mod Super_Length (Right)))),
2615 Global => null;
2617 function Super_Replicate
2618 (Count : Natural;
2619 Item : Character;
2620 Drop : Truncation := Error;
2621 Max_Length : Positive) return Super_String
2622 with
2623 Pre => (if Count > Max_Length then Drop /= Error),
2624 Post => Super_Replicate'Result.Max_Length = Max_Length
2625 and then Super_To_String (Super_Replicate'Result) =
2626 [1 .. Natural'Min (Max_Length, Count) => Item],
2627 Global => null;
2628 -- Note the additional parameter Max_Length
2630 function Super_Replicate
2631 (Count : Natural;
2632 Item : String;
2633 Drop : Truncation := Error;
2634 Max_Length : Positive) return Super_String
2635 with
2636 Pre =>
2637 (if Count /= 0 and then Item'Length > Max_Length / Count
2638 then Drop /= Error),
2639 Post => Super_Replicate'Result.Max_Length = Max_Length,
2640 Contract_Cases =>
2641 (Count = 0 or else Item'Length <= Max_Length / Count
2642 =>
2643 Super_Length (Super_Replicate'Result) = Count * Item'Length
2644 and then
2645 (if Item'Length > 0 then
2646 (for all K in 1 .. Count * Item'Length =>
2647 Super_Element (Super_Replicate'Result, K) =
2648 Item (Item'First + (K - 1) mod Item'Length))),
2649 Count /= 0
2650 and then Item'Length > Max_Length / Count
2651 and then Drop = Right
2652 =>
2653 Super_Length (Super_Replicate'Result) = Max_Length
2654 and then
2655 (for all K in 1 .. Max_Length =>
2656 Super_Element (Super_Replicate'Result, K) =
2657 Item (Item'First + (K - 1) mod Item'Length)),
2658 others -- Drop = Left
2659 =>
2660 Super_Length (Super_Replicate'Result) = Max_Length
2661 and then
2662 (for all K in 1 .. Max_Length =>
2663 Super_Element (Super_Replicate'Result, K) =
2664 Item (Item'Last - (Max_Length - K) mod Item'Length))),
2665 Global => null;
2666 -- Note the additional parameter Max_Length
2668 function Super_Replicate
2669 (Count : Natural;
2670 Item : Super_String;
2671 Drop : Truncation := Error) return Super_String
2672 with
2673 Pre =>
2674 (if Count /= 0
2675 and then Super_Length (Item) > Item.Max_Length / Count
2676 then Drop /= Error),
2677 Post => Super_Replicate'Result.Max_Length = Item.Max_Length,
2678 Contract_Cases =>
2679 ((if Count /= 0 then Super_Length (Item) <= Item.Max_Length / Count)
2680 =>
2681 Super_Length (Super_Replicate'Result) = Count * Super_Length (Item)
2682 and then
2683 (if Super_Length (Item) > 0 then
2684 (for all K in 1 .. Count * Super_Length (Item) =>
2685 Super_Element (Super_Replicate'Result, K) =
2686 Super_Element (Item,
2687 1 + (K - 1) mod Super_Length (Item)))),
2688 Count /= 0
2689 and then Super_Length (Item) > Item.Max_Length / Count
2690 and then Drop = Right
2691 =>
2692 Super_Length (Super_Replicate'Result) = Item.Max_Length
2693 and then
2694 (for all K in 1 .. Item.Max_Length =>
2695 Super_Element (Super_Replicate'Result, K) =
2696 Super_Element (Item, 1 + (K - 1) mod Super_Length (Item))),
2697 others -- Drop = Left
2698 =>
2699 Super_Length (Super_Replicate'Result) = Item.Max_Length
2700 and then
2701 (for all K in 1 .. Item.Max_Length =>
2702 Super_Element (Super_Replicate'Result, K) =
2703 Super_Element (Item,
2704 Super_Length (Item)
2705 - (Item.Max_Length - K) mod Super_Length (Item)))),
2706 Global => null;
2708 procedure Put_Image
2709 (S : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class;
2710 Source : Super_String);
2712 private
2713 -- Pragma Inline declarations
2715 pragma Inline ("=");
2716 pragma Inline (Less);
2717 pragma Inline (Less_Or_Equal);
2718 pragma Inline (Greater);
2719 pragma Inline (Greater_Or_Equal);
2720 pragma Inline (Concat);
2721 pragma Inline (Super_Count);
2722 pragma Inline (Super_Element);
2723 pragma Inline (Super_Find_Token);
2724 pragma Inline (Super_Index);
2725 pragma Inline (Super_Index_Non_Blank);
2726 pragma Inline (Super_Length);
2727 pragma Inline (Super_Replace_Element);
2728 pragma Inline (Super_Slice);
2729 pragma Inline (Super_To_String);
2731 end Ada.Strings.Superbounded;