Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Binary insertion sort #3

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
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
72 changes: 72 additions & 0 deletions src/lib/array/insertionSort.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,72 @@
(** Binary insertion sort *)

type 'a cmp = 'a -> 'a -> int


(** Search where to insert x in the sorted slice t[lo: hi + 1].
Performs O(log(hi - lo)) comparisons. *)
let rec binary_search cmp t x lo hi =
(* assert a[lo: hi + 1] is sorted *)
assert (0 <= lo);
assert (lo <= hi + 1); (* lo should generally be <= hi except eventually in
the last recursive call where hi might be equal to
lo - 1. In this case lo is "correct" and hi is "out
of bounds" and must be replaced by hi + 1. *)
assert (hi < Array.length t);
(* ensures: (forall i < result. cmp a.(i) x <= 0)
/\ (forall i >= result. cmp a.(i) x > 0) *)

let mid = lo + (hi - lo) / 2 in
assert (lo >= hi || mid < hi);

let mid_le_x = cmp t.(mid) x <= 0 in

if lo >= hi then
if mid_le_x then lo + 1 else lo
(* Or the "branching-free": *)
(* lo + (Obj.magic mid_le_x: int) *)
else if mid_le_x then
binary_search cmp t x (mid + 1) hi
else
binary_search cmp t x lo (mid - 1)


(** Sort the slice t[lo: hi + 1] assuming that t[lo: i] is already sorted. *)
let rec sort_from_i cmp t lo hi i =
(* variant: hi - i *)
assert (0 <= lo);
assert (lo < i);
assert (i <= hi + 1);
assert (hi < Array.length t);
(* assert t[lo: i] is sorted *)
(* ensures t[lo: hi + 1] is sorted *)
if i > hi then ()
else begin
let x = t.(i) in
let pos = binary_search cmp t x lo (i - 1) in
for j = i downto pos + 1 do
t.(j) <- t.(j - 1)
done;
t.(pos) <- x;
sort_from_i cmp t lo hi (i + 1)
end

let%test _ =
let t = [|9; 1; 4; 5; 3; 2; 0|] in
let i = 4 in
sort_from_i Int.compare t 1 5 i;
t = [|9; 1; 2; 3; 4; 5; 0|]


(** Sort the slice t[lo: hi + 1]. *)
let sort cmp t lo hi = sort_from_i cmp t lo hi (lo + 1)

let%test _ =
let t = [|4; 2; 6; 3|] in
sort Int.compare t 0 3;
t = [|2; 3; 4; 6|]

let%test _ =
let t = [|9; 4; 8; 2; 1; 0|] in
sort Int.compare t 1 4;
t = [|9; 1; 2; 4; 8; 0|]
2 changes: 1 addition & 1 deletion tests/array/dune
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
(tests
(names timsort)
(names timsort insertionSort)
(libraries sorting_array genlib))
19 changes: 19 additions & 0 deletions tests/array/insertionSort.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
open Sorting_array
open Genlib

let rec test gen ~nb ~len =
if nb <= 0 then ()
else begin
let t = gen len in
let t' = Array.copy t in
Array.stable_sort Int.compare t';
InsertionSort.sort Int.compare t 0 (len - 1);
assert (t = t');
test gen ~nb:(nb - 1) ~len
end

let () =
let nb = 100 in
let len = 1000 in
test Genarray.gen_unif ~nb ~len;
test (Genarray.gen_k_runs 5) ~nb ~len