Sorting algorithms/Radix sort: Difference between revisions
→{{header|AutoHotkey}}
Line 586:
<pre>1 2 3 4 5 6 7 8 9</pre>
=={{header|ATS}}==
<lang ats>(*
Stable integer-keyed radix sorts for unsigned and signed integers
of the various typekinds.
The radix is 256.
*)
(*------------------------------------------------------------------*)
#include "share/atspre_staload.hats"
staload UN = "prelude/SATS/unsafe.sats"
(*------------------------------------------------------------------*)
extern fn {a : vt@ype}
{tk : tkind}
g0uint_radix_sort
{n : int}
(arr : &array (a, n) >> _,
n : size_t n)
:<!wrt> void
extern fn {a : vt@ype}
{tk : tkind}
g0uint_radix_sort$key
{n : int}
{i : nat | i < n}
(arr : &RD(array (a, n)),
i : size_t i)
:<> g0uint tk
(*------------------------------------------------------------------*)
extern fn {a : vt@ype}
{tki, tku : tkind}
g0int_radix_sort
{n : int}
(arr : &array (a, n) >> _,
n : size_t n)
:<!wrt> void
extern fn {a : vt@ype}
{tki : tkind}
g0int_radix_sort$key
{n : int}
{i : nat | i < n}
(arr : &RD(array (a, n)),
i : size_t i)
:<> g0int tki
(*------------------------------------------------------------------*)
(* WARNING: Much of the following code does NOT take into account
the linearity of array entries. But this unsafeness is
hidden from the user. *)
fn {}
bin_sizes_to_indices
(bin_indices : &array (size_t, 256) >> _)
:<!wrt> void =
let
fun
loop {i : int | i <= 256}
{accum : int}
.<256 - i>.
(bin_indices : &array (size_t, 256) >> _,
i : size_t i,
accum : size_t accum)
:<!wrt> void =
if i <> i2sz 256 then
let
prval () = lemma_g1uint_param i
val elem = bin_indices[i]
in
if elem = i2sz 0 then
loop (bin_indices, succ i, accum)
else
begin
bin_indices[i] := accum;
loop (bin_indices, succ i, accum + g1ofg0 elem)
end
end
in
loop (bin_indices, i2sz 0, i2sz 0)
end
fn {a : vt@ype}
{tk : tkind}
count_entries
{n : int}
{shift : nat}
(arr : &RD(array (a, n)),
n : size_t n,
bin_indices : &array (size_t?, 256)
>> array (size_t, 256),
all_expended : &bool? >> bool,
shift : int shift)
:<!wrt> void =
let
fun
loop {i : int | i <= n}
.<n - i>.
(arr : &RD(array (a, n)),
bin_indices : &array (size_t, 256) >> _,
all_expended : &bool >> bool,
i : size_t i)
:<!wrt> void =
if i <> n then
let
prval () = lemma_g1uint_param i
val key : g0uint tk = g0uint_radix_sort$key<a><tk> (arr, i)
val key_shifted = key >> shift
val digit = ($UN.cast{uint} key_shifted) land 255U
val [digit : int] digit = g1ofg0 digit
extern praxi set_range :
() -<prf> [0 <= digit; digit <= 255] void
prval () = set_range ()
val count = bin_indices[digit]
val () = bin_indices[digit] := succ count
in
all_expended := all_expended * iseqz key_shifted;
loop (arr, bin_indices, all_expended, succ i)
end
prval () = lemma_array_param arr
in
array_initize_elt<size_t> (bin_indices, i2sz 256, i2sz 0);
all_expended := true;
loop (arr, bin_indices, all_expended, i2sz 0)
end
fn {a : vt@ype}
{tk : tkind}
sort_by_digit
{n : int}
{shift : nat}
(arr1 : &RD(array (a, n)),
arr2 : &array (a, n) >> _,
n : size_t n,
all_expended : &bool? >> bool,
shift : int shift)
:<!wrt> void =
let
var bin_indices : array (size_t, 256)
in
count_entries<a><tk> (arr1, n, bin_indices, all_expended, shift);
if all_expended then
()
else
let
fun
rearrange {i : int | i <= n}
.<n - i>.
(arr1 : &RD(array (a, n)),
arr2 : &array (a, n) >> _,
bin_indices : &array (size_t, 256) >> _,
i : size_t i)
:<!wrt> void =
if i <> n then
let
prval () = lemma_g1uint_param i
val key = g0uint_radix_sort$key<a><tk> (arr1, i)
val key_shifted = key >> shift
val digit = ($UN.cast{uint} key_shifted) land 255U
val [digit : int] digit = g1ofg0 digit
extern praxi set_range :
() -<prf> [0 <= digit; digit <= 255] void
prval () = set_range ()
val [j : int] j = g1ofg0 bin_indices[digit]
(* One might wish to get rid of this assertion somehow,
to eliminate the branch, should it prove a
problem. *)
val () = $effmask_exn assertloc (j < n)
val p_dst = ptr_add<a> (addr@ arr2, j)
and p_src = ptr_add<a> (addr@ arr1, i)
val _ = $extfcall (ptr, "memcpy", p_dst, p_src,
sizeof<a>)
val () = bin_indices[digit] := succ (g0ofg1 j)
in
rearrange (arr1, arr2, bin_indices, succ i)
end
prval () = lemma_array_param arr1
in
bin_sizes_to_indices<> bin_indices;
rearrange (arr1, arr2, bin_indices, i2sz 0)
end
end
fn {a : vt@ype}
{tk : tkind}
g0uint_sort {n : pos}
(arr1 : &array (a, n) >> _,
arr2 : &array (a, n) >> _,
n : size_t n)
:<!wrt> void =
let
fun
loop {idigit_max, idigit : nat | idigit <= idigit_max}
.<idigit_max - idigit>.
(arr1 : &array (a, n) >> _,
arr2 : &array (a, n) >> _,
from1to2 : bool,
idigit_max : int idigit_max,
idigit : int idigit)
:<!wrt> void =
if idigit = idigit_max then
begin
if ~from1to2 then
let
val _ =
$extfcall (ptr, "memcpy", addr@ arr1, addr@ arr2,
sizeof<a> * n)
in
end
end
else if from1to2 then
let
var all_expended : bool
in
sort_by_digit<a><tk> (arr1, arr2, n, all_expended,
8 * idigit);
if all_expended then
()
else
loop (arr1, arr2, false, idigit_max, succ idigit)
end
else
let
var all_expended : bool
in
sort_by_digit<a><tk> (arr2, arr1, n, all_expended,
8 * idigit);
if all_expended then
let
val _ =
$extfcall (ptr, "memcpy", addr@ arr1, addr@ arr2,
sizeof<a> * n)
in
end
else
loop (arr1, arr2, true, idigit_max, succ idigit)
end
in
loop (arr1, arr2, true, sz2i sizeof<g1uint tk>, 0)
end
#define SIZE_THRESHOLD 256
extern praxi
unsafe_cast_array
{a : vt@ype}
{b : vt@ype}
{n : int}
(arr : &array (b, n) >> array (a, n))
:<prf> void
implement {a} {tk}
g0uint_radix_sort {n} (arr, n) =
if n <> 0 then
let
prval () = lemma_array_param arr
fn
sort {n : pos}
(arr1 : &array (a, n) >> _,
arr2 : &array (a, n) >> _,
n : size_t n)
:<!wrt> void =
g0uint_sort<a><tk> (arr1, arr2, n)
in
if n <= SIZE_THRESHOLD then
let
var arr2 : array (a, SIZE_THRESHOLD)
prval @(pf_left, pf_right) =
array_v_split {a?} {..} {SIZE_THRESHOLD} {n} (view@ arr2)
prval () = view@ arr2 := pf_left
prval () = unsafe_cast_array{a} arr2
val () = sort (arr, arr2, n)
prval () = unsafe_cast_array{a?} arr2
prval () = view@ arr2 :=
array_v_unsplit (view@ arr2, pf_right)
in
end
else
let
val @(pf_arr2, pfgc_arr2 | p_arr2) = array_ptr_alloc<a> n
macdef arr2 = !p_arr2
prval () = unsafe_cast_array{a} arr2
val () = sort (arr, arr2, n)
prval () = unsafe_cast_array{a?} arr2
val () = array_ptr_free (pf_arr2, pfgc_arr2 | p_arr2)
in
end
end
(*------------------------------------------------------------------*)
fn {a : vt@ype}
{tki, tku : tkind}
g0int_sort {n : int}
(arr : &array (a, n) >> _,
n : size_t n)
:<!wrt> void =
let
macdef get_key = g0int_radix_sort$key<a><tki>
prval () = lemma_array_param arr
in
if n = 0 then
()
else
let
val () = $effmask_exn
assertloc (sizeof<g0int tki> = sizeof<g0uint tku>)
fn
find_least_key (arr : &RD(array (a, n)))
:<> g0int tki =
let
fun
loop {i : int | i <= n}
.<n - i>.
(arr : &RD(array (a, n)),
least_key : g0int tki,
i : size_t i)
:<> g0int tki =
if i <> n then
let
prval () = lemma_g1uint_param i
val key = get_key (arr, i)
in
loop (arr, min (least_key, key), succ i)
end
else
least_key
in
if n = 0 then
get_key (arr, i2sz 0)
else
let
val first_key = get_key (arr, i2sz 0)
in
loop (arr, first_key, i2sz 1)
end
end
val least_key = find_least_key arr
(* The offset is the two's complement of the least key. Thus the
least key is mapped to zero and the order of keys is
preserved. *)
val offset = succ (lnot ($UN.cast{g1uint tku} least_key))
implement
g0uint_radix_sort$key<a><tku> (arr, i) =
let
val keyi = get_key (arr, i)
in
g0i2u keyi + offset
end
in
g0uint_radix_sort<a><tku> (arr, n)
end
end
implement {a} {tki, tku}
g0int_radix_sort (arr, n) =
g0int_sort<a><tki, tku> (arr, n)
(*------------------------------------------------------------------*)
implement
main0 () =
let
implement
g0int_radix_sort$key<int><intknd> (arr, i) =
arr[i]
var arr : array (int, 10)
val () =
array_initize_list<int>
(arr, 10, $list (1, 2, 1, ~2, 330, 5000, 16, ~20000, 1, 2))
val () = g0int_radix_sort<int><intknd, uintknd> (arr, i2sz 10)
val () = println! (list_vt2t (array2list (arr, i2sz 10)))
in
end
(*------------------------------------------------------------------*)</lang>
{{out}}
<pre>$ patscc -O3 -DATS_MEMALLOC_LIBC radix_sort_task.dats && ./a.out
-20000, -2, 1, 1, 1, 2, 2, 16, 330, 5000</pre>
=={{header|AutoHotkey}}==
| |||