3 files changed, 23 insertions, 30 deletions

diff --git a/kernel/main.dats b/kernel/main.dats
index bbec179..9bff703 100644
--- a/kernel/main.dats
+++ b/kernel/main.dats
@@ -3,11 +3,4 @@
 staload "kernel/writer.sats"
 dynload "kernel/writer.dats"
 
-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 () = print_char('X')
diff --git a/kernel/writer.dats b/kernel/writer.dats
index 7d0383f..9ea10b8 100644
--- a/kernel/writer.dats
+++ b/kernel/writer.dats
@@ -4,6 +4,14 @@ staload "kernel/writer.sats"
 
 extern castfn i2u8 {n: nat} (i: int n): uint8 n
 
+extern fun get_vram():<> [l: agz] (@[screenChar][N] @ l | ptr l) = "mac#"
+
+extern prfun eat_writer (pf: writer): void
+
+%{^
+  #define get_vram() ((void *) 0xB8000 + 1988)
+%}
+
 fun color_value(c : color): uint8 = 
   case+ c of 
     | Black() => i2u8 0
@@ -26,32 +34,25 @@ fun color_value(c : color): uint8 =
 fun code_value(foreground: color, background:color): uint8 = 
   (color_value(background) << 4) lor color_value(foreground)
 
-fun output_char(c : char, writer : !writer) : void = let
-  val p = writer.buffer.1
-  val () = p->[writer.column_position] := @{ ascii_character = c , color_code = writer.color_code }
+fun put_char (c : char, writer: &writer) : void = let
+  val v = writer.buffer.1
+  val pos = writer.position
 in
-  ()
-end
+    v->[writer.position] := @{ ascii_character = c, color_code = writer.color_code};
 
-%{^
-  #define get_vram() ((void *) 0xB8000 + 1988)
-%}
-
-extern fun get_vram():<> [l: addr] (@[screenChar][N] @ l | ptr l) = "mac#"
-
-extern prfun eat_writer (pf: writer): void
-
-extern castfn uint8_of {n: nat} (i: int n): uint8 n
+    if (pos < N - 1) then
+      writer.position := succ(pos)
+end
 
 implement print_char(c : char) : void = let
   val (pf_vram | vram) = get_vram()
-  val writer = @{
-    column_position = i2sz 0,
-    color_code = code_value(Yellow,Black),
-    buffer = (pf_vram | vram)
-  }
+  var writer = @{position = 0, color_code = code_value(Black,Yellow), buffer = (pf_vram | vram)} : writer
 in 
-  output_char(c,writer);
+  put_char(c,writer);
+  put_char(c,writer);
+  put_char(c,writer);
+  put_char(c,writer);
+  put_char(c,writer);
   let prval () = eat_writer writer in () end
 end
 
diff --git a/kernel/writer.sats b/kernel/writer.sats
index c9b8814..43881b1 100644
--- a/kernel/writer.sats
+++ b/kernel/writer.sats
@@ -1,4 +1,4 @@
-#define N 80 * 25
+#define N 2000
 
 datatype color =
   | Black 
@@ -21,7 +21,6 @@ datatype color =
 
 typedef screenChar = @{ ascii_character = char, color_code = uint8}
 
-vtypedef tptr (a: t@ype, l:addr) = (a @ l | ptr l)
-vtypedef writer = [l: addr] [n:nat | n < N] @{ column_position = size_t n, color_code = uint8 , buffer = tptr(@[screenChar][N],l)}
+vtypedef writer  = [l : agz] @{position = [a:int | a >= 0 && a < N] int (a), color_code = uint8 , buffer = (@[screenChar][N] @ l | ptr l)}
 
 fun print_char(c : char) : void