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.
