array-msort-inplace.timl

(* Array-based merge sort (in-place) *)

structure ArrayMSortInplace = struct

open Basic
open Nat
open Array

datatype natnum : {Nat} =
         NumO of natnum {0}
       | NumS {n' : Nat} of nat {n'} * natnum {n'} --> natnum {n' + 1}

absidx T_nat_2_natnum : BigO (fn n => $n) = fn n => 11.0 * $n + 8.0 with
fun nat_2_natnum {n : Nat} (n : nat {n}) return natnum {n} using T_nat_2_natnum n =
    case le (n, #0) return using (T_nat_2_natnum n) - 8.0 of
        Le => NumO
      | @Gt {m} {_} {pf} =>
        let
          val n' = @nat_minus {m} {1} {pf} (n, #1)
        in
          NumS (n', nat_2_natnum n')
        end
end

fun swap ['a] {len i j : Nat} {i < len} {j < len} (a : array 'a {len}, i : nat {i}, j : nat {j}) =
    let
      val tmp = sub (a, i)
      val () = update (a, i, sub (a, j))
      val () = update (a, j, tmp)
    in
      ()
    end

absidx T_array_imerge_helper : BigO (fn m n => $m * $n) with
fun array_imerge_helper ['a] {t len i m j n w s : Nat} {i + m <= len} {j + n <= len} {w + m + n <= len} {s = m + n} (le : 'a * 'a -- $t --> bool) (a : array 'a {len}, i : nat {i}, m : natnum {m}, j : nat {j}, n : natnum {n}, w : nat {w}, s : natnum {s}) return unit using T_array_imerge_helper t s =
    case m of
        NumO =>
        (case n of
             NumO =>
             (case s of
                  NumO => ()
                | NumS _ => never)
           | NumS (vn, n') =>
             (case s of
                  NumO => never
                | NumS (vs, s') =>
                  let
                    val from = nat_plus (j, vn)
                    val to = nat_plus (w, vs)
                    val () = swap (a, from, to)
                  in
                    array_imerge_helper le (a, i, m, j, n', w, s')
                  end))
      | NumS (vm, m') =>
        (case n of
             NumO =>
             (case s of
                  NumO => never
                | NumS (vs, s') =>
                  let
                    val from = nat_plus (i, vm)
                    val to = nat_plus (w, vs)
                    val () = swap (a, from, to)
                  in
                    array_imerge_helper le (a, i, m', j, n, w, s')
                  end)
           | NumS (vn, n') =>
             (case s of
                  NumO => never
                | NumS (vs, s') =>
                  let
                    val from1 = nat_plus (i, vm)
                    val from2 = nat_plus (j, vn)
                    val ele1 = sub (a, from1)
                    val ele2 = sub (a, from2)
                    val to = nat_plus (w, vs)
                  in
                    if le (ele1, ele2) then
                      let
                        val () = swap (a, from2, to)
                      in
                        array_imerge_helper le (a, i, m, j, n', w, s')
                      end
                    else
                      let
                        val () = swap (a, from1, to)
                      in
                        array_imerge_helper le (a, i, m', j, n, w, s')
                      end
                  end))
end

fun array_imerge ['a] {t len i m j n w : Nat} {i + m <= len} {j + n <= len} {w + m + n <= len} (le : 'a * 'a -- $t --> bool) (a : array 'a {len}, i : nat {i}, m : nat {m}, j : nat {j}, n : nat {n}, w : nat {w}) =
    array_imerge_helper le (a, i, nat_2_natnum m, j, nat_2_natnum n, w, nat_2_natnum (nat_plus (m, n)))

absidx T_array_insert : BigO (fn m n => $m * $n) with
fun array_insert ['a] {m len w p : Nat} {w + p < len} (le : 'a * 'a -- $m --> bool) (a : array 'a {len}, w : nat {w}, p : natnum {p}) return unit using T_array_insert m p =
    case p of
        NumO => ()
      | NumS (vp, p') =>
        if le (sub (a, nat_plus (w, vp)), sub (a, nat_plus (nat_plus (w, vp), #1))) then
          ()
        else
          let
            val () = swap (a, nat_plus (w, vp), (nat_plus (nat_plus (w, vp), #1)))
          in
            array_insert le (a, w, p')
          end
end

absidx T_array_imsort_on_range : BigO (* (fn m n => $m * $n * log2 $n) *) (fn m n => $m * $n * $n) with
fun array_imsort_on_range ['a] {m len w left right : Nat} {right > 0} {w + left + right <= len} (le : 'a * 'a -- $m --> bool) (a : array 'a {len}, w : nat {w}, left : nat {left}, right : nat {right}) return unit (* using 1.0 + 7.0 + T_array_imsort_on_range m (left + right)  *)=
    case Nat.le (right, #1) return using T_array_imsort_on_range m (left + right) of
        Le => array_insert le (a, w, nat_2_natnum left)
      | Gt =>
        let
          val half = ceil_half right
          val rest : nat {floor ($right/2)} = nat_minus (right, half)
          val m = nat_plus (nat_plus (w, left), half)
          val () = array_imsort_on_range le (a, m, #0, rest)
          val () = array_imerge le (a, w, left, m, rest, w)
          val () = array_imsort_on_range le (a, w, nat_plus (left, rest), half)
        in
          ()
        end
end

fun array_imsort ['a] {m len : Nat} (le : 'a * 'a -- $m --> bool) (a : array 'a {len}) =
    case Nat.le (length a, #0) of
        Le => ()
      | Gt => array_imsort_on_range le (a, #0, #0, length a)

end