80 lines
2.1 KiB
Plaintext
80 lines
2.1 KiB
Plaintext
(* 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
|