#include "share/atspre_staload.hats"

staload "lib/SATS/writer.sats"
staload "lib/SATS/init.sats"

// when this .dats file not staloaded I get weird error from template function
staload "lib/DATS/init.dats" 

#define ATS_DYNLOADFLAG 0

%{^
  #define get_buffer() ((void *) 0xB8000)
%}

vtypedef buffer = [l : agz] (@[screenChar][N] @ l | ptr l)
typedef writer_t  = @{position = [a:int | a >= 0 && a < N] int (a), color_code = uint8}

extern fun get_buffer():<> buffer = "mac#"
extern prfun eat_buffer (pf: buffer): void


fn color_value(c : color):<> uint8 = let
  extern castfn i2u8 {n: nat} (i: int n):<> uint8 n
in
  case+ c of 
    | Black() => i2u8 0
    | Blue() => i2u8 1
    | Green() => i2u8 2
    | Cyan() => i2u8 3
    | Red() => i2u8 4
    | Magenta() => i2u8 5
    | Brown() => i2u8 6
    | LightGray() => i2u8 7
    | DarkGray() => i2u8 8
    | LightBlue() => i2u8 9
    | LightGreen() => i2u8 10
    | LightCyan() => i2u8 11
    | LightRed() => i2u8 12
    | Pink() => i2u8 13
    | Yellow() => i2u8 14
    | White() => i2u8 15
end

fn code_value(foreground: color, background:color):<> uint8 = 
  (color_value(background) << 4) lor color_value(foreground)

local
  extern fn put_char(c : char, w: &writer_t) :<!wrt> void
  extern fn _clear_screen(w : &writer_t) :<!wrt> void 
in
  implement _clear_screen(w) = let
    fun loop {n : nat | n < N - 1} .<N-n>. (i : int n, w : &writer_t) :<!wrt> void = 
      (put_char('\0', w); if (i < N - 2) then loop(i+1,w))
    val () = w := @{position = 0, color_code = code_value(White,Black)}
  in
    loop(0,w);
    w.position := 0;
  end

  implement put_char (c,w) = let
    val buf = get_buffer()
    val pos = w.position
  in
    if (c = '\n') then
      let 
        val new_pos = (pos /  BUFFER_WIDTH + 1) * BUFFER_WIDTH
      in
        if (new_pos < N) then
          w.position := new_pos
        else
          _clear_screen(w)
      end
    else (
      buf.1->[w.position] := @{ ascii_character = c, color_code = w.color_code};

      if (pos < N - 1) then
        w.position := succ(pos)
      else
        _clear_screen(w));

    let prval() = eat_buffer buf in () end
  end


  local

  local
    // Static variable
    var _writer : writer_t?
    prval () = opt_none _writer
    var writer = uninitialized<writer_t>(_writer)
  in
    // Reference to writer
    val writer_ref = ref_make_viewptr{initializable writer_t} (view@writer | addr@writer)
  end

  in

    implement initialize$fwork<writer_t>(v) =
        (
          v := @{position = 0, color_code = code_value(White,Black)}; 
          let prval() = opt_some v in true end
        )

    implement put_string (str : string) : void = let
      implement exec_void$fwork<writer_t>(v) = let 
        implement string_foreach$fwork<writer_t> (c,env) = put_char(c,env)
        val _ = $effmask_all(string_foreach_env<writer_t> (g1ofg0(str),v))
      in 
      end
    in  
      $effmask_ref(exec_init<writer_t>(writer_ref))
    end

    implement clear_screen() : void = let
      implement exec_void$fwork<writer_t>(v) = _clear_screen(v)
    in
      exec_init<writer_t>(writer_ref)
    end

  end

end