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.redm...@gmail.com>:
> 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>:
>
>>
>> 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
>>
>>
>> On Fri, Jul 10, 2020 at 2:23 AM Hongwei Xi <gmh...@gmail.com> wrote:
>>
>>> 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/CAPPSPLqgDVOsUsH-O10YH6L_bkR4H4rOLSohp_Kk80FpGyuNOQ%40mail.gmail.com
>> <https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqgDVOsUsH-O10YH6L_bkR4H4rOLSohp_Kk80FpGyuNOQ%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/CAHjn2KxLHfAHuGYEiook0UNF_%2BBj-BObQi8rVvc4D%3DTSy9awrw%40mail.gmail.com.
