1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
#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 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->initialized 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)
implement init_exec$fwork<writer_t>(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
|
