Surprising answer, because I don't understand the details at the moment.
It comes earlier than I expected. But I will take the chance. Thanks.
Am 25.07.20 um 21:32 schrieb Hongwei Xi:
Your code should work if you add the following lines
at the beginning:
prfun
lemma_char_size()
: [sizeof(char) > 0] void
prval () = lemma_char_size()
These lines tell the type-checker that sizeof(char) is positive.
Right now, the type system only knows that 'sizeof(char)' is an int.
On Sat, Jul 25, 2020 at 9:59 AM [email protected]
<mailto:[email protected]> <[email protected]
<mailto:[email protected]>> wrote:
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 [email protected]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/9e71a4f6-6be7-44ed-8e61-c7b44d260b34o%40googlegroups.com
<https://groups.google.com/d/msgid/ats-lang-users/9e71a4f6-6be7-44ed-8e61-c7b44d260b34o%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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 [email protected]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoo4t-5ZisDftmGV1rUuHLqnuLWiw_he%3DLQYY2PUww9ZA%40mail.gmail.com
<https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoo4t-5ZisDftmGV1rUuHLqnuLWiw_he%3DLQYY2PUww9ZA%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/3159e612-bc45-e896-f00a-776c03261c2d%40bejocama.de.
