/[eiffelstudio]/FreeELKS/trunk/library/kernel/string.e
ViewVC logotype

Contents of /FreeELKS/trunk/library/kernel/string.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 91475 - (show annotations)
Fri Mar 3 10:19:32 2006 UTC (13 years, 10 months ago) by ericb
File size: 68928 byte(s)
Synchronized with ISE 5.7.0726

1 indexing
2 description: "[
3 Sequences of characters, accessible through integer indices
4 in a contiguous range.
5 ]"
6 library: "Free implementation of ELKS library"
7 copyright: "Copyright (c) 1986-2006, Eiffel Software and others"
8 license: "Eiffel Forum License v2 (see forum.txt)"
9 date: "$Date$"
10 revision: "$Revision$"
11
12 class
13 STRING
14
15 inherit
16 INDEXABLE [CHARACTER, INTEGER]
17 rename
18 item as item
19 redefine
20 copy, is_equal, out, prune_all,
21 changeable_comparison_criterion
22 end
23
24 RESIZABLE [CHARACTER]
25 redefine
26 copy, is_equal, out,
27 changeable_comparison_criterion
28 end
29
30 HASHABLE
31 redefine
32 copy, is_equal, out
33 end
34
35 COMPARABLE
36 redefine
37 copy, is_equal, out
38 end
39
40 TO_SPECIAL [CHARACTER]
41 rename
42 item as item
43 redefine
44 copy, is_equal, out,
45 item, infix "@", put, valid_index
46 end
47
48 STRING_HANDLER
49 redefine
50 copy, is_equal, out
51 end
52
53 MISMATCH_CORRECTOR
54 redefine
55 copy, is_equal, out, correct_mismatch
56 end
57
58 create
59 make,
60 make_empty,
61 make_filled,
62 make_from_string,
63 make_from_c,
64 make_from_cil
65
66 convert
67 to_cil: {SYSTEM_STRING},
68 make_from_cil ({SYSTEM_STRING})
69
70 feature -- Initialization
71
72 make (n: INTEGER) is
73 -- Allocate space for at least `n' characters.
74 require
75 non_negative_size: n >= 0
76 do
77 count := 0
78 internal_hash_code := 0
79 make_area (n + 1)
80 ensure
81 empty_string: count = 0
82 area_allocated: capacity >= n
83 end
84
85 make_empty is
86 -- Create empty string.
87 do
88 make (0)
89 ensure
90 empty: count = 0
91 area_allocated: capacity >= 0
92 end
93
94 make_filled (c: CHARACTER; n: INTEGER) is
95 -- Create string of length `n' filled with `c'.
96 require
97 valid_count: n >= 0
98 do
99 make (n)
100 fill_character (c)
101 ensure
102 count_set: count = n
103 area_allocated: capacity >= n
104 filled: occurrences (c) = count
105 end
106
107 make_from_string (s: STRING) is
108 -- Initialize from the characters of `s'.
109 -- (Useful in proper descendants of class STRING,
110 -- to initialize a string-like object from a manifest string.)
111 require
112 string_exists: s /= Void
113 do
114 if Current /= s then
115 area := s.area.twin
116 count := s.count
117 internal_hash_code := 0
118 end
119 ensure
120 not_shared_implementation: Current /= s implies not shared_with (s)
121 initialized: same_string (s)
122 end
123
124 make_from_c (c_string: POINTER) is
125 -- Initialize from contents of `c_string',
126 -- a string created by some C function
127 require
128 c_string_exists: c_string /= default_pointer
129 local
130 l_count: INTEGER
131 do
132 if area = Void then
133 c_string_provider.share_from_pointer (c_string)
134 l_count := c_string_provider.count
135 make_area (l_count + 1)
136 count := l_count
137 internal_hash_code := 0
138 c_string_provider.read_string_into (Current)
139 else
140 from_c (c_string)
141 end
142 end
143
144 make_from_cil (a_system_string: SYSTEM_STRING) is
145 -- Initialize Current with `a_system_string'.
146 require
147 is_dotnet: {PLATFORM}.is_dotnet
148 local
149 l_count: INTEGER
150 do
151 if a_system_string /= Void then
152 l_count := a_system_string.length
153 make_area (l_count + 1)
154 count := l_count
155 internal_hash_code := 0
156 a_system_string.copy_to (0, area.native_array, 0, l_count)
157 else
158 make (0)
159 end
160 end
161
162 from_c (c_string: POINTER) is
163 -- Reset contents of string from contents of `c_string',
164 -- a string created by some C function.
165 require
166 c_string_exists: c_string /= default_pointer
167 local
168 l_count: INTEGER
169 do
170 c_string_provider.share_from_pointer (c_string)
171 -- Resize string in case it is not big enough
172 l_count := c_string_provider.count
173 resize (l_count + 1)
174 count := l_count
175 internal_hash_code := 0
176 c_string_provider.read_string_into (Current)
177 ensure
178 no_zero_byte: not has ('%/0/')
179 -- characters: for all i in 1..count, item (i) equals
180 -- ASCII character at address c_string + (i - 1)
181 -- correct_count: the ASCII character at address c_string + count
182 -- is NULL
183 end
184
185 from_c_substring (c_string: POINTER; start_pos, end_pos: INTEGER) is
186 -- Reset contents of string from substring of `c_string',
187 -- a string created by some C function.
188 require
189 c_string_exists: c_string /= default_pointer
190 start_position_big_enough: start_pos >= 1
191 end_position_big_enough: start_pos <= end_pos + 1
192 local
193 l_count: INTEGER
194 do
195 l_count := end_pos - start_pos + 1
196 c_string_provider.share_from_pointer_and_count (c_string + (start_pos - 1), l_count)
197 -- Resize string in case it is not big enough
198 resize (l_count + 1)
199 count := l_count
200 internal_hash_code := 0
201 c_string_provider.read_substring_into (Current, 1, l_count)
202 ensure
203 valid_count: count = end_pos - start_pos + 1
204 -- characters: for all i in 1..count, item (i) equals
205 -- ASCII character at address c_string + (i - 1)
206 end
207
208 adapt (s: STRING): like Current is
209 -- Object of a type conforming to the type of `s',
210 -- initialized with attributes from `s'
211 do
212 Result := new_string (0)
213 Result.share (s)
214 ensure
215 adapt_not_void: Result /= Void
216 shared_implementation: Result.shared_with (s)
217 end
218
219 remake (n: INTEGER) is
220 -- Allocate space for at least `n' characters.
221 obsolete
222 "Use `make' instead"
223 require
224 non_negative_size: n >= 0
225 do
226 make (n)
227 ensure
228 empty_string: count = 0
229 area_allocated: capacity >= n
230 end
231
232 feature -- Access
233
234 item, infix "@" (i: INTEGER): CHARACTER assign put is
235 -- Character at position `i'
236 do
237 Result := area.item (i - 1)
238 end
239
240 item_code (i: INTEGER): INTEGER is
241 -- Numeric code of character at position `i'
242 require
243 index_small_enough: i <= count
244 index_large_enough: i > 0
245 do
246 Result := area.item (i - 1).code
247 end
248
249 hash_code: INTEGER is
250 -- Hash code value
251 local
252 i, nb: INTEGER
253 l_area: like area
254 do
255 Result := internal_hash_code
256 if Result = 0 then
257 -- The magic number `8388593' below is the greatest prime lower than
258 -- 2^23 so that this magic number shifted to the left does not exceed 2^31.
259 from
260 i := 0
261 nb := count
262 l_area := area
263 until
264 i = nb
265 loop
266 Result := ((Result \\ 8388593) |<< 8) + l_area.item (i).code
267 i := i + 1
268 end
269 internal_hash_code := Result
270 end
271 end
272
273 false_constant: STRING is "false"
274 -- Constant string "false"
275
276 true_constant: STRING is "true"
277 -- Constant string "true"
278
279 shared_with (other: STRING): BOOLEAN is
280 -- Does string share the text of `other'?
281 do
282 Result := (other /= Void) and then (area = other.area)
283 end
284
285 index_of (c: CHARACTER; start_index: INTEGER): INTEGER is
286 -- Position of first occurrence of `c' at or after `start_index';
287 -- 0 if none.
288 require
289 start_large_enough: start_index >= 1
290 start_small_enough: start_index <= count + 1
291 local
292 a: like area
293 i, nb: INTEGER
294 do
295 nb := count
296 if start_index <= nb then
297 from
298 i := start_index - 1
299 a := area
300 until
301 i = nb or else a.item (i) = c
302 loop
303 i := i + 1
304 end
305 if i < nb then
306 -- We add +1 due to the area starting at 0 and not at 1.
307 Result := i + 1
308 end
309 end
310 ensure
311 valid_result: Result = 0 or (start_index <= Result and Result <= count)
312 zero_if_absent: (Result = 0) = not substring (start_index, count).has (c)
313 found_if_present: substring (start_index, count).has (c) implies item (Result) = c
314 none_before: substring (start_index, count).has (c) implies
315 not substring (start_index, Result - 1).has (c)
316 end
317
318 last_index_of (c: CHARACTER; start_index_from_end: INTEGER): INTEGER is
319 -- Position of last occurrence of `c'.
320 -- 0 if none
321 require
322 start_index_small_enough: start_index_from_end <= count
323 start_index_large_enough: start_index_from_end >= 1
324 local
325 a: like area
326 i: INTEGER
327 do
328 from
329 i := start_index_from_end - 1
330 a := area
331 until
332 i < 0 or else a.item (i) = c
333 loop
334 i := i - 1
335 end
336 -- We add +1 due to the area starting at 0 and not at 1.
337 Result := i + 1
338 ensure
339 last_index_of_non_negative: Result >= 0
340 correct_place: Result > 0 implies item (Result) = c
341 -- forall x : Result..last, item (x) /= c
342 end
343
344 substring_index_in_bounds (other: STRING; start_pos, end_pos: INTEGER): INTEGER is
345 -- Position of first occurrence of `other' at or after `start_pos'
346 -- and to or before `end_pos';
347 -- 0 if none.
348 require
349 other_nonvoid: other /= Void
350 other_notempty: not other.is_empty
351 start_pos_large_enough: start_pos >= 1
352 start_pos_small_enough: start_pos <= count
353 end_pos_large_enough: end_pos >= start_pos
354 end_pos_small_enough: end_pos <= count
355 do
356 Result := string_searcher.substring_index (Current, other, start_pos, end_pos)
357 ensure
358 correct_place: Result > 0 implies
359 other.is_equal (substring (Result, Result + other.count - 1))
360 -- forall x : start_pos..Result
361 -- not substring (x, x+other.count -1).is_equal (other)
362 end
363
364 string: STRING is
365 -- New STRING having same character sequence as `Current'.
366 do
367 create Result.make (count)
368 Result.append (Current)
369 ensure
370 string_not_void: Result /= Void
371 string_type: Result.same_type ("")
372 first_item: count > 0 implies Result.item (1) = item (1)
373 recurse: count > 1 implies Result.substring (2, count).is_equal (
374 substring (2, count).string)
375 end
376
377 substring_index (other: STRING; start_index: INTEGER): INTEGER is
378 -- Index of first occurrence of other at or after start_index;
379 -- 0 if none
380 require
381 other_not_void: other /= Void
382 valid_start_index: start_index >= 1 and start_index <= count + 1
383 do
384 Result := string_searcher.substring_index (Current, other, start_index, count)
385 ensure
386 valid_result: Result = 0 or else
387 (start_index <= Result and Result <= count - other.count + 1)
388 zero_if_absent: (Result = 0) =
389 not substring (start_index, count).has_substring (other)
390 at_this_index: Result >= start_index implies
391 other.same_string (substring (Result, Result + other.count - 1))
392 none_before: Result > start_index implies
393 not substring (start_index, Result + other.count - 2).has_substring (other)
394 end
395
396 fuzzy_index (other: STRING; start: INTEGER; fuzz: INTEGER): INTEGER is
397 -- Position of first occurrence of `other' at or after `start'
398 -- with 0..`fuzz' mismatches between the string and `other'.
399 -- 0 if there are no fuzzy matches
400 require
401 other_exists: other /= Void
402 other_not_empty: not other.is_empty
403 start_large_enough: start >= 1
404 start_small_enough: start <= count
405 acceptable_fuzzy: fuzz <= other.count
406 do
407 Result := string_searcher.fuzzy_index (Current, other, start, count, fuzz)
408 end
409
410 feature -- Measurement
411
412 capacity: INTEGER is
413 -- Allocated space
414 do
415 Result := area.count - 1
416 end
417
418 count: INTEGER
419 -- Actual number of characters making up the string
420
421 occurrences (c: CHARACTER): INTEGER is
422 -- Number of times `c' appears in the string
423 local
424 i, nb: INTEGER
425 a: SPECIAL [CHARACTER]
426 do
427 from
428 nb := count
429 a := area
430 until
431 i = nb
432 loop
433 if a.item (i) = c then
434 Result := Result + 1
435 end
436 i := i + 1
437 end
438 ensure then
439 zero_if_empty: count = 0 implies Result = 0
440 recurse_if_not_found_at_first_position:
441 (count > 0 and then item (1) /= c) implies
442 Result = substring (2, count).occurrences (c)
443 recurse_if_found_at_first_position:
444 (count > 0 and then item (1) = c) implies
445 Result = 1 + substring (2, count).occurrences (c)
446 end
447
448 index_set: INTEGER_INTERVAL is
449 -- Range of acceptable indexes
450 do
451 create Result.make (1, count)
452 ensure then
453 Result.count = count
454 end
455
456 feature -- Comparison
457
458 is_equal (other: like Current): BOOLEAN is
459 -- Is string made of same character sequence as `other'
460 -- (possibly with a different capacity)?
461 local
462 l_count: INTEGER
463 do
464 if other = Current then
465 Result := True
466 else
467 l_count := count
468 if l_count = other.count then
469 Result := str_strict_cmp (area, other.area, l_count) = 0
470 end
471 end
472 end
473
474 is_case_insensitive_equal (other: like Current): BOOLEAN is
475 -- Is string made of same character sequence as `other' regardless of casing
476 -- (possibly with a different capacity)?
477 require
478 other_not_void: other /= Void
479 local
480 l_area, l_other_area: like area
481 i, nb: INTEGER
482 do
483 if other = Current then
484 Result := True
485 else
486 nb := count
487 if nb = other.count then
488 from
489 l_area := area
490 l_other_area := other.area
491 Result := True
492 until
493 i = nb
494 loop
495 if l_area.item (i).as_lower /= l_other_area.item (i).as_lower then
496 Result := False
497 i := nb - 1 -- Jump out of loop
498 end
499 i := i + 1
500 end
501 end
502 end
503 ensure
504 symmetric: Result implies other.is_case_insensitive_equal (Current)
505 consistent: standard_is_equal (other) implies Result
506 valid_result: as_lower.is_equal (other.as_lower) implies Result
507 end
508
509 same_string (other: STRING): BOOLEAN is
510 -- Do `Current' and `other' have same character sequence?
511 require
512 other_not_void: other /= Void
513 local
514 i, nb: INTEGER
515 l_area, l_other_area: like area
516 do
517 if other = Current then
518 Result := True
519 elseif other.count = count then
520 Result := True
521 nb := count
522 if same_type (other) then
523 from
524 l_area := area
525 l_other_area := other.area
526 until
527 i = nb
528 loop
529 if l_area.item (i) /= l_other_area.item (i) then
530 Result := False
531 i := nb -- Jump out of the loop.
532 else
533 i := i + 1
534 end
535 end
536 else
537 from
538 i := 1
539 nb := nb + 1
540 until
541 i = nb
542 loop
543 if item (i) /= other.item (i) then
544 Result := False
545 i := nb -- Jump out of the loop.
546 else
547 i := i + 1
548 end
549 end
550 end
551 end
552 ensure
553 definition: Result = string.is_equal (other.string)
554 end
555
556 infix "<" (other: like Current): BOOLEAN is
557 -- Is string lexicographically lower than `other'?
558 local
559 other_count: INTEGER
560 current_count: INTEGER
561 do
562 if other /= Current then
563 other_count := other.count
564 current_count := count
565 if other_count = current_count then
566 Result := str_strict_cmp (other.area, area, other_count) > 0
567 else
568 if current_count < other_count then
569 Result := str_strict_cmp (other.area, area, current_count) >= 0
570 else
571 Result := str_strict_cmp (other.area, area, other_count) > 0
572 end
573 end
574 end
575 end
576
577 feature -- Status report
578
579 has (c: CHARACTER): BOOLEAN is
580 -- Does string include `c'?
581 local
582 i, nb: INTEGER
583 l_area: like area
584 do
585 nb := count
586 if nb > 0 then
587 from
588 l_area := area
589 until
590 i = nb or else (l_area.item (i) = c)
591 loop
592 i := i + 1
593 end
594 Result := (i < nb)
595 end
596 ensure then
597 false_if_empty: count = 0 implies not Result
598 true_if_first: count > 0 and then item (1) = c implies Result
599 recurse: (count > 0 and then item (1) /= c) implies
600 (Result = substring (2, count).has (c))
601 end
602
603 has_substring (other: STRING): BOOLEAN is
604 -- Does `Current' contain `other'?
605 require
606 other_not_void: other /= Void
607 do
608 if other = Current then
609 Result := True
610 elseif other.count <= count then
611 Result := substring_index (other, 1) > 0
612 end
613 ensure
614 false_if_too_small: count < other.count implies not Result
615 true_if_initial: (count >= other.count and then
616 other.same_string (substring (1, other.count))) implies Result
617 recurse: (count >= other.count and then
618 not other.same_string (substring (1, other.count))) implies
619 (Result = substring (2, count).has_substring (other))
620 end
621
622 extendible: BOOLEAN is True
623 -- May new items be added? (Answer: yes.)
624
625 prunable: BOOLEAN is
626 -- May items be removed? (Answer: yes.)
627 do
628 Result := True
629 end
630
631 valid_index (i: INTEGER): BOOLEAN is
632 -- Is `i' within the bounds of the string?
633 do
634 Result := (i > 0) and (i <= count)
635 end
636
637 changeable_comparison_criterion: BOOLEAN is False
638
639 is_number_sequence: BOOLEAN is
640 -- Does `Current' represent a number sequence?
641 do
642 Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_no_limitation)
643 ensure
644 syntax_and_range:
645 -- Result is true if and only if the following two
646 -- conditions are satisfied:
647 --
648 -- In the following BNF grammar, the value of
649 -- Current can be produced by "Integer_literal":
650 --
651 -- Integer_literal = [Space] [Sign] Integer [Space]
652 -- Space = " " | " " Space
653 -- Sign = "+" | "-"
654 -- Integer = Digit | Digit Integer
655 -- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
656 end
657
658 is_real: BOOLEAN is
659 -- Does `Current' represent a REAL?
660 do
661 Result := is_double
662 ensure
663 syntax_and_range:
664 -- 'Result' is True if and only if the following two
665 -- conditions are satisfied:
666 --
667 -- 1. In the following BNF grammar, the value of
668 -- 'Current' can be produced by "Real_literal":
669 --
670 -- Real_literal = Mantissa [Exponent_part]
671 -- Exponent_part = "E" Exponent
672 -- | "e" Exponent
673 -- Exponent = Integer_literal
674 -- Mantissa = Decimal_literal
675 -- Decimal_literal = Integer_literal ["." [Integer]] | "." Integer
676 -- Integer_literal = [Sign] Integer
677 -- Sign = "+" | "-"
678 -- Integer = Digit | Digit Integer
679 -- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
680 --
681 -- 2. The numerical value represented by 'Current'
682 -- is within the range that can be represented
683 -- by an instance of type REAL.
684 end
685
686 is_double: BOOLEAN is
687 -- Does `Current' represent a DOUBLE?
688 do
689 ctor_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_double)
690 Result := ctor_convertor.is_integral_double
691 ensure
692 syntax_and_range:
693 -- 'Result' is True if and only if the following two
694 -- conditions are satisfied:
695 --
696 -- 1. In the following BNF grammar, the value of
697 -- 'Current' can be produced by "Real_literal":
698 --
699 -- Real_literal = Mantissa [Exponent_part]
700 -- Exponent_part = "E" Exponent
701 -- | "e" Exponent
702 -- Exponent = Integer_literal
703 -- Mantissa = Decimal_literal
704 -- Decimal_literal = Integer_literal ["." [Integer]] | "." Integer
705 -- Integer_literal = [Sign] Integer
706 -- Sign = "+" | "-"
707 -- Integer = Digit | Digit Integer
708 -- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
709 --
710 -- 2. The numerical value represented by 'Current'
711 -- is within the range that can be represented
712 -- by an instance of type DOUBLE.
713 end
714
715 is_boolean: BOOLEAN is
716 -- Does `Current' represent a BOOLEAN?
717 local
718 nb: INTEGER
719 l_area: like area
720 do
721 nb := count
722 if nb = 4 then
723 -- Check if this is `true_constant'
724 l_area := area
725 Result := l_area.item (0).lower = 't' and then
726 l_area.item (1).lower = 'r' and then
727 l_area.item (2).lower = 'u' and then
728 l_area.item (3).lower = 'e'
729 elseif nb = 5 then
730 -- Check if this is `false_constant'
731 l_area := area
732 Result := l_area.item (0).lower = 'f' and then
733 l_area.item (1).lower = 'a' and then
734 l_area.item (2).lower = 'l' and then
735 l_area.item (3).lower = 's' and then
736 l_area.item (4).lower = 'e'
737 end
738 ensure
739 is_boolean: Result = (true_constant.same_string (as_lower) or false_constant.same_string (as_lower))
740 end
741
742 is_integer_8: BOOLEAN is
743 -- Does `Current' represent an INTEGER_8?
744 do
745 Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_integer_8)
746 end
747
748 is_integer_16: BOOLEAN is
749 -- Does `Current' represent an INTEGER_16?
750 do
751 Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_integer_16)
752 end
753
754 is_integer, is_integer_32: BOOLEAN is
755 -- Does `Current' represent an INTEGER?
756 do
757 Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_integer_32)
758 end
759
760 is_integer_64: BOOLEAN is
761 -- Does `Current' represent an INTEGER_64?
762 do
763 Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_integer_64)
764 end
765
766 is_natural_8: BOOLEAN is
767 -- Does `Current' represent a NATURAL_8?
768 do
769 Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_natural_8)
770 end
771
772 is_natural_16: BOOLEAN is
773 -- Does `Current' represent a NATURAL_16?
774
775 do
776 Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_natural_16)
777 end
778
779 is_natural, is_natural_32: BOOLEAN is
780 -- Does `Current' represent a NATURAL_32?
781 do
782 Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_natural_32)
783 end
784
785 is_natural_64: BOOLEAN is
786 -- Does `Current' represent a NATURAL_64?
787 do
788 Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_natural_64)
789 end
790
791 feature -- Element change
792
793 set (t: like Current; n1, n2: INTEGER) is
794 -- Set current string to substring of `t' from indices `n1'
795 -- to `n2', or to empty string if no such substring.
796 require
797 argument_not_void: t /= Void
798 local
799 s: STRING
800 do
801 s := t.substring (n1, n2)
802 area := s.area
803 count := s.count
804 internal_hash_code := 0
805 ensure
806 is_substring: is_equal (t.substring (n1, n2))
807 end
808
809 copy (other: like Current) is
810 -- Reinitialize by copying the characters of `other'.
811 -- (This is also used by `twin'.)
812 local
813 old_area: like area
814 do
815 if other /= Current then
816 old_area := area
817 standard_copy (other)
818 -- Note: <= is needed as all Eiffel string should have an
819 -- extra character to insert null character at the end.
820 if old_area = Void or else old_area.count <= count then
821 area := area.twin
822 else
823 old_area.copy_data (area, 0, 0, count)
824 area := old_area
825 end
826 internal_hash_code := 0
827 end
828 ensure then
829 new_result_count: count = other.count
830 -- same_characters: For every `i' in 1..`count', `item' (`i') = `other'.`item' (`i')
831 end
832
833 subcopy (other: like Current; start_pos, end_pos, index_pos: INTEGER) is
834 -- Copy characters of `other' within bounds `start_pos' and
835 -- `end_pos' to current string starting at index `index_pos'.
836 require
837 other_not_void: other /= Void
838 valid_start_pos: other.valid_index (start_pos)
839 valid_end_pos: other.valid_index (end_pos)
840 valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
841 valid_index_pos: valid_index (index_pos)
842 enough_space: (count - index_pos) >= (end_pos - start_pos)
843 local
844 l_other_area, l_area: like area
845 do
846 l_other_area := other.area
847 l_area := area
848 if end_pos >= start_pos then
849 if l_area /= l_other_area then
850 l_area.copy_data (l_other_area, start_pos - 1, index_pos - 1,
851 end_pos - start_pos + 1)
852 else
853 l_area.overlapping_move (start_pos - 1, index_pos - 1,
854 end_pos - start_pos + 1)
855 end
856 internal_hash_code := 0
857 end
858 ensure
859 same_count: count = old count
860 copied: elks_checking implies
861 (is_equal (old substring (1, index_pos - 1) +
862 old other.substring (start_pos, end_pos) +
863 old substring (index_pos + (end_pos - start_pos + 1), count)))
864 end
865
866 replace_substring (s: STRING; start_index, end_index: INTEGER) is
867 -- Replace characters from `start_index' to `end_index' with `s'.
868 require
869 string_not_void: s /= Void
870 valid_start_index: 1 <= start_index
871 valid_end_index: end_index <= count
872 meaningfull_interval: start_index <= end_index + 1
873 local
874 new_size: INTEGER
875 diff: INTEGER
876 l_area: like area
877 s_count: INTEGER
878 old_count: INTEGER
879 do
880 s_count := s.count
881 old_count := count
882 diff := s_count - (end_index - start_index + 1)
883 new_size := diff + old_count
884 if diff > 0 then
885 -- We need to resize the string.
886 grow (new_size)
887 end
888
889 l_area := area
890 --| We move the end of the string forward (if diff is > 0), backward (if diff < 0),
891 --| and nothing otherwise.
892 if diff /= 0 then
893 l_area.overlapping_move (end_index, end_index + diff, old_count - end_index)
894 end
895 --| Set new count
896 set_count (new_size)
897 --| We copy the substring.
898 l_area.copy_data (s.area, 0, start_index - 1, s_count)
899 ensure
900 new_count: count = old count + old s.count - end_index + start_index - 1
901 replaced: elks_checking implies
902 (is_equal (old (substring (1, start_index - 1) +
903 s + substring (end_index + 1, count))))
904 end
905
906 replace_substring_all (original, new: like Current) is
907 -- Replace every occurrence of `original' with `new'.
908 require
909 original_exists: original /= Void
910 new_exists: new /= Void
911 original_not_empty: not original.is_empty
912 local
913 l_first_pos, l_next_pos: INTEGER
914 l_orig_count, l_new_count, l_count: INTEGER
915 l_area, l_new_area: like area
916 l_offset: INTEGER
917 l_string_searcher: like string_searcher
918 do
919 if not is_empty then
920 l_count := count
921 l_string_searcher := string_searcher
922 l_string_searcher.initialize_deltas (original)
923 l_first_pos := l_string_searcher.substring_index_with_deltas (Current, original, 1, l_count)
924 if l_first_pos > 0 then
925 l_orig_count := original.count
926 l_new_count := new.count
927 if l_orig_count = l_new_count then
928 -- String will not be resized, simply perform character substitution
929 from
930 l_area := area
931 l_new_area := new.area
932 until
933 l_first_pos = 0
934 loop
935 l_area.copy_data (l_new_area, 0, l_first_pos - 1, l_new_count)
936 if l_first_pos + l_new_count <= l_count then
937 l_first_pos := l_string_searcher.substring_index_with_deltas (Current, original, l_first_pos + l_new_count, l_count)
938 else
939 l_first_pos := 0
940 end
941 end
942 elseif l_orig_count > l_new_count then
943 -- New string is smaller than previous string, we can optimize
944 -- substitution by only moving block between two occurrences of `orginal'.
945 from
946 l_next_pos := l_string_searcher.substring_index_with_deltas (Current, original, l_first_pos + l_orig_count, l_count)
947 l_area := area
948 l_new_area := new.area
949 until
950 l_next_pos = 0
951 loop
952 -- Copy new string into Current
953 l_area.copy_data (l_new_area, 0, l_first_pos - 1 - l_offset, l_new_count)
954 -- Shift characters between `l_first_pos' and `l_next_pos'
955 l_area.overlapping_move (l_first_pos + l_orig_count - 1,
956 l_first_pos + l_new_count - 1 - l_offset, l_next_pos - l_first_pos - l_orig_count)
957 l_first_pos := l_next_pos
958 l_offset := l_offset + (l_orig_count - l_new_count)
959 if l_first_pos + l_new_count <= l_count then
960 l_next_pos := l_string_searcher.substring_index_with_deltas (Current, original, l_first_pos + l_orig_count, l_count)
961 else
962 l_next_pos := 0
963 end
964 end
965 -- Perform final substitution:
966 -- Copy new string into Current
967 l_area.copy_data (l_new_area, 0, l_first_pos - 1 - l_offset, l_new_count)
968 -- Shift characters between `l_first_pos' and the end of the string
969 l_area.overlapping_move (l_first_pos + l_orig_count - 1,
970 l_first_pos + l_new_count - 1 - l_offset, l_count + 1 - l_first_pos - l_orig_count)
971 -- Perform last substitution
972 l_offset := l_offset + (l_orig_count - l_new_count)
973
974 -- Update `count'
975 set_count (l_count - l_offset)
976 else
977 -- Optimization is harder as we don't know how many times we need to resize
978 -- the string. For now, we do like we did in our previous implementation
979 from
980 until
981 l_first_pos = 0
982 loop
983 replace_substring (new, l_first_pos, l_first_pos + l_orig_count - 1)
984 l_count := count
985 if l_first_pos + l_new_count <= l_count then
986 l_first_pos := l_string_searcher.substring_index_with_deltas (Current, original, l_first_pos + l_new_count, l_count)
987 else
988 l_first_pos := 0
989 end
990 end
991 end
992 internal_hash_code := 0
993 end
994 end
995 end
996
997 replace_blank is
998 -- Replace all current characters with blanks.
999 do
1000 fill_with (' ')
1001 ensure
1002 same_size: (count = old count) and (capacity >= old capacity)
1003 all_blank: elks_checking implies occurrences (' ') = count
1004 end
1005
1006 fill_blank is
1007 -- Fill with `capacity' blank characters.
1008 do
1009 fill_character (' ')
1010 ensure
1011 filled: full
1012 same_size: (count = capacity) and (capacity = old capacity)
1013 -- all_blank: For every `i' in `count'..`capacity', `item' (`i') = `Blank'
1014 end
1015
1016 fill_with (c: CHARACTER) is
1017 -- Replace every character with `c'.
1018 local
1019 l_count: INTEGER
1020 do
1021 l_count := count
1022 if l_count /= 0 then
1023 area.fill_with (c, 0, count - 1)
1024 internal_hash_code := 0
1025 end
1026 ensure
1027 same_count: (count = old count) and (capacity >= old capacity)
1028 filled: elks_checking implies occurrences (c) = count
1029 end
1030
1031 replace_character (c: CHARACTER) is
1032 -- Replace every character with `c'.
1033 obsolete
1034 "ELKS 2001: use `fill_with' instead'"
1035 do
1036 fill_with (c)
1037 ensure
1038 same_count: (count = old count) and (capacity >= old capacity)
1039 filled: elks_checking implies occurrences (c) = count
1040 end
1041
1042 fill_character (c: CHARACTER) is
1043 -- Fill with `capacity' characters all equal to `c'.
1044 local
1045 l_cap: like capacity
1046 do
1047 l_cap := capacity
1048 if l_cap /= 0 then
1049 area.fill_with (c, 0, l_cap - 1)
1050 count := l_cap
1051 internal_hash_code := 0
1052 end
1053 ensure
1054 filled: full
1055 same_size: (count = capacity) and (capacity = old capacity)
1056 -- all_char: For every `i' in 1..`capacity', `item' (`i') = `c'
1057 end
1058
1059 head (n: INTEGER) is
1060 -- Remove all characters except for the first `n';
1061 -- do nothing if `n' >= `count'.
1062 obsolete
1063 "ELKS 2001: use `keep_head' instead'"
1064 require
1065 non_negative_argument: n >= 0
1066 do
1067 keep_head (n)
1068 ensure
1069 new_count: count = n.min (old count)
1070 kept: elks_checking implies is_equal (old substring (1, n.min (count)))
1071 end
1072
1073 keep_head (n: INTEGER) is
1074 -- Remove all characters except for the first `n';
1075 -- do nothing if `n' >= `count'.
1076 require
1077 non_negative_argument: n >= 0
1078 do
1079 if n < count then
1080 count := n
1081 internal_hash_code := 0
1082 end
1083 ensure
1084 new_count: count = n.min (old count)
1085 kept: elks_checking implies is_equal (old substring (1, n.min (count)))
1086 end
1087
1088 tail (n: INTEGER) is
1089 -- Remove all characters except for the last `n';
1090 -- do nothing if `n' >= `count'.
1091 obsolete
1092 "ELKS 2001: use `keep_tail' instead'"
1093 require
1094 non_negative_argument: n >= 0
1095 do
1096 keep_tail (n)
1097 ensure
1098 new_count: count = n.min (old count)
1099 kept: elks_checking implies is_equal (old substring (count - n.min(count) + 1, count))
1100 end
1101
1102 keep_tail (n: INTEGER) is
1103 -- Remove all characters except for the last `n';
1104 -- do nothing if `n' >= `count'.
1105 require
1106 non_negative_argument: n >= 0
1107 local
1108 nb: like count
1109 do
1110 nb := count
1111 if n < nb then
1112 area.overlapping_move (nb - n, 0, n)
1113 count := n
1114 internal_hash_code := 0
1115 end
1116 ensure
1117 new_count: count = n.min (old count)
1118 kept: elks_checking implies is_equal (old substring (count - n.min(count) + 1, count))
1119 end
1120
1121 left_adjust is
1122 -- Remove leading whitespace.
1123 local
1124 nb, nb_space: INTEGER
1125 l_area: like area
1126 do
1127 -- Compute number of spaces at the left of current string.
1128 from
1129 nb := count - 1
1130 l_area := area
1131 until
1132 nb_space > nb or else not l_area.item (nb_space).is_space
1133 loop
1134 nb_space := nb_space + 1
1135 end
1136
1137 if nb_space > 0 then
1138 -- Set new count value.
1139 nb := nb + 1 - nb_space
1140 -- Shift characters to the left.
1141 l_area.overlapping_move (nb_space, 0, nb)
1142 -- Set new count.
1143 count := nb
1144 internal_hash_code := 0
1145 end
1146 ensure
1147 valid_count: count <= old count
1148 new_count: not is_empty implies not item (1).is_space
1149 kept: elks_checking implies is_equal ((old twin).substring (old count - count + 1, old count))
1150 end
1151
1152 right_adjust is
1153 -- Remove trailing whitespace.
1154 local
1155 i, nb: INTEGER
1156 nb_space: INTEGER
1157 l_area: like area
1158 do
1159 -- Compute number of spaces at the right of current string.
1160 from
1161 nb := count - 1
1162 i := nb
1163 l_area := area
1164 until
1165 i < 0 or else not l_area.item (i).is_space
1166 loop
1167 nb_space := nb_space + 1
1168 i := i - 1
1169 end
1170
1171 if nb_space > 0 then
1172 -- Set new count.
1173 count := nb + 1 - nb_space
1174 internal_hash_code := 0
1175 end
1176 ensure
1177 valid_count: count <= old count
1178 new_count: (count /= 0) implies
1179 ((item (count) /= ' ') and
1180 (item (count) /= '%T') and
1181 (item (count) /= '%R') and
1182 (item (count) /= '%N'))
1183 kept: elks_checking implies is_equal ((old twin).substring (1, count))
1184 end
1185
1186 share (other: STRING) is
1187 -- Make current string share the text of `other'.
1188 -- Subsequent changes to the characters of current string
1189 -- will also affect `other', and conversely.
1190 require
1191 argument_not_void: other /= Void
1192 do
1193 area := other.area
1194 count := other.count
1195 internal_hash_code := 0
1196 ensure
1197 shared_count: other.count = count
1198 shared_area: other.area = area
1199 end
1200
1201 put (c: CHARACTER; i: INTEGER) is
1202 -- Replace character at position `i' by `c'.
1203 do
1204 area.put (c, i - 1)
1205 internal_hash_code := 0
1206 ensure then
1207 stable_count: count = old count
1208 stable_before_i: elks_checking implies substring (1, i - 1).is_equal (old substring (1, i - 1))
1209 stable_after_i: elks_checking implies substring (i + 1, count).is_equal (old substring (i + 1, count))
1210 end
1211
1212 precede, prepend_character (c: CHARACTER) is
1213 -- Add `c' at front.
1214 local
1215 l_area: like area
1216 do
1217 if count = capacity then
1218 resize (count + additional_space)
1219 end
1220 l_area := area
1221 l_area.overlapping_move (0, 1, count)
1222 l_area.put (c, 0)
1223 count := count + 1
1224 internal_hash_code := 0
1225 ensure
1226 new_count: count = old count + 1
1227 end
1228
1229 prepend (s: STRING) is
1230 -- Prepend a copy of `s' at front.
1231 require
1232 argument_not_void: s /= Void
1233 do
1234 insert_string (s, 1)
1235 ensure
1236 new_count: count = old (count + s.count)
1237 inserted: elks_checking implies string.is_equal (old (s.twin) + old substring (1, count))
1238 end
1239
1240 prepend_boolean (b: BOOLEAN) is
1241 -- Prepend the string representation of `b' at front.
1242 do
1243 prepend (b.out)
1244 end
1245
1246 prepend_double (d: DOUBLE) is
1247 -- Prepend the string representation of `d' at front.
1248 do
1249 prepend (d.out)
1250 end
1251
1252 prepend_integer (i: INTEGER) is
1253 -- Prepend the string representation of `i' at front.
1254 do
1255 prepend (i.out)
1256 end
1257
1258 prepend_real (r: REAL) is
1259 -- Prepend the string representation of `r' at front.
1260 do
1261 prepend (r.out)
1262 end
1263
1264 prepend_string (s: STRING) is
1265 -- Prepend a copy of `s', if not void, at front.
1266 do
1267 if s /= Void then
1268 prepend (s)
1269 end
1270 end
1271
1272 append (s: STRING) is
1273 -- Append a copy of `s' at end.
1274 require
1275 argument_not_void: s /= Void
1276 local
1277 l_count, l_s_count, l_new_size: INTEGER
1278 do
1279 l_s_count := s.count
1280 if l_s_count > 0 then
1281 l_count := count
1282 l_new_size := l_s_count + l_count
1283 if l_new_size > capacity then
1284 resize (l_new_size + additional_space)
1285 end
1286 area.copy_data (s.area, 0, l_count, l_s_count)
1287 count := l_new_size
1288 internal_hash_code := 0
1289 end
1290 ensure
1291 new_count: count = old count + old s.count
1292 appended: elks_checking implies is_equal (old twin + old s.twin)
1293 end
1294
1295 infix "+" (s: STRING): like Current is
1296 -- Append a copy of 's' at the end of a copy of Current,
1297 -- Then return the Result.
1298 require
1299 argument_not_void: s /= Void
1300 do
1301 Result := new_string (count + s.count)
1302 Result.append (Current)
1303 Result.append (s)
1304 ensure
1305 Result_exists: Result /= Void
1306 new_count: Result.count = count + s.count
1307 initial: elks_checking implies Result.substring (1, count).is_equal (Current)
1308 final: elks_checking implies Result.substring (count + 1, count + s.count).same_string (s)
1309 end
1310
1311 append_string (s: STRING) is
1312 -- Append a copy of `s', if not void, at end.
1313 do
1314 if s /= Void then
1315 append (s)
1316 end
1317 ensure
1318 appended: s /= Void implies
1319 (elks_checking implies is_equal (old twin + old s.twin))
1320 end
1321
1322 append_integer (i: INTEGER) is
1323 -- Append the string representation of `i' at end.
1324 local
1325 l_value: INTEGER
1326 l_starting_index, l_ending_index: INTEGER
1327 l_temp: CHARACTER
1328 l_area: like area
1329 do
1330 if i = 0 then
1331 append_character ('0')
1332 else
1333 -- Extract integer value digit by digit from right to left.
1334 from
1335 l_starting_index := count
1336 if i < 0 then
1337 append_character ('-')
1338 l_starting_index := l_starting_index + 1
1339 l_value := -i
1340 -- Special case for minimum integer value as negating it
1341 -- as no effect.
1342 if l_value = {INTEGER_REF}.Min_value then
1343 append_character ((-(l_value \\ 10) + 48).to_character)
1344 l_value := -(l_value // 10)
1345 end
1346 else
1347 l_value := i
1348 end
1349 until
1350 l_value = 0
1351 loop
1352 append_character (((l_value \\ 10)+ 48).to_character)
1353 l_value := l_value // 10
1354 end
1355
1356 -- Now put digits in correct order from left to right.
1357 from
1358 l_ending_index := count - 1
1359 l_area := area
1360 until
1361 l_starting_index >= l_ending_index
1362 loop
1363 l_temp := l_area.item (l_starting_index)
1364 l_area.put (l_area.item (l_ending_index), l_starting_index)
1365 l_area.put (l_temp, l_ending_index)
1366 l_ending_index := l_ending_index - 1
1367 l_starting_index := l_starting_index + 1
1368 end
1369 end
1370 end
1371
1372 append_integer_8 (i: INTEGER_8) is
1373 -- Append the string representation of `i' at end.
1374 local
1375 l_value: INTEGER_8
1376 l_starting_index, l_ending_index: INTEGER
1377 l_temp: CHARACTER
1378 l_area: like area
1379 do
1380 if i = 0 then
1381 append_character ('0')
1382 else
1383 -- Extract integer value digit by digit from right to left.
1384 from
1385 l_starting_index := count
1386 if i < 0 then
1387 append_character ('-')
1388 l_starting_index := l_starting_index + 1
1389 l_value := -i
1390 -- Special case for minimum integer value as negating it
1391 -- as no effect.
1392 if l_value = feature {INTEGER_8_REF}.Min_value then
1393 append_character ((-(l_value \\ 10) + 48).to_character)
1394 l_value := -(l_value // 10)
1395 end
1396 else
1397 l_value := i
1398 end
1399 until
1400 l_value = 0
1401 loop
1402 append_character (((l_value \\ 10)+ 48).to_character)
1403 l_value := l_value // 10
1404 end
1405
1406 -- Now put digits in correct order from left to right.
1407 from
1408 l_ending_index := count - 1
1409 l_area := area
1410 until
1411 l_starting_index >= l_ending_index
1412 loop
1413 l_temp := l_area.item (l_starting_index)
1414 l_area.put (l_area.item (l_ending_index), l_starting_index)
1415 l_area.put (l_temp, l_ending_index)
1416 l_ending_index := l_ending_index - 1
1417 l_starting_index := l_starting_index + 1
1418 end
1419 end
1420 end
1421
1422 append_integer_16 (i: INTEGER_16) is
1423 -- Append the string representation of `i' at end.
1424 local
1425 l_value: INTEGER_16
1426 l_starting_index, l_ending_index: INTEGER
1427 l_temp: CHARACTER
1428 l_area: like area
1429 do
1430 if i = 0 then
1431 append_character ('0')
1432 else
1433 -- Extract integer value digit by digit from right to left.
1434 from
1435 l_starting_index := count
1436 if i < 0 then
1437 append_character ('-')
1438 l_starting_index := l_starting_index + 1
1439 l_value := -i
1440 -- Special case for minimum integer value as negating it
1441 -- as no effect.
1442 if l_value = feature {INTEGER_16_REF}.Min_value then
1443 append_character ((-(l_value \\ 10) + 48).to_character)
1444 l_value := -(l_value // 10)
1445 end
1446 else
1447 l_value := i
1448 end
1449 until
1450 l_value = 0
1451 loop
1452 append_character (((l_value \\ 10)+ 48).to_character)
1453 l_value := l_value // 10
1454 end
1455
1456 -- Now put digits in correct order from left to right.
1457 from
1458 l_ending_index := count - 1
1459 l_area := area
1460 until
1461 l_starting_index >= l_ending_index
1462 loop
1463 l_temp := l_area.item (l_starting_index)
1464 l_area.put (l_area.item (l_ending_index), l_starting_index)
1465 l_area.put (l_temp, l_ending_index)
1466 l_ending_index := l_ending_index - 1
1467 l_starting_index := l_starting_index + 1
1468 end
1469 end
1470 end
1471
1472 append_integer_64 (i: INTEGER_64) is
1473 -- Append the string representation of `i' at end.
1474 local
1475 l_value: INTEGER_64
1476 l_starting_index, l_ending_index: INTEGER
1477 l_temp: CHARACTER
1478 l_area: like area
1479 do
1480 if i = 0 then
1481 append_character ('0')
1482 else
1483 -- Extract integer value digit by digit from right to left.
1484 from
1485 l_starting_index := count
1486 if i < 0 then
1487 append_character ('-')
1488 l_starting_index := l_starting_index + 1
1489 l_value := -i
1490 -- Special case for minimum integer value as negating it
1491 -- as no effect.
1492 if l_value = feature {INTEGER_64_REF}.Min_value then
1493 append_character ((-(l_value \\ 10) + 48).to_character)
1494 l_value := -(l_value // 10)
1495 end
1496 else
1497 l_value := i
1498 end
1499 until
1500 l_value = 0
1501 loop
1502 append_character (((l_value \\ 10)+ 48).to_character)
1503 l_value := l_value // 10
1504 end
1505
1506 -- Now put digits in correct order from left to right.
1507 from
1508 l_ending_index := count - 1
1509 l_area := area
1510 until
1511 l_starting_index >= l_ending_index
1512 loop
1513 l_temp := l_area.item (l_starting_index)
1514 l_area.put (l_area.item (l_ending_index), l_starting_index)
1515 l_area.put (l_temp, l_ending_index)
1516 l_ending_index := l_ending_index - 1
1517 l_starting_index := l_starting_index + 1
1518 end
1519 end
1520 end
1521
1522 append_natural_8 (i: NATURAL_8) is
1523 -- Append the string representation of `i' at end.
1524 local
1525 l_value: NATURAL_8
1526 l_starting_index, l_ending_index: INTEGER
1527 l_temp: CHARACTER
1528 l_area: like area
1529 do
1530 if i = 0 then
1531 append_character ('0')
1532 else
1533 -- Extract integer value digit by digit from right to left.
1534 from
1535 l_starting_index := count
1536 l_value := i
1537 until
1538 l_value = 0
1539 loop
1540 append_character (((l_value \\ 10)+ 48).to_character)
1541 l_value := l_value // 10
1542 end
1543
1544 -- Now put digits in correct order from left to right.
1545 from
1546 l_ending_index := count - 1
1547 l_area := area
1548 until
1549 l_starting_index >= l_ending_index
1550 loop
1551 l_temp := l_area.item (l_starting_index)
1552 l_area.put (l_area.item (l_ending_index), l_starting_index)
1553 l_area.put (l_temp, l_ending_index)
1554 l_ending_index := l_ending_index - 1
1555 l_starting_index := l_starting_index + 1
1556 end
1557 end
1558 end
1559
1560 append_natural_16 (i: NATURAL_16) is
1561 -- Append the string representation of `i' at end.
1562 local
1563 l_value: NATURAL_16
1564 l_starting_index, l_ending_index: INTEGER
1565 l_temp: CHARACTER
1566 l_area: like area
1567 do
1568 if i = 0 then
1569 append_character ('0')
1570 else
1571 -- Extract integer value digit by digit from right to left.
1572 from
1573 l_starting_index := count
1574 l_value := i
1575 until
1576 l_value = 0
1577 loop
1578 append_character (((l_value \\ 10)+ 48).to_character)
1579 l_value := l_value // 10
1580 end
1581
1582 -- Now put digits in correct order from left to right.
1583 from
1584 l_ending_index := count - 1
1585 l_area := area
1586 until
1587 l_starting_index >= l_ending_index
1588 loop
1589 l_temp := l_area.item (l_starting_index)
1590 l_area.put (l_area.item (l_ending_index), l_starting_index)
1591 l_area.put (l_temp, l_ending_index)
1592 l_ending_index := l_ending_index - 1
1593 l_starting_index := l_starting_index + 1
1594 end
1595 end
1596 end
1597
1598 append_natural_32 (i: NATURAL_32) is
1599 -- Append the string representation of `i' at end.
1600 local
1601 l_value: NATURAL_32
1602 l_starting_index, l_ending_index: INTEGER
1603 l_temp: CHARACTER
1604 l_area: like area
1605 do
1606 if i = 0 then
1607 append_character ('0')
1608 else
1609 -- Extract integer value digit by digit from right to left.
1610 from
1611 l_starting_index := count
1612 l_value := i
1613 until
1614 l_value = 0
1615 loop
1616 append_character (((l_value \\ 10)+ 48).to_character)
1617 l_value := l_value // 10
1618 end
1619
1620 -- Now put digits in correct order from left to right.
1621 from
1622 l_ending_index := count - 1
1623 l_area := area
1624 until
1625 l_starting_index >= l_ending_index
1626 loop
1627 l_temp := l_area.item (l_starting_index)
1628 l_area.put (l_area.item (l_ending_index), l_starting_index)
1629 l_area.put (l_temp, l_ending_index)
1630 l_ending_index := l_ending_index - 1
1631 l_starting_index := l_starting_index + 1
1632 end
1633 end
1634 end
1635
1636 append_natural_64 (i: NATURAL_64) is
1637 -- Append the string representation of `i' at end.
1638 local
1639 l_value: NATURAL_64
1640 l_starting_index, l_ending_index: INTEGER
1641 l_temp: CHARACTER
1642 l_area: like area
1643 do
1644 if i = 0 then
1645 append_character ('0')
1646 else
1647 -- Extract integer value digit by digit from right to left.
1648 from
1649 l_starting_index := count
1650 l_value := i
1651 until
1652 l_value = 0
1653 loop
1654 append_character (((l_value \\ 10)+ 48).to_character)
1655 l_value := l_value // 10
1656 end
1657
1658 -- Now put digits in correct order from left to right.
1659 from
1660 l_ending_index := count - 1
1661 l_area := area
1662 until
1663 l_starting_index >= l_ending_index
1664 loop
1665 l_temp := l_area.item (l_starting_index)
1666 l_area.put (l_area.item (l_ending_index), l_starting_index)
1667 l_area.put (l_temp, l_ending_index)
1668 l_ending_index := l_ending_index - 1
1669 l_starting_index := l_starting_index + 1
1670 end
1671 end
1672 end
1673
1674 append_real (r: REAL) is
1675 -- Append the string representation of `r' at end.
1676 do
1677 append (r.out)
1678 end
1679
1680 append_double (d: DOUBLE) is
1681 -- Append the string representation of `d' at end.
1682 do
1683 append (d.out)
1684 end
1685
1686 append_character, extend (c: CHARACTER) is
1687 -- Append `c' at end.
1688 local
1689 current_count: INTEGER
1690 do
1691 current_count := count
1692 if current_count = capacity then
1693 resize (current_count + additional_space)
1694 end
1695 area.put (c, current_count)
1696 count := current_count + 1
1697 internal_hash_code := 0
1698 ensure then
1699 item_inserted: item (count) = c
1700 new_count: count = old count + 1
1701 stable_before: elks_checking implies substring (1, count - 1).is_equal (old twin)
1702 end
1703
1704 append_boolean (b: BOOLEAN) is
1705 -- Append the string representation of `b' at end.
1706 do
1707 append (b.out)
1708 end
1709
1710 insert (s: STRING; i: INTEGER) is
1711 -- Add `s' to left of position `i' in current string.
1712 obsolete
1713 "ELKS 2001: use `insert_string' instead"
1714 require
1715 string_exists: s /= Void
1716 index_small_enough: i <= count + 1
1717 index_large_enough: i > 0
1718 do
1719 insert_string (s, i)
1720 ensure
1721 inserted: elks_checking implies
1722 (is_equal (old substring (1, i - 1) + old (s.twin) + old substring (i, count)))
1723 end
1724
1725 insert_string (s: STRING; i: INTEGER) is
1726 -- Insert `s' at index `i', shifting characters between ranks
1727 -- `i' and `count' rightwards.
1728 require
1729 string_exists: s /= Void
1730 valid_insertion_index: 1 <= i and i <= count + 1
1731 local
1732 pos, new_size: INTEGER
1733 l_s_count: INTEGER
1734 l_area: like area
1735 do
1736 -- Insert `s' if `s' is not empty, otherwise is useless.
1737 l_s_count := s.count
1738 if l_s_count /= 0 then
1739 -- Resize Current if necessary.
1740 new_size := l_s_count + count
1741 if new_size > capacity then
1742 resize (new_size + additional_space)
1743 end
1744
1745 -- Perform all operations using a zero based arrays.
1746 l_area := area
1747 pos := i - 1
1748
1749 -- First shift from `s.count' position all characters starting at index `pos'.
1750 l_area.overlapping_move (pos, pos + l_s_count, count - pos)
1751
1752 -- Copy string `s' at index `pos'.
1753 l_area.copy_data (s.area, 0, pos, l_s_count)
1754
1755 count := new_size
1756 internal_hash_code := 0
1757 end
1758 ensure
1759 inserted: elks_checking implies
1760 (is_equal (old substring (1, i - 1) + old (s.twin) + old substring (i, count)))
1761 end
1762
1763 insert_character (c: CHARACTER; i: INTEGER) is
1764 -- Insert `c' at index `i', shifting characters between ranks
1765 -- `i' and `count' rightwards.
1766 require
1767 valid_insertion_index: 1 <= i and i <= count + 1
1768 local
1769 pos, new_size: INTEGER
1770 l_area: like area
1771 do
1772 -- Resize Current if necessary.
1773 new_size := 1 + count
1774 if new_size > capacity then
1775 resize (new_size + additional_space)
1776 end
1777
1778 -- Perform all operations using a zero based arrays.
1779 pos := i - 1
1780 l_area := area
1781
1782 -- First shift from `s.count' position all characters starting at index `pos'.
1783 l_area.overlapping_move (pos, pos + 1, count - pos)
1784
1785 -- Insert new character
1786 l_area.put (c, pos)
1787
1788 count := new_size
1789 internal_hash_code := 0
1790 ensure
1791 one_more_character: count = old count + 1
1792 inserted: item (i) = c
1793 stable_before_i: elks_checking implies substring (1, i - 1).is_equal (old substring (1, i - 1))
1794 stable_after_i: elks_checking implies substring (i + 1, count).is_equal (old substring (i, count))
1795 end
1796
1797 feature -- Removal
1798
1799 remove (i: INTEGER) is
1800 -- Remove `i'-th character.
1801 require
1802 index_small_enough: i <= count
1803 index_large_enough: i > 0
1804 local
1805 l_count: INTEGER
1806 do
1807 l_count := count
1808 -- Shift characters to the left.
1809 area.overlapping_move (i, i - 1, l_count - i)
1810 -- Update content.
1811 count := l_count - 1
1812 internal_hash_code := 0
1813 ensure
1814 new_count: count = old count - 1
1815 removed: elks_checking implies is_equal (old substring (1, i - 1) + old substring (i + 1, count))
1816 end
1817
1818 remove_head (n: INTEGER) is
1819 -- Remove first `n' characters;
1820 -- if `n' > `count', remove all.
1821 require
1822 n_non_negative: n >= 0
1823 do
1824 if n > count then
1825 count := 0
1826 internal_hash_code := 0
1827 else
1828 keep_tail (count - n)
1829 end
1830 ensure
1831 removed: elks_checking implies is_equal (old substring (n.min (count) + 1, count))
1832 end
1833
1834 remove_substring (start_index, end_index: INTEGER) is
1835 -- Remove all characters from `start_index'
1836 -- to `end_index' inclusive.
1837 require
1838 valid_start_index: 1 <= start_index
1839 valid_end_index: end_index <= count
1840 meaningful_interval: start_index <= end_index + 1
1841 local
1842 l_count, nb_removed: INTEGER
1843 do
1844 nb_removed := end_index - start_index + 1
1845 if nb_removed > 0 then
1846 l_count := count
1847 area.overlapping_move (start_index + nb_removed - 1, start_index - 1, l_count - end_index)
1848 count := l_count - nb_removed
1849 end
1850 ensure
1851 removed: elks_checking implies
1852 is_equal (old substring (1, start_index - 1) + old substring (end_index + 1, count))
1853 end
1854
1855 remove_tail (n: INTEGER) is
1856 -- Remove last `n' characters;
1857 -- if `n' > `count', remove all.
1858 require
1859 n_non_negative: n >= 0
1860 local
1861 l_count: INTEGER
1862 do
1863 l_count := count
1864 if n > l_count then
1865 count := 0
1866 internal_hash_code := 0
1867 else
1868 keep_head (l_count - n)
1869 end
1870 ensure
1871 removed: elks_checking implies is_equal (old substring (1, count - n.min (count)))
1872 end
1873
1874 prune (c: CHARACTER) is
1875 -- Remove first occurrence of `c', if any.
1876 require else
1877 True
1878 local
1879 counter: INTEGER
1880 do
1881 from
1882 counter := 1
1883 until
1884 counter > count or else (item (counter) = c)
1885 loop
1886 counter := counter + 1
1887 end
1888 if counter <= count then
1889 remove (counter)
1890 end
1891 end
1892
1893 prune_all (c: CHARACTER) is
1894 -- Remove all occurrences of `c'.
1895 require else
1896 True
1897 local
1898 i, j, nb: INTEGER
1899 l_area: like area
1900 l_char: CHARACTER
1901 do
1902 -- Traverse string and shift characters to the left
1903 -- each time we find an occurrence of `c'.
1904 from
1905 l_area := area
1906 nb := count
1907 until
1908 i = nb
1909 loop
1910 l_char := l_area.item (i)
1911 if l_char /= c then
1912 l_area.put (l_char, j)
1913 j := j + 1
1914 end
1915 i := i + 1
1916 end
1917 count := j
1918 internal_hash_code := 0
1919 ensure then
1920 changed_count: count = (old count) - (old occurrences (c))
1921 -- removed: For every `i' in 1..`count', `item' (`i') /= `c'
1922 end
1923
1924 prune_all_leading (c: CHARACTER) is
1925 -- Remove all leading occurrences of `c'.
1926 do
1927 from
1928 until
1929 is_empty or else item (1) /= c
1930 loop
1931 remove (1)
1932 end
1933 end
1934
1935 prune_all_trailing (c: CHARACTER) is
1936 -- Remove all trailing occurrences of `c'.
1937 do
1938 from
1939 until
1940 is_empty or else item (count) /= c
1941 loop
1942 remove (count)
1943 end
1944 end
1945
1946 wipe_out is
1947 -- Remove all characters.
1948 do
1949 create area.make (1)
1950 count := 0
1951 internal_hash_code := 0
1952 ensure then
1953 is_empty: count = 0
1954 empty_capacity: capacity = 0
1955 end
1956
1957 clear_all is
1958 -- Reset all characters.
1959 do
1960 count := 0
1961 internal_hash_code := 0
1962 ensure
1963 is_empty: count = 0
1964 same_capacity: capacity = old capacity
1965 end
1966
1967 feature -- Resizing
1968
1969 adapt_size is
1970 -- Adapt the size to accommodate `count' characters.
1971 do
1972 resize (count)
1973 end
1974
1975 resize (newsize: INTEGER) is
1976 -- Rearrange string so that it can accommodate
1977 -- at least `newsize' characters.
1978 -- Do not lose any previously entered character.
1979 require
1980 new_size_non_negative: newsize >= 0
1981 local
1982 area_count: INTEGER
1983 do
1984 area_count := area.count
1985 if newsize >= area_count then
1986 area := area.aliased_resized_area (newsize + 1)
1987 end
1988 end
1989
1990 grow (newsize: INTEGER) is
1991 -- Ensure that the capacity is at least `newsize'.
1992 do
1993 if newsize > capacity then
1994 resize (newsize)
1995 end
1996 end
1997
1998 feature -- Conversion
1999
2000 as_lower: like Current is
2001 -- New object with all letters in lower case.
2002 do
2003 Result := twin
2004 Result.to_lower
2005 ensure
2006 length: Result.count = count
2007 anchor: count > 0 implies Result.item (1) = item (1).as_lower
2008 recurse: count > 1 implies Result.substring (2, count).
2009 is_equal (substring (2, count).as_lower)
2010 end
2011
2012 as_upper: like Current is
2013 -- New object with all letters in upper case
2014 do
2015 Result := twin
2016 Result.to_upper
2017 ensure
2018 length: Result.count = count
2019 anchor: count > 0 implies Result.item (1) = item (1).as_upper
2020 recurse: count > 1 implies Result.substring (2, count).
2021 is_equal (substring (2, count).as_upper)
2022 end
2023
2024 left_justify is
2025 -- Left justify Current using `count' as witdth.
2026 local
2027 i, nb: INTEGER
2028 l_area: like area
2029 do
2030 -- Remove leading white spaces.
2031 nb := count
2032 left_adjust
2033
2034 -- Get new count
2035 i := count
2036 if i < nb then
2037 -- `left_adjust' did remove some characters, so we need to add
2038 -- some white spaces at the end of the string.
2039 from
2040 l_area := area
2041 until
2042 i = nb
2043 loop
2044 l_area.put (' ', i)
2045 i := i + 1
2046 end
2047 -- Restore `count'
2048 count := nb
2049 internal_hash_code := 0
2050 end
2051 end
2052
2053 center_justify is
2054 -- Center justify Current using `count' as width.
2055 local
2056 i, nb, l_offset: INTEGER
2057 left_nb_space, right_nb_space: INTEGER
2058 l_area: like area
2059 do
2060 -- Compute number of spaces at the left of current string.
2061 from
2062 nb := count
2063 l_area := area
2064 until
2065 left_nb_space = nb or else not l_area.item (left_nb_space).is_space
2066 loop
2067 left_nb_space := left_nb_space + 1
2068 end
2069
2070 -- Compute number of spaces at the right of current string.
2071 from
2072 i := nb - 1
2073 l_area := area
2074 until
2075 i = -1 or else not l_area.item (i).is_space
2076 loop
2077 right_nb_space := right_nb_space + 1
2078 i := i - 1
2079 end
2080
2081 -- We encourage that more spaces will be put to the left, when
2082 -- number of spaces is not even.
2083 l_offset := left_nb_space + right_nb_space
2084 if l_offset \\ 2 = 0 then
2085 l_offset := left_nb_space - l_offset // 2
2086 else
2087 l_offset := left_nb_space - l_offset // 2 - 1
2088 end
2089 if l_offset = 0 then
2090 -- Nothing to be done.
2091 else
2092 -- Shift characters to the right or left (depending on sign of
2093 -- `l_offset' by `l_offset' position.
2094 l_area.move_data (left_nb_space, left_nb_space - l_offset,
2095 nb - left_nb_space - right_nb_space)
2096
2097 if l_offset < 0 then
2098 -- Fill left part with spaces.
2099 l_area.fill_with (' ', left_nb_space, left_nb_space - l_offset - 1)
2100 else
2101 -- Fill right part with spaces.
2102 l_area.fill_with (' ', nb - right_nb_space - l_offset, nb - 1)
2103 end
2104 internal_hash_code := 0
2105 end
2106 end
2107
2108 right_justify is
2109 -- Right justify Current using `count' as width.
2110 local
2111 i, nb: INTEGER
2112 nb_space: INTEGER
2113 l_area: like area
2114 do
2115 nb := count
2116 right_adjust
2117 i := count
2118 nb_space := nb - i
2119 if nb_space > 0 then
2120 -- Shift characters to the right.
2121 from
2122 l_area := area
2123 variant
2124 i + 1
2125 until
2126 i = 0
2127 loop
2128 i := i - 1
2129 l_area.put (l_area.item (i), i + nb_space)
2130 end
2131
2132 -- Fill left part with spaces.
2133 from
2134 variant
2135 nb_space + 1
2136 until
2137 nb_space = 0
2138 loop
2139 nb_space := nb_space - 1
2140 l_area.put (' ', nb_space)
2141 end
2142 -- Restore `count'
2143 count := nb
2144 internal_hash_code := 0
2145 end
2146 ensure
2147 same_count: count = old count
2148 end
2149
2150 character_justify (pivot: CHARACTER; position: INTEGER) is
2151 -- Justify a string based on a `pivot'
2152 -- and the `position' it needs to be in
2153 -- the final string.
2154 -- This will grow the string if necessary
2155 -- to get the pivot in the correct place.
2156 require
2157 valid_position: position <= capacity
2158 positive_position: position >= 1
2159 pivot_not_space: pivot /= ' '
2160 not_empty: not is_empty
2161 local
2162 l_index_of_pivot, l_new_size: INTEGER
2163 l_area: like area
2164 do
2165 l_index_of_pivot := index_of (pivot, 1)
2166 if l_index_of_pivot /= 0 then
2167 if l_index_of_pivot < position then
2168 -- We need to resize Current so that we can shift Current by
2169 -- `l_index_of_pivot - position'.
2170 l_new_size := count + position - l_index_of_pivot
2171 grow (l_new_size)
2172 l_area := area
2173 l_area.move_data (0, position - l_index_of_pivot, count)
2174 l_area.fill_with (' ', 0, position - l_index_of_pivot - 1)
2175 count := l_new_size
2176 else
2177 -- Simply shift content to the left and reset trailing with spaces.
2178 l_area := area
2179 l_area.move_data (l_index_of_pivot - position, 0, count - l_index_of_pivot + position)
2180 l_area.fill_with (' ', count - l_index_of_pivot + position, count - 1)
2181 end
2182 internal_hash_code := 0
2183 end
2184 end
2185
2186 to_lower is
2187 -- Convert to lower case.
2188 local
2189 i: INTEGER
2190 a: like area
2191 do
2192 from
2193 i := count - 1
2194 a := area
2195 until
2196 i < 0
2197 loop
2198 a.put (a.item (i).lower, i)
2199 i := i - 1
2200 end
2201 internal_hash_code := 0
2202 ensure
2203 length_end_content: elks_checking implies is_equal (old as_lower)
2204 end
2205
2206 to_upper is
2207 -- Convert to upper case.
2208 local
2209 i: INTEGER
2210 a: like area
2211 do
2212 from
2213 i := count - 1
2214 a := area
2215 until
2216 i < 0
2217 loop
2218 a.put (a.item (i).upper, i)
2219 i := i - 1
2220 end
2221 internal_hash_code := 0
2222 ensure
2223 length_end_content: elks_checking implies is_equal (old as_upper)
2224 end
2225
2226 to_integer_8: INTEGER_8 is
2227 -- 8-bit integer value
2228 require
2229 is_integer_8: is_integer_8
2230 do
2231 ctoi_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_integer_8)
2232 Result := ctoi_convertor.parsed_integer_8
2233 end
2234
2235 to_integer_16: INTEGER_16 is
2236 -- 16-bit integer value
2237 require
2238 is_integer_16: is_integer_16
2239 do
2240 ctoi_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_integer_16)
2241 Result := ctoi_convertor.parsed_integer_16
2242 end
2243
2244 to_integer, to_integer_32: INTEGER is
2245 -- 32-bit integer value
2246 require
2247 is_integer: is_integer_32
2248 do
2249 ctoi_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_integer_32)
2250 Result := ctoi_convertor.parsed_integer
2251 end
2252
2253 to_integer_64: INTEGER_64 is
2254 -- 64-bit integer value
2255 require
2256 is_integer_64: is_integer_64
2257 do
2258 ctoi_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_integer_64)
2259 Result := ctoi_convertor.parsed_integer_64
2260 end
2261
2262 to_natural_8: NATURAL_8 is
2263 -- 8-bit natural value
2264 require
2265 is_natural_8: is_natural_8
2266 do
2267 ctoi_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_natural_8)
2268 Result := ctoi_convertor.parsed_natural_8
2269 end
2270
2271 to_natural_16: NATURAL_16 is
2272 -- 16-bit natural value
2273 require
2274 is_natural_16: is_natural_16
2275 do
2276 ctoi_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_natural_16)
2277 Result := ctoi_convertor.parsed_natural_16
2278 end
2279
2280 to_natural, to_natural_32: NATURAL_32 is
2281 -- 32-bit natural value
2282 require
2283 is_natural: is_natural
2284 do
2285 ctoi_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_natural_32)
2286 Result := ctoi_convertor.parsed_natural_32
2287 end
2288
2289 to_natural_64: NATURAL_64 is
2290 -- 64-bit natural value
2291 require
2292 is_natural_64: is_natural_64
2293 do
2294 ctoi_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_natural_64)
2295 Result := ctoi_convertor.parsed_natural_64
2296 end
2297
2298 to_real: REAL is
2299 -- Real value;
2300 -- for example, when applied to "123.0", will yield 123.0
2301 require
2302 represents_a_real: is_real
2303 do
2304 Result := to_double
2305 end
2306
2307 to_double: DOUBLE is
2308 -- "Double" value;
2309 -- for example, when applied to "123.0", will yield 123.0 (double)
2310 require
2311 represents_a_double: is_double
2312 do
2313 ctor_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_double)
2314 Result := ctor_convertor.parsed_double
2315 end
2316
2317 to_boolean: BOOLEAN is
2318 -- Boolean value;
2319 -- "True" yields `True', "False" yields `False'
2320 -- (case-insensitive)
2321 require
2322 is_boolean: is_boolean
2323 do
2324 check true_constant.count = 4 end
2325 if count = 4 then
2326 Result := True
2327 end
2328 ensure
2329 to_boolean: (Result = true_constant.same_string (as_lower)) or
2330 (not Result = false_constant.same_string (as_lower))
2331 end
2332
2333 linear_representation: LINEAR [CHARACTER] is
2334 -- Representation as a linear structure
2335 local
2336 temp: ARRAYED_LIST [CHARACTER]
2337 i: INTEGER
2338 do
2339 create temp.make (capacity)
2340 from
2341 i := 1
2342 until
2343 i > count
2344 loop
2345 temp.extend (item (i))
2346 i := i + 1
2347 end
2348 Result := temp
2349 end
2350
2351 split (a_separator: CHARACTER): LIST [STRING] is
2352 -- Split on `a_separator'.
2353 local
2354 l_list: ARRAYED_LIST [STRING]
2355 part: STRING
2356 i, j, c: INTEGER
2357 do
2358 c := count
2359 -- Worse case allocation: every character is a separator
2360 create l_list.make (c + 1)
2361 if c > 0 then
2362 from
2363 i := 1
2364 until
2365 i > c
2366 loop
2367 j := index_of (a_separator, i)
2368 if j = 0 then
2369 -- No separator was found, we will
2370 -- simply create a list with a copy of
2371 -- Current in it.
2372 j := c + 1
2373 end
2374 part := substring (i, j - 1)
2375 l_list.extend (part)
2376 i := j + 1
2377 end
2378 if j = c then
2379 check
2380 last_character_is_a_separator: item (j) = a_separator
2381 end
2382 -- A separator was found at the end of the string
2383 l_list.extend ("")
2384 end
2385 else
2386 -- Extend empty string, since Current is empty.
2387 l_list.extend ("")
2388 end
2389 Result := l_list
2390 check
2391 l_list.count = occurrences (a_separator) + 1
2392 end
2393 ensure
2394 Result /= Void
2395 end
2396
2397 frozen to_c: ANY is
2398 -- A reference to a C form of current string.
2399 -- Useful only for interfacing with C software.
2400 require
2401 not_is_dotnet: not {PLATFORM}.is_dotnet
2402 local
2403 l_area: like area
2404 do
2405 l_area := area
2406 l_area.put ('%U', count)
2407 Result := l_area
2408 end
2409
2410 frozen to_cil: SYSTEM_STRING is
2411 -- Create an instance of SYSTEM_STRING using characters
2412 -- of Current between indices `1' and `count'.
2413 require
2414 is_dotnet: {PLATFORM}.is_dotnet
2415 do
2416 create Result.make (area.native_array, 0, count)
2417 ensure
2418 to_cil_not_void: Result /= Void
2419 end
2420
2421 mirrored: like Current is
2422 -- Mirror image of string;
2423 -- Result for "Hello world" is "dlrow olleH".
2424 do
2425 Result := twin
2426 if count > 0 then
2427 Result.mirror
2428 end
2429 ensure
2430 same_count: Result.count = count
2431 -- reversed: For every `i' in 1..`count', `Result'.`item' (`i') = `item' (`count'+1-`i')
2432 end
2433
2434 mirror is
2435 -- Reverse the order of characters.
2436 -- "Hello world" -> "dlrow olleH".
2437 local
2438 a: like area
2439 c: CHARACTER
2440 i, j: INTEGER
2441 do
2442 if count > 0 then
2443 from
2444 i := count - 1
2445 a := area
2446 until
2447 i <= j
2448 loop
2449 c := a.item (i)
2450 a.put (a.item (j), i)
2451 a.put (c, j)
2452 i := i - 1
2453 j := j + 1
2454 end
2455 internal_hash_code := 0
2456 end
2457 ensure
2458 same_count: count = old count
2459 -- reversed: For every `i' in 1..`count', `item' (`i') = old `item' (`count'+1-`i')
2460 end
2461
2462 feature -- Duplication
2463
2464 substring (start_index, end_index: INTEGER): like Current is
2465 -- Copy of substring containing all characters at indices
2466 -- between `start_index' and `end_index'
2467 do
2468 if (1 <= start_index) and (start_index <= end_index) and (end_index <= count) then
2469 Result := new_string (end_index - start_index + 1)
2470 Result.area.copy_data (area, start_index - 1, 0, end_index - start_index + 1)
2471 Result.set_count (end_index - start_index + 1)
2472 else
2473 Result := new_string (0)
2474 end
2475 ensure
2476 substring_not_void: Result /= Void
2477 substring_count: Result.count = end_index - start_index + 1 or Result.count = 0
2478 first_item: Result.count > 0 implies Result.item (1) = item (start_index)
2479 recurse: Result.count > 0 implies
2480 Result.substring (2, Result.count).is_equal (substring (start_index + 1, end_index))
2481 end
2482
2483 multiply (n: INTEGER) is
2484 -- Duplicate a string within itself
2485 -- ("hello").multiply(3) => "hellohellohello"
2486 require
2487 meaningful_multiplier: n >= 1
2488 local
2489 s: like Current
2490 i: INTEGER
2491 do
2492 s := twin
2493 grow (n * count)
2494 from
2495 i := n
2496 until
2497 i = 1
2498 loop
2499 append (s)
2500 i := i - 1
2501 end
2502 end
2503
2504 feature -- Output
2505
2506 out: STRING is
2507 -- Printable representation
2508 do
2509 create Result.make (count)
2510 Result.append (Current)
2511 ensure then
2512 out_not_void: Result /= Void
2513 same_items: same_type ("") implies Result.same_string (Current)
2514 end
2515
2516 feature {STRING_HANDLER} -- Implementation
2517
2518 frozen set_count (number: INTEGER) is
2519 -- Set `count' to `number' of characters.
2520 require
2521 valid_count: 0 <= number and number <= capacity
2522 do
2523 count := number
2524 internal_hash_code := 0
2525 ensure
2526 new_count: count = number
2527 end
2528
2529 feature {NONE} -- Empty string implementation
2530
2531 elks_checking: BOOLEAN is False
2532 -- Are ELKS checkings verified? Must be True when changing implementation of STRING or descendant.
2533
2534 internal_hash_code: INTEGER
2535 -- Computed hash-code.
2536
2537 frozen set_internal_hash_code (v: like internal_hash_code) is
2538 -- Set `internal_hash_code' with `v'.
2539 require
2540 v_nonnegative: v >= 0
2541 do
2542 internal_hash_code := v
2543 ensure
2544 internal_hash_code_set: internal_hash_code = v
2545 end
2546
2547 feature {NONE} -- Implementation
2548
2549 new_string (n: INTEGER): like Current is
2550 -- New instance of current with space for at least `n' characters.
2551 require
2552 n_non_negative: n >= 0
2553 do
2554 create Result.make (n)
2555 ensure
2556 new_string_not_void: Result /= Void
2557 new_string_empty: Result.is_empty
2558 new_string_area_big_enough: Result.capacity >= n
2559 end
2560
2561 feature {NONE} -- Transformation
2562
2563 correct_mismatch is
2564 -- Attempt to correct object mismatch during retrieve using `mismatch_information'.
2565 do
2566 -- Nothing to be done because we only added `internal_hash_code' that will
2567 -- be recomputed next time we query `hash_code'.
2568 end
2569
2570 feature {NONE} -- Implementation
2571
2572 is_valid_integer_or_natural (type: INTEGER) : BOOLEAN is
2573 -- Is `Current' a valid number according to given `type'?
2574 do
2575 ctoi_convertor.reset (type)
2576 ctoi_convertor.parse_string_with_type (Current, type)
2577 Result := ctoi_convertor.is_integral_integer
2578 end
2579
2580 str_strict_cmp (this, other: like area; nb: INTEGER): INTEGER is
2581 -- Compare `this' and `other' strings
2582 -- for the first `nb' characters.
2583 -- 0 if equal, < 0 if `this' < `other',
2584 -- > 0 if `this' > `other'
2585 require
2586 this_not_void: this /= Void or else nb = 0
2587 other_not_void: other /= Void
2588 nb_non_negative: nb >= 0
2589 nb_valid: (this /= Void implies nb <= this.count) and nb <= other.count
2590 local
2591 i, l_current_code, l_other_code: INTEGER
2592 do
2593 from
2594 until
2595 i = nb
2596 loop
2597 l_current_code := this.item (i).code
2598 l_other_code := other.item (i).code
2599 if l_current_code /= l_other_code then
2600 Result := l_current_code - l_other_code
2601 i := nb - 1 -- Jump out of loop
2602 end
2603 i := i + 1
2604 end
2605 end
2606
2607 string_searcher: STRING_SEARCHER is
2608 -- Facilities to search string in another string.
2609 once
2610 create Result.make
2611 ensure
2612 string_searcher_not_void: Result /= Void
2613 end
2614
2615 c_string_provider: C_STRING is
2616 -- To create Eiffel strings from C string.
2617 once
2618 create Result.make_empty (0)
2619 ensure
2620 c_string_provider_not_void: Result /= Void
2621 end
2622
2623 empty_area: SPECIAL [CHARACTER] is
2624 -- Empty `area' to avoid useless creation of empty areas when wiping out a STRING.
2625 obsolete
2626 "Simply create `area' directly."
2627 do
2628 create Result.make (1)
2629 ensure
2630 empty_area_not_void: Result /= Void
2631 end
2632
2633 ctoi_convertor: STRING_TO_INTEGER_CONVERTOR is
2634 -- Convertor used to convert string to integer or natural
2635 once
2636 create Result.make
2637 Result.set_leading_separators (" ")
2638 Result.set_trailing_separators (" ")
2639 Result.set_leading_separators_acceptable (True)
2640 Result.set_trailing_separators_acceptable (True)
2641 end
2642
2643 ctor_convertor: STRING_TO_REAL_CONVERTOR is
2644 -- Convertor used to convert string to real or double
2645 once
2646 create Result.make
2647 Result.set_leading_separators (" ")
2648 Result.set_trailing_separators (" ")
2649 Result.set_leading_separators_acceptable (True)
2650 Result.set_trailing_separators_acceptable (True)
2651 end
2652
2653 invariant
2654 extendible: extendible
2655 compare_character: not object_comparison
2656 index_set_has_same_count: index_set.count = count
2657 area_not_void: area /= Void
2658
2659 end

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.23