91 lines
2.4 KiB
Plaintext
91 lines
2.4 KiB
Plaintext
(* Remove duplicate elements.
|
|
|
|
This implementation is for elements that have an "equals" (or
|
|
"equivalence") predicate. It runs O(n*n) in the number of
|
|
elements. *)
|
|
|
|
#include "share/atspre_staload.hats"
|
|
|
|
(* How the remove_dups template function will be called. *)
|
|
extern fn {a : t@ype}
|
|
remove_dups
|
|
{n : int}
|
|
(eq : (a, a) -<cloref> bool,
|
|
src : arrayref (a, n),
|
|
n : size_t n,
|
|
dst : arrayref (a, n),
|
|
m : &size_t? >> size_t m)
|
|
:<!refwrt> #[m : nat | m <= n]
|
|
void
|
|
|
|
(* An implementation of the remove_dups template function. *)
|
|
implement {a}
|
|
remove_dups {n} (eq, src, n, dst, m) =
|
|
if n = i2sz 0 then
|
|
m := i2sz 0
|
|
else
|
|
let
|
|
fun
|
|
peruse_src
|
|
{i : int | 1 <= i; i <= n}
|
|
{j : int | 1 <= j; j <= i}
|
|
.<n - i>.
|
|
(i : size_t i,
|
|
j : size_t j)
|
|
:<!refwrt> [m : int | 1 <= m; m <= n]
|
|
size_t m =
|
|
let
|
|
fun
|
|
already_seen
|
|
{k : int | 0 <= k; k <= j}
|
|
.<j - k>.
|
|
(x : a,
|
|
k : size_t k)
|
|
:<!ref> bool =
|
|
if k = j then
|
|
false
|
|
else if eq (x, dst[k]) then
|
|
true
|
|
else
|
|
already_seen (x, succ k)
|
|
in
|
|
if i = n then
|
|
j
|
|
else if already_seen (src[i], i2sz 0) then
|
|
peruse_src (succ i, j)
|
|
else
|
|
begin
|
|
dst[j] := src[i];
|
|
peruse_src (succ i, succ j)
|
|
end
|
|
end
|
|
|
|
prval () = lemma_arrayref_param src (* Prove 0 <= n. *)
|
|
in
|
|
dst[0] := src[0];
|
|
m := peruse_src (i2sz 1, i2sz 1)
|
|
end
|
|
|
|
implement (* A demonstration with strings. *)
|
|
main0 () =
|
|
let
|
|
val eq = lam (x : string, y : string) : bool =<cloref> (x = y)
|
|
|
|
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> (eq, 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] : string);
|
|
println! ()
|
|
end
|
|
end
|