There are indeed two raw_pf in this case. Try this:
val (recv_buf_pf, raw_pf1 | _) = tmp prval () = raw_pf := raw_pf1 On Fri, Jul 10, 2020 at 2:16 AM Dambaev Alexander <ice.redm...@gmail.com> wrote: > 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.shalkha...@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.redm...@gmail.com> >> wrote: >> >> >> 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.redm...@gmail.com>: >> >>> 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.redm...@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 >>>> >>>> -- >>>> 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-users+unsubscr...@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 >>>> <https://groups.google.com/d/msgid/ats-lang-users/6826800e-17e0-4554-8470-3a7e304bc71bn%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/CAHjn2KzgHoKJMAVypUCv17xYrB%2BFoycUySXYJknvrNVackkGqw%40mail.gmail.com >> <https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KzgHoKJMAVypUCv17xYrB%2BFoycUySXYJknvrNVackkGqw%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/9E97682A-394E-4218-B590-EFADE0DA505B%40gmail.com >> <https://groups.google.com/d/msgid/ats-lang-users/9E97682A-394E-4218-B590-EFADE0DA505B%40gmail.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/CAHjn2Kxygbn9WykBZzmFeaGbn8W4K0_%2Bxr5gAvyMLRkqFMCDXA%40mail.gmail.com > <https://groups.google.com/d/msgid/ats-lang-users/CAHjn2Kxygbn9WykBZzmFeaGbn8W4K0_%2Bxr5gAvyMLRkqFMCDXA%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/CAPPSPLohqPB3-1e%3DLazNH5pzE0L3vvuJZn42isgxNAv3unb2qQ%40mail.gmail.com.