Remove duplicate elements: Difference between revisions
→ATS2 implementation using a radix sort
Line 654:
{{out}}
<pre> a c b e d</pre>
=== ATS2 implementation for elements have both ''order'' and ''equality'' predicates ===
Sort the elements and then keep only the first element of each run of equal elements.
This method is limited in speed by the speed of the sorting algorithm. That can vary greatly according to algorithm and circumstances, but typically is much better than O(n*n). Below (simply because it is convenient) I use the quicksort that is in the ATS2 prelude.
<syntaxhighlight lang="ats">
(* Remove duplicate elements.
The elements are sorted and then only unique values are kept. *)
#include "share/atspre_staload.hats"
(* How the remove_dups template function will be called. *)
extern fn {a : t@ype}
remove_dups
{n : int}
(lt : (a, a) -<cloref> bool, (* "less than" *)
eq : (a, a) -<cloref> bool, (* "equals" *)
src : arrayref (a, n),
n : size_t n,
dst : arrayref (a, n),
m : &size_t? >> size_t m)
: #[m : nat | m <= n]
void
implement {a}
remove_dups {n} (lt, eq, src, n, dst, m) =
if n = i2sz 0 then
m := i2sz 0
else
let
prval () = lemma_arrayref_param src (* Prove 0 <= n. *)
(* Sort a copy of src. *)
val arr = arrayptr_refize (arrayref_copy (src, n))
implement array_quicksort$cmp<a> (x, y) =
if x \lt y then ~1 else 1
val () = arrayref_quicksort<a> (arr, n)
(* Copy only the first element of each run of equal elements. *)
val () = dst[0] := arr[0]
fun
loop {i : int | 1 <= i; i <= n}
{j : int | 1 <= j; j <= i}
.<n - i>.
(i : size_t i,
j : size_t j)
: [m : int | 1 <= m; m <= n]
size_t m =
if i = n then
j
else if arr[pred i] \eq arr[i] then
loop (succ i, j)
else
begin
dst[j] := arr[i];
loop (succ i, succ j)
end
val () = m := loop (i2sz 1, i2sz 1)
in
end
implement (* A demonstration. *)
main0 () =
let
val src =
arrayref_make_list<string>
(10, $list ("a", "c", "b", "e", "a",
"a", "d", "d", "b", "c"))
val dst = arrayref_make_elt<string> (i2sz 10, "?")
var m : size_t
in
remove_dups<string> (lam (x, y) => x < y,
lam (x, y) => x = y,
src, i2sz 10, dst, m);
let
prval [m : int] EQINT () = eqint_make_guint m
var i : natLte m
in
for (i := 0; i2sz i <> m; i := succ i)
print! (" ", dst[i]);
println! ()
end
end
</syntaxhighlight>
{{out}}
<pre> a b c d e</pre>
=== ATS2 implementation using a radix sort ===
| |||