Skip to content
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
132 changes: 78 additions & 54 deletions src/lib/array/timsort.ml
Original file line number Diff line number Diff line change
Expand Up @@ -63,63 +63,86 @@ let%test_module _ =

let rec merge_lo
cmp
dest ofs
src0 ofs0 len0
src1 ofs1 len1
dest beg
src0 beg0 end0 x0
src1 beg1 end1 x1
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it would be worth having comments like (* x0 = src0.(beg0) *) already at this point. It's readable in the assertions below but I think it's better to have it here!

=
assert (Array.length dest >= ofs + len0 + len1);
assert (Array.length src0 >= ofs0 + len0);
assert (Array.length src1 >= ofs1 + len1);
if len0 = 0 then
Array.blit src1 ofs1 dest ofs len1
else if len1 = 0 then
Array.blit src0 ofs0 dest ofs len0
else if cmp src0.(ofs0) src1.(ofs1) <= 0 then begin
dest.(ofs) <- src0.(ofs0);
merge_lo
cmp
dest (ofs + 1)
src0 (ofs0 + 1) (len0 - 1)
src1 ofs1 len1
assert (Array.length dest >= beg + (end0 - beg0 + 1) + (end1 - beg1 + 1));
assert (Array.length src0 > end0);
assert (Array.length src1 > end1);
assert (x0 = src0.(beg0));
assert (x1 = src1.(beg1));
assert (end0 >= beg0);
assert (end1 >= beg1);

(* This is used to optimise the case len0 = 1 below. *)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This comment does not make sense to me. I think it would deserve more text!

assert (dest == src1 && beg + (end0 - beg0 + 1) = beg1);

if cmp x0 x1 <= 0 then begin
dest.(beg) <- x0;
(* If this was the last element of run0 we stop. Besides, since we have
* [dest == src1], the remaining element of run1 are already where they
* are supposed to be and we can exit. *)
if beg0 < end0 then
merge_lo
cmp
dest (beg + 1)
src0 (beg0 + 1) end0 src0.(beg0 + 1)
src1 beg1 end1 x1
end else begin
dest.(ofs) <- src1.(ofs1);
merge_lo
cmp
dest (ofs + 1)
src0 ofs0 len0
src1 (ofs1 + 1) (len1 - 1)
dest.(beg) <- x1;
(* If this was the last element of run1 we stop. There remains to move all
* the elements of run0 at the beginning of dest. *)
if beg1 < end1 then
merge_lo
cmp
dest (beg + 1)
src0 beg0 end0 x0
src1 (beg1 + 1) end1 src1.(beg1 + 1)
else
Array.blit src0 beg0 dest (beg + 1) (end0 - beg0 + 1)
end


let rec merge_hi
cmp
dest ofs
src0 ofs0 len0
src1 ofs1 len1
dest end_
src0 beg0 end0 x0 (* run0 *)
src1 beg1 end1 x1 (* run1 *)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

cf before

=
assert (Array.length dest >= ofs + len0 + len1);
assert (Array.length src0 >= ofs0 + len0);
assert (Array.length src1 >= ofs1 + len1);
assert (len0 >= 0);
assert (len1 >= 0);
if len0 = 0 then
Array.blit src1 ofs1 dest ofs len1
else if len1 = 0 then
Array.blit src0 ofs0 dest ofs len0
else if cmp src0.(ofs0 + len0 - 1) src1.(ofs1 + len1 - 1) <= 0 then begin
dest.(ofs + len0 + len1 - 1) <- src1.(ofs1 + len1 - 1);
merge_hi
cmp
dest ofs
src0 ofs0 len0
src1 ofs1 (len1 - 1)
assert (Array.length dest > end_);
assert (Array.length src0 > end0);
assert (Array.length src1 > end1);
assert (x0 = src0.(end0));
assert (x1 = src1.(end1));
assert (end0 >= beg0);
assert (end1 >= beg1);
(* This is used to optimise the case len1 = 1 below. *)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

cf before (+ missing space?)

assert (dest == src0 && end_ - (end1 - beg1 + 1) = end0);

if cmp x0 x1 <= 0 then begin
dest.(end_) <- x1;
(* If this was the last element of run1 we stop. Besides, since we have
* [dest == src0], the remaining element of run0 are already where they
* are supposed to be and we can exit. *)
if beg1 < end1 then
merge_hi
cmp
dest (end_ - 1)
src0 beg0 end0 x0
src1 beg1 (end1 - 1) src1.(end1 - 1)
end else begin
dest.(ofs + len0 + len1 - 1) <- src0.(ofs0 + len0 - 1);
merge_hi
cmp
dest ofs
src0 ofs0 (len0 - 1)
src1 ofs1 len1
dest.(end_) <- x0;
(* If this was the last element of run0 we stop. There remains to move all
* the elements of run1 at the end of dest. *)
if beg0 < end0 then
merge_hi
cmp
dest (end_ - 1)
src0 beg0 (end0 - 1) src0.(end0 - 1)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We use end0 - 1 twice here, is it worth having an intermediary value? (Same in other branch; same in merge_lo.)

src1 beg1 end1 x1
else
let len1 = end1 - beg1 + 1 in
Array.blit src1 beg1 dest (end_ - len1) len1
end


Expand All @@ -131,15 +154,16 @@ let merge ~buffer cmp t (ofs0, len0) (ofs1, len1) =
merge_lo
cmp
t ofs0
buffer 0 len0
t ofs1 len1
buffer 0 (len0 - 1) buffer.(0)
t ofs1 (ofs1 + len1 - 1) t.(ofs1)
end else begin
Array.blit t ofs1 buffer 0 len1;
let top0 = ofs0 + len0 - 1 in
merge_hi
cmp
t ofs0
t ofs0 len0
buffer 0 len1
t (top0 + len1)
t ofs0 top0 t.(top0)
buffer 0 (len1 - 1) buffer.(len1 - 1)
end;
ofs0, len0 + len1

Expand Down