aboutsummaryrefslogtreecommitdiff
path: root/kernel/itoa.dats
diff options
context:
space:
mode:
authorXander <xander@biltopia.org>2023-07-13 00:52:37 +0200
committerXander <xander@biltopia.org>2023-07-13 00:52:37 +0200
commit67245a7eebeb135427d50171fda7af58770afc6d (patch)
tree38378d0507ee79f8631134ec24f94cf9969bc6e8 /kernel/itoa.dats
parente02a7e790650b31b713dde5c39ad6172c048f571 (diff)
downloadats-os-67245a7eebeb135427d50171fda7af58770afc6d.tar.xz
ats-os-67245a7eebeb135427d50171fda7af58770afc6d.zip
Full restructure
Diffstat (limited to 'kernel/itoa.dats')
-rw-r--r--kernel/itoa.dats63
1 files changed, 0 insertions, 63 deletions
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