1 files changed, 25 insertions, 9 deletions
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