diff options
| author | Xander <xander@biltopia.org> | 2023-07-28 21:38:35 +0200 |
|---|---|---|
| committer | Xander <xander@biltopia.org> | 2023-07-28 21:38:35 +0200 |
| commit | b78762c92afee705e618f29f89897db8b45df3dd (patch) | |
| tree | 90833dc90cd3b58ee84d19357fb1d945d40823ec /lib/DATS/itoa.dats | |
| parent | c6ad352a25b6b1d45e56090ccc0432d123b043bc (diff) | |
| download | ats-os-b78762c92afee705e618f29f89897db8b45df3dd.tar.xz ats-os-b78762c92afee705e618f29f89897db8b45df3dd.zip | |
optional implementation of multboot 1
Diffstat (limited to 'lib/DATS/itoa.dats')
| -rw-r--r-- | lib/DATS/itoa.dats | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/lib/DATS/itoa.dats b/lib/DATS/itoa.dats index 2fef14c..29697b5 100644 --- a/lib/DATS/itoa.dats +++ b/lib/DATS/itoa.dats @@ -3,8 +3,8 @@ #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 +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]; @@ -23,7 +23,7 @@ local staload UN = "prelude/SATS/unsafe.sats" -extern castfn char_arr2string (arr : &(@[char][BUFFER_SIZE])) : [n : nat | n < BUFFER_SIZE] string n +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 @@ -31,12 +31,12 @@ 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 +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} (pf : !(@[char][BUFFER_SIZE] @ l) | p : ptr l , n : int, i : int i): void = let + 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 |