Fix an implementation/specification mismatch in BatVect.insert #767
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
BatVect.insert : int -> 'a t -> 'a t
is specified so thatinsert n r u
inserts the roper
between the elements of indexn
andn+1
inu
. Its implementation does something different, it insertsr
strictly before the element of indexn
inu
.The present commit changes the specification to match the implementation.
First, we expect users to have tested their program instead of trusting (or, unfortunately, even reading) the documentation, so it is likely that the uses of
BatVect.insert
with the current implementation is correct for their needs; changing it would break user program.Second, we argue that the implemented behavior is actually far more
natural:
the implementation (in terms of
sub
andconcat
) is nicer -- hear the code!the ranges of integer values valid for
insert
is0 .. (length u - 1)
, as one would expect, instead of(-1) .. (length u - 2)
as with the current specification.this gives a very natural invariant between
insert
andBatVect.remove : (*start*)int -> (*len*)int -> 'a t -> 'a t
:u
is equal tou |> insert n r |> remove n (length r))
.fixes #766.