]>
Commit | Line | Data |
---|---|---|
e487f350 AC |
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 | -- -- | |
4b490c1e | 9 | -- Copyright (C) 1992-2020, Free Software Foundation, Inc. -- |
e487f350 AC |
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- -- | |
c47c02ae | 17 | -- ware Foundation; either version 3, or (at your option) any later ver- -- |
e487f350 AC |
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 -- | |
c47c02ae AC |
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/>. -- | |
e487f350 AC |
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 | ||
0b6694b4 JH |
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 | ||
e487f350 AC |
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 | |
811aa6e0 | 51 | -- - all x86 platforms |
e487f350 AC |
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 | |
308e6f3a | 59 | -- the object mutation can't be used or it is inefficient to use it. |
e487f350 AC |
60 | |
61 | -- - Object mutation. Shared data object can be reused without memory | |
62 | -- reallocation when all of the following requirements are met: | |
6611da37 AC |
63 | -- - the shared data object is no longer used by anyone else; |
64 | -- - the size is sufficient to store the new value; | |
d99ff0f4 | 65 | -- - the gap after reuse is less than a defined threshold. |
e487f350 AC |
66 | |
67 | -- - Memory preallocation. Most of used memory allocation algorithms | |
6611da37 | 68 | -- align allocated segments on the some boundary, thus some amount of |
e487f350 AC |
69 | -- additional memory can be preallocated without any impact. Such |
70 | -- preallocated memory can used later by Append/Insert operations | |
71 | -- without reallocation. | |
72 | ||
6782b1ef AC |
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 | |
308e6f3a | 76 | -- accessed by several tasks simultaneously. |
e487f350 AC |
77 | |
78 | with Ada.Strings.Maps; | |
79 | private with Ada.Finalization; | |
26e7e1a0 | 80 | private with System.Atomic_Counters; |
e487f350 | 81 | |
0b6694b4 JH |
82 | package Ada.Strings.Unbounded with |
83 | Initial_Condition => Length (Null_Unbounded_String) = 0 | |
84 | is | |
e487f350 AC |
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 | ||
0b6694b4 JH |
92 | function Length (Source : Unbounded_String) return Natural with |
93 | Global => null; | |
e487f350 AC |
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 | |
0b6694b4 JH |
104 | (Source : String) return Unbounded_String |
105 | with | |
106 | Post => Length (To_Unbounded_String'Result) = Source'Length, | |
107 | Global => null; | |
e487f350 AC |
108 | |
109 | function To_Unbounded_String | |
0b6694b4 JH |
110 | (Length : Natural) return Unbounded_String |
111 | with | |
112 | Post => | |
113 | Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length, | |
114 | Global => null; | |
e487f350 | 115 | |
0b6694b4 JH |
116 | function To_String (Source : Unbounded_String) return String with |
117 | Post => To_String'Result'Length = Length (Source), | |
118 | Global => null; | |
e487f350 AC |
119 | |
120 | procedure Set_Unbounded_String | |
121 | (Target : out Unbounded_String; | |
0b6694b4 JH |
122 | Source : String) |
123 | with | |
124 | Global => null; | |
e487f350 AC |
125 | pragma Ada_05 (Set_Unbounded_String); |
126 | ||
127 | procedure Append | |
128 | (Source : in out Unbounded_String; | |
0b6694b4 JH |
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; | |
e487f350 AC |
134 | |
135 | procedure Append | |
136 | (Source : in out Unbounded_String; | |
0b6694b4 JH |
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; | |
e487f350 AC |
142 | |
143 | procedure Append | |
144 | (Source : in out Unbounded_String; | |
0b6694b4 JH |
145 | New_Item : Character) |
146 | with | |
147 | Pre => Length (Source) < Natural'Last, | |
148 | Post => Length (Source) = Length (Source)'Old + 1, | |
149 | Global => null; | |
e487f350 AC |
150 | |
151 | function "&" | |
152 | (Left : Unbounded_String; | |
0b6694b4 JH |
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; | |
e487f350 AC |
158 | |
159 | function "&" | |
160 | (Left : Unbounded_String; | |
0b6694b4 JH |
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; | |
e487f350 AC |
166 | |
167 | function "&" | |
168 | (Left : String; | |
0b6694b4 JH |
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; | |
e487f350 AC |
174 | |
175 | function "&" | |
176 | (Left : Unbounded_String; | |
0b6694b4 JH |
177 | Right : Character) return Unbounded_String |
178 | with | |
179 | Pre => Length (Left) < Natural'Last, | |
180 | Post => Length ("&"'Result) = Length (Left) + 1, | |
181 | Global => null; | |
e487f350 AC |
182 | |
183 | function "&" | |
184 | (Left : Character; | |
0b6694b4 JH |
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; | |
e487f350 AC |
190 | |
191 | function Element | |
192 | (Source : Unbounded_String; | |
0b6694b4 JH |
193 | Index : Positive) return Character |
194 | with | |
195 | Pre => Index <= Length (Source), | |
196 | Global => null; | |
e487f350 AC |
197 | |
198 | procedure Replace_Element | |
199 | (Source : in out Unbounded_String; | |
200 | Index : Positive; | |
0b6694b4 JH |
201 | By : Character) |
202 | with | |
203 | Pre => Index <= Length (Source), | |
204 | Post => Length (Source) = Length (Source)'Old, | |
205 | Global => null; | |
e487f350 AC |
206 | |
207 | function Slice | |
208 | (Source : Unbounded_String; | |
209 | Low : Positive; | |
0b6694b4 JH |
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; | |
e487f350 AC |
215 | |
216 | function Unbounded_Slice | |
217 | (Source : Unbounded_String; | |
218 | Low : Positive; | |
0b6694b4 JH |
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; | |
e487f350 AC |
225 | pragma Ada_05 (Unbounded_Slice); |
226 | ||
227 | procedure Unbounded_Slice | |
228 | (Source : Unbounded_String; | |
229 | Target : out Unbounded_String; | |
230 | Low : Positive; | |
0b6694b4 JH |
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; | |
e487f350 AC |
236 | pragma Ada_05 (Unbounded_Slice); |
237 | ||
238 | function "=" | |
239 | (Left : Unbounded_String; | |
0b6694b4 JH |
240 | Right : Unbounded_String) return Boolean |
241 | with | |
242 | Global => null; | |
e487f350 AC |
243 | |
244 | function "=" | |
245 | (Left : Unbounded_String; | |
0b6694b4 JH |
246 | Right : String) return Boolean |
247 | with | |
248 | Global => null; | |
e487f350 AC |
249 | |
250 | function "=" | |
251 | (Left : String; | |
0b6694b4 JH |
252 | Right : Unbounded_String) return Boolean |
253 | with | |
254 | Global => null; | |
e487f350 AC |
255 | |
256 | function "<" | |
257 | (Left : Unbounded_String; | |
0b6694b4 JH |
258 | Right : Unbounded_String) return Boolean |
259 | with | |
260 | Global => null; | |
e487f350 AC |
261 | |
262 | function "<" | |
263 | (Left : Unbounded_String; | |
0b6694b4 JH |
264 | Right : String) return Boolean |
265 | with | |
266 | Global => null; | |
e487f350 AC |
267 | |
268 | function "<" | |
269 | (Left : String; | |
0b6694b4 JH |
270 | Right : Unbounded_String) return Boolean |
271 | with | |
272 | Global => null; | |
e487f350 AC |
273 | |
274 | function "<=" | |
275 | (Left : Unbounded_String; | |
0b6694b4 JH |
276 | Right : Unbounded_String) return Boolean |
277 | with | |
278 | Global => null; | |
e487f350 AC |
279 | |
280 | function "<=" | |
281 | (Left : Unbounded_String; | |
0b6694b4 JH |
282 | Right : String) return Boolean |
283 | with | |
284 | Global => null; | |
e487f350 AC |
285 | |
286 | function "<=" | |
287 | (Left : String; | |
0b6694b4 JH |
288 | Right : Unbounded_String) return Boolean |
289 | with | |
290 | Global => null; | |
e487f350 AC |
291 | |
292 | function ">" | |
293 | (Left : Unbounded_String; | |
0b6694b4 JH |
294 | Right : Unbounded_String) return Boolean |
295 | with | |
296 | Global => null; | |
e487f350 AC |
297 | |
298 | function ">" | |
299 | (Left : Unbounded_String; | |
0b6694b4 JH |
300 | Right : String) return Boolean |
301 | with | |
302 | Global => null; | |
e487f350 AC |
303 | |
304 | function ">" | |
305 | (Left : String; | |
0b6694b4 JH |
306 | Right : Unbounded_String) return Boolean |
307 | with | |
308 | Global => null; | |
e487f350 AC |
309 | |
310 | function ">=" | |
311 | (Left : Unbounded_String; | |
0b6694b4 JH |
312 | Right : Unbounded_String) return Boolean |
313 | with | |
314 | Global => null; | |
e487f350 AC |
315 | |
316 | function ">=" | |
317 | (Left : Unbounded_String; | |
0b6694b4 JH |
318 | Right : String) return Boolean |
319 | with | |
320 | Global => null; | |
e487f350 AC |
321 | |
322 | function ">=" | |
323 | (Left : String; | |
0b6694b4 JH |
324 | Right : Unbounded_String) return Boolean |
325 | with | |
326 | Global => null; | |
e487f350 AC |
327 | |
328 | ------------------------ | |
329 | -- Search Subprograms -- | |
330 | ------------------------ | |
331 | ||
332 | function Index | |
333 | (Source : Unbounded_String; | |
334 | Pattern : String; | |
335 | Going : Direction := Forward; | |
0b6694b4 JH |
336 | Mapping : Maps.Character_Mapping := Maps.Identity) return Natural |
337 | with | |
338 | Pre => Pattern'Length /= 0, | |
339 | Global => null; | |
e487f350 AC |
340 | |
341 | function Index | |
342 | (Source : Unbounded_String; | |
343 | Pattern : String; | |
344 | Going : Direction := Forward; | |
0b6694b4 JH |
345 | Mapping : Maps.Character_Mapping_Function) return Natural |
346 | with | |
347 | Pre => Pattern'Length /= 0, | |
348 | Global => null; | |
e487f350 AC |
349 | |
350 | function Index | |
351 | (Source : Unbounded_String; | |
352 | Set : Maps.Character_Set; | |
353 | Test : Membership := Inside; | |
0b6694b4 JH |
354 | Going : Direction := Forward) return Natural |
355 | with | |
356 | Global => null; | |
e487f350 AC |
357 | |
358 | function Index | |
359 | (Source : Unbounded_String; | |
360 | Pattern : String; | |
361 | From : Positive; | |
362 | Going : Direction := Forward; | |
0b6694b4 JH |
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; | |
e487f350 AC |
369 | pragma Ada_05 (Index); |
370 | ||
371 | function Index | |
372 | (Source : Unbounded_String; | |
373 | Pattern : String; | |
374 | From : Positive; | |
375 | Going : Direction := Forward; | |
0b6694b4 JH |
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 | ||
e487f350 AC |
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; | |
0b6694b4 JH |
390 | Going : Direction := Forward) return Natural |
391 | with | |
392 | Pre => (if Length (Source) /= 0 then From <= Length (Source)), | |
393 | Global => null; | |
e487f350 AC |
394 | pragma Ada_05 (Index); |
395 | ||
396 | function Index_Non_Blank | |
397 | (Source : Unbounded_String; | |
0b6694b4 JH |
398 | Going : Direction := Forward) return Natural |
399 | with | |
400 | Global => null; | |
e487f350 AC |
401 | |
402 | function Index_Non_Blank | |
403 | (Source : Unbounded_String; | |
404 | From : Positive; | |
0b6694b4 JH |
405 | Going : Direction := Forward) return Natural |
406 | with | |
407 | Pre => (if Length (Source) /= 0 then From <= Length (Source)), | |
408 | Global => null; | |
e487f350 AC |
409 | pragma Ada_05 (Index_Non_Blank); |
410 | ||
411 | function Count | |
412 | (Source : Unbounded_String; | |
413 | Pattern : String; | |
0b6694b4 JH |
414 | Mapping : Maps.Character_Mapping := Maps.Identity) return Natural |
415 | with | |
416 | Pre => Pattern'Length /= 0, | |
417 | Global => null; | |
e487f350 AC |
418 | |
419 | function Count | |
420 | (Source : Unbounded_String; | |
421 | Pattern : String; | |
0b6694b4 JH |
422 | Mapping : Maps.Character_Mapping_Function) return Natural |
423 | with | |
424 | Pre => Pattern'Length /= 0, | |
425 | Global => null; | |
e487f350 AC |
426 | |
427 | function Count | |
428 | (Source : Unbounded_String; | |
0b6694b4 JH |
429 | Set : Maps.Character_Set) return Natural |
430 | with | |
431 | Global => null; | |
e487f350 | 432 | |
af31bffb AC |
433 | procedure Find_Token |
434 | (Source : Unbounded_String; | |
435 | Set : Maps.Character_Set; | |
436 | From : Positive; | |
437 | Test : Membership; | |
438 | First : out Positive; | |
0b6694b4 JH |
439 | Last : out Natural) |
440 | with | |
441 | Pre => (if Length (Source) /= 0 then From <= Length (Source)), | |
442 | Global => null; | |
af31bffb AC |
443 | pragma Ada_2012 (Find_Token); |
444 | ||
e487f350 AC |
445 | procedure Find_Token |
446 | (Source : Unbounded_String; | |
447 | Set : Maps.Character_Set; | |
448 | Test : Membership; | |
449 | First : out Positive; | |
0b6694b4 JH |
450 | Last : out Natural) |
451 | with | |
452 | Global => null; | |
e487f350 AC |
453 | |
454 | ------------------------------------ | |
455 | -- String Translation Subprograms -- | |
456 | ------------------------------------ | |
457 | ||
458 | function Translate | |
459 | (Source : Unbounded_String; | |
0b6694b4 JH |
460 | Mapping : Maps.Character_Mapping) return Unbounded_String |
461 | with | |
462 | Post => Length (Translate'Result) = Length (Source), | |
463 | Global => null; | |
e487f350 AC |
464 | |
465 | procedure Translate | |
466 | (Source : in out Unbounded_String; | |
0b6694b4 JH |
467 | Mapping : Maps.Character_Mapping) |
468 | with | |
469 | Post => Length (Source) = Length (Source)'Old, | |
470 | Global => null; | |
e487f350 AC |
471 | |
472 | function Translate | |
473 | (Source : Unbounded_String; | |
0b6694b4 JH |
474 | Mapping : Maps.Character_Mapping_Function) return Unbounded_String |
475 | with | |
476 | Post => Length (Translate'Result) = Length (Source), | |
477 | Global => null; | |
e487f350 AC |
478 | |
479 | procedure Translate | |
480 | (Source : in out Unbounded_String; | |
0b6694b4 JH |
481 | Mapping : Maps.Character_Mapping_Function) |
482 | with | |
483 | Post => Length (Source) = Length (Source)'Old, | |
484 | Global => null; | |
e487f350 AC |
485 | |
486 | --------------------------------------- | |
487 | -- String Transformation Subprograms -- | |
488 | --------------------------------------- | |
489 | ||
490 | function Replace_Slice | |
491 | (Source : Unbounded_String; | |
492 | Low : Positive; | |
493 | High : Natural; | |
0b6694b4 JH |
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; | |
e487f350 AC |
510 | |
511 | procedure Replace_Slice | |
512 | (Source : in out Unbounded_String; | |
513 | Low : Positive; | |
514 | High : Natural; | |
0b6694b4 JH |
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; | |
e487f350 AC |
531 | |
532 | function Insert | |
533 | (Source : Unbounded_String; | |
534 | Before : Positive; | |
0b6694b4 JH |
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; | |
e487f350 AC |
541 | |
542 | procedure Insert | |
543 | (Source : in out Unbounded_String; | |
544 | Before : Positive; | |
0b6694b4 JH |
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; | |
e487f350 AC |
551 | |
552 | function Overwrite | |
553 | (Source : Unbounded_String; | |
554 | Position : Positive; | |
0b6694b4 JH |
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; | |
e487f350 AC |
565 | |
566 | procedure Overwrite | |
567 | (Source : in out Unbounded_String; | |
568 | Position : Positive; | |
0b6694b4 JH |
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; | |
e487f350 AC |
580 | |
581 | function Delete | |
582 | (Source : Unbounded_String; | |
583 | From : Positive; | |
0b6694b4 JH |
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; | |
e487f350 AC |
593 | |
594 | procedure Delete | |
595 | (Source : in out Unbounded_String; | |
596 | From : Positive; | |
0b6694b4 JH |
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; | |
e487f350 AC |
606 | |
607 | function Trim | |
608 | (Source : Unbounded_String; | |
0b6694b4 JH |
609 | Side : Trim_End) return Unbounded_String |
610 | with | |
611 | Post => Length (Trim'Result) <= Length (Source), | |
612 | Global => null; | |
e487f350 AC |
613 | |
614 | procedure Trim | |
615 | (Source : in out Unbounded_String; | |
0b6694b4 JH |
616 | Side : Trim_End) |
617 | with | |
618 | Post => Length (Source) <= Length (Source)'Old, | |
619 | Global => null; | |
e487f350 AC |
620 | |
621 | function Trim | |
622 | (Source : Unbounded_String; | |
623 | Left : Maps.Character_Set; | |
0b6694b4 JH |
624 | Right : Maps.Character_Set) return Unbounded_String |
625 | with | |
626 | Post => Length (Trim'Result) <= Length (Source), | |
627 | Global => null; | |
e487f350 AC |
628 | |
629 | procedure Trim | |
630 | (Source : in out Unbounded_String; | |
631 | Left : Maps.Character_Set; | |
0b6694b4 JH |
632 | Right : Maps.Character_Set) |
633 | with | |
634 | Post => Length (Source) <= Length (Source)'Old, | |
635 | Global => null; | |
e487f350 AC |
636 | |
637 | function Head | |
638 | (Source : Unbounded_String; | |
639 | Count : Natural; | |
0b6694b4 JH |
640 | Pad : Character := Space) return Unbounded_String |
641 | with | |
642 | Post => Length (Head'Result) = Count, | |
643 | Global => null; | |
e487f350 AC |
644 | |
645 | procedure Head | |
646 | (Source : in out Unbounded_String; | |
647 | Count : Natural; | |
0b6694b4 JH |
648 | Pad : Character := Space) |
649 | with | |
650 | Post => Length (Source) = Count, | |
651 | Global => null; | |
e487f350 AC |
652 | |
653 | function Tail | |
654 | (Source : Unbounded_String; | |
655 | Count : Natural; | |
0b6694b4 JH |
656 | Pad : Character := Space) return Unbounded_String |
657 | with | |
658 | Post => Length (Tail'Result) = Count, | |
659 | Global => null; | |
e487f350 AC |
660 | |
661 | procedure Tail | |
662 | (Source : in out Unbounded_String; | |
663 | Count : Natural; | |
0b6694b4 JH |
664 | Pad : Character := Space) |
665 | with | |
666 | Post => Length (Source) = Count, | |
667 | Global => null; | |
e487f350 AC |
668 | |
669 | function "*" | |
670 | (Left : Natural; | |
0b6694b4 JH |
671 | Right : Character) return Unbounded_String |
672 | with | |
673 | Pre => Left <= Natural'Last, | |
674 | Post => Length ("*"'Result) = Left, | |
675 | Global => null; | |
e487f350 AC |
676 | |
677 | function "*" | |
678 | (Left : Natural; | |
0b6694b4 JH |
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; | |
e487f350 AC |
684 | |
685 | function "*" | |
686 | (Left : Natural; | |
0b6694b4 JH |
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; | |
e487f350 AC |
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 | |
26e7e1a0 | 699 | Counter : System.Atomic_Counters.Atomic_Counter; |
e487f350 AC |
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 | |
7504523e | 717 | (Item : not null Shared_String_Access; |
e487f350 AC |
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 | ||
7504523e AC |
724 | function Allocate |
725 | (Max_Length : Natural) return not null Shared_String_Access; | |
e487f350 | 726 | -- Allocates new Shared_String with at least specified maximum length. |
308e6f3a | 727 | -- Actual maximum length of the allocated Shared_String can be slightly |
e487f350 AC |
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 | |
7504523e | 738 | Reference : not null Shared_String_Access := Empty_Shared_String'Access; |
e487f350 AC |
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); | |
5a7aacd1 | 750 | pragma Inline (Initialize, Adjust); |
e487f350 AC |
751 | |
752 | Null_Unbounded_String : constant Unbounded_String := | |
753 | (AF.Controlled with | |
754 | Reference => Empty_Shared_String'Access); | |
755 | ||
756 | end Ada.Strings.Unbounded; |