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
|
#include "share/atspre_staload.hats"
%{^
#define get_vram(_) ((void *) 0xB8000 + 1988)
%}
typedef cell = @{ ch = char, attrib = uint8 }
extern fun get_vram {n: nat} (n : size_t n):<> [l: agz] (@[cell][n] @ l | ptr l) = "mac#"
extern prfun eat_vram {l: agz} {n: int} (pf: @[cell][n] @ l): void
extern castfn uint8_of {n: nat} (i: int n): uint8 n
fn string_length {n:nat} (str: string (n)) : size_t (n) = let
fun loop {i:nat | i <= n} .<n-i>. (str: string n, i: size_t i): size_t (n) =
if string_isnot_atend (str, i) then loop (str, succ(i)) else i
in
loop (str, i2sz(0))
end
implement main0 () = let
val hello = "Hello world!"
val length = string_length hello
val color_byte = 0x1f
val (pf_vram | vram) = get_vram(length)
fun loop {l : agz} {n,i: nat | i <= n} .<n-i>. (pf: !(@[cell][n] @ l) | n : size_t n, i : int i, p : ptr l, str: string (n)) : void =
if n > i then (
p->[i] := @{ ch = str[i], attrib = uint8_of color_byte };
loop(pf | n,i+1,p,str))
else ()
in
loop(pf_vram | length, 0, vram, hello);
let prval () = eat_vram pf_vram in () end
end
|
