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 matthias.wo...@bejocama.de < matthias.wo...@bejocama.de> 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 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 > <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 ats-lang-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoo4t-5ZisDftmGV1rUuHLqnuLWiw_he%3DLQYY2PUww9ZA%40mail.gmail.com.