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.
