Hi,
after migrating the string functions in the lib of the linux kernel to ats
I'm now starting to
to improve the code in an ats sense. A first step was to change from
ptr0_get/set to
ptr1 (sure, still unsafe stuff - but better type checked regarding implicit
type conversions).
The code at the end demonstrates a little problem. ptr1_succ<char>(pp)
doesn't have the
property l:agz even pp has it. Second, looking on the template parameter of
ptr1_succ
I get vt0p which stands for viewt@ype. I cannot actually get this in sync
with documentation,
because a viewt@ype should be something like vtypedef VT(T:t@ype,l:addr) =
( T@l | ptr(l) ).
So I think the template parameter should be of t0p = t@ype. Otherwise I
have wrong expectations
in how to use these functions - and I don't really understand why my code
compiles.
Finally an last minute insight regarding the usage of ptr1_pred: l:addr | l
> (null + sizeof(a)) .. works -
without the null not. I know, in this case I should not be surprised. But
l,r:agz | r == (l + sizeof(a)) --
doesn't imply r >= l.
Here is the code - c-style strlen - very often called by the kernel and the
performance seems
to be good. The ptr0 version works (and also my pointer type modification
pgz):
#define ATS_DYNLOADFLAG 0
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
staload "prelude/SATS/unsafe.sats"
fn strlen{l:agz}(p:ptr(l)) : [r:nat] size_t(r) =
let
fun loop{ll:agz| ll >= l}(pp:ptr(ll)) : [r:agz| r >= ll] ptr(r) =
case+ ptr1_get<char>(pp) = '\0' of
| true => pp
| false => loop(ptr1_succ<char>(pp))
in
g1ofg0(cast{size_t}(loop(p) - p))
end
implement main0 () =
let
var s = @[char][4]('A','B','C','\0')
val x = strlen(addr@(s))
in
println!(x)
end
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/9e71a4f6-6be7-44ed-8e61-c7b44d260b34o%40googlegroups.com.
