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.
