aboutsummaryrefslogtreecommitdiff
path: root/lib/DATS/writer.dats
diff options
context:
space:
mode:
Diffstat (limited to 'lib/DATS/writer.dats')
-rw-r--r--lib/DATS/writer.dats134
1 files changed, 86 insertions, 48 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