int to string conversion implementation

3 files changed, 73 insertions, 4 deletions

diff --git a/kernel/interrupts/idt.dats b/kernel/interrupts/idt.dats
index ba6bb20..851a2b0 100644
--- a/kernel/interrupts/idt.dats
+++ b/kernel/interrupts/idt.dats
@@ -64,7 +64,7 @@ var idt : @[idt_entry_t][IDT_MAX_DESCRIPTORS] // The table
 var idtr : idtr_t // interrupt descriptor table register instance
 
 fun idt_set_descriptor  {n : nat | n < IDT_MAX_DESCRIPTORS} (vector: int n, isr: uint64, flags: uint8) : void = let
-  extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (@[idt_entry_t][IDT_MAX_DESCRIPTORS]@l)
+  extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (@[idt_entry_t][IDT_MAX_DESCRIPTORS]@l) // takeout proof  UNSAFE:
   prval (pf, fpf) = __assert (addr@(idt))
   val x = $UN.cast{uint64}(0xFFFF)
   val y = $UN.cast{uint64}(0xFFFFFFF)
@@ -118,7 +118,7 @@ end
 
 implement idt_init() : void = let 
   extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (idtr_t@l)
-  prval (pf, fpf) = __assert (addr@(idtr))
+  prval (pf, fpf) = __assert (addr@(idtr)) // takeout proof  UNSAFE:
 in 
   idtr.base := addr@(idt);
   idtr.limit := $UN.cast(8 * IDT_MAX_DESCRIPTORS);
diff --git a/kernel/itoa.dats b/kernel/itoa.dats
new file mode 100644
index 0000000..7557dac
--- /dev/null
+++ b/kernel/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 to string  UNSAFE: 
+in
+  let prval () = fpf(pf) in end;
+  str // Return string
+end
+
+end
diff --git a/kernel/output/print.dats b/kernel/output/print.dats
index 22fe575..9b5def0 100644
--- a/kernel/output/print.dats
+++ b/kernel/output/print.dats
@@ -2,14 +2,20 @@
 
 #define ATS_DYNLOADFLAG 0
 
+
 staload "kernel/output/writer.sats"
+staload "kernel/itoa.dats"
 
 extern fun print_newline() : void
-implement print_newline() : void = put_string("\n")
+implement print_newline() = put_string("\n")
 
 extern fun assert_errmsg(b: bool, msg: string) : void
-implement assert_errmsg(b: bool, msg: string) : void = put_string(msg)
+implement assert_errmsg(b,msg) = if (~b) then put_string(msg)
 
+extern fun print_int {n : nat | n > 0} (n : int n) : void 
+implement print_int(n) = put_string(itoa(n,10))
+ 
 overload print with put_string of 1
+overload print with print_int of 1
 
 macdef assertloc(tf) = assert_errmsg (,(tf), $mylocation)