arrays and viewtypes

[ice.r...@gmail.com]

Hi,

I am trying to understand how to use array_foreach_env function to pass to fwork environment of more than 1 variables (of viewt@ype).

For example, I can successfully use following:

vtypedef VT = (array_v(char?, l, recv_sz | ptr l)

fn walker

    ( array_v(pollfd_t, fdsl, nfds)

    , x : &pollfd_t >> _

    , env: !VT

    ): void =

    (* body goes here *)

val tmp = (recv_buf_pf | recv_buf)

val () = array_foreach_funenv

               <pollfd_t>

               {array_v(pollfd_t, fdsl,nfds)}

               {VT}

               ( fds_pf | fds, nfds, walker, tmp)

val (recv_buf_pf | _) = tmp

But, as soon as I want to use VT of type

vtypedef VT = (array_v(char?, l, recv_sz) | ptr l, size_t recv_sz)

(* ... *)

val tmp = (recv_buf_pf | recv_buf, recv_sz)

(* .. *)

val (recv_buf_pf | _) = tmp

I am getting the following error:
error(3): mismatch of sorts:

the needed sort is [S2RTbas(S2RTBASimp(2; viewtype))];

the actual sort is [S2RTbas(S2RTBASimp(3; viewt0ype))].

How can I fix this error? Thanks in andvance

[Dambaev Alexander]

And again, I had mistyped one thing in initial email:

(* ... *)

var tmp = (recv_buf_pf | recv_buf) (* var instead of val in both similar lines *)

(* ... *)

чт, 9 июл. 2020 г. в 23:47, 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/A60YvQACw4c/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/6826800e-17e0-4554-8470-3a7e304bc71bn%40googlegroups.com.

[Dambaev Alexander]

For now, I have found the only way to achieve my goal is by using boxed tuples/boxed records:

vtypedef VT = (array_v(char?,l,recv_sz) | '( ptr l, size_t recv_sz))

(*...*)

var tmp = (recv_buf_pf | '( recv_buf, recv_sz))

I don't know if this a best way though, as I suppose, that boxed tuple is heap-allocated and I don't know how to cleanup such tuple without GC

чт, 9 июл. 2020 г. в 23:54, Dambaev Alexander <ice.r...@gmail.com>:

[Hongwei Xi]

I took a quick look. In this particular case, you could do

something like this:

datavtype VT =

VT of (array_v(char?,l,recv_sz) | ptr l, size_t recv_sz)

val env = VT ( ... )

val (   ) = array_foreach_funenv(...)

val+~VT(pf | p, sz)  = env

In this way, you get to free the created env.

In retrospect, the function array_foreach_funenv should probably

given the following type:

fun
{a:vt0p}
array_foreach_funenv
  {v:view}
  {vt:vt0p}
  {n:int}
  {fe:eff}
(
  pf: !v
| A0: &(@[INV(a)][n]) >> @[a][n], asz: size_t(n)
, f0: (!v | &a >> _, &vt) -<fun,fe> void, env: &vt >> vt
) :<fe> void

This function is supposed to be used to implement other similar

functions with more convenient interfaces.

Will try to get it right in ATS3 :)

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/CAHjn2KzgHoKJMAVypUCv17xYrB%2BFoycUySXYJknvrNVackkGqw%40mail.gmail.com.

[artyom.s...@gmail.com]

Hi Alexander,

I guess you could also pass a reference to a stack allocated variable, but that would probably be very difficult to use due to proofs, initialization and the fact you’d be using a tuple.

Much easier to use what you’ve already found or what Hongwei describes.

Sent from my iPhone

On 10 Jul 2020, at 04:12, Dambaev Alexander <ice.r...@gmail.com> wrote:



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/CAHjn2KzgHoKJMAVypUCv17xYrB%2BFoycUySXYJknvrNVackkGqw%40mail.gmail.com.

[Dambaev Alexander]

Hi,

Thanks for your answers.

For now, I had tried this:

vtypedef VT = [l1:agz]

                       ( array_v(char?, l, recv_sz)

                       , (ptr l, size_t recv_sz) @ l1

                       | ptr l1

                       )

(* ... *)

var raw with raw_pf = (recv_buf, recv_sz)

var tmp = (recv_buf_pf, raw_pf | addr@ raw)

val _ = array_foreach_funenv( ..., tmp)

val (recv_buf_pf, raw_pf | _) = tmp

But I am getting compile error:
error(3): the linear dynamic variable [raw_pf$4825(-1)] needs to be preserved but it is consumed instead.
error(3): the linear dynamic variable [raw_pf$4828(-1)] needs to be consumed but it is preserved with the type [S2Eat(S2Etyrec(flt0; npf=-1; 0=S2Eapp(S2Ecst(ptr); S2Evar(l(8545))), 1=S2Eapp(S2Ecst(size_t); S2Evar(recv_sz(8544)))), S2Evar(l1$8709(14460)))] instead.

so it looks like compiler thinks, that there are 2 different raw_pf proofs. Is it expected or had I found some bug?

Now I will try with datavtypes

пт, 10 июл. 2020 г. в 05:48, <artyom.s...@gmail.com>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9E97682A-394E-4218-B590-EFADE0DA505B%40gmail.com.

[Hongwei Xi]

There are indeed two raw_pf in this case.

Try this:

val (recv_buf_pf, raw_pf1 | _) = tmp

prval () = raw_pf := raw_pf1

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAHjn2Kxygbn9WykBZzmFeaGbn8W4K0_%2Bxr5gAvyMLRkqFMCDXA%40mail.gmail.com.

[Hongwei Xi]

Here is another possibility:

var raw = (recv_buf, recv_sz)

var tmp = (recv_buf_pf, view@raw | addr@ raw)

val _ = array_foreach_funenv( ..., tmp)

val (recv_buf_pf, raw_pf | _) = tmp

prval () = view@raw := raw_pf

[Dambaev Alexander]

Thanks, datavtype way is working, but I will try more to not to use heap, including latest suggestions

пт, 10 июл. 2020 г. в 06:26, Hongwei Xi <gmh...@gmail.com>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqgDVOsUsH-O10YH6L_bkR4H4rOLSohp_Kk80FpGyuNOQ%40mail.gmail.com.

[Dambaev Alexander]

This what worked at the end

val (recv_buf_pf, raw_pf1 | raw1) = tmp

val () = assert_errmsg( raw1 = addr@raw, "raw had been changed")

prval () = raw_pf := raw_pf1

So I had to prove, that pointer haven't been changed. The interesting thing is that I will not be able to use 'raw' after this: compiler says, that it is unable to search proof for it, but using 'raw1' is ok

пт, 10 июл. 2020 г. в 06:29, Dambaev Alexander <ice.r...@gmail.com>: