How to specify a concrete type on absvtype?

[Kiwamu Okabe]

Dear all,

Now I'm writing following code:

https://github.com/metasepi/postmortem/blob/master/Security-Advisory/FreeBSD-kernel/FreeBSD-SA-20:20.ipv6/Resolution/ATS2/error/main.dats

```ats
absvtype shared(a:vt@ype, l:addr) = (a@l | ptr l)
extern fun shared_make{a:vt@ype}{l:addr} (a@l | ptr l): shared(a, l)
// --snip--
implement main0() = let
var opts: ip6_pktopts
val sh_inp0 = shared_make{ip6_pktopts}(view@opts | addr@opts)
val sh_inp1 = shared_ref(sh_inp0)
val sh_inp2 = shared_ref(sh_inp0)
val sh_inp3 = shared_ref(sh_inp0)
val _ = athread_create_cloptr_exn (llam () => ip6_thread(sh_inp1))
// --snip--
in
ignoret(usleep(1000u))
end
```

I specified a concrete type `ip6_pktopts`, because I would like to dereference
the pointer kept in `shared`.
But the code causes following error:

```
patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC main.dats -lpthread
/home/kiwamu/src/metasepi-postmortem/Security-Advisory/FreeBSD-kernel/FreeBSD-SA-20:20.ipv6/Resolution/ATS2/error/main.dats:
3277(line=122, offs=44) -- 3286(line=122, offs=53): error(3): the
dynamic expression cannot be assigned the type [S2Eat(S2Etyrec(flt0;
npf=-1; ip6po_hlim=S2Ecst(int)), S2EVar(5377))].
/home/kiwamu/src/metasepi-postmortem/Security-Advisory/FreeBSD-kernel/FreeBSD-SA-20:20.ipv6/Resolution/ATS2/error/main.dats:
3277(line=122, offs=44) -- 3286(line=122, offs=53): error(3): mismatch
of static terms (tyleq):
The actual term is: S2Etop(knd=0; S2Eapp(S2Ecst(g0int_t0ype);
S2Eextkind(atstype_int)))
The needed term is: S2Eapp(S2Ecst(g0int_t0ype); S2Eextkind(atstype_int))
/home/kiwamu/src/metasepi-postmortem/Security-Advisory/FreeBSD-kernel/FreeBSD-SA-20:20.ipv6/Resolution/ATS2/error/main.dats:
3277(line=122, offs=44) -- 3286(line=122, offs=53): error(3): mismatch
of static terms (tyleq):
The actual term is: S2Etyrec(flt0; npf=-1; ip6po_hlim=S2Etop(knd=0;
S2Ecst(int)))
The needed term is: S2Etyrec(flt0; npf=-1; ip6po_hlim=S2Ecst(int))
/home/kiwamu/src/metasepi-postmortem/Security-Advisory/FreeBSD-kernel/FreeBSD-SA-20:20.ipv6/Resolution/ATS2/error/main.dats:
3277(line=122, offs=44) -- 3286(line=122, offs=53): error(3): mismatch
of static terms (tyleq):
The actual term is: S2Eat(S2Etyrec(flt0; npf=-1;
ip6po_hlim=S2Etop(knd=0; S2Ecst(int))); S2Evar(opts(8637)))
The needed term is: S2Eat(S2Etyrec(flt0; npf=-1;
ip6po_hlim=S2Ecst(int)); S2EVar(5377->S2Evar(opts(8637))))
patsopt(TRANS3): there are [1] errors in total.
exit(ATS): uncaught exception:
_2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
```

Does anyone know how to fix it?

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[Hongwei Xi]

The variable 'opts' is uninitialized but shared_make requires something that is initialized.

--
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/CAEvX6d%3D6A%3DtiL7-vJDtV%3DZbwPJ4hvzqFiLiGmOg3PTBu1NdNjQ%40mail.gmail.com.

[Kiwamu Okabe]

On Tue, Sep 1, 2020 at 10:37 AM Hongwei Xi <gmh...@gmail.com> wrote:
> The variable 'opts' is uninitialized but shared_make requires something that is initialized.

Thanks. It's fixed.

https://github.com/metasepi/postmortem/commit/1be2a88ef0dbdb7d908269d8172bb31152fd56d9

```ats

implement main0() = let
var opts: ip6_pktopts

val () = opts.ip6po_hlim := 0

val sh_inp0 = shared_make{ip6_pktopts}(view@opts | addr@opts)

```

And I found it's already explained at Wiki page:

https://github.com/githwxi/ATS-Postiats/wiki/Internal-types

> * S2Etop(knd=0; T) means T?

Thanks,