Lab Session 5

Quick Sort

Algorithm

Quicksort is an efficient sorting algorithm, serving as a systematic method for placing the elements of an array in order.

In efficient implementations it is not a stable sort, meaning that the relative order of equal sort items is not preserved. Quicksort can operate in-place on an array, requiring small additional amounts of memory to perform the sorting.

Mathematical analysis of quicksort shows that, on average, the algorithm takes \(O(n log n)\) comparisons to sort \(n\) items. In the worst case, it makes \(O(n^2)\) comparisons, though this behavior is rare.

Bullet Points

  • Form up a metric which gets decreased each time invoking a function recursively.
  • Assignment formal meaning to function parameters.
  • Form up invariant that is valid in the beginning and end of a recursive function.

Code

Makefile

The file quicksort.dats is an implementation for array of integers.

#define
ATS_PACKNAME "LAB_QUICKSORT"

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

#include "share/HATS/atspre_staload_libats_ML.hats"


// return value ret: new position for the pivot
// ret < enda
extern fun array0_partition (
  arr: array0 int, beg: size_t, enda: size_t): size_t

extern fun array0_quicksort (arr: array0 int): void

implement array0_quicksort (arr) = let
  val sz = arr.size ()

  fun array0_quicksort_size (
    arr: array0 int, 
    beg: size_t,
    enda: size_t
    ): void =
    if enda <= beg then () else let
      // val () = fprint! (stdout_ref, "arr = ")
      // val () = fprint_array0 (stdout_ref,arr)
      // val () = fprintln! (stdout_ref)
      val mid = array0_partition (arr, beg, enda)
      // val () = println! ("array0_quicksort_size, mid is ", mid)
    in
      let
        val () = array0_quicksort_size (arr, beg, mid)
        val () = array0_quicksort_size (arr, succ mid, enda)
      in end
    end
in
  array0_quicksort_size (arr, i2sz 0, sz)
end

implement array0_partition (arr, beg, enda) = let
  // val () = println! ("array0_partition start ",
  //                    " beg is ", beg,
  //                    " enda is ", enda)

  val pivot = arr[enda - i2sz(1)]

  // return value ret: new position for the pivot
  // ret < enda
  // elements in [beg, div) are less than p
  // elements in [div, cur) are no less than p
  fun loop (arr: array0 int,
            beg: size_t,
            div: size_t,
            cur: size_t,
            enda: size_t,
            p: int
            ): size_t = 
  let
    // val () = println! ("loop: beg is ", beg,
    //                    " div is ", div,
    //                    " cur is ", cur,
    //                    " enda is ", enda,
    //                    " pivot is ", p)
  in
    // put pivot at the appropriate position
    if cur = pred (enda) then let
      val v = arr[cur]
      val () = arr[cur] := arr[div]
      val () = arr[div] := v
    in
      div
    end
    else let
      val v = arr[cur]
    in
      if v < p then // swap elements arr[div] and arr[cur]
        if cur = div then loop (arr, beg, succ (div), succ (cur), enda, p)
        else let
          val () = arr[cur] := arr[div]
          val () = arr[div] := v
        in
          loop (arr, beg, succ (div), succ (cur), enda, p)
        end
      else  // div is unchanged
        loop (arr, beg, div, succ (cur), enda, p)
    end
  end  // end of [fun loop]
  val ret = loop (arr, beg, beg, beg, enda, pivot)

  // val () = println! ("array0_partition end, div is ", ret)
in
  ret  // end of array0_partition
end

implement main0 () = let

  // create an array0 in an easy way
  val xs = $arrpsz{int} (2, 9, 8, 4, 5, 3, 1, 7, 6, 0): arrpsz(int, 10) (* end of [val] *)
  val xs = array0 (xs): array0 int

  val () = fprint! (stdout_ref, "xs(*input*)  = ")
  val () = fprint_array0 (stdout_ref, xs)
  val () = fprintln! (stdout_ref)

  val () = array0_quicksort (xs)

  val () = fprint! (stdout_ref, "xs(*output*)  = ")
  val () = fprint_array0 (stdout_ref, xs)
  val () = fprintln! (stdout_ref)

in
end

The file quicksort_generic.dats is a generic implementation based on the template system of ATS. This implementation is derived on the previous implementation with tiny modification (e.g. using gcompare_val_val instead of < for comparison.

#define
ATS_PACKNAME "LAB_QUICKSORT"

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

#include "share/HATS/atspre_staload_libats_ML.hats"


// return value ret: new position for the pivot
// ret < enda
extern fun {a:t@ype} array0_partition (
  arr: array0 a, beg: size_t, enda: size_t): size_t

extern fun {a:t@ype} array0_quicksort (arr: array0 a): void

implement {a} array0_quicksort (arr) = let
  val sz = arr.size ()

  fun {a:t@ype} array0_quicksort_size (
    arr: array0 a, 
    beg: size_t,
    enda: size_t
    ): void =
    if enda <= beg then () else let
      val mid = array0_partition (arr, beg, enda)
    in
      let
        val () = array0_quicksort_size (arr, beg, mid)
        val () = array0_quicksort_size (arr, succ mid, enda)
      in end
    end
in
  array0_quicksort_size (arr, i2sz 0, sz)
end

implement {a} array0_partition (arr, beg, enda) = let
  val pivot = arr[enda - i2sz(1)]

  // return value ret: new position for the pivot
  // ret < enda
  // elements in [beg, div) are less than p
  // elements in [div, cur) are no less than p
  fun loop (arr: array0 a,
            beg: size_t,
            div: size_t,
            cur: size_t,
            enda: size_t,
            p: a
            ): size_t = 
  if cur = pred (enda) then let
    val v = arr[cur]
    val () = arr[cur] := arr[div]
    val () = arr[div] := v
  in
    div
  end
  else let
    val v = arr[cur]
    val sgn = gcompare_val_val (v, p)  // generic comparison function
  in
    if sgn < 0 then // swap elements arr[div] and arr[cur]
      if cur = div then loop (arr, beg, succ (div), succ (cur), enda, p)
      else let
        val () = arr[cur] := arr[div]
        val () = arr[div] := v
      in
        loop (arr, beg, succ (div), succ (cur), enda, p)
      end
    else  // div is unchanged
      loop (arr, beg, div, succ (cur), enda, p)
  end  // end of [fun loop]
  val ret = loop (arr, beg, beg, beg, enda, pivot)

in
  ret  // end of array0_partition
end

implement main0 () = let

  typedef T = int
  // create an array0 in an easy way
  val xs = $arrpsz{T} (2, 9, 8, 4, 5, 3, 1, 7, 6, 0) (* end of [val] *)
  val xs = array0 (xs)

  val () = fprint! (stdout_ref, "xs(*input*)  = ")
  val () = fprint_array0 (stdout_ref, xs)
  val () = fprintln! (stdout_ref)

  // override the default implementation for gcompare_val_val for int
  implement gcompare_val_val<int> (x1, x2) = ~(x1 - x2)

  val () = array0_quicksort<int> (xs)

  val () = fprint! (stdout_ref, "xs(*output*)  = ")
  val () = fprint_array0 (stdout_ref, xs)
  val () = fprintln! (stdout_ref)

in
end