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
|
#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 init_exec$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
init_exec<writer_t>(!p)
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<writer_t> (!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
|
