aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/DATS/itoa.dats63
-rw-r--r--lib/DATS/writer.dats91
-rw-r--r--lib/SATS/writer.sats32
3 files changed, 186 insertions, 0 deletions
diff --git a/lib/DATS/itoa.dats b/lib/DATS/itoa.dats
new file mode 100644
index 0000000..35b8c47
--- /dev/null
+++ b/lib/DATS/itoa.dats
@@ -0,0 +1,63 @@
+#include "share/atspre_staload.hats"
+
+#define ATS_DYNLOADFLAG 0
+
+
+fun reverse {l : addr} {n,m:nat | n < m} (pf : !(@[char][m] @ l) | p : ptr l, n : int n) : void = let
+ fun loop {i,j,n:nat | i < j && j < n} (pf : !(@[char][n] @ l) | p : ptr l , i : int i, j : int j) : void = let
+ val tmp = p->[i]
+ in
+ p->[i] := p->[j];
+ p->[j] := tmp;
+ if (i+1 < j-1) then
+ loop(pf | p, i+1,j-1)
+ end
+in
+ if (n > 0) then
+ loop(pf | p, 0, n)
+end
+
+local
+
+#define BUFFER_SIZE 50
+
+staload UN = "prelude/SATS/unsafe.sats"
+
+extern castfn char_arr2string (arr : &(@[char][BUFFER_SIZE])) : [n : nat | n < BUFFER_SIZE] string n
+extern praxi __assert {l:addr} (ptr: ptr (l)): vtakeout0 (@[char][BUFFER_SIZE]@l)
+var buffer : @[char][BUFFER_SIZE] // Size should be BUFFER_SIZE
+
+in
+
+//TODO: make function better by handling to large number for buffer
+
+extern fun itoa {v,n:nat | n > 1 && n < 33 && v > 0} (value : int v, base : int n) : [k : nat | k < BUFFER_SIZE] string k
+implement itoa(value,base) = let
+ prval (pf , fpf) = __assert(addr@buffer) // Get proofs UNSAFE:
+
+ fun loop {n,i : nat | n > 0 && i < BUFFER_SIZE} {l:addr} (pf : !(@[char][BUFFER_SIZE] @ l) | p : ptr l , n : int n, i : size_t i): void = let
+ val r = n % base
+ val k = n / base
+ in
+ if (r >= 10) then
+ p->[i] := $UN.cast{char}(65 + (r - 10))
+ else
+ p->[i] := $UN.cast{char}(48 + r);
+
+ if (i + 2 < BUFFER_SIZE) then
+ if (k > 0) then
+ loop(pf | p, k, succ(i))
+ else (
+ p->[succ(i)] := '\0';
+ reverse(pf | p, sz2i(i)))
+ end
+
+ // Run loop
+ val () = loop(pf | addr@buffer, value, i2sz(0));
+ val str = char_arr2string(buffer); // Convert arr to string UNSAFE:
+in
+ let prval () = fpf(pf) in end;
+ str // Return string
+end
+
+end
diff --git a/lib/DATS/writer.dats b/lib/DATS/writer.dats
new file mode 100644
index 0000000..24246a1
--- /dev/null
+++ b/lib/DATS/writer.dats
@@ -0,0 +1,91 @@
+#include "share/atspre_staload.hats"
+
+staload "lib/SATS/writer.sats"
+
+#define ATS_DYNLOADFLAG 0
+
+%{^
+ #define get_buffer() ((void *) 0xB8000)
+%}
+
+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 =
+ 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
+
+fun 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))
+in
+ (pf, fpf | addr@(_val))
+end
+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
+ else
+ clear_screen()
+ end
+ else (
+ buf.1->[writer.position] := @{ ascii_character = c, color_code = writer.color_code};
+
+ if (pos < N - 1) then
+ writer.position := succ(pos)
+ else
+ clear_screen());
+
+ let prval() = eat_buffer buf in () end
+end
+
+
+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
+
+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
new file mode 100644
index 0000000..65a2ea9
--- /dev/null
+++ b/lib/SATS/writer.sats
@@ -0,0 +1,32 @@
+#define BUFFER_HEIGHT 23
+#define BUFFER_WIDTH 80
+#define N BUFFER_HEIGHT * BUFFER_WIDTH
+
+datatype color =
+ | Black
+ | Blue
+ | Green
+ | Cyan
+ | Red
+ | Magenta
+ | Brown
+ | LightGray
+ | DarkGray
+ | LightBlue
+ | LightGreen
+ | LightCyan
+ | LightRed
+ | Pink
+ | 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