|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT RUN-TIME COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- A D A . S T R I N G S . U N B O U N D E D --
|
|
|
6 -- --
|
|
|
7 -- S p e c --
|
|
|
8 -- --
|
|
145
|
9 -- Copyright (C) 1992-2019, Free Software Foundation, Inc. --
|
|
111
|
10 -- --
|
|
|
11 -- This specification is derived from the Ada Reference Manual for use with --
|
|
|
12 -- GNAT. The copyright notice above, and the license provisions that follow --
|
|
|
13 -- apply solely to the contents of the part following the private keyword. --
|
|
|
14 -- --
|
|
|
15 -- GNAT is free software; you can redistribute it and/or modify it under --
|
|
|
16 -- terms of the GNU General Public License as published by the Free Soft- --
|
|
|
17 -- ware Foundation; either version 3, or (at your option) any later ver- --
|
|
|
18 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
|
|
|
19 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
|
|
|
20 -- or FITNESS FOR A PARTICULAR PURPOSE. --
|
|
|
21 -- --
|
|
|
22 -- As a special exception under Section 7 of GPL version 3, you are granted --
|
|
|
23 -- additional permissions described in the GCC Runtime Library Exception, --
|
|
|
24 -- version 3.1, as published by the Free Software Foundation. --
|
|
|
25 -- --
|
|
|
26 -- You should have received a copy of the GNU General Public License and --
|
|
|
27 -- a copy of the GCC Runtime Library Exception along with this program; --
|
|
|
28 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
|
|
|
29 -- <http://www.gnu.org/licenses/>. --
|
|
|
30 -- --
|
|
|
31 -- GNAT was originally developed by the GNAT team at New York University. --
|
|
|
32 -- Extensive contributions were provided by Ada Core Technologies Inc. --
|
|
|
33 -- --
|
|
|
34 ------------------------------------------------------------------------------
|
|
|
35
|
|
145
|
36 -- Preconditions in this unit are meant for analysis only, not for run-time
|
|
|
37 -- checking, so that the expected exceptions are raised. This is enforced by
|
|
|
38 -- setting the corresponding assertion policy to Ignore.
|
|
|
39
|
|
|
40 pragma Assertion_Policy (Pre => Ignore);
|
|
|
41
|
|
111
|
42 -- This package provides an implementation of Ada.Strings.Unbounded that uses
|
|
|
43 -- reference counts to implement copy on modification (rather than copy on
|
|
|
44 -- assignment). This is significantly more efficient on many targets.
|
|
|
45
|
|
|
46 -- This version is supported on:
|
|
|
47 -- - all Alpha platforms
|
|
|
48 -- - all ia64 platforms
|
|
|
49 -- - all PowerPC platforms
|
|
|
50 -- - all SPARC V9 platforms
|
|
|
51 -- - all x86 platforms
|
|
|
52 -- - all x86_64 platforms
|
|
|
53
|
|
|
54 -- This package uses several techniques to increase speed:
|
|
|
55
|
|
|
56 -- - Implicit sharing or copy-on-write. An Unbounded_String contains only
|
|
|
57 -- the reference to the data which is shared between several instances.
|
|
|
58 -- The shared data is reallocated only when its value is changed and
|
|
|
59 -- the object mutation can't be used or it is inefficient to use it.
|
|
|
60
|
|
|
61 -- - Object mutation. Shared data object can be reused without memory
|
|
|
62 -- reallocation when all of the following requirements are met:
|
|
|
63 -- - the shared data object is no longer used by anyone else;
|
|
|
64 -- - the size is sufficient to store the new value;
|
|
|
65 -- - the gap after reuse is less than a defined threshold.
|
|
|
66
|
|
|
67 -- - Memory preallocation. Most of used memory allocation algorithms
|
|
|
68 -- align allocated segments on the some boundary, thus some amount of
|
|
|
69 -- additional memory can be preallocated without any impact. Such
|
|
|
70 -- preallocated memory can used later by Append/Insert operations
|
|
|
71 -- without reallocation.
|
|
|
72
|
|
|
73 -- Reference counting uses GCC builtin atomic operations, which allows safe
|
|
|
74 -- sharing of internal data between Ada tasks. Nevertheless, this does not
|
|
|
75 -- make objects of Unbounded_String thread-safe: an instance cannot be
|
|
|
76 -- accessed by several tasks simultaneously.
|
|
|
77
|
|
|
78 with Ada.Strings.Maps;
|
|
|
79 private with Ada.Finalization;
|
|
|
80 private with System.Atomic_Counters;
|
|
|
81
|
|
145
|
82 package Ada.Strings.Unbounded with
|
|
|
83 Initial_Condition => Length (Null_Unbounded_String) = 0
|
|
|
84 is
|
|
111
|
85 pragma Preelaborate;
|
|
|
86
|
|
|
87 type Unbounded_String is private;
|
|
|
88 pragma Preelaborable_Initialization (Unbounded_String);
|
|
|
89
|
|
|
90 Null_Unbounded_String : constant Unbounded_String;
|
|
|
91
|
|
145
|
92 function Length (Source : Unbounded_String) return Natural with
|
|
|
93 Global => null;
|
|
111
|
94
|
|
|
95 type String_Access is access all String;
|
|
|
96
|
|
|
97 procedure Free (X : in out String_Access);
|
|
|
98
|
|
|
99 --------------------------------------------------------
|
|
|
100 -- Conversion, Concatenation, and Selection Functions --
|
|
|
101 --------------------------------------------------------
|
|
|
102
|
|
|
103 function To_Unbounded_String
|
|
145
|
104 (Source : String) return Unbounded_String
|
|
|
105 with
|
|
|
106 Post => Length (To_Unbounded_String'Result) = Source'Length,
|
|
|
107 Global => null;
|
|
111
|
108
|
|
|
109 function To_Unbounded_String
|
|
145
|
110 (Length : Natural) return Unbounded_String
|
|
|
111 with
|
|
|
112 Post =>
|
|
|
113 Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length,
|
|
|
114 Global => null;
|
|
111
|
115
|
|
145
|
116 function To_String (Source : Unbounded_String) return String with
|
|
|
117 Post => To_String'Result'Length = Length (Source),
|
|
|
118 Global => null;
|
|
111
|
119
|
|
|
120 procedure Set_Unbounded_String
|
|
|
121 (Target : out Unbounded_String;
|
|
145
|
122 Source : String)
|
|
|
123 with
|
|
|
124 Global => null;
|
|
111
|
125 pragma Ada_05 (Set_Unbounded_String);
|
|
|
126
|
|
|
127 procedure Append
|
|
|
128 (Source : in out Unbounded_String;
|
|
145
|
129 New_Item : Unbounded_String)
|
|
|
130 with
|
|
|
131 Pre => Length (New_Item) <= Natural'Last - Length (Source),
|
|
|
132 Post => Length (Source) = Length (Source)'Old + Length (New_Item),
|
|
|
133 Global => null;
|
|
111
|
134
|
|
|
135 procedure Append
|
|
|
136 (Source : in out Unbounded_String;
|
|
145
|
137 New_Item : String)
|
|
|
138 with
|
|
|
139 Pre => New_Item'Length <= Natural'Last - Length (Source),
|
|
|
140 Post => Length (Source) = Length (Source)'Old + New_Item'Length,
|
|
|
141 Global => null;
|
|
111
|
142
|
|
|
143 procedure Append
|
|
|
144 (Source : in out Unbounded_String;
|
|
145
|
145 New_Item : Character)
|
|
|
146 with
|
|
|
147 Pre => Length (Source) < Natural'Last,
|
|
|
148 Post => Length (Source) = Length (Source)'Old + 1,
|
|
|
149 Global => null;
|
|
111
|
150
|
|
|
151 function "&"
|
|
|
152 (Left : Unbounded_String;
|
|
145
|
153 Right : Unbounded_String) return Unbounded_String
|
|
|
154 with
|
|
|
155 Pre => Length (Right) <= Natural'Last - Length (Left),
|
|
|
156 Post => Length ("&"'Result) = Length (Left) + Length (Right),
|
|
|
157 Global => null;
|
|
111
|
158
|
|
|
159 function "&"
|
|
|
160 (Left : Unbounded_String;
|
|
145
|
161 Right : String) return Unbounded_String
|
|
|
162 with
|
|
|
163 Pre => Right'Length <= Natural'Last - Length (Left),
|
|
|
164 Post => Length ("&"'Result) = Length (Left) + Right'Length,
|
|
|
165 Global => null;
|
|
111
|
166
|
|
|
167 function "&"
|
|
|
168 (Left : String;
|
|
145
|
169 Right : Unbounded_String) return Unbounded_String
|
|
|
170 with
|
|
|
171 Pre => Left'Length <= Natural'Last - Length (Right),
|
|
|
172 Post => Length ("&"'Result) = Left'Length + Length (Right),
|
|
|
173 Global => null;
|
|
111
|
174
|
|
|
175 function "&"
|
|
|
176 (Left : Unbounded_String;
|
|
145
|
177 Right : Character) return Unbounded_String
|
|
|
178 with
|
|
|
179 Pre => Length (Left) < Natural'Last,
|
|
|
180 Post => Length ("&"'Result) = Length (Left) + 1,
|
|
|
181 Global => null;
|
|
111
|
182
|
|
|
183 function "&"
|
|
|
184 (Left : Character;
|
|
145
|
185 Right : Unbounded_String) return Unbounded_String
|
|
|
186 with
|
|
|
187 Pre => Length (Right) < Natural'Last,
|
|
|
188 Post => Length ("&"'Result) = Length (Right) + 1,
|
|
|
189 Global => null;
|
|
111
|
190
|
|
|
191 function Element
|
|
|
192 (Source : Unbounded_String;
|
|
145
|
193 Index : Positive) return Character
|
|
|
194 with
|
|
|
195 Pre => Index <= Length (Source),
|
|
|
196 Global => null;
|
|
111
|
197
|
|
|
198 procedure Replace_Element
|
|
|
199 (Source : in out Unbounded_String;
|
|
|
200 Index : Positive;
|
|
145
|
201 By : Character)
|
|
|
202 with
|
|
|
203 Pre => Index <= Length (Source),
|
|
|
204 Post => Length (Source) = Length (Source)'Old,
|
|
|
205 Global => null;
|
|
111
|
206
|
|
|
207 function Slice
|
|
|
208 (Source : Unbounded_String;
|
|
|
209 Low : Positive;
|
|
145
|
210 High : Natural) return String
|
|
|
211 with
|
|
|
212 Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
|
|
|
213 Post => Slice'Result'Length = Natural'Max (0, High - Low + 1),
|
|
|
214 Global => null;
|
|
111
|
215
|
|
|
216 function Unbounded_Slice
|
|
|
217 (Source : Unbounded_String;
|
|
|
218 Low : Positive;
|
|
145
|
219 High : Natural) return Unbounded_String
|
|
|
220 with
|
|
|
221 Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
|
|
|
222 Post =>
|
|
|
223 Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
|
|
|
224 Global => null;
|
|
111
|
225 pragma Ada_05 (Unbounded_Slice);
|
|
|
226
|
|
|
227 procedure Unbounded_Slice
|
|
|
228 (Source : Unbounded_String;
|
|
|
229 Target : out Unbounded_String;
|
|
|
230 Low : Positive;
|
|
145
|
231 High : Natural)
|
|
|
232 with
|
|
|
233 Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
|
|
|
234 Post => Length (Target) = Natural'Max (0, High - Low + 1),
|
|
|
235 Global => null;
|
|
111
|
236 pragma Ada_05 (Unbounded_Slice);
|
|
|
237
|
|
|
238 function "="
|
|
|
239 (Left : Unbounded_String;
|
|
145
|
240 Right : Unbounded_String) return Boolean
|
|
|
241 with
|
|
|
242 Global => null;
|
|
111
|
243
|
|
|
244 function "="
|
|
|
245 (Left : Unbounded_String;
|
|
145
|
246 Right : String) return Boolean
|
|
|
247 with
|
|
|
248 Global => null;
|
|
111
|
249
|
|
|
250 function "="
|
|
|
251 (Left : String;
|
|
145
|
252 Right : Unbounded_String) return Boolean
|
|
|
253 with
|
|
|
254 Global => null;
|
|
111
|
255
|
|
|
256 function "<"
|
|
|
257 (Left : Unbounded_String;
|
|
145
|
258 Right : Unbounded_String) return Boolean
|
|
|
259 with
|
|
|
260 Global => null;
|
|
111
|
261
|
|
|
262 function "<"
|
|
|
263 (Left : Unbounded_String;
|
|
145
|
264 Right : String) return Boolean
|
|
|
265 with
|
|
|
266 Global => null;
|
|
111
|
267
|
|
|
268 function "<"
|
|
|
269 (Left : String;
|
|
145
|
270 Right : Unbounded_String) return Boolean
|
|
|
271 with
|
|
|
272 Global => null;
|
|
111
|
273
|
|
|
274 function "<="
|
|
|
275 (Left : Unbounded_String;
|
|
145
|
276 Right : Unbounded_String) return Boolean
|
|
|
277 with
|
|
|
278 Global => null;
|
|
111
|
279
|
|
|
280 function "<="
|
|
|
281 (Left : Unbounded_String;
|
|
145
|
282 Right : String) return Boolean
|
|
|
283 with
|
|
|
284 Global => null;
|
|
111
|
285
|
|
|
286 function "<="
|
|
|
287 (Left : String;
|
|
145
|
288 Right : Unbounded_String) return Boolean
|
|
|
289 with
|
|
|
290 Global => null;
|
|
111
|
291
|
|
|
292 function ">"
|
|
|
293 (Left : Unbounded_String;
|
|
145
|
294 Right : Unbounded_String) return Boolean
|
|
|
295 with
|
|
|
296 Global => null;
|
|
111
|
297
|
|
|
298 function ">"
|
|
|
299 (Left : Unbounded_String;
|
|
145
|
300 Right : String) return Boolean
|
|
|
301 with
|
|
|
302 Global => null;
|
|
111
|
303
|
|
|
304 function ">"
|
|
|
305 (Left : String;
|
|
145
|
306 Right : Unbounded_String) return Boolean
|
|
|
307 with
|
|
|
308 Global => null;
|
|
111
|
309
|
|
|
310 function ">="
|
|
|
311 (Left : Unbounded_String;
|
|
145
|
312 Right : Unbounded_String) return Boolean
|
|
|
313 with
|
|
|
314 Global => null;
|
|
111
|
315
|
|
|
316 function ">="
|
|
|
317 (Left : Unbounded_String;
|
|
145
|
318 Right : String) return Boolean
|
|
|
319 with
|
|
|
320 Global => null;
|
|
111
|
321
|
|
|
322 function ">="
|
|
|
323 (Left : String;
|
|
145
|
324 Right : Unbounded_String) return Boolean
|
|
|
325 with
|
|
|
326 Global => null;
|
|
111
|
327
|
|
|
328 ------------------------
|
|
|
329 -- Search Subprograms --
|
|
|
330 ------------------------
|
|
|
331
|
|
|
332 function Index
|
|
|
333 (Source : Unbounded_String;
|
|
|
334 Pattern : String;
|
|
|
335 Going : Direction := Forward;
|
|
145
|
336 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
|
|
|
337 with
|
|
|
338 Pre => Pattern'Length /= 0,
|
|
|
339 Global => null;
|
|
111
|
340
|
|
|
341 function Index
|
|
|
342 (Source : Unbounded_String;
|
|
|
343 Pattern : String;
|
|
|
344 Going : Direction := Forward;
|
|
145
|
345 Mapping : Maps.Character_Mapping_Function) return Natural
|
|
|
346 with
|
|
|
347 Pre => Pattern'Length /= 0,
|
|
|
348 Global => null;
|
|
111
|
349
|
|
|
350 function Index
|
|
|
351 (Source : Unbounded_String;
|
|
|
352 Set : Maps.Character_Set;
|
|
|
353 Test : Membership := Inside;
|
|
145
|
354 Going : Direction := Forward) return Natural
|
|
|
355 with
|
|
|
356 Global => null;
|
|
111
|
357
|
|
|
358 function Index
|
|
|
359 (Source : Unbounded_String;
|
|
|
360 Pattern : String;
|
|
|
361 From : Positive;
|
|
|
362 Going : Direction := Forward;
|
|
145
|
363 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
|
|
|
364 with
|
|
|
365 Pre => (if Length (Source) /= 0
|
|
|
366 then From <= Length (Source))
|
|
|
367 and then Pattern'Length /= 0,
|
|
|
368 Global => null;
|
|
111
|
369 pragma Ada_05 (Index);
|
|
|
370
|
|
|
371 function Index
|
|
|
372 (Source : Unbounded_String;
|
|
|
373 Pattern : String;
|
|
|
374 From : Positive;
|
|
|
375 Going : Direction := Forward;
|
|
145
|
376 Mapping : Maps.Character_Mapping_Function) return Natural
|
|
|
377 with
|
|
|
378 Pre => (if Length (Source) /= 0
|
|
|
379 then From <= Length (Source))
|
|
|
380 and then Pattern'Length /= 0,
|
|
|
381 Global => null;
|
|
|
382
|
|
111
|
383 pragma Ada_05 (Index);
|
|
|
384
|
|
|
385 function Index
|
|
|
386 (Source : Unbounded_String;
|
|
|
387 Set : Maps.Character_Set;
|
|
|
388 From : Positive;
|
|
|
389 Test : Membership := Inside;
|
|
145
|
390 Going : Direction := Forward) return Natural
|
|
|
391 with
|
|
|
392 Pre => (if Length (Source) /= 0 then From <= Length (Source)),
|
|
|
393 Global => null;
|
|
111
|
394 pragma Ada_05 (Index);
|
|
|
395
|
|
|
396 function Index_Non_Blank
|
|
|
397 (Source : Unbounded_String;
|
|
145
|
398 Going : Direction := Forward) return Natural
|
|
|
399 with
|
|
|
400 Global => null;
|
|
111
|
401
|
|
|
402 function Index_Non_Blank
|
|
|
403 (Source : Unbounded_String;
|
|
|
404 From : Positive;
|
|
145
|
405 Going : Direction := Forward) return Natural
|
|
|
406 with
|
|
|
407 Pre => (if Length (Source) /= 0 then From <= Length (Source)),
|
|
|
408 Global => null;
|
|
111
|
409 pragma Ada_05 (Index_Non_Blank);
|
|
|
410
|
|
|
411 function Count
|
|
|
412 (Source : Unbounded_String;
|
|
|
413 Pattern : String;
|
|
145
|
414 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
|
|
|
415 with
|
|
|
416 Pre => Pattern'Length /= 0,
|
|
|
417 Global => null;
|
|
111
|
418
|
|
|
419 function Count
|
|
|
420 (Source : Unbounded_String;
|
|
|
421 Pattern : String;
|
|
145
|
422 Mapping : Maps.Character_Mapping_Function) return Natural
|
|
|
423 with
|
|
|
424 Pre => Pattern'Length /= 0,
|
|
|
425 Global => null;
|
|
111
|
426
|
|
|
427 function Count
|
|
|
428 (Source : Unbounded_String;
|
|
145
|
429 Set : Maps.Character_Set) return Natural
|
|
|
430 with
|
|
|
431 Global => null;
|
|
111
|
432
|
|
|
433 procedure Find_Token
|
|
|
434 (Source : Unbounded_String;
|
|
|
435 Set : Maps.Character_Set;
|
|
|
436 From : Positive;
|
|
|
437 Test : Membership;
|
|
|
438 First : out Positive;
|
|
145
|
439 Last : out Natural)
|
|
|
440 with
|
|
|
441 Pre => (if Length (Source) /= 0 then From <= Length (Source)),
|
|
|
442 Global => null;
|
|
111
|
443 pragma Ada_2012 (Find_Token);
|
|
|
444
|
|
|
445 procedure Find_Token
|
|
|
446 (Source : Unbounded_String;
|
|
|
447 Set : Maps.Character_Set;
|
|
|
448 Test : Membership;
|
|
|
449 First : out Positive;
|
|
145
|
450 Last : out Natural)
|
|
|
451 with
|
|
|
452 Global => null;
|
|
111
|
453
|
|
|
454 ------------------------------------
|
|
|
455 -- String Translation Subprograms --
|
|
|
456 ------------------------------------
|
|
|
457
|
|
|
458 function Translate
|
|
|
459 (Source : Unbounded_String;
|
|
145
|
460 Mapping : Maps.Character_Mapping) return Unbounded_String
|
|
|
461 with
|
|
|
462 Post => Length (Translate'Result) = Length (Source),
|
|
|
463 Global => null;
|
|
111
|
464
|
|
|
465 procedure Translate
|
|
|
466 (Source : in out Unbounded_String;
|
|
145
|
467 Mapping : Maps.Character_Mapping)
|
|
|
468 with
|
|
|
469 Post => Length (Source) = Length (Source)'Old,
|
|
|
470 Global => null;
|
|
111
|
471
|
|
|
472 function Translate
|
|
|
473 (Source : Unbounded_String;
|
|
145
|
474 Mapping : Maps.Character_Mapping_Function) return Unbounded_String
|
|
|
475 with
|
|
|
476 Post => Length (Translate'Result) = Length (Source),
|
|
|
477 Global => null;
|
|
111
|
478
|
|
|
479 procedure Translate
|
|
|
480 (Source : in out Unbounded_String;
|
|
145
|
481 Mapping : Maps.Character_Mapping_Function)
|
|
|
482 with
|
|
|
483 Post => Length (Source) = Length (Source)'Old,
|
|
|
484 Global => null;
|
|
111
|
485
|
|
|
486 ---------------------------------------
|
|
|
487 -- String Transformation Subprograms --
|
|
|
488 ---------------------------------------
|
|
|
489
|
|
|
490 function Replace_Slice
|
|
|
491 (Source : Unbounded_String;
|
|
|
492 Low : Positive;
|
|
|
493 High : Natural;
|
|
145
|
494 By : String) return Unbounded_String
|
|
|
495 with
|
|
|
496 Pre =>
|
|
|
497 Low - 1 <= Length (Source)
|
|
|
498 and then (if High >= Low
|
|
|
499 then Low - 1
|
|
|
500 <= Natural'Last - By'Length
|
|
|
501 - Natural'Max (Length (Source) - High, 0)
|
|
|
502 else Length (Source) <= Natural'Last - By'Length),
|
|
|
503 Contract_Cases =>
|
|
|
504 (High >= Low =>
|
|
|
505 Length (Replace_Slice'Result)
|
|
|
506 = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
|
|
|
507 others =>
|
|
|
508 Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
|
|
|
509 Global => null;
|
|
111
|
510
|
|
|
511 procedure Replace_Slice
|
|
|
512 (Source : in out Unbounded_String;
|
|
|
513 Low : Positive;
|
|
|
514 High : Natural;
|
|
145
|
515 By : String)
|
|
|
516 with
|
|
|
517 Pre =>
|
|
|
518 Low - 1 <= Length (Source)
|
|
|
519 and then (if High >= Low
|
|
|
520 then Low - 1
|
|
|
521 <= Natural'Last - By'Length
|
|
|
522 - Natural'Max (Length (Source) - High, 0)
|
|
|
523 else Length (Source) <= Natural'Last - By'Length),
|
|
|
524 Contract_Cases =>
|
|
|
525 (High >= Low =>
|
|
|
526 Length (Source)
|
|
|
527 = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
|
|
|
528 others =>
|
|
|
529 Length (Source) = Length (Source)'Old + By'Length),
|
|
|
530 Global => null;
|
|
111
|
531
|
|
|
532 function Insert
|
|
|
533 (Source : Unbounded_String;
|
|
|
534 Before : Positive;
|
|
145
|
535 New_Item : String) return Unbounded_String
|
|
|
536 with
|
|
|
537 Pre => Before - 1 <= Length (Source)
|
|
|
538 and then New_Item'Length <= Natural'Last - Length (Source),
|
|
|
539 Post => Length (Insert'Result) = Length (Source) + New_Item'Length,
|
|
|
540 Global => null;
|
|
111
|
541
|
|
|
542 procedure Insert
|
|
|
543 (Source : in out Unbounded_String;
|
|
|
544 Before : Positive;
|
|
145
|
545 New_Item : String)
|
|
|
546 with
|
|
|
547 Pre => Before - 1 <= Length (Source)
|
|
|
548 and then New_Item'Length <= Natural'Last - Length (Source),
|
|
|
549 Post => Length (Source) = Length (Source)'Old + New_Item'Length,
|
|
|
550 Global => null;
|
|
111
|
551
|
|
|
552 function Overwrite
|
|
|
553 (Source : Unbounded_String;
|
|
|
554 Position : Positive;
|
|
145
|
555 New_Item : String) return Unbounded_String
|
|
|
556 with
|
|
|
557 Pre => Position - 1 <= Length (Source)
|
|
|
558 and then (if New_Item'Length /= 0
|
|
|
559 then
|
|
|
560 New_Item'Length <= Natural'Last - (Position - 1)),
|
|
|
561 Post =>
|
|
|
562 Length (Overwrite'Result)
|
|
|
563 = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
|
|
|
564 Global => null;
|
|
111
|
565
|
|
|
566 procedure Overwrite
|
|
|
567 (Source : in out Unbounded_String;
|
|
|
568 Position : Positive;
|
|
145
|
569 New_Item : String)
|
|
|
570 with
|
|
|
571 Pre => Position - 1 <= Length (Source)
|
|
|
572 and then (if New_Item'Length /= 0
|
|
|
573 then
|
|
|
574 New_Item'Length <= Natural'Last - (Position - 1)),
|
|
|
575 Post =>
|
|
|
576 Length (Source)
|
|
|
577 = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
|
|
|
578
|
|
|
579 Global => null;
|
|
111
|
580
|
|
|
581 function Delete
|
|
|
582 (Source : Unbounded_String;
|
|
|
583 From : Positive;
|
|
145
|
584 Through : Natural) return Unbounded_String
|
|
|
585 with
|
|
|
586 Pre => (if Through <= From then From - 1 <= Length (Source)),
|
|
|
587 Contract_Cases =>
|
|
|
588 (Through >= From =>
|
|
|
589 Length (Delete'Result) = Length (Source) - (Through - From + 1),
|
|
|
590 others =>
|
|
|
591 Length (Delete'Result) = Length (Source)),
|
|
|
592 Global => null;
|
|
111
|
593
|
|
|
594 procedure Delete
|
|
|
595 (Source : in out Unbounded_String;
|
|
|
596 From : Positive;
|
|
145
|
597 Through : Natural)
|
|
|
598 with
|
|
|
599 Pre => (if Through <= From then From - 1 <= Length (Source)),
|
|
|
600 Contract_Cases =>
|
|
|
601 (Through >= From =>
|
|
|
602 Length (Source) = Length (Source)'Old - (Through - From + 1),
|
|
|
603 others =>
|
|
|
604 Length (Source) = Length (Source)'Old),
|
|
|
605 Global => null;
|
|
111
|
606
|
|
|
607 function Trim
|
|
|
608 (Source : Unbounded_String;
|
|
145
|
609 Side : Trim_End) return Unbounded_String
|
|
|
610 with
|
|
|
611 Post => Length (Trim'Result) <= Length (Source),
|
|
|
612 Global => null;
|
|
111
|
613
|
|
|
614 procedure Trim
|
|
|
615 (Source : in out Unbounded_String;
|
|
145
|
616 Side : Trim_End)
|
|
|
617 with
|
|
|
618 Post => Length (Source) <= Length (Source)'Old,
|
|
|
619 Global => null;
|
|
111
|
620
|
|
|
621 function Trim
|
|
|
622 (Source : Unbounded_String;
|
|
|
623 Left : Maps.Character_Set;
|
|
145
|
624 Right : Maps.Character_Set) return Unbounded_String
|
|
|
625 with
|
|
|
626 Post => Length (Trim'Result) <= Length (Source),
|
|
|
627 Global => null;
|
|
111
|
628
|
|
|
629 procedure Trim
|
|
|
630 (Source : in out Unbounded_String;
|
|
|
631 Left : Maps.Character_Set;
|
|
145
|
632 Right : Maps.Character_Set)
|
|
|
633 with
|
|
|
634 Post => Length (Source) <= Length (Source)'Old,
|
|
|
635 Global => null;
|
|
111
|
636
|
|
|
637 function Head
|
|
|
638 (Source : Unbounded_String;
|
|
|
639 Count : Natural;
|
|
145
|
640 Pad : Character := Space) return Unbounded_String
|
|
|
641 with
|
|
|
642 Post => Length (Head'Result) = Count,
|
|
|
643 Global => null;
|
|
111
|
644
|
|
|
645 procedure Head
|
|
|
646 (Source : in out Unbounded_String;
|
|
|
647 Count : Natural;
|
|
145
|
648 Pad : Character := Space)
|
|
|
649 with
|
|
|
650 Post => Length (Source) = Count,
|
|
|
651 Global => null;
|
|
111
|
652
|
|
|
653 function Tail
|
|
|
654 (Source : Unbounded_String;
|
|
|
655 Count : Natural;
|
|
145
|
656 Pad : Character := Space) return Unbounded_String
|
|
|
657 with
|
|
|
658 Post => Length (Tail'Result) = Count,
|
|
|
659 Global => null;
|
|
111
|
660
|
|
|
661 procedure Tail
|
|
|
662 (Source : in out Unbounded_String;
|
|
|
663 Count : Natural;
|
|
145
|
664 Pad : Character := Space)
|
|
|
665 with
|
|
|
666 Post => Length (Source) = Count,
|
|
|
667 Global => null;
|
|
111
|
668
|
|
|
669 function "*"
|
|
|
670 (Left : Natural;
|
|
145
|
671 Right : Character) return Unbounded_String
|
|
|
672 with
|
|
|
673 Pre => Left <= Natural'Last,
|
|
|
674 Post => Length ("*"'Result) = Left,
|
|
|
675 Global => null;
|
|
111
|
676
|
|
|
677 function "*"
|
|
|
678 (Left : Natural;
|
|
145
|
679 Right : String) return Unbounded_String
|
|
|
680 with
|
|
|
681 Pre => (if Left /= 0 then Right'Length <= Natural'Last / Left),
|
|
|
682 Post => Length ("*"'Result) = Left * Right'Length,
|
|
|
683 Global => null;
|
|
111
|
684
|
|
|
685 function "*"
|
|
|
686 (Left : Natural;
|
|
145
|
687 Right : Unbounded_String) return Unbounded_String
|
|
|
688 with
|
|
|
689 Pre => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
|
|
|
690 Post => Length ("*"'Result) = Left * Length (Right),
|
|
|
691 Global => null;
|
|
111
|
692
|
|
|
693 private
|
|
|
694 pragma Inline (Length);
|
|
|
695
|
|
|
696 package AF renames Ada.Finalization;
|
|
|
697
|
|
|
698 type Shared_String (Max_Length : Natural) is limited record
|
|
|
699 Counter : System.Atomic_Counters.Atomic_Counter;
|
|
|
700 -- Reference counter
|
|
|
701
|
|
|
702 Last : Natural := 0;
|
|
|
703 Data : String (1 .. Max_Length);
|
|
|
704 -- Last is the index of last significant element of the Data. All
|
|
|
705 -- elements with larger indexes are currently insignificant.
|
|
|
706 end record;
|
|
|
707
|
|
|
708 type Shared_String_Access is access all Shared_String;
|
|
|
709
|
|
|
710 procedure Reference (Item : not null Shared_String_Access);
|
|
|
711 -- Increment reference counter
|
|
|
712
|
|
|
713 procedure Unreference (Item : not null Shared_String_Access);
|
|
|
714 -- Decrement reference counter, deallocate Item when counter goes to zero
|
|
|
715
|
|
|
716 function Can_Be_Reused
|
|
|
717 (Item : not null Shared_String_Access;
|
|
|
718 Length : Natural) return Boolean;
|
|
|
719 -- Returns True if Shared_String can be reused. There are two criteria when
|
|
|
720 -- Shared_String can be reused: its reference counter must be one (thus
|
|
|
721 -- Shared_String is owned exclusively) and its size is sufficient to
|
|
|
722 -- store string with specified length effectively.
|
|
|
723
|
|
|
724 function Allocate
|
|
|
725 (Max_Length : Natural) return not null Shared_String_Access;
|
|
|
726 -- Allocates new Shared_String with at least specified maximum length.
|
|
|
727 -- Actual maximum length of the allocated Shared_String can be slightly
|
|
|
728 -- greater. Returns reference to Empty_Shared_String when requested length
|
|
|
729 -- is zero.
|
|
|
730
|
|
|
731 Empty_Shared_String : aliased Shared_String (0);
|
|
|
732
|
|
|
733 function To_Unbounded (S : String) return Unbounded_String
|
|
|
734 renames To_Unbounded_String;
|
|
|
735 -- This renames are here only to be used in the pragma Stream_Convert
|
|
|
736
|
|
|
737 type Unbounded_String is new AF.Controlled with record
|
|
|
738 Reference : not null Shared_String_Access := Empty_Shared_String'Access;
|
|
|
739 end record;
|
|
|
740
|
|
|
741 pragma Stream_Convert (Unbounded_String, To_Unbounded, To_String);
|
|
|
742 -- Provide stream routines without dragging in Ada.Streams
|
|
|
743
|
|
|
744 pragma Finalize_Storage_Only (Unbounded_String);
|
|
|
745 -- Finalization is required only for freeing storage
|
|
|
746
|
|
|
747 overriding procedure Initialize (Object : in out Unbounded_String);
|
|
|
748 overriding procedure Adjust (Object : in out Unbounded_String);
|
|
|
749 overriding procedure Finalize (Object : in out Unbounded_String);
|
|
131
|
750 pragma Inline (Initialize, Adjust);
|
|
111
|
751
|
|
|
752 Null_Unbounded_String : constant Unbounded_String :=
|
|
|
753 (AF.Controlled with
|
|
|
754 Reference => Empty_Shared_String'Access);
|
|
|
755
|
|
|
756 end Ada.Strings.Unbounded;
|
