fun {n: nat | n > 0}{l: addr}
poll
should be changed to
fun poll{n: nat | n > 0}{l: addr}
Or you can write
fun poll{n:pos}{l: addr}
On Tue, Jul 7, 2020 at 3:31 AM Dambaev Alexander <ice.redm...@gmail.com>
wrote:
> Missed the return type of poll()
> ```
> fun {n: nat | n > 0}{l: addr}
> poll
> ( fds_pf: !array_v( pollfd_t, l, n) >> _ (* proof, that we have
> access to address range (l,n), which contains initialized array of elements
> of type pollfd_t *)
> | fds: ptr l (* address *)
> , nfds: size_t n (* range size *)
> , timeout: int
> ): int = "ext#"
> ```
>
>
> вт, 7 июл. 2020 г. в 07:28, ice.r...@gmail.com <ice.redm...@gmail.com>:
>
>>
>> Hi,
>> I need to provide a type for exteenal call poll() from libc.
>>
>> My initial try was that:
>> ```
>> typedef pollfd_t = $extype_struct"struct pollfd" of
>> { fd = int
>> , events = sint
>> , revents = sint
>> }
>> fun {n: nat | n > 0}{l: addr}
>> poll
>> ( fds_pf: !array_v( pollfd_t, l, n) >> _ (* proof, that we have
>> access to address range (l,n), which contains initialized array of elements
>> of type pollfd_t *)
>> | fds: ptr l (* address *)
>> , nfds: size_t n (* range size *)
>> , timeout: int
>> ) = "ext#"
>> ```
>>
>> Then I try to use it:
>> ```
>> fn foo(): void = {
>> val nfds = g1int2uint_int_size(1)
>> val (fds_pf, fds_free_pf | fds_addr) = array_ptr_alloc<pollfd_t>(nfds)
>> (* how should I initialize array here so fds_pf will switch it's type
>> from array_v(pollfd_t?, l, nfds) into array_v(pollfd_t, l, nfds)? *)
>> val _ = poll( fds_pf | fds_addr, nfds)
>> val () = array_ptr_free( fds_pf, fds_free_pf | fds_addr)
>> }
>> ```
>>
>> I was not able to understand how should I proof to compiler,. that I had
>> initialized array at fds_addr. I had tried to use `array_iforeach`, but it
>> does not require any proofs, so fds_pf keeps being uninitialized
>>
>> Based on:
>> 1. type of array_ptr_free (which expects fds_pf to be of type
>> array_v(pollfd_t?,l,n));
>> 2. the fact, that most of functions in array.sats are working with flat
>> arrays, for example, array_iforeach, which has type
>> ```
>> fun {a:vt0p}
>> array_iforeach
>> {n:int}
>> ( A0: &(@[INV(a)][n]) >> @[a][n]
>> , asz: size_t(n)
>> ) : sizeLte(n) // end of [array_iforeach]
>> ```
>> I conclude, that I misunderstood the purpose of array_v and it's
>> interconnection with flat arrays.
>>
>> So my questions are:
>> 1. what should be the type of poll()?
>> 2. Am I using array_v(pollfd_t,l,n) correctly or is there other
>> motivation behind array_v?
>> 3. why array_foreach and etc do not require proofs?
>> 4. And how could I switch fds_pf's type from uninitialized to initialized
>> array with some library function (I saw the implementation of
>> array_ptr_tabulate in the tutorial, but I thought, that if std library does
>> not use similar types for functions, then I misunderstood something)
>>
>> --
>> You received this message because you are subscribed to a topic in the
>> Google Groups "ats-lang-users" group.
>> To unsubscribe from this topic, visit
>> https://groups.google.com/d/topic/ats-lang-users/w6OiwDxucBM/unsubscribe.
>> To unsubscribe from this group and all its topics, 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/558eb0ab-3306-45e6-ad62-5054afbe26ebn%40googlegroups.com
>> <https://groups.google.com/d/msgid/ats-lang-users/558eb0ab-3306-45e6-ad62-5054afbe26ebn%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/CAHjn2Kzy3_ntef7S%2BdDGGNnONAGwvsxO%2BmmaPa0D5NNQx-oO7A%40mail.gmail.com
> <https://groups.google.com/d/msgid/ats-lang-users/CAHjn2Kzy3_ntef7S%2BdDGGNnONAGwvsxO%2BmmaPa0D5NNQx-oO7A%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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrP6oh95aMsTYbsQkJiRR_GGh4gP6KwnYHT2hoCC1Nxng%40mail.gmail.com.
