Source code in the ats programming language

(*------------------------------------------------------------------*)
(* Mergesort in ATS2, for linear lists.                             *)
(*------------------------------------------------------------------*)

#include "share/atspre_staload.hats"

staload UN = "prelude/SATS/unsafe.sats"

#define NIL list_vt_nil ()
#define ::  list_vt_cons

(*------------------------------------------------------------------*)

(* Destructive stable merge. *)
extern fun {a : vt@ype}
list_vt_merge {m, n : int}
              (lst1 : list_vt (a, m),
               lst2 : list_vt (a, n))
    : list_vt (a, m + n)

(* Order predicate for list_vt_merge. You have to implement this to
   suit your needs. *)
extern fun {a : vt@ype}
list_vt_merge$lt : (&a, &a) -<> bool

(* Destructive stable mergesort. *)
extern fun {a : vt@ype}
list_vt_mergesort {n   : int}
                  (lst : list_vt (a, n))
    : list_vt (a, n)

(* Order predicate for list_vt_mergesort. You have to implement this
   to suit your needs. *)
extern fun {a : vt@ype}
list_vt_mergesort$lt : (&a, &a) -<> bool

(*------------------------------------------------------------------*)

implement {a}
list_vt_merge {m, n} (lst1, lst2) =
  let
    macdef lt = list_vt_merge$lt

    fun
    loop {m, n       : nat} ..
         (lst1       : list_vt (a, m),
          lst2       : list_vt (a, n),
          lst_merged : &List_vt a? >> list_vt (a, m + n))
        : void =
      case+ lst1 of
      | ~ NIL => lst_merged := lst2
      | @ elem1 :: tail1 =>
        begin
          case+ lst2 of
          | ~ NIL =>
            let
              prval () = fold@ lst1
            in
              lst_merged := lst1
            end
          | @ elem2 :: tail2 =>
            if ~(elem2 \lt elem1) then
              let
                val () = lst_merged := lst1
                prval () = fold@ lst2
                val () = loop (tail1, lst2, tail1)
                prval () = fold@ lst_merged
              in
              end
            else
              let
                val () = lst_merged := lst2
                prval () = fold@ lst1
                val () = loop (lst1, tail2, tail2)
                prval () = fold@ lst_merged
              in
              end
        end

    prval () = lemma_list_vt_param lst1 (* Proves 0 <= m. *)
    prval () = lemma_list_vt_param lst2 (* Proves 0 <= n. *)
    prval () = prop_verify {0 <= m} ()
    prval () = prop_verify {0 <= n} ()

    var lst_merged : List_vt a?
    val () = loop {m, n} (lst1, lst2, lst_merged)
  in
    lst_merged
  end

(*------------------------------------------------------------------*)

implement {a}
list_vt_mergesort {n} lst =
  let
    implement
    list_vt_merge$lt (x, y) =
      list_vt_mergesort$lt (x, y)

    (* You can make SMALL larger than 1 and write small_sort as a fast
       stable sort for small lists. *)
    #define SMALL 1
    fn
    small_sort {m   : pos | m <= SMALL}
               (lst : list_vt (a, m),
                m   : int m)
        : list_vt (a, m) =
      lst

    fun
    recurs {m   : pos} ..
           (lst : list_vt (a, m),
            m   : int m)
        : list_vt (a, m) =
      if m <= SMALL then
        small_sort (lst, m)
      else
        let
          prval () = prop_verify {2 <= m} ()
          val i = m / 2
          val @(lst1, lst2) = list_vt_split_at (lst, i)
          val lst1 = recurs (lst1, i)
          val lst2 = recurs (lst2, m - i)
        in
          list_vt_merge (lst1, lst2)
        end

    prval () = lemma_list_vt_param lst (* Proves 0 <= n. *)
    prval () = prop_verify {0 <= n} ()
  in
    case+ lst of
    | NIL => lst
    | _ :: _ => recurs (lst, length lst)
  end

(*------------------------------------------------------------------*)

extern fun
list_vt_mergesort_int {n   : int}
                      (lst : list_vt (int, n))
    : list_vt (int, n)

implement
list_vt_mergesort_int {n} lst =
  let
    implement
    list_vt_mergesort$lt (x, y) =
      x < y
  in
    list_vt_mergesort {n} lst
  end

implement
main0 () =
  let
    val lst = $list_vt (22, 15, 98, 82, 22, 4, 58, 70, 80, 38, 49,
                        48, 46, 54, 93, 8, 54, 2, 72, 84, 86, 76,
                        53, 37, 90)
    val () = println! ("before : ", $UN.castvwtp1{List int} lst)
    val lst = list_vt_mergesort_int lst
    val () = println! ("after  : ", $UN.castvwtp1{List int} lst)
  in
    list_vt_free lst
  end

(*------------------------------------------------------------------*)

//--------------------------------------------------------------------
//
//  A mergesort for 32-bit signed integers.
//
//--------------------------------------------------------------------

#include "share/atspre_staload.hats"

(*------------------------------------------------------------------*)

#define ENTIER_MAX 2147483647

(* We do not include the most negative two's-complement number. *)
stadef entier (i : int) = ~ENTIER_MAX <= i && i <= ENTIER_MAX
sortdef entier          = {i : int | entier i}

typedef entier (i : int) = [entier i] int i
typedef entier           = [i : entier] entier i

datatype sorted_entier_list (int, int) =
| sorted_entier_list_nil (0, ENTIER_MAX)
| {n : nat}
  {i, j : entier | ~(j < i)}
  sorted_entier_list_cons (n + 1, i) of
    (entier i, sorted_entier_list (n, j))
typedef sorted_entier_list (n : int) =
  [i : entier] sorted_entier_list (n, i)
typedef sorted_entier_list =
  [n : int] sorted_entier_list n

infixr ( :: ) :::
#define NIL  list_nil ()
#define ::   list_cons
#define SNIL sorted_entier_list_nil ()
#define :::  sorted_entier_list_cons

(*------------------------------------------------------------------*)

extern prfn
lemma_sorted_entier_list_param
          {n   : int}
          (lst : sorted_entier_list n)
    : [0 <= n] void

extern fn
sorted_entier_list_length
          {n   : int}
          (lst : sorted_entier_list n)
    :<> [0 <= n] int n

extern fn
sorted_entier_list_merge
          {m, n : int}
          {i, j : entier}
          (lst1 : sorted_entier_list (m, i),
           lst2 : sorted_entier_list (n, j))
    :<> sorted_entier_list (m + n, min (i, j))

extern fn
entier_list_mergesort
          {n   : int}
          (lst : list (entier, n)) (* An ordinary list. *)
    : sorted_entier_list n

extern fn
sorted_entier_list2list
          {n   : int}
          (lst : sorted_entier_list n)
    :<> list (entier, n)

overload length with sorted_entier_list_length
overload merge with sorted_entier_list_merge
overload mergesort with entier_list_mergesort
overload to_list with sorted_entier_list2list

(*------------------------------------------------------------------*)

primplement
lemma_sorted_entier_list_param {n} lst =
  case+ lst of
  | SNIL => ()
  | _ ::: _ => ()

implement
sorted_entier_list_length {n} lst =
  (* This implementation is tail-recursive. *)
  let
    fun
    count {m   : nat | m <= n} ..
          (lst : sorted_entier_list (n - m),
           m   : int m)
        :<> [0 <= n] int n =
      case+ lst of
      | SNIL => m
      | _ ::: tail => count {m + 1} (tail, succ m)

    prval () = lemma_sorted_entier_list_param lst
  in
    count (lst, 0)
  end

implement
sorted_entier_list_merge (lst1, lst2) =
  (* This implementation is *NOT* tail recursive. It will use O(m+n)
     stack space. *)
  let
    fun
    recurs {m, n : nat}
           {i, j : entier} ..
           (lst1 : sorted_entier_list (m, i),
            lst2 : sorted_entier_list (n, j))
        :<> sorted_entier_list (m + n, min (i, j)) =
      case+ lst1 of
      | SNIL => lst2
      | i ::: tail1 =>
        begin
          case+ lst2 of
          | SNIL => lst1
          | j ::: tail2 =>
            if ~(j < i) then
              i ::: recurs (tail1, lst2)
            else
              j ::: recurs (lst1, tail2)
        end

    prval () = lemma_sorted_entier_list_param lst1
    prval () = lemma_sorted_entier_list_param lst2
  in
    recurs (lst1, lst2)
  end

implement
entier_list_mergesort lst =
  let
    fun
    recurs {m   : nat} ..
           (lst : list (entier, m),
            m   : int m)
        : sorted_entier_list m =
      if m = 1 then
        let
          val+ head :: NIL = lst
        in
          head ::: SNIL
        end
      else if m = 0 then
        SNIL
      else
        let
          val m_left = m \g1int_ndiv 2
          val m_right = m - m_left
          val @(left, right) = list_split_at (lst, m_left)
          val left = recurs (list_vt2t left, m_left)
          and right = recurs (right, m_right)
        in
          left \merge right
        end

    prval () = lemma_list_param lst
  in
    recurs (lst, length lst)
  end

implement
sorted_entier_list2list lst =
  (* This implementation is *NOT* tail recursive. It will use O(n)
     stack space. *)
  let
    fun
    recurs {n   : nat} ..
           (lst : sorted_entier_list n)
        :<> list (entier, n) =
      case+ lst of
      | SNIL => NIL
      | head ::: tail => head :: recurs tail

    prval () = lemma_sorted_entier_list_param lst
  in
    recurs lst
  end

(*------------------------------------------------------------------*)

fn
print_Int_list
          {n   : int}
          (lst : list (Int, n))
    : void =
  let
    fun
    loop {n   : nat} ..
         (lst : list (Int, n))
        : void =
      case+ lst of
      | NIL => ()
      | head :: tail =>
        begin
          print! (" ");
          print! (head);
          loop tail
        end
    prval () = lemma_list_param lst
  in
    loop lst
  end

implement
main0 () =
  let
    val example_list =
      $list (22, 15, 98, 82, 22, 4, 58, 70, 80, 38, 49, 48, 46, 54,
             93, 8, 54, 2, 72, 84, 86, 76, 53, 37, 90)
    val sorted_list = mergesort example_list
  in
    print! ("unsorted  ");
    print_Int_list example_list;
    println! ();
    print! ("sorted    ");
    print_Int_list (to_list sorted_list);
    println! ()
  end

(*------------------------------------------------------------------*)