#include "share/atspre_staload.hats"

#define ATS_DYNLOADFLAG 0


fn reverse {l : addr} {n,m:nat | n < m} (pf : !(@[char][m] @ l) | p : ptr l, n : int n) :<!wrt> void = let
  fun loop {i,j,n:nat | i < j && j < n} .<j-i>. (pf : !(@[char][n] @ l) | p : ptr l , i : int i, j : int j) :<!wrt> 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  {n:nat | n > 1 && n < 33} (value : int, base : int n) :<!wrt> [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 {i : nat | i < BUFFER_SIZE} {l:addr} .<BUFFER_SIZE - i>. (pf : !(@[char][BUFFER_SIZE] @ l) | p : ptr l , n : int, i : int i):<!wrt> 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->[i+1+offset] := '\0';
        reverse(pf | p, i+offset)
      )
  end

in
  
  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