msort.timl

(* List based merge sort *)

structure MSort = struct

open Basic
open List

(* evenly split *)
absidx T_split: BigO _ (* (fn n => $n) *) = _ with
fun split ['a] {n: Nat} (xs: list 'a {n}) return list 'a {ceil ($n/2)} * list 'a {floor ($n/2)} using T_split n =
    case xs of
        [] => ([], [])
      | [x] => (xs, [])
      | x1 :: x2 :: xs =>
        let val (xs1, xs2) = split xs in
        (x1 :: xs1, x2 :: xs2) end
end

absidx T_merge: BigO (fn m n => $m * $n) = _ with
fun merge ['a] {m n1 n2: Nat} (le: 'a*'a --$m--> bool) (xs: list 'a {n1}, ys: list 'a {n2}) return list 'a {n1 + n2} using T_merge m (n1 + n2) =
    case (xs, ys) of
        ([], _) => ys
      | (_, []) => xs
      | (x :: xs', y :: ys') =>
        if le (x, y) then x :: merge le (xs', ys)
        else y :: merge le (xs, ys')
end

absidx {T_msort | T_msort <== (fn m n => $m * $n * log2 $n)} with
fun msort ['a] {m : Nat} {n : Nat} (le : 'a * 'a -- $m --> bool) (xs : list 'a {n}) return list 'a {n} using T_msort m n =
    case xs of
        Nil => xs
      | (Cons (_, Nil)) => xs
      | (Cons (_, Cons (_, _))) =>
        case split xs of
            (xs1, xs2) => merge le (msort le xs1, msort le xs2)
end

(* the same, but use module-scoped abstract index to hide T_msort *)
absidx T_msort: BigO (fn m n => $m*$n*log2 $n) = _
fun msort ['a] {m n: Nat} (le: 'a*'a --$m--> bool) (xs: list 'a {n}) return list 'a {n} using T_msort m n =
    case xs of
        [] => xs
      | [_] => xs
      | _ :: _ :: _ =>
        let val (xs1, xs2) = split xs in
          merge le (msort le xs1, msort le xs2) end
          
end