(* The Rosetta Code lexicographic sort task. *)

#include "share/atspre_staload.hats"
staload UN = "prelude/SATS/unsafe.sats"

#define NIL list_nil ()
#define ::  list_cons

fn
uint_to_digit (n : uint)
    : char =
  int2char0 (g0u2i n + char2int0 '0')

fn
int_to_string {n : nat}
              (n : int n)
    : string =
  if iseqz n then
    "0"
  else
    let
      fun
      loop {i : nat | i <= 20}
           .<i>.
           (buf : &array (char, 21),
            i   : int i,
            n   : uint)
          : [j : nat | j <= 20]
            int j =
        if (i = 0) + (iseqz n) then
          i
        else
          let
            val i1 = pred i
          in
            buf[i1] := uint_to_digit (n mod 10u);
            loop (buf, i1, n / 10u)
          end

      var buf = @[char][21] ('\0')
      val j = loop (buf, 20, g0i2u n)
      val p = ptr_add<char> (addr@ buf, j)
    in
      strptr2string (string0_copy ($UN.cast{string} p))
    end

fn
iota1 {n : pos}
      (n : int n)
    : list ([i : pos | i <= n] int i, n) =
  let
    typedef t = [i : pos | i <= n] int i

    fun
    loop {i : nat | i <= n}
         .<i>.
         (i     : int i,
          accum : list (t, n - i))
        : list (t, n) =
      if i = 0 then
        accum
      else
        loop (pred i, i :: accum)
  in
    loop (n, NIL)
  end

fn
reverse_map_numbers_to_strings
          {n    : int}
          (nums : list ([i : nat] int i, n))
    : list (string, n) =
  let
    typedef t = [i : nat] int i

    fun
    loop {i : nat | i <= n}
         .<n - i>.
         (nums  : list (t, n - i),
          accum : list (string, i))
        : list (string, n) =
      case+ nums of
      | NIL => accum
      | head :: tail =>
        loop {i + 1} (tail, int_to_string head :: accum)

    prval () = lemma_list_param nums
  in
    loop {0} (nums, NIL)
  end

fn
reverse_map_strings_to_numbers
          {n       : int}
          (strings : list (string, n))
    : list (int, n) =
  let
    macdef string_to_int (s) =
      $extfcall (int, "atoi", ,(s))

    fun
    loop {i : nat | i <= n}
         .<n - i>.
         (strings : list (string, n - i),
          accum   : list (int, i))
        : list (int, n) =
      case+ strings of
      | NIL => accum
      | head :: tail =>
        loop {i + 1} (tail, string_to_int head :: accum)

    prval () = lemma_list_param strings
  in
    loop {0} (strings, NIL)
  end

fn
lexicographic_iota1
          {n : pos}
          (n : int n)
    : list (int, n) =
  let
    val numstrings =
      reverse_map_numbers_to_strings (iota1 n)

    (* One could use a MSB-first radix sort here, but I will use what
       is readily available. *)
    implement
    list_mergesort$cmp<string> (x, y) =
      ~compare (x, y)
  in
    reverse_map_strings_to_numbers
      (list_vt2t (list_mergesort<string> numstrings))
  end

implement
main0 () =
  begin
    println! (lexicographic_iota1 13);
    println! (lexicographic_iota1 100)
  end