(* 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