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