[m-rev.] for review: Define string.between_codepoints more precisely and fix bug.

[Mark Brown]

On Wed, Oct 23, 2019 at 3:03 PM Peter Wang <novalazy at gmail.com> wrote:
>
> library/string.m:
>     Define string.between_codepoints in terms of codepoint_offset.
>
>     Fix behaviour in the case where
>         Start < 0,
>         End < 0,
>         End > Start
>
> tests/hard_coded/string_codepoint.exp:
> tests/hard_coded/string_codepoint.exp2:
> tests/hard_coded/string_codepoint.m:
>     Extend test case.
> ---
>  library/string.m                       | 25 ++++++++++++++++++-------
>  tests/hard_coded/string_codepoint.exp  | 19 +++++++++++++++++++
>  tests/hard_coded/string_codepoint.exp2 | 19 +++++++++++++++++++
>  tests/hard_coded/string_codepoint.m    | 11 ++++++++---
>  4 files changed, 64 insertions(+), 10 deletions(-)
>
> diff --git a/library/string.m b/library/string.m
> index c978476ab..16888d12f 100644
> --- a/library/string.m
> +++ b/library/string.m
> @@ -756,11 +756,21 @@
>      % between_codepoints(String, Start, End, Substring):
>      %
>      % `Substring' is the part of `String' between the code point positions
> -    % `Start' and `End'.
> -    % (If `Start' is out of the range [0, length of `String'], it is treated
> -    % as if it were the nearest end-point of that range.
> -    % If `End' is out of the range [`Start', length of `String'],
> -    % it is treated as if it were the nearest end-point of that range.)
> +    % `Start' and `End'. The result is equivalent to:
> +    %
> +    %   between(String, StartOffset, EndOffset, Substring)
> +    %
> +    % where:
> +    %
> +    %   StartOffset is from codepoint_offset(String, Start, StartOffset)
> +    %     if Start is in [0, count_codepoints(String)],
> +    %   StartOffset = 0 if Start < 0,
> +    %   StartOffset = length(String) otherwise;
> +    %
> +    %   EndOffset is from codepoint_offset(String, End, EndOffset)
> +    %     if End is in [Start, count_codepoints(String)],

This range should start at zero, to match the next clause.

> +    %   EndOffset = 0 if End < 0,
> +    %   EndOffset = length(String) otherwise.

You could add a note here that between/4 will enforce StartOffset =< EndOffset.

Otherwise this looks good.

Mark