From 67245a7eebeb135427d50171fda7af58770afc6d Mon Sep 17 00:00:00 2001
From: Xander <xander@biltopia.org>
Date: Thu, 13 Jul 2023 00:52:37 +0200
Subject: Full restructure

---
 kernel/itoa.dats | 63 --------------------------------------------------------
 1 file changed, 63 deletions(-)
 delete mode 100644 kernel/itoa.dats

(limited to 'kernel/itoa.dats')

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
-- 
cgit v1.2.3