lines.dats

#include
"share/atspre_staload.hats"

staload UN = "prelude/SATS/unsafe.sats"

staload
_ = "prelude/DATS/integer.dats"
staload
_ = "prelude/DATS/integer_fixed.dats"
staload
_ = "prelude/DATS/array.dats"
staload
_ = "prelude/DATS/matrix.dats"

(* ****** ****** *)

typedef vec3 (a:t@ype) = @{
  x= a
, y= a
, z= a
} (* end of [vec3] *)

extern
fun{a:t@ype}
vec3_new (v: &vec3 (a?) >> vec3 (a), a, a, a): void

extern
fun{a:t@ype}
eq_vec3_vec3 (&vec3 (INV(a)), &vec3 (a)): bool
overload = with eq_vec3_vec3
extern
fun{a:t@ype}
neq_vec3_vec3 (&vec3 (INV(a)), &vec3 (a)): bool
overload != with neq_vec3_vec3

extern
fun{a:t@ype}
vec3_get_at_int (v: &vec3 (INV(a)), i: natLt(3)): a
overload [] with vec3_get_at_int
// overload .get with vec3_get_at_int

extern
fun{a:t@ype}
vec3_set_at_int (v: &vec3 (INV(a)), i: natLt(3), x: a): void
overload [] with vec3_set_at_int
// overload .set with vec3_set_at_int

implement{a}
vec3_new (v, x, y, z) = {
  val () = v.x := x
  val () = v.y := y
  val () = v.z := z
} (* end of [vec3_new] *)

implement
eq_vec3_vec3<int> (a, b) = (a.x = b.x && a.y = b.y && a.z = b.z)
implement
neq_vec3_vec3<int> (a, b) = ~(eq_vec3_vec3<int> (a, b))

implement{a}
vec3_get_at_int (v, i) =
  case+ i of
  | 0 => v.x
  | 1 => v.y
  | 2 => v.z

implement{a}
vec3_set_at_int (v, i, x) =
  case+ i of
  | 0 => v.x := x
  | 1 => v.y := x
  | 2 => v.z := x

typedef vec3 = vec3 (int)

(* ****** ****** *)

absvt@ype pixmap (t:t@ype, m:int, n:int) = (size_t, size_t, ptr)

extern
fun{a:t@ype}
pixmap_new {m,n:pos} (&pixmap (a, 0, 0)? >> pixmap (a, m, n), size_t m, size_t n, a): void
extern
fun{a:t@ype}
pixmap_delete {m,n:int} (&pixmap (a, m, n) >> pixmap (a, 0, 0)?): void
extern
fun{a:t@ype}
pixmap_set_at_int {m,n:int} (&pixmap (INV(a), m, n), natLt(m), natLt(n), a): void
extern
fun{a:t@ype}
pixmap_get_width {m,n:int} (&pixmap (INV(a), m, n)): size_t m
extern
fun{a:t@ype}
pixmap_get_height {m,n:int} (&pixmap (INV(a), m, n)): size_t n
extern
fun
pixmap_clear {m,n:int} (&pixmap (INV(a), m, n), a): void
extern
fun
pixmap_save_ppm {m,n:int} (&pixmap (uint32, m, n), string): void

overload [] with pixmap_set_at_int

local

assume pixmap (t:t@ype, m:int, n:int) = [l:addr] (
  matrix_v (t, l, m, n)
, mfree_gc_v (l)
| size_t m, size_t n, ptr l
) (* end of [pixmap] *)

in // in of [local]

implement{a}
pixmap_new {m,n} (res, m, n, fill) = let
  val (pf_mat, pf_free | p_mat) = matrix_ptr_alloc<a> (m, n)
  implement
  matrix_initize$init<a> (i, j, x) = (x := fill)
  val () = matrix_initize<a> (!p_mat, m, n)
  val () = res := (pf_mat, pf_free | m, n, p_mat)
in

end // end of [pixmap_new]

implement{a}
pixmap_delete {m,n} (pm) = {
  val (pf_mat, pf_free | m, n, p_mat) = pm
  prval [l:addr] EQADDR () = eqaddr_make_ptr (p_mat)
  prval pf_mn = mul_make {m,n} ()
  val mn = g1uint_mul (m, n)
  prval () = mul_elim (pf_mn)
  prval pf_arr = matrix2array_v {a} (pf_mat)
  implement
  array_uninitize$clear<a> (i, x) = ()
  val () = array_uninitize<a> (!p_mat, mn)
  prval pf_mat = array2matrix_v {a?} {l} {m,n} (pf_arr)
  val () = matrix_ptr_free {a} (pf_mat, pf_free | p_mat)
} (* end of [pixmap_delete] *)

implement{a}
pixmap_set_at_int (pm, i, j, x) = let
  val (pf_mat, pf_free | m, n, p_mat) = pm
  val i = (i2sz)i
  val j = (i2sz)j
  val () = matrix_set_at_size<a> (!p_mat, i, n, j, x)
  val () = pm := (pf_mat, pf_free | m, n, p_mat)
in
end // end of [pixmap_set_at_int]

implement{a}
pixmap_get_width {m,n} (pm) = pm.2
implement{a}
pixmap_get_height {m,n} (pm) = pm.3

implement{a}
pixmap_clear {m,n} (pm, fill) = {
  implement(env)
  matrix_foreach$fwork<a><env> (x, env) = {
    val () = x := fill
  } (* end of [matrix_foreach$fwork] *)
  val (pf_mat, pf_free | m, n, p_mat) = pm
  val () = matrix_foreach<a> (!p_mat, m, n)
  val () = pm := (pf_mat, pf_free | m, n, p_mat)
} (* end of [pixmap_clear] *)

implement
pixmap_save_ppm {m,n} (pm, filename) = {
  val fp = fileref_open_exn (filename, file_mode_w)

  val (pf_mat, pf_free | m, n, p_mat) = pm

  val () = fprintln!(fp, "P3")
  val () = fprintln!(fp, "# generated by ATS/Postiats")
  val () = fprintln!(fp, m, " ", n)
  val () = fprintln!(fp, "255") // max color value
  
  implement
  fprint_matrix$sep1<> (out) = fprint!(out, " ")
  implement
  fprint_matrix$sep2<> (out) = fprintln!(out)
  implement
  fprint_ref<uint32> (out, x) = {
    val c = $UN.castvwtp0{uint} (x)
    val r = (c >> 16) land 0xFFu
    val g = (c >> 8) land 0xFFu
    val b = (c >> 0) land 0xFFu
    val () = fprint!(fp, r, " ", g, " ", b)
  }
  val () = fprint_matrix<uint32> (fp, !p_mat, m, n)
//
  val () = fileref_close (fp)
//
  val () = pm := (pf_mat, pf_free | m, n, p_mat)
//
} (* end of [pixmap_save_ppm] *)

end // end of [local]

vtypedef pixmap (m:int, n:int) = pixmap (uint32, m, n)

(* ****** ****** *)

extern
fun{env:vt@ype}
line_raster$fwork (&vec3, &(env) >> _): void
extern
fun{env:vt@ype}
line_raster_foreach_env (&vec3, &vec3, &(env) >> _): void

implement{env}
line_raster_foreach_env (from, to, env) = {
//
  typedef raster_state = @{step= vec3, d= vec3, major_axis= natLt(3)}
//
  var from = from
  var to = to
  var state : raster_state
  val () = vec3_new (state.step, 0, 0, 0)
  val () = vec3_new (state.d, 0, 0, 0)
  val () = state.major_axis := 0
//
  var max = (g0ofg1)0
  var i: int = 0
  val () =
    while* {i:nat | i <= 3}
      (i: int(i), state: raster_state, from: vec3, to: vec3, max: int):
      (state: raster_state, from: vec3, to: vec3, max: int) =>
      (i < 3) {
      val d = to[i] - from[i]
      val () = vec3_set_at_int<int> (state.step, i, if d > 0 then 1 else ~1)
      val d = abs(d)
      val () =
        if :(state: raster_state, max: int) => d > max then begin
          max := d;
          state.major_axis := i
        end // end of [val]
      val () = i := i + 1
    } (* end of [for] *)
  val () = line_raster$fwork<env> (from, env)
//
  fun
  calc_rs (from: &vec3, to: &vec3, axis: natLt(3)): int = abs (to[axis] - from[axis])
//
  val () =
    while*
      (state: raster_state, from: vec3, to: vec3, env: env):
      (state: raster_state, from: vec3, to: vec3, env: env) =>
      (from != to) {
        val () =
          from[state.major_axis] :=
          from[state.major_axis] + vec3_get_at_int<int> (state.step, state.major_axis)
        // end of [val]
        val rs_base = calc_rs (from, to, state.major_axis)

        var i: int = 0
        val () =
          while* {i:nat | i <= 3}
            (i: int(i), state: raster_state, from: vec3, to: vec3):
            (state: raster_state, from: vec3, to: vec3) =>
            (i < 3)
          {
            val rs = calc_rs (from, to, i)
            val () =
              if :(from: vec3, state: raster_state) => (rs > 0 && i != state.major_axis) then {
                val () = vec3_set_at_int<int> (state.d, i, vec3_get_at_int<int> (state.d, i) + rs)
                val () =
                  if :(from: vec3, state: raster_state) => (vec3_get_at_int<int> (state.d, i) >= rs_base) then {
                    val () = vec3_set_at_int<int> (state.d, i, vec3_get_at_int<int> (state.d, i) - rs_base)
                    val () = from[i] := from[i] + vec3_get_at_int<int> (state.step, i)
                  }
              } (* end of [val] *)
            val () = i := i + 1
          } (* end of [while] *)
        val () = line_raster$fwork<env> (from, env)
      } (* end of [while] *)
} (* end of [line_raster_foreach_env] *)

(* ****** ****** *)

extern
fun
test_code {m,n:int} (&pixmap (m, n)): void

implement
test_code {m,n} (canvas) = {
//
  var a: vec3
  var b: vec3
  val () = vec3_new<int> (a, 0, 0, 0)
  val () = vec3_new<int> (b, 50, 55, ~20)
//
  val p_canvas = addr@(canvas)
  prval pf_canvas = view@(canvas)
//
  implement{env}
  line_raster$fwork (point, env) = {
    prval (pf_canvas, fpf) = decode($vcopyenv_v(pf_canvas))
    val color = $UN.castvwtp0{uint32}(0xFFFFFF)
    val i = point.x
    val i = (g1ofg0)i
    val-true = i >= 0
    val w = pixmap_get_width (canvas)
    prval () = lemma_g1uint_param (w)
    val w = g1uint2int_size_int (w)
    val-true = i < w
    val j = point.y
    val j = (g1ofg0)j
    val-true = j >= 0
    val h = pixmap_get_height (canvas)
    prval () = lemma_g1uint_param (h)
    val h = g1uint2int_size_int (h)
    val-true = j < h
    val () = pixmap_set_at_int (canvas, i, j, color)
    prval () = fpf (pf_canvas)
  } (* end of [line_raster$fwork] *)
  var env = 0: int
  val () = line_raster_foreach_env<int> (a, b, env)
//
  prval () = view@(canvas) := pf_canvas
//
} (* end of [test_code] *)

(* ****** ****** *)

implement
main0 () = {
//
  var pixmap: pixmap (uint32, 0, 0)
  val () = pixmap_new<uint32> (pixmap, (i2sz)300, (i2sz)300, $UN.castvwtp0{uint32}(0))
  prval pf_pixmap = view@(pixmap)
//  
  var a: vec3
  var b: vec3
  val () = vec3_new (a, 0, 0, 0)
  val () = vec3_new (b, 10, 5, ~4)
//
  implement{env}
  line_raster$fwork (point, env) = {
    prval (pf_pixmap, fpf) = decode($vcopyenv_v(pf_pixmap))
    val color = $UN.castvwtp0{uint32} (0xffffff)
    //
    val i = point.x
    val i = (g1ofg0)i
    val-true = i >= 0
    val w = pixmap_get_width (pixmap)
    prval () = lemma_g1uint_param (w)
    val w = g1uint2int_size_int (w)
    val-true = i < w
    val j = point.y
    val j = (g1ofg0)j
    val-true = j >= 0
    val h = pixmap_get_height (pixmap)
    prval () = lemma_g1uint_param (h)
    val h = g1uint2int_size_int (h)
    val-true = j < h
    val () = pixmap_set_at_int (pixmap, i, j, color)
    val () = println!("ATS: point x:", point.x, " y:", point.y, " z:", point.z, " color: ", color)
    prval () = fpf (pf_pixmap)
  } (* end of [line_raster$fwork] *)
  var env = 0: int
  val () = line_raster_foreach_env<int> (a, b, env)
//
  implement{env}
  intrange_foreach$fwork (i, env) = let
    prval (pf_pixmap, fpf) = decode($vcopyenv_v(pf_pixmap))
    val () = test_code (pixmap)
    prval () = fpf (pf_pixmap)
  in
  end
  val _ = intrange_foreach (0, 1000000)
//
(*
val () = pixmap_save_ppm (pixmap, "./output.ppm")
*)
//
  prval () = view@pixmap := pf_pixmap  
  val () = pixmap_delete (pixmap)
} (* end of [main0] *)