diff --git a/src/lib/array/insertionSort.ml b/src/lib/array/insertionSort.ml new file mode 100644 index 0000000..49ecd38 --- /dev/null +++ b/src/lib/array/insertionSort.ml @@ -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|] diff --git a/tests/array/dune b/tests/array/dune index d84df11..13c9d7a 100644 --- a/tests/array/dune +++ b/tests/array/dune @@ -1,3 +1,3 @@ (tests - (names timsort) + (names timsort insertionSort) (libraries sorting_array genlib)) diff --git a/tests/array/insertionSort.ml b/tests/array/insertionSort.ml new file mode 100644 index 0000000..3be42e7 --- /dev/null +++ b/tests/array/insertionSort.ml @@ -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