141 lines
2.9 KiB
Text
141 lines
2.9 KiB
Text
(* 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
|