1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
#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 {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 {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
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
|
