diff options
| -rw-r--r-- | lib/DATS/writer.dats | 134 | ||||
| -rw-r--r-- | lib/SATS/writer.sats | 6 |
2 files changed, 86 insertions, 54 deletions
diff --git a/lib/DATS/writer.dats b/lib/DATS/writer.dats index 24246a1..92314b7 100644 --- a/lib/DATS/writer.dats +++ b/lib/DATS/writer.dats @@ -1,6 +1,7 @@ #include "share/atspre_staload.hats" staload "lib/SATS/writer.sats" +staload "lib/SATS/init.sats" #define ATS_DYNLOADFLAG 0 @@ -8,11 +9,16 @@ staload "lib/SATS/writer.sats" #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 -extern fun getref (): [l:addr] vtakeoutptr (writer) -fun color_value(c : color): uint8 = + +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 @@ -30,62 +36,94 @@ fun color_value(c : color): uint8 = | Pink() => i2u8 13 | Yellow() => i2u8 14 | White() => i2u8 15 +end -fun code_value(foreground: color, background:color): uint8 = +fn code_value(foreground: color, background:color):<> uint8 = (color_value(background) << 4) lor color_value(foreground) local -var _val: writer - -in -implement getref () = let - extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (writer@l) - prval (pf, fpf) = __assert (addr@(_val)) + extern fn put_char(c : char, w: &writer_t) :<!wrt> void + extern fn _clear_screen(w : &writer_t) :<!wrt> void in - (pf, fpf | addr@(_val)) -end -end + 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)) + in + loop(0,w); + w.position := 0; + end -fun put_char (c : char, writer: &writer) : void = let - val buf = get_buffer() - val pos = writer.position -in - if (c = '\n') then - let - val new_pos = (pos / BUFFER_WIDTH + 1) * BUFFER_WIDTH - in - if (new_pos < N) then - writer.position := new_pos + 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() - end - else ( - buf.1->[writer.position] := @{ ascii_character = c, color_code = writer.color_code}; + _clear_screen(w)); - if (pos < N - 1) then - writer.position := succ(pos) - else - clear_screen()); + let prval() = eat_buffer buf in () end + end - let prval() = eat_buffer buf in () end -end + local -implement put_string (str : string) : void = let - val (pf, fpf | p_val) = getref() - implement string_foreach$fwork<writer> (c,env) = put_char(c,env) - val _ = string_foreach_env<writer> (g1ofg0(str),!p_val) - prval() = fpf(pf) -in -end + local + // Static variable + var _writer : writer_t? + prval () = opt_none _writer + var writer = empty<writer_t>(_writer) + in + val writer_ref = ref_make_viewptr{enablable 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 string_foreach$fwork<writer_t> (c,env) = put_char(c,env) + in + if p->enabled then let + prval () = opt_unsome p->obj + val _ = $effmask_ref(string_foreach_env<writer_t> (g1ofg0(str),p->obj)) + prval () = opt_some p->obj + in + end + end + + implement clear_screen() : void = let + val (vbox pf | p) = ref_get_viewptr(writer_ref) + in + if p->enabled then + let + prval () = opt_unsome p->obj + val () = _clear_screen(p->obj) + prval () = opt_some p->obj + in + end + else + let + prval () = opt_unnone p->obj + val () = p->obj := @{position = 0, color_code = code_value(White,Black)} + val () = p->enabled := true + val () = _clear_screen(p->obj) + prval () = opt_some p->obj + in + end + end + + end -implement clear_screen() : void = let - val (pf, fpf | p_val) = getref() - fun loop {n : nat | n < N - 1} .<N-n>. (i : int n, wr : &writer) : void = - (put_char('\0', wr); if (i < N - 2) then loop(i+1,wr)) - val () = !p_val := @{position = 0, color_code = code_value(White,Black)} -in - loop(0,!p_val); - !p_val.position := 0; - let prval() = fpf(pf) in () end end diff --git a/lib/SATS/writer.sats b/lib/SATS/writer.sats index 65a2ea9..14773ea 100644 --- a/lib/SATS/writer.sats +++ b/lib/SATS/writer.sats @@ -20,13 +20,7 @@ datatype color = | Yellow | White - typedef screenChar = @{ ascii_character = char, color_code = uint8} -vtypedef buffer = [l : agz] (@[screenChar][N] @ l | ptr l) -typedef writer = @{position = [a:int | a >= 0 && a < N] int (a), color_code = uint8} - -castfn i2u8 {n: nat} (i: int n): uint8 n - fun put_string (str : string) : void fun clear_screen() : void |