it works when you alias view of opts and proof, that x is the same as
addr@opts
```
implement main0 () = let
var opts: ip6_pktopts with opts_pf
var inp: inpcb
val () = inp.in6p_outputopts := addr@opts
val () = inp.sh := shared_make(opts_pf | addr@opts)
val (pf_oopts | x, count) = shared_unref(inp.sh)
val () = assertloc(count <= 1)
prval Some_v(pf_opts) = pf_oopts
val () = assertloc( x = addr@opts)
prval () = opts_pf := pf_opts
in
ignoret(usleep(1000u))
end
```
вс, 30 авг. 2020 г. в 01:44, gmhwxi <gmh...@gmail.com>:
>
> shared(a) should be changed to shared(a, l) if you need to make sure that
> the returned
> proof is also of the view a@l (instead of a@l2 for some l2). Otherwise,
> you may have to
> do a bit of casting:
>
> extern
> prfun
> vborrow
> {a:view}(pf: !INV(a)): a
>
> implement main0 () = let
> var opts: ip6_pktopts
> var inp: inpcb
> prval pf = vborrow(view@opts)
> val () = inp.in6p_outputopts := addr@opts
> val () = inp.sh := shared_make(pf | addr@opts)
> val (pf_oopts | x, count) = shared_unref(inp.sh)
> val () = assertloc(count <= 1)
> prval Some_v(pf_opts) = pf_oopts
> prval () = $UN.castview0{void}(pf_opts)
> in
> ignoret(usleep(1000u))
> end
>
> On Saturday, August 29, 2020 at 9:26:38 PM UTC-4 Kiwamu Okabe wrote:
>
>> Dear Hongwei,
>>
>> On Sun, Aug 30, 2020 at 10:19 AM Hongwei Xi <gmh...@gmail.com> wrote:
>> > Well, you did not prove that the one returned is the same as the one
>> borrowed :)
>>
>> Umm... Do you mean following eats original `a@l`:
>>
>> ```ats
>> extern fun shared_make{a:vt@ype}{l:addr} (a@l | ptr l): shared(a)
>> ```
>>
>> and the following introduces another one?
>>
>> ```ats
>> extern fun shared_unref{a:vt@ype} (shared(a)): [l:addr][c:int]
>> (option_v(a@l, c <= 1) | ptr l, int c)
>> ```
>>
>> I would like to take more hints.
>> If I prove they have same `l:addr` in `shared(a:vt@ype)`, ATS2 accepts
>> them as the same?
>>
>> ```ats
>> absvtype shared(a:vt@ype) = [l:addr] (a@l | ptr l)
>> ```
>>
>> Best regards,
>> --
>> Kiwamu Okabe at METASEPI DESIGN
>>
> --
> 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/a6f5a77c-ea89-43d6-a7b0-4545b1d88c6en%40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/a6f5a77c-ea89-43d6-a7b0-4545b1d88c6en%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/CAHjn2KwbY1tY4qR3p52UUEe-ujxRL1WNiSoo8W3X90e%2BCOAC%2BA%40mail.gmail.com.
