Merge Sort

(* merge: int list * int list -> int list
  REQUIRES: A and B are sorted
  ENSURES: merge(A,B) is a sorted permutation of A@B
*)
fun merge([] : int list, B : int list) : int list = B
  | merge(A, []) = A
  | merge(x::xs, y::ys) =
    case Int.compare(x, y) of
      LESS => x::merge(xs, y::ys)
    | GREATER => y::merge(x::xs, ys)
    | EQUAL => x::y::merge(xs, ys)

(* split : int list -> int list * int list
  REQUIRES: true
  ENSURES: split L returns (A,B) such that A@B is a permutation of L & |length A - length B | <= 1
*)
fun split([] : int list) : int list * int list = ([], [])
  | split([x]) = ([x], [])
  | split(x::y::xs) =
    let
      val (A : int list, B : int list) = split xs
    in
      (x::A, y::B)
    end

(* msort : int list -> int list
  REQUIRES: true
  ENSURES: msort L returns a sorted permutation of L
*)
fun msort([]: int list) : int list = []
  | msort([x]) = [x]
  | msort L =
    let
      val (A,B) : int list * int list = split L
    in
      merge(msort A, msort B)
    end