Full restructure

7 files changed, 6 insertions, 193 deletions

diff --git a/kernel/interrupts/idt.dats b/kernel/interrupts/idt.dats
index 851a2b0..ea25ced 100644
--- a/kernel/interrupts/idt.dats
+++ b/kernel/interrupts/idt.dats
@@ -1,4 +1,4 @@
-#include "kernel/kernel_prelude.hats"
+#include "kernel/prelude/kernel_prelude.hats"
 
 #define ATS_DYNLOADFLAG 0
 
diff --git a/kernel/itoa.dats b/kernel/itoa.dats
deleted file mode 100644
index 7557dac..0000000
--- a/kernel/itoa.dats
+++ /dev/null
@@ -1,63 +0,0 @@
-#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 to string  UNSAFE: 
-in
-  let prval () = fpf(pf) in end;
-  str // Return string
-end
-
-end
diff --git a/kernel/main.dats b/kernel/main.dats
index 26db859..d6e29f4 100644
--- a/kernel/main.dats
+++ b/kernel/main.dats
@@ -1,4 +1,4 @@
-#include "kernel/kernel_prelude.hats"
+#include "./prelude/kernel_prelude.hats"
 
 staload "kernel/interrupts/idt.sats"
 
diff --git a/kernel/output/writer.dats b/kernel/output/writer.dats
deleted file mode 100644
index c7731f6..0000000
--- a/kernel/output/writer.dats
+++ /dev/null
@@ -1,91 +0,0 @@
-#include "kernel/kernel_prelude.hats"
-
-staload "./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/kernel/output/writer.sats b/kernel/output/writer.sats
deleted file mode 100644
index 65a2ea9..0000000
--- a/kernel/output/writer.sats
+++ /dev/null
@@ -1,32 +0,0 @@
-#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
diff --git a/kernel/output/print.dats b/kernel/prelude/DATS/print.dats
index 9b5def0..5049a98 100644
--- a/kernel/output/print.dats
+++ b/kernel/prelude/DATS/print.dats
@@ -2,9 +2,8 @@
 
 #define ATS_DYNLOADFLAG 0
 
-
-staload "kernel/output/writer.sats"
-staload "kernel/itoa.dats"
+staload "lib/SATS/writer.sats"
+staload "lib/DATS/itoa.dats"
 
 extern fun print_newline() : void
 implement print_newline() = put_string("\n")
diff --git a/kernel/kernel_prelude.hats b/kernel/prelude/kernel_prelude.hats
index 048cba1..eb1990d 100644
--- a/kernel/kernel_prelude.hats
+++ b/kernel/prelude/kernel_prelude.hats
@@ -3,10 +3,10 @@
 
 #include "share/atspre_staload.hats"
 
-staload "kernel/output/writer.sats"
+staload "lib/SATS/writer.sats"
 val () = clear_screen()
 
-staload "kernel/output/print.dats"
+staload "./DATS/print.dats"
 
 #endif