A modular implementation of mergesort (the complexity is O(n.log n) in the length of the list)

Notations and conventions

We implement mergesort using an explicit stack of pending mergings. Pending merging are represented like a binary number where digits are either None (denoting 0) or Some list to merge (denoting 1). The n-th digit represents the pending list to be merged at level n, if any. Merging a list to a stack is like adding 1 to the binary number represented by the stack but the carry is propagated by merging the lists. In practice, when used in mergesort, the n-th digit, if non 0, carries a list of length 2^n. For instance, adding singleton list 3 to the stack Some 4::Some 2;6::None::Some 1;3;5;5 reduces to propagate the carry 3;4 (resulting of the merge of 3 and 4) to the list Some 2;6::None::Some 1;3;5;5, which reduces to propagating the carry 2;3;4;6 (resulting of the merge of 3;4 and 2;6) to the list None::Some 1;3;5;5, which locally produces Some 2;3;4;6::Some 1;3;5;5, i.e. which produces the final result None::None::Some 2;3;4;6::Some 1;3;5;5. For instance, here is how 6;2;3;1;5 is sorted:

       operation             stack                list
       iter_merge            []                   [6;2;3;1;5]
    =  append_list_to_stack  [ + [6]]             [2;3;1;5]
    → iter_merge            [[6]]                [2;3;1;5]
    =  append_list_to_stack  [[6] + [2]]          [3;1;5]
    =  append_list_to_stack  [ + [2;6];]          [3;1;5]
    → iter_merge            [[2;6];]             [3;1;5]
    =  append_list_to_stack  [[2;6]; + [3]]       [1;5]
    → merge_list            [[2;6];[3]]          [1;5]
    =  append_list_to_stack  [[2;6];[3] + [1]     [5]
    =  append_list_to_stack  [[2;6] + [1;3];]     [5]
    =  append_list_to_stack  [ + [1;2;3;6];;]     [5]
    → merge_list            [[1;2;3;6];;]        [5]
    =  append_list_to_stack  [[1;2;3;6];; + [5]]  []
    → merge_stack           [[1;2;3;6];;[5]]
    =                                             [1;2;3;5;6]

The complexity of the algorithm is n*log n, since there are 2^(p-1) mergings to do of length 2, 2^(p-2) of length 4, ..., 2^0 of length 2^p for a list of length 2^p. The algorithm does not need explicitly cutting the list in 2 parts at each step since it the successive accumulation of fragments on the stack which ensures that lists are merged on a dichotomic basis.

The proof of correctness