From 947331444708d2dc622ad6d8d3eb069e29a1898f Mon Sep 17 00:00:00 2001
From: Xander <xander@biltopia.org>
Date: Thu, 13 Jul 2023 21:41:37 +0200
Subject: Allow negative number conversion

---
 kernel/interrupts/idt.dats     |  6 +++---
 kernel/prelude/DATS/print.dats |  2 +-
 lib/DATS/itoa.dats             | 34 +++++++++++++++++++++++++---------
 3 files changed, 29 insertions(+), 13 deletions(-)

diff --git a/kernel/interrupts/idt.dats b/kernel/interrupts/idt.dats
index ea25ced..0b91253 100644
--- a/kernel/interrupts/idt.dats
+++ b/kernel/interrupts/idt.dats
@@ -43,7 +43,7 @@ end
 extern fun default_exception_handler_e2(frame: &int_frame, error_code : uint64) : void = "mac#"
 implement default_exception_handler_e2(frame,error_code) = let
 in
-  println!("DEFAULT EXCEPTION HANDLER - WIDTH ERROR CODE");
+  println!("DEFAULT EXCEPTION HANDLER - WIDTH ERROR CODE:", $UN.cast{int}(error_code));
 end
 
 extern fun default_interrupt_handler2(frame: &int_frame) : void = "mac#"
@@ -52,10 +52,10 @@ in
   println!("DEFAULT INTERRUPT HANDLER - NO ERROR CODE");
 end
 
-extern fun default_interrupt_handler_e2(frame: &int_frame, error_code : uint64) : void = "mac#"
+extern fun default_interrupt_handler_e2 (frame: &int_frame, error_code : uint64) : void = "mac#"
 implement default_interrupt_handler_e2(frame,error_code) = let
 in
-  println!("DEFAULT INTERRUPT HANDLER - WIDTH ERROR CODE");
+  println!("DEFAULT INTERRUPT HANDLER - WIDTH ERROR CODE:", $UN.cast{int}(error_code));
 end
 
 //-------------------------------------------------------
diff --git a/kernel/prelude/DATS/print.dats b/kernel/prelude/DATS/print.dats
index 5049a98..6d378fa 100644
--- a/kernel/prelude/DATS/print.dats
+++ b/kernel/prelude/DATS/print.dats
@@ -11,7 +11,7 @@ implement print_newline() = put_string("\n")
 extern fun assert_errmsg(b: bool, msg: string) : void
 implement assert_errmsg(b,msg) = if (~b) then put_string(msg)
 
-extern fun print_int {n : nat | n > 0} (n : int n) : void 
+extern fun print_int (n : int) : void 
 implement print_int(n) = put_string(itoa(n,10))
  
 overload print with put_string of 1
diff --git a/lib/DATS/itoa.dats b/lib/DATS/itoa.dats
index 35b8c47..2fef14c 100644
--- a/lib/DATS/itoa.dats
+++ b/lib/DATS/itoa.dats
@@ -31,11 +31,12 @@ 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
+extern fun itoa  {n:nat | n > 1 && n < 33} (value : int, base : int n) : [k : nat | k < BUFFER_SIZE] string k
 implement itoa(value,base) = let
   prval (pf , fpf) = __assert(addr@buffer) // Get proofs  UNSAFE:
+  val offset = (if(value < 0) then 1 else 0) : [n: nat | n == 0 || n == 1] int n
 
-  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
+  fun loop {i : nat | i < BUFFER_SIZE} {l:addr} (pf : !(@[char][BUFFER_SIZE] @ l) | p : ptr l , n : int, i : int i): void = let
     val r = n % base
     val k = n / base
   in
@@ -48,16 +49,31 @@ implement itoa(value,base) = let
       if (k > 0) then
         loop(pf | p, k, succ(i))
       else (
-        p->[succ(i)] := '\0';
-        reverse(pf | p, sz2i(i)))
+        p->[i+1+offset] := '\0';
+        reverse(pf | p, i+offset)
+      )
   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
+  
+  if (value != 0) then
+    loop(pf | addr@buffer, abs(value), 0)
+  else (
+    buffer[0] := '0';
+    buffer[1] := '\0'
+  );
+
+  if (value < 0) then
+    buffer[0] := '-';
+
+  // Run loop
+  let 
+    val str = char_arr2string(buffer) // Convert arr to string  UNSAFE: 
+    prval () = fpf(pf)
+  in 
+    str // Return string
+  end 
+
 end
 
 end
-- 
cgit v1.2.3