[m-rev.] for post-commit review: fix doc of version_array.resize

[Peter Wang]

On Sat, 03 Dec 2022 09:50:19 +1100 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> It seems that the comment on resize had three bugs
> in three lines: the two ranges were both individually wrong,
> and they had a clash between them, since they overlapped.
> 
> Zoltan.
> 
> -    % resize(A, N, X) returns a new array whose items from
> -    % 0..min(size(A), N - 1) are taken from A and whose items
> -    % from min(size(A), N - 1)..(N - 1) (if any) are initialised to X.
> -    % A predicate version is also provided.
> +    % resize(Array0, NewSize, NewValue) = Array:
> +    % resize(NewSize, NewValue, Array0, Array):
> +    %
> +    % Return in Array a new array of size NewSize
> +    %
> +    % - whose items at indices from 0 to min(size(Array0), NewSize) - 1
> +    %   are taken from Array0, and
> +    %
> +    % - whose items at indices from min(size(Array0), NewSize) to (NewSize - 1)
> +    %   (if any such items exist) are initialised to NewValue.
>      %
>  :- func resize(version_array(T), int, T) = version_array(T).
>  :- pred resize(int::in, T::in, version_array(T)::in, version_array(T)::out)

Ok. That's precise but I find it a bit hard to follow for such a simple
operation. The documentation for array.resize is simpler but assumes
destructive update.

Here's an attempt without spelling out the bounds:

    Returns in Array a new array of size NewSize.

    Each slot in Array is filled with the item from the corresponding
    slot in Array0, if any.

    When NewSize is greater than size(Array0), Array will have more
    slots than Array0. Those extra slots will be initialised to
    NewValue.

Peter