ATS2: need help with arrays

[ice.r...@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)

[Dambaev Alexander]

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.r...@gmail.com>:

--
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-user...@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.

[Hongwei Xi]

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}

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-user...@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.

[Dambaev Alexander]

ah. my bad: I had actually used
```

fun poll

      {n: nat | n > 0}{l: addr}

      ( 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#"

```

But misplaced refinement spec, while was writing email.

[gmhwxi]

  >> (* 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)? *)

You have an array of size 1 in your code.

prval (pf1, pf2) = array_v_uncons(fds_pf)

val () = !fds_addr.fd = ...

val () = !fds_addr.events = ...

val () = !fds_addr.revents = ...

prval pf2 = array_v_unnil_nil(pf2)

prval () = fds_pf := array_v_uncons(pf1, pf2)

This can be quite involved. In general, writing C-style code in ATS2 is labor intensive :(