//
// How to compile:
// patscc -DATS_MEMALLOC_LIBC -o hamming hamming.dats
//
#include
"share/atspre_staload.hats"

fun
min3
(
  A: arrayref(int, 3)
) : natLt(3) = i where
{
  var x: int = A[0]
  var i: natLt(3) = 0
  val () = if A[1] < x then (x := A[1]; i := 1)
  val () = if A[2] < x then (x := A[2]; i := 2)
} (* end of [min3] *)

fun
hamming
{n:pos}
(
  n: int(n)
) : int = let
//
var A = @[int](2, 3, 5)
val A = $UNSAFE.cast{arrayref(int, 3)}(addr@A)
var I = @[int](1, 1, 1)
val I = $UNSAFE.cast{arrayref(int, 3)}(addr@I)
val H = arrayref_make_elt<int> (i2sz(succ(n)), 0)
val () = H[0] := 1
//
fun
loop{k:pos}
  (k: int(k)) : void =
(
//
if
k < n
then let
  val i = min3(A)
  val k =
  (
    if A[i] > H[k-1] then (H[k] := A[i]; k+1) else k
  ) : intBtwe(k, k+1)
  val ii = I[i]
  val () = I[i] := ii+1
  val ii = $UNSAFE.cast{natLte(n)}(ii)
  val () = if i = 0 then A[i] := 2*H[ii]
  val () = if i = 1 then A[i] := 3*H[ii]
  val () = if i = 2 then A[i] := 5*H[ii]
in
  loop(k)
end // end of [then]
else () // end of [else]
//
) (* end of [loop] *)
//
in
  loop (1); H[n-1]
end (* end of [hamming] *)

implement
main0 () =
{
val () =
loop(1) where
{
fun
loop
{n:pos}
(
  n: int(n)
) : void =
if
n <= 20
then let
  val () =
  println! ("hamming(",n,") = ", hamming(n))
in
  loop(n+1)
end // end of [then]
// end of [if]
} (* end of [val] *)
val n = 1691
val () = println! ("hamming(",n,") = ", hamming(n))
//
} (* end of [main0] *)