Re: Solving compiler error

2020-08-31 Thread Dambaev Alexander 
*Kiwamu: *wow, thanks for your trust, but after my quick view of your wiki
page http://jats-ug.metasepi.org/doc/ATS2/ATS_Foundations/showtype.html and
at the moment, I don't think, that I can add much more to it





















*Hongwei: thanks, you are right. glib's bindings provide 2 separate SATS
files: glib.sats and glib-object.sats, so I created a sats file, in which I
had included those 2 SATS files with '#include' pragma and used this one
sats file for staloading. I wanted to get this:```main.datsstaload
GLIB="glib-ext.sats"(* $GLIB.glib1 available here *)(* $GLIB.glib2
available here *)``glib-ext.sats#include
"contrib/glib/SATS/glib.sats"#include "contrib/glib/SATS/glib-object.sats"
(* staloads glib.sats *)``contrib/glib/SATS/glib.satsfn
glib1():void``contrib/glib/SATS/glib-object.satsfn glib2():void``` So
for now I have to staload them both in all modules, in which I need to use
declarations from both. As far as I understand, there is no other way to
achieve the same case without using #include pragma, am I right?Other than
that, is it ok for compiler to not to throw an error of multiple
declarations of gpointer?*

-- 
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/CAHjn2KxAnsELa38_HvB49_YY2LmUOj6RVhbkc8oC3LXSJ6ubBg%40mail.gmail.com.

Re: Solving compiler error

2020-08-31 Thread Hongwei Xi 
*'#include' means copy/paste. It is not meant to be used*

*in the following manner:*

*```glib-ext.sats*


*#include "contrib/glib/SATS/glib.sats"#include
"contrib/glib/SATS/glib-object.sats" (* staloads glib.sats *)*
*```*

*You can create glib-ext.hats containing the following lines:*


*#staload "contrib/glib/SATS/glib.sats"#staload
"contrib/glib/SATS/glib-object.sats" (* staloads glib.sats *)*

*Then add the following line*


*#include "glib-ext.hats"*

*This allows you to staload both glib.sats and glib-object.sats*

*Here is a real example:*

*https://github.com/githwxi/ATS-Postiats/blob/master/share/HATS/atspre_staload_prelude.hats
*


*By the way, '#staload' is idempotent. Staloading a file multiple times
causes NO problems:*

*#staload "contrib/glib/SATS/glib.sats"*
*#staload "contrib/glib/SATS/glib.sats"*



On Mon, Aug 31, 2020 at 5:30 AM Dambaev Alexander 
wrote:

> *Kiwamu: *wow, thanks for your trust, but after my quick view of your
> wiki page
> http://jats-ug.metasepi.org/doc/ATS2/ATS_Foundations/showtype.html and at
> the moment, I don't think, that I can add much more to it
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
> *Hongwei: thanks, you are right. glib's bindings provide 2 separate SATS
> files: glib.sats and glib-object.sats, so I created a sats file, in which I
> had included those 2 SATS files with '#include' pragma and used this one
> sats file for staloading. I wanted to get this:```main.datsstaload
> GLIB="glib-ext.sats"(* $GLIB.glib1 available here *)(* $GLIB.glib2
> available here *)``glib-ext.sats#include
> "contrib/glib/SATS/glib.sats"#include "contrib/glib/SATS/glib-object.sats"
> (* staloads glib.sats *)``contrib/glib/SATS/glib.satsfn
> glib1():void``contrib/glib/SATS/glib-object.satsfn glib2():void``` So
> for now I have to staload them both in all modules, in which I need to use
> declarations from both. As far as I understand, there is no other way to
> achieve the same case without using #include pragma, am I right?Other than
> that, is it ok for compiler to not to throw an error of multiple
> declarations of gpointer?*
>
> --
> 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/CAHjn2KxAnsELa38_HvB49_YY2LmUOj6RVhbkc8oC3LXSJ6ubBg%40mail.gmail.com
> 
> .
>

-- 
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/CAPPSPLr8RT%3DV5ocOuBd%2BVdGA9sXtNT73n4trGnce2G9WR6ckKw%40mail.gmail.com.

How to specify a concrete type on absvtype?

2020-08-31 Thread 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

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

Re: How to specify a concrete type on absvtype?

2020-08-31 Thread Hongwei Xi 
The variable 'opts' is uninitialized but shared_make requires something
that is initialized.


On Mon, Aug 31, 2020 at 8:47 PM Kiwamu Okabe  wrote:

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

-- 
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/CAPPSPLrhJWhEA3ixDy5ZzkZi9BKXC%3Dp-3K07jPYEh9TMK%3Dsq2w%40mail.gmail.com.

Re: How to specify a concrete type on absvtype?

2020-08-31 Thread Kiwamu Okabe 
On Tue, Sep 1, 2020 at 10:37 AM Hongwei Xi  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,
--
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/CAEvX6dkYbjEuG6mQA%2BWTu2ZPpVHptoGApGc_JC14J4QJcdmAJA%40mail.gmail.com.