Remove duplicate elements: Difference between revisions
→ATS2 implementation for values having an equality or equivalence predicate
Line 553:
=={{header|ATS}}==
=== ATS2 implementation for values having an ''equality
This method runs no worse than O(n*n) in the number of elements. It is an example of the brute-force technique.
Line 650:
end
end
</syntaxhighlight>
{{out}}
<pre> a c b e d</pre>
=== ATS2 implementation for linear values having an ''equality'' predicate ===
<syntaxhighlight lang="ats">
(* 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. It uses a linked list and supports linear types.
The equality predicate is implemented as a template function. *)
#include "share/atspre_staload.hats"
staload UN = "prelude/SATS/unsafe.sats"
#define NIL list_vt_nil ()
#define :: list_vt_cons
(*------------------------------------------------------------------*)
(* Interfaces *)
extern fn {a : vt@ype}
array_remove_dups
{n : int}
{p_arr : addr}
(pf_arr : array_v (a, p_arr, n) |
p_arr : ptr p_arr,
n : size_t n)
:<!wrt> [m : nat | m <= n]
@(array_v (a, p_arr, m),
array_v (a?, p_arr + (m * sizeof a), n - m) |
size_t m)
extern fn {a : vt@ype}
list_vt_remove_dups
{n : int}
(lst : list_vt (a, n))
:<!wrt> [m : nat | m <= n]
list_vt (a, m)
extern fn {a : vt@ype}
remove_dups$eq :
(&a, &a) -<> bool
extern fn {a : vt@ype}
remove_dups$clear :
(&a >> a?) -< !wrt > void
(*------------------------------------------------------------------*)
(* Implementation of array_remove_dups *)
(* The implementation for arrays converts to a list_vt, does the
removal duplicates, and then writes the data back into the original
array. *)
implement {a}
array_remove_dups {n} {p_arr} (pf_arr | p_arr, n) =
let
var lst = array_copy_to_list_vt<a> (!p_arr, n)
var m : int
val lst = list_vt_remove_dups<a> lst
val m = list_vt_length lst
prval [m : int] EQINT () = eqint_make_gint m
prval @(pf_uniq, pf_rest) =
array_v_split {a?} {p_arr} {n} {m} pf_arr
val () = array_copy_from_list_vt<a> (!p_arr, lst)
in
@(pf_uniq, pf_rest | i2sz m)
end
(*------------------------------------------------------------------*)
(* Implementation of list_vt_remove_dups *)
(* The list is worked on "in place". That is, no nodes are copied or
moved to new locations, except those that are removed and freed. *)
fn {a : vt@ype}
remove_equal_elements
{n : int}
(x : &a,
lst : &list_vt (a, n) >> list_vt (a, m))
:<!wrt> #[m : nat | m <= n]
void =
let
fun {a : vt@ype}
remove_elements
{n : nat}
.<n>.
(x : &a,
lst : &list_vt (a, n) >> list_vt (a, m))
:<!wrt> #[m : nat | m <= n]
void =
case+ lst of
| NIL => ()
| @ (head :: tail) =>
if remove_dups$eq (head, x) then
let
val new_lst = tail
val () = remove_dups$clear<a> head
val () = free@{a}{0} lst
val () = lst := new_lst
in
remove_elements {n - 1} (x, lst)
end
else
let
val () = remove_elements {n - 1} (x, tail)
prval () = fold@ lst
in
end
prval () = lemma_list_vt_param lst
in
remove_elements {n} (x, lst)
end
fn {a : vt@ype}
remove_dups
{n : int}
(lst : &list_vt (a, n) >> list_vt (a, m))
:<!wrt> #[m : nat | m <= n]
void =
let
fun
rmv_dups {n : nat}
.<n>.
(lst : &list_vt (a, n) >> list_vt (a, m))
:<!wrt> #[m : nat | m <= n]
void =
case+ lst of
| NIL => ()
| head :: NIL => ()
| @ head :: tail =>
let
val () = remove_equal_elements (head, tail)
val () = rmv_dups tail
prval () = fold@ lst
in
end
prval () = lemma_list_vt_param lst
in
rmv_dups {n} lst
end
implement {a}
list_vt_remove_dups {n} lst =
let
var lst = lst
in
remove_dups {n} lst;
lst
end
(*------------------------------------------------------------------*)
implement
remove_dups$eq<Strptr1> (s, t) =
($UN.strptr2string s = $UN.strptr2string t)
implement
remove_dups$clear<Strptr1> s =
strptr_free s
implement
array_uninitize$clear<Strptr1> (i, s) =
strptr_free s
implement
fprint_ref<Strptr1> (outf, s) =
print! ($UN.strptr2string s)
implement (* A demonstration with linear strings. *)
main0 () =
let
#define N 10
val data =
$list_vt{Strptr1}
(string0_copy "a", string0_copy "c", string0_copy "b",
string0_copy "e", string0_copy "a", string0_copy "a",
string0_copy "d", string0_copy "d", string0_copy "b",
string0_copy "c")
var arr : @[Strptr1][N]
val () = array_copy_from_list_vt<Strptr1> (arr, data)
prval pf_arr = view@ arr
val p_arr = addr@ arr
val [m : int]
@(pf_uniq, pf_abandoned | m) =
array_remove_dups<Strptr1> (pf_arr | p_arr, i2sz N)
val () = fprint_array_sep<Strptr1> (stdout_ref, !p_arr, m, " ")
val () = println! ()
val () = array_uninitize<Strptr1> (!p_arr, m)
prval () = view@ arr :=
array_v_unsplit (pf_uniq, pf_abandoned)
in
end
(*------------------------------------------------------------------*)
</syntaxhighlight>
| |||