#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) : void extern fn _clear_screen(w : &writer_t) : void in implement _clear_screen(w) = let fun loop {n : nat | n < N - 1} .. (i : int n, w : &writer_t) : 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) in // Reference to writer val writer_ref = ref_make_viewptr{initializable writer_t} (view@writer | addr@writer) end in implement put_string (str : string) : void = let val (vbox pf | p) = ref_get_viewptr(writer_ref) implement init_exec$fwork(v) = let implement string_foreach$fwork (c,env) = put_char(c,env) val _ = $effmask_all(string_foreach_env (g1ofg0(str),v)) in end in init_exec(!p) end implement clear_screen() : void = let val (vbox pf | p) = ref_get_viewptr(writer_ref) implement init_exec$fwork(v) = _clear_screen(v) in if p->initialized then init_exec (!p) else let prval () = opt_unnone p->obj val () = p->obj := @{position = 0, color_code = code_value(White,Black)} val () = p->initialized := true val () = _clear_screen(p->obj) prval () = opt_some p->obj in end end end end