Sorting algorithms/Patience sort: Difference between revisions
Content deleted Content added
Line 1,122:
.include "../affichage.inc"
</lang>
=={{header|ATS}}==
===A patience sort for non-linear lists of integers, guaranteeing a sorted result===
<lang ats>//--------------------------------------------------------------------
//
// A patience sort for 32-bit signed integers.
//
// This implementation proves that result is sorted, though it
// does not prove that the result is of the same length as the
// original.
//
//--------------------------------------------------------------------
#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)
:<prf> [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_patience_sort
{n : int}
(lst : list (entier, n)) (* An ordinary list. *)
:<!wrt> sorted_entier_list (* No proof of the length. *)
extern fn
sorted_entier_list2list
{n : int}
(lst : sorted_entier_list n)
:<> list (entier, n)
overload merge with sorted_entier_list_merge
overload patience_sort with entier_list_patience_sort
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} .<n - m>.
(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} .<m + n>.
(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_patience_sort {n} lst =
let
prval () = lemma_list_param lst
val n : int n = length lst
in
if n = 0 then
SNIL
else if n = 1 then
let
val+ head :: NIL = lst
in
head ::: SNIL
end
else
let
val @(pf, pfgc | p) =
array_ptr_alloc<sorted_entier_list> (i2sz n)
macdef piles = !p
val () = array_initize_elt (piles, i2sz n, SNIL)
fn
find_pile {m : nat | m <= n}
{x : entier}
(num_piles : int m,
piles : &array (sorted_entier_list, n),
x : entier x)
:<> [i : nat | i < n]
[len : int]
[y : entier | ~(y < x)]
@(int i, sorted_entier_list (len, y)) =
//
// Bottenbruch search for the leftmost pile whose top is
// greater than or equal to some element x.
//
// References:
//
// * H. Bottenbruch, "Structure and use of ALGOL 60",
// Journal of the ACM, Volume 9, Issue 2, April 1962,
// pp.161-221. https://doi.org/10.1145/321119.321120
//
// The general algorithm is described on pages 214
// and 215.
//
// * https://en.wikipedia.org/w/index.php?title=Binary_search_algorithm&oldid=1062988272#Alternative_procedure
//
let
fun
loop {j, k : nat | j < k; k < m}
{x : entier} .<k - j>.
(piles : &array (sorted_entier_list, n),
j : int j,
k : int k,
x : entier x)
:<> [i : nat | i < n]
[len : int]
[y : entier | ~(y < x)]
@(int i, sorted_entier_list (len, y)) =
let
val i = j + g1int_ndiv (k - j, 2)
val pile = piles[i]
val- head ::: _ = pile
in
if head < x then
begin
if succ i <> k then
loop (piles, succ i, k, x)
else
let
val pile1 = piles[k]
in
case- pile1 of
| head1 ::: _ =>
if head1 < x then
let
(* Runtime check for buffer overrun. *)
val () =
$effmask_exn assertloc (k + 1 < n)
in
(* No pile satisfies the binary search.
Start a new pile. *)
@(k + 1, SNIL)
end
else
@(k, pile1)
end
end
else
begin
if j <> i then
loop (piles, j, i, x)
else
@(j, pile)
end
end
in
if 1 < num_piles then
let
prval () = prop_verify {m >= 1} ()
in
loop (piles, 0, pred num_piles, x)
end
else if num_piles = 1 then
let
prval () = prop_verify {m == 1} ()
val pile = piles[0]
in
case- pile of
| head ::: _ =>
if head < x then
@(1, SNIL)
else
@(0, pile)
end
else
let
prval () = prop_verify {m == 0} ()
in
@(0, SNIL)
end
end
fun
deal {m : nat | m <= n}
{j : nat | j <= n} .<m>.
(num_piles : &int j >> int k,
piles : &array (sorted_entier_list, n) >> _,
lst : list (entier, m))
:<!wrt> #[k : nat | j <= k; k <= n] void =
(* This implementation verifies at compile time that the
piles are sorted. *)
case+ lst of
| NIL => ()
| head :: tail =>
let
val @(i, pile) = find_pile (num_piles, piles, head)
prval () = lemma_sorted_entier_list_param pile
in
piles[i] := head ::: pile;
num_piles := max (num_piles, succ i);
deal (num_piles, piles, tail);
end
fun
make_list_of_piles
{num_piles, i : nat | num_piles <= n;
i <= num_piles}
.<num_piles - i>.
(num_piles : int num_piles,
piles : &array (sorted_entier_list, n),
i : int i)
:<> [m : nat] @(list (sorted_entier_list, m), int m) =
(* I do NOT bother to make this implementation tail
recursive. *)
if i = num_piles then
@(NIL, 0)
else
let
val @(lst, m) =
make_list_of_piles (num_piles, piles, succ i)
in
@(piles[i] :: lst, succ m)
end
var num_piles : Int = 0
val () = deal (num_piles, piles, lst)
val @(list_of_piles, m) =
make_list_of_piles (num_piles, piles, 0)
val () = array_ptr_free (pf, pfgc | p)
fun
merge_piles {m : nat} .<m>.
(list_of_piles : list (sorted_entier_list, m),
m : int m)
:<!wrt> sorted_entier_list =
(* This is essentially the same algorithm as a
NON-tail-recursive mergesort. *)
if m = 1 then
let
val+ sorted_lst :: NIL = list_of_piles
in
sorted_lst
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 (list_of_piles, m_left)
val left = merge_piles (list_vt2t left, m_left)
and right = merge_piles (right, m_right)
in
left \merge right
end
in
merge_piles (list_of_piles, m)
end
end
implement
sorted_entier_list2list lst =
(* This implementation is *NOT* tail recursive. It will use O(n)
stack space. *)
let
fun
recurs {n : nat} .<n>.
(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} .<n>.
(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 = patience_sort example_list
in
print! ("unsorted ");
print_Int_list example_list;
println! ();
print! ("sorted ");
print_Int_list (to_list sorted_list);
println! ()
end
(*------------------------------------------------------------------*)</lang>
{{out}}
<pre>$ patscc -O3 -DATS_MEMALLOC_GCBDW patience_sort_task_verified.dats -lgc && ./a.out
unsorted 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
sorted 2 4 8 15 22 22 37 38 46 48 49 53 54 54 58 70 72 76 80 82 84 86 90 93 98</pre>
=={{header|AutoHotkey}}==
|