from:"Hongwei Xi"

I see.

It may help if the existential quantifier [l:addr] is moved
out of the record:

vtypedef
rib_cmd_info = [l:addr]
@{
rc_rt = (rtentry @ l | ptr l)
}

But programming using such a type is still quite burdensome.
I do have some designs for low-level programming in ATS3 but
right now my hands are tied with the very task of implementing ATS3.


On Wed, Apr 7, 2021 at 12:50 AM Kiwamu Okabe  wrote:

> On Tue, Apr 6, 2021 at 3:50 PM Hongwei Xi  wrote:
> > vtypedef rib_cmd_info = @{
> >   rc_rt = [l:addr] (rtentry @ l | ptr l)
> > }
> >
> > It seems that you are trying to do C-style programming in ATS directly.
> This would
> > be difficult; it may not even be practical for large scale programming.
>
> But... Another person tried to use the style:
>
> https://github.com/xlq/aos/blob/master/vga-text.dats#L37
>
> 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%3D6TJddME53Y%2BzjdAinb0DhZiyAmhDd4j7gZ8jeL%2BGGfw%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/CAPPSPLqukzL6EzxgN2Zje7PR4hRAMTv9ANUrY_V08LAj7m21MA%40mail.gmail.com.

Re: How to use the datavtype for tagged union?

Okay. I put some 'topize' functions in basic_dyn.dats.
Changes have been uploaded.

On Tue, Apr 6, 2021 at 3:44 AM Kiwamu Okabe  wrote:

> Dear Hongwei,
>
> On Tue, Apr 6, 2021 at 3:32 PM Hongwei Xi  wrote:
> > >>I feel the uninitize function is not safe...
> >
> > Such a function is always safe as initialized data can always
> > be treated as uninitialized.
>
> I understood.
> If so, could you include the `uninitize` praxi on ATS3 prelude library?
>
> I think this idiom is common for all of ATS programmer.
>
> 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%3DGG%2BiU8%2B_JiK%3D6zrC0WBQyRTM8BcD7FJQ5P0jFLGxaRA%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/CAPPSPLoXZDkaSeX6z5XEhr6RCkPDXPXqJcq9%2BCJ6mnPOD8yyUA%40mail.gmail.com.

Re: How to use view in vtypedef?

It is difficult to work as the following type as one cannot easily take out
the rc_rt
component:

vtypedef rib_cmd_info = @{
  rc_rt = [l:addr] (rtentry @ l | ptr l)
}

It seems that you are trying to do C-style programming in ATS directly.
This would
be difficult; it may not even be practical for large scale programming.


On Tue, Apr 6, 2021 at 2:11 AM Kiwamu Okabe  wrote:

> Dear all,
>
> I'm trying to write following code:
>
> ```ats
> #include "share/atspre_define.hats"
> #include "share/atspre_staload.hats"
>
> #define RTM_DELETE 0x2
> #define ENOTSUP 45
>
> typedef rtentry = @{
>   member_a = int
> }
>
> typedef nhop_object = @{
>   member_b = int
> }
>
> vtypedef rib_cmd_info = @{
>   rc_rt = [l:addr] (rtentry @ l | ptr l)
> }
>
> fun rtsock_routemsg
> {l1,l2:addr}
> (pfrt: !rtentry@l1, pfnh: !nhop_object@l2 | cmd: int, rt: ptr l1, nh:
> ptr l2, fibnum: int):
> int =
>   cmd + !rt.member_a + !nh.member_b
>
> fun rib_del_route
> {l:addr}
> (pf: !rib_cmd_info? >> rib_cmd_info @ l | rc: ptr l):
> int =
>   undefined()
>
> fun rib_action
> {l:addr}
> (pf: !rib_cmd_info? >> rib_cmd_info @ l | action: int, rc: ptr l):
> int =
>   case+ action of
> | RTM_DELETE => rib_del_route(pf | rc)
> | _ => ENOTSUP
>
> implement main0 () = {
>   var rc: rib_cmd_info
>   prval pfrc = view@rc
>   val error = rib_action(pfrc | RTM_DELETE, addr@rc)
>   prval () = view@rc := pfrc
> }
> ```
>
> But above code causes following error:
>
> ```
> $ patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC main.dats -lpthread
>
> /home/kiwamu/src/metasepi-postmortem/PR/FreeBSD-kernel/253800/Resolution/ATS2/fix/main.dats:
> 694(line=36, offs=35) -- 696(line=36, offs=37): error(3): the function
> argument needs to be a left-va
> lue.
>
> /home/kiwamu/src/metasepi-postmortem/PR/FreeBSD-kernel/253800/Resolution/ATS2/fix/main.dats:
> 680(line=36, offs=21) -- 702(line=36, offs=43): error(3): the linear
> dynamic variable [pf$4748(-1)] i
> s preserved but with an incompatible type.
>
> /home/kiwamu/src/metasepi-postmortem/PR/FreeBSD-kernel/253800/Resolution/ATS2/fix/main.dats:
> 680(line=36, offs=21) -- 702(line=36, offs=43): error(3): mismatch of
> static terms (tyleq):
> The actual term is: S2Etyrec(flt0; npf=-1; rc_rt=S2Etop(knd=0;
> S2Eexi(l(8480); ; S2Etyrec(flt0; npf=1; 0=S2Eapp(S2Ecst(@);
> S2Ecst(rtentry), S2Evar(l(8480))), 1=S2Eapp(S2Ecst(ptr);
> S2Evar(l(8480)
> ))
> The needed term is: S2Eat(S2Etyrec(flt0; npf=-1;
> rc_rt=S2Eexi(l$8631(14298); ; S2Etyrec(flt0; npf=1;
> 0=S2Eapp(S2Ecst(@); S2Ecst(rtentry), S2Evar(l$8631(14298))),
> 1=S2Eapp(S2Ecst(ptr); S2Evar(l$8
> 631(14298)); S2Evar(l(8484)))
>
> /home/kiwamu/src/metasepi-postmortem/PR/FreeBSD-kernel/253800/Resolution/ATS2/fix/main.dats:
> 817(line=42, offs=26) -- 821(line=42, offs=30): error(3): the dynamic
> expression cannot be assigned t
> he type [S2Etyrec(flt0; npf=-1; rc_rt=S2Etop(knd=0; S2Eexi(l(8480); ;
> S2Etyrec(flt0; npf=1; 0=S2Eapp(S2Ecst(@); S2Ecst(rtentry),
> S2Evar(l(8480))), 1=S2Eapp(S2Ecst(ptr); S2Evar(l(8480)))].
>
> /home/kiwamu/src/metasepi-postmortem/PR/FreeBSD-kernel/253800/Resolution/ATS2/fix/main.dats:
> 817(line=42, offs=26) -- 821(line=42, offs=30): error(3): mismatch of
> static terms (tyleq):
> The actual term is: S2Eat(S2Etyrec(flt0; npf=-1; rc_rt=S2Etop(knd=0;
> S2Eexi(l(8480); ; S2Etyrec(flt0; npf=1; 0=S2Eapp(S2Ecst(@);
> S2Ecst(rtentry), S2Evar(l(8480))), 1=S2Eapp(S2Ecst(ptr); S2Evar(l
> (8480))); S2Evar(rc(8485)))
> The needed term is: S2Etyrec(flt0; npf=-1; rc_rt=S2Etop(knd=0;
> S2Eexi(l(8480); ; S2Etyrec(flt0; npf=1; 0=S2Eapp(S2Ecst(@);
> S2Ecst(rtentry), S2Evar(l(8480))), 1=S2Eapp(S2Ecst(ptr);
> S2Evar(l(8480)
> ))
>
> /home/kiwamu/src/metasepi-postmortem/PR/FreeBSD-kernel/253800/Resolution/ATS2/fix/main.dats:
> 744(line=39, offs=22) -- 875(line=44, offs=2): error(3): the linear
> dynamic variable [rc$view$5549(-1
> )] is preserved but with an incompatible type.
>
> /home/kiwamu/src/metasepi-postmortem/PR/FreeBSD-kernel/253800/Resolution/ATS2/fix/main.dats:
> 744(line=39, offs=22) -- 875(line=44, offs=2): error(3): mismatch of
> static terms (tyleq):
> The actual term is: S2Etyrec(flt0; npf=1; 0=S2Eapp(S2Ecst(@);
> S2Ecst(rtentry), S2Evar(l$8634$8635(14302))), 1=S2Eapp(S2Ecst(ptr);
> S2Evar(l$8634$8635(14302
> The needed term is: S2Ecst(ptr_type)
>
> /home/kiwamu/src/metasepi-postmortem/PR/FreeBSD-kernel/253800/Resolution/ATS2/fix/main.dats:
> 744(line=39, offs=22) -- 875(line=44, offs=2): error(3): mismatch of
> static terms (tyleq):
> The actual term is: S2Eexi(l$8634(14301); ; S2Etyrec(flt0; npf=1;
> 0=S2Eapp(S2Ecst(@); S2Ecst(rtentry), S2Evar(l$8634(14301))),
> 1=S2Eapp(S2Ecst(ptr); S2Evar(l$8634(14301)
> The needed term is: S2Ecst(ptr_type)
>
> /home/kiwamu/src/metasepi-postmortem/PR/FreeBSD-kernel/253800/Resolution/ATS2/fix/main.dats:
> 744(line=39, offs=22) -- 875(line=44, offs=2): error(3): mismatch of
> static terms (tyleq):
> The actual term is: S2Etyrec(flt0; npf=-1; rc_rt=S2Eexi(l$8634(14301);
> ;

Re: How to use the datavtype for tagged union?

>>I feel the uninitize function is not safe...

Such a function is always safe as initialized data can always
be treated as uninitialized.

On Tue, Apr 6, 2021 at 2:08 AM Kiwamu Okabe  wrote:

> Dear Hongwei,
>
> On Tue, Apr 6, 2021 at 3:00 PM Hongwei Xi  wrote:
> > It seems that you need to unintialize 'e' explicitly:
> > --snip--
> >   prval () = uninitize(e)
>
> Umm... We should take care to change uninitize it?
> The wg_input would like to take both:
>
> A. uninitized `e`
> B. initialized `e`
>
> I feel the uninitize function is not safe...
>
> 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%3DFmGs0x4HYEGU%2B2sGKf4cAW_Y_VhJCGwG%2Bb%3DDT4cL_xQ%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/CAPPSPLpF6pAx9%3D3fej-dZ_uyD7W_172Y4QKB1ZaBxCmRAnfmSQ%40mail.gmail.com.

Re: How to use the datavtype for tagged union?

It seems that you need to unintialize 'e' explicitly:

extern
praxi
uninitize
{a:t0ype}
(x: (a) >> a?): void

implement main0 () = {
  var e: wg_endpoint
  var so: sockaddr = Af_inet @{
sin_port = 1,
sin_addr = 2,
sin_zero = 3
  }
  var so6: sockaddr = Af_inet6 @{
sin6_port = 1,
sin6_flowinfo = 2,
sin6_addr = 3,
sin6_scope_id = 4
  }
//


  prval pre = view@e
  prval prso = view@so
  val () = wg_input(pre, prso | addr@e, addr@so)
  prval () = view@e := pre
  prval () = view@so := prso
//


  prval () = uninitize(e)
//


  prval pre = view@e
  prval prso6 = view@so6
  val () = wg_input(pre, prso6 | addr@e, addr@so6)
  prval () = view@e := pre
  prval () = view@so6 := prso6
}

On Mon, Apr 5, 2021 at 11:39 PM Kiwamu Okabe  wrote:

> But second calling `wg_input` causes error:
>
> ```ats
> #include "share/atspre_define.hats"
> #include "share/atspre_staload.hats"
>
> typedef sockaddr_in = @{
>   sin_port = int,
>   sin_addr = int,
>   sin_zero = int
> }
>
> typedef sockaddr_in6 = @{
>   sin6_port = int,
>   sin6_flowinfo = int,
>   sin6_addr = int,
>   sin6_scope_id = int
> }
>
> datatype sockaddr =
> | Af_inet of sockaddr_in
> | Af_inet6 of sockaddr_in6
>
> vtypedef wg_endpoint = @{
>   e_remote = sockaddr
> }
>
> fun wg_input
> {l1,l2:addr}
> (pfe: !wg_endpoint? @ l1 >> wg_endpoint @ l1, pfso: !sockaddr@l2 | e:
> ptr l1, so: ptr l2):
> void = let
> val () = !e.e_remote := !so
>   in
> ()
>   end
>
> implement main0 () = {
>   var e: wg_endpoint
>   var so: sockaddr = Af_inet @{
> sin_port = 1,
> sin_addr = 2,
> sin_zero = 3
>   }
>   var so6: sockaddr = Af_inet6 @{
> sin6_port = 1,
> sin6_flowinfo = 2,
> sin6_addr = 3,
> sin6_scope_id = 4
>   }
>
>   prval pre = view@e
>   prval prso = view@so
>   val () = wg_input(pre, prso | addr@e, addr@so)
>   prval () = view@e := pre
>   prval () = view@so := prso
>
>   prval pre = view@e
>   prval prso6 = view@so6
>   val () = wg_input(pre, prso6 | addr@e, addr@so6)
>   prval () = view@e := pre
>   prval () = view@so6 := prso6
> }
> ```
>
> ```
> $ patscc -o a.out main.dats -DATS_MEMALLOC_LIBC
> /home/kiwamu/src/practice-ats/tagged_union/main.dats: 1042(line=56,
> offs=21) -- 1045(line=56, offs=24): error(3): the dynamic expression
> cannot be assigned the type [S2Eat(S2Etyrec(flt0; npf=-1;
>  e_remote=S2Etop(knd=0; S2Ecst(sockaddr))), S2EVar(5246))].
> /home/kiwamu/src/practice-ats/tagged_union/main.dats: 1042(line=56,
> offs=21) -- 1045(line=56, offs=24): error(3): mismatch of static terms
> (tyleq):
> The actual term is: S2Ecst(sockaddr)
> The needed term is: S2Ecst(ptr_type)
> /home/kiwamu/src/practice-ats/tagged_union/main.dats: 1042(line=56,
> offs=21) -- 1045(line=56, offs=24): error(3): mismatch of static terms
> (tyleq):
> The actual term is: S2Etyrec(flt0; npf=-1; e_remote=S2Ecst(sockaddr))
> The needed term is: S2Etyrec(flt0; npf=-1; e_remote=S2Etop(knd=0;
> S2Ecst(sockaddr)))
> /home/kiwamu/src/practice-ats/tagged_union/main.dats: 1042(line=56,
> offs=21) -- 1045(line=56, offs=24): error(3): mismatch of static terms
> (tyleq):
> The actual term is: S2Eat(S2Etyrec(flt0; npf=-1;
> e_remote=S2Ecst(sockaddr)); S2Evar(e(8482)))
> The needed term is: S2Eat(S2Etyrec(flt0; npf=-1;
> e_remote=S2Etop(knd=0; S2Ecst(sockaddr)));
> S2EVar(5246->S2Evar(e(8482
> ```
>
> Following patch does fix the error:
>
> ```diff
> --- a/tagged_union/main.dats
> +++ b/tagged_union/main.dats
> @@ -51,6 +51,7 @@ implement main0 () = {
>prval () = view@e := pre
>prval () = view@so := prso
>
> +  var e: wg_endpoint
>prval pre = view@e
>prval prso6 = view@so6
>val () = wg_input(pre, prso6 | addr@e, addr@so6)
> ```
>
> How to re-use initialized argument on `wg_input` function?
>
> Best regards,
> --
> Kiwamu Okabe
>
> --
> 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%3Dzhbz4Oxtu1vTLjRBjov0pnxDKDrF16hoOmrADz0hoQg%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/CAPPSPLpYWpbK6i5MQNnj%2BW2qv_VBaVTxmRfd%3DbLRg2C%2BhsZoDg%40mail.gmail.com.

Re: How to use the datavtype for tagged union?

2021-04-05 Thread Hongwei Xi

>>val () = !e.e_remote := so

The original linear content in !e.e_remote is discarded, resulting in a
leak. Also, 'so' is
a pointer (instead of a sockaddr).



On Sun, Apr 4, 2021 at 1:33 AM Kiwamu Okabe  wrote:

> I think I miss-undertood datavtype.
> In this case, it doesn't need to depend to int.
>
> Following is a more simple version:
>
> ```ats
> #include "share/atspre_define.hats"
> #include "share/atspre_staload.hats"
>
> typedef sockaddr_in = @{
>   sin_port = int,
>   sin_addr = int,
>   sin_zero = int
> }
>
> typedef sockaddr_in6 = @{
>   sin6_port = int,
>   sin6_flowinfo = int,
>   sin6_addr = int,
>   sin6_scope_id = int
> }
>
> datavtype sockaddr =
> | Af_inet of sockaddr_in
> | Af_inet6 of sockaddr_in6
>
> vtypedef wg_endpoint = @{
>   e_remote = sockaddr
> }
>
> fun wg_input
> {l1,l2:addr}
> (pfe: !wg_endpoint@l1, pfso: !sockaddr@l2 | e: ptr l1, so: ptr l2):
> void = let
> val () = !e.e_remote := so
>   in
> ()
>   end
>
> implement main0 () = {
>   var e: wg_endpoint
>   var so: sockaddr
>   prval pre = view@e
>   prval prso = view@so
> //  val () = wg_input(pre, prso | e, so)
>   prval () = view@e := pre
>   prval () = view@so := prso
> }
> ```
>
> But above causes the other errors:
>
> ```
> $ patscc -o a.out main.dats -DATS_MEMALLOC_LIBC
> /home/kiwamu/src/practice-ats/tagged_union/main.dats: 511(line=29,
> offs=14) -- 528(line=29, offs=31): error(3): a linear component of the
> following type is abandoned: [S2Ecst(sockaddr)].
> /home/kiwamu/src/practice-ats/tagged_union/main.dats: 538(line=31,
> offs=5) -- 540(line=31, offs=7): error(3): the linear dynamic variable
> [pfe$4738(-1)] is preserved but with an incompatible typ
> e.
> /home/kiwamu/src/practice-ats/tagged_union/main.dats: 538(line=31,
> offs=5) -- 540(line=31, offs=7): error(3): mismatch of static terms
> (tyleq):
> The actual term is: S2Eapp(S2Ecst(ptr_addr_type); S2Evar(l2(8481)))
> The needed term is: S2Ecst(sockaddr)
> /home/kiwamu/src/practice-ats/tagged_union/main.dats: 538(line=31,
> offs=5) -- 540(line=31, offs=7): error(3): mismatch of static terms
> (tyleq):
> The actual term is: S2Etyrec(flt0; npf=-1;
> e_remote=S2Eapp(S2Ecst(ptr_addr_type); S2Evar(l2(8481
> The needed term is: S2Etyrec(flt0; npf=-1; e_remote=S2Ecst(sockaddr))
> /home/kiwamu/src/practice-ats/tagged_union/main.dats: 538(line=31,
> offs=5) -- 540(line=31, offs=7): error(3): mismatch of static terms
> (tyleq):
> The actual term is: S2Eat(S2Etyrec(flt0; npf=-1;
> e_remote=S2Eapp(S2Ecst(ptr_addr_type); S2Evar(l2(8481;
> S2Evar(l1(8480)))
> The needed term is: S2Eat(S2Etyrec(flt0; npf=-1;
> e_remote=S2Ecst(sockaddr)); S2Evar(l1(8480)))
> ```
>
> Something is wrong?
>
> Best regards,
> --
> Kiwamu Okabe
>
> --
> 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/CAEvX6dmgZGvdUkVG93ajPVscqD44A8t2P4_ucemqPkR%2BA52mCQ%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/CAPPSPLq9dGuDo-SkoLsX6u4SacUwhhbfuSSEupOqCq0wBoo-5g%40mail.gmail.com.

Re: How to avoid an unsolved constraint error on `if pagesizes > 0UL then pagesizes else 1UL`

2021-03-31 Thread Hongwei Xi

For such a use, you need a type annotation:

fun concat_exec_imgact {i:int} (pagesizes: ulint i): ulint = let
val
psize =
(
if
pagesizes > 0UL
then pagesizes else 1UL
) : [i:pos] ulint(i)
in
  concat_rnd_base(psize)
end

On Wed, Mar 31, 2021 at 8:31 AM Kiwamu Okabe  wrote:

> Dear all,
>
> I wrote following ATS code:
>
> ```ats
> #include "share/atspre_define.hats"
> #include "share/atspre_staload.hats"
>
> fun concat_rnd_base {i:int | i > 0}  (align: ulint i): ulint =
>   undefined()
>
> fun concat_exec_imgact {i:int} (pagesizes: ulint i): ulint = let
> val psize = if pagesizes > 0UL then pagesizes else 1UL
>   in
> concat_rnd_base(psize)
>   end
>
> implement main0 () = {
> }
> ```
>
> but above code causes following error:
>
> ```
> $ patscc main.dats
> .../main.dats: 302(line=10, offs=21) -- 307(line=10, offs=26):
> error(3): unsolved constraint: C3NSTRprop(C3TKmain();
> S2Eeqeq(S2Evar(i(8481)); S2Eintinf
> (1)))
> ```
>
> I belive the `psize` depends on `{i:int | i > 0}`.
> How to avoid the unsolved constraint error?
>
> 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/CAEvX6dnue3oRHsd0oFR9R1Y0WjsGfOu2YfYJ2pvpOm8mBHQBPQ%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/CAPPSPLrrAa7sxyhFQgDySRrL6gDd7vdQRdf%2BBjPdnzapckDPBg%40mail.gmail.com.

Re: Constraint solving (integer inequalities)

2021-02-10 Thread Hongwei Xi

The implementation of FM in ATS/Postiats is largely standard.

One small improvement lies in its handling of an inequality of the
following kind:

2x + 2y >= 1

This inequality is first changed to 2x + 2y >= 2 and then simplified to x +
y >= 1.

The implementation uses linear types to ensure efficient memory management,
which
is quite important as FM often needs to use a large amount of memory.




On Wed, Feb 10, 2021 at 7:48 PM Vanessa McHale  wrote:

> Hi all,
>
> I've read that ATS uses the Fourier-Mitzkin method to handle
> constraints/inequalities but what I've read has been light on details.
>
> Does ATS do anything interesting for integer constraints?
>
> (Also: where in the ATS compiler is the constraint-solving code? I've only
> looked a bit but I didn't find it at first glance).
>
> Cheers,
> Vanessa McHale
>
> --
> 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/9592166f-877e-43aa-bd9d-2cf0b178c286n%40googlegroups.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/CAPPSPLqLjyceWVmtr1QzdvOo6-1Wyu_m9XPRhbhchy%2BYGzXb-g%40mail.gmail.com.

Re: Having Trouble Using Call-By-Reference

2021-01-22 Thread Hongwei Xi

(x:   >> _) means that the argument is call-by-reference; the integer
in it may be updated.

BTW, (x: ) means that the argument is read-only call-by-reference, but
it is not enforced in ATS2

Note that ( >> _) is just a shorthand for ( >> T).



On Fri, Jan 22, 2021 at 8:24 AM d4v3y_5c0n3s  wrote:

> Thanks, this works perfectly!  By the way, what does the " >>  _"
> syntax mean in this case?
>
> On Friday, January 22, 2021 at 1:46:15 AM UTC-5 gmhwxi wrote:
>
>> There are a couple of issues. Maybe the following code is what
>> you wanted:
>>
>> fn chng_int_test ( i:  >> _ ) : void = i := i + 1
>>
>>
>> fn test_chnge () : int = let
>>   var i: int = 0
>>
>>   val () = chng_int_test(i)
>> in
>>   i
>> end
>> On Fri, Jan 22, 2021 at 12:51 AM d4v3y_5c0n3s  wrote:
>>
>>> I'm trying to use call by reference in the following example, but I'm
>>> running into issues trying to get it to compile.  It's late, so I'll
>>> explain more tomorrow, but any help is appreciated.
>>>
>>> fn chng_int_test ( i: ? >> _ ) : void = i + 1
>>>
>>> fn test_chnge () : int = let
>>> var i = 0
>>> val () = chng_int_test(i)
>>> in
>>> i
>>> end
>>>
>>> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 47(line=2, offs=46):
>>> error(3): the dynamic expression cannot be assigned the type
>>> [S2Eapp(S2Ecst(g1uint_int_t0ype); S2Eextkind(atstype_size), S2EVar(0))].
>>> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 47(line=2, offs=46):
>>> 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(g1uint_int_t0ype);
>>> S2Eextkind(atstype_size), S2EVar(0))
>>> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 51(line=2, offs=50):
>>> error(3): the linear dynamic variable [i$view$74(-1)] is preserved but with
>>> an incompatible type.
>>> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 51(line=2, offs=50):
>>> 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))
>>> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 51(line=2, offs=50):
>>> error(3): mismatch of static terms (tyleq):
>>> The actual term is: S2Eat(S2Etop(knd=0; S2Eapp(S2Ecst(g0int_t0ype);
>>> S2Eextkind(atstype_int))); S2Evar(i(4314)))
>>> The needed term is: S2Eat(S2Eapp(S2Ecst(g0int_t0ype);
>>> S2Eextkind(atstype_int)); S2Evar(i(4314)))
>>> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 51(line=2, offs=50):
>>> error(3): the dynamic expression cannot be assigned the type
>>> [S2Ecst(atsvoid_t0ype)].
>>> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 51(line=2, offs=50):
>>> error(3): mismatch of static terms (tyleq):
>>> The actual term is: S2Eapp(S2Ecst(g1uint_int_t0ype);
>>> S2Eextkind(atstype_size), S2Eapp(S2Ecst(add_int_int); S2EVar(0),
>>> S2Eintinf(1)))
>>> The needed term is: S2Ecst(atsvoid_t0ype)
>>> /tmp/patsopt_tcats_SwYDb2: 78(line=4, offs=26) -- 138(line=9, offs=4):
>>> error(3): the linear dynamic variable [i$view$75(-1)] is preserved but with
>>> an incompatible type.
>>> /tmp/patsopt_tcats_SwYDb2: 78(line=4, offs=26) -- 138(line=9, offs=4):
>>> error(3): mismatch of static terms (tyleq):
>>> The actual term is: S2Eapp(S2Ecst(g0int_t0ype); S2Eextkind(atstype_int))
>>> The needed term is: S2Eapp(S2Ecst(g1int_int_t0ype);
>>> S2Eextkind(atstype_int), S2Eintinf(0))
>>> /tmp/patsopt_tcats_SwYDb2: 78(line=4, offs=26) -- 138(line=9, offs=4):
>>> 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: S2Etop(knd=0; S2Eapp(S2Ecst(g1int_int_t0ype);
>>> S2Eextkind(atstype_int), S2Eintinf(0)))
>>> /tmp/patsopt_tcats_SwYDb2: 78(line=4, offs=26) -- 138(line=9, offs=4):
>>> error(3): mismatch of static terms (tyleq):
>>> The actual term is: S2Eat(S2Etop(knd=0; S2Eapp(S2Ecst(g0int_t0ype);
>>> S2Eextkind(atstype_int))); S2Evar(i(4313)))
>>> The needed term is: S2Eat(S2Etop(knd=0; S2Eapp(S2Ecst(g1int_int_t0ype);
>>> S2Eextkind(atstype_int), S2Eintinf(0))); S2Evar(i(4313)))
>>> patsopt(TRANS3): there are [4] errors in total.
>>> exit(ATS): uncaught exception:
>>> _2home_2hwxi_2Research_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
>>>
>>> --
>>> 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/b7580da8-275c-4d17-b796-90e81404ee5dn%40googlegroups.com
>>> 
>>> .
>>>
>> --
> You received this message because you are subscribed to the Google Groups
>

Re: Having Trouble Using Call-By-Reference

There are a couple of issues. Maybe the following code is what
you wanted:

fn chng_int_test ( i:  >> _ ) : void = i := i + 1

fn test_chnge () : int = let
  var i: int = 0
  val () = chng_int_test(i)
in
  i
end


On Fri, Jan 22, 2021 at 12:51 AM d4v3y_5c0n3s  wrote:

> I'm trying to use call by reference in the following example, but I'm
> running into issues trying to get it to compile.  It's late, so I'll
> explain more tomorrow, but any help is appreciated.
>
> fn chng_int_test ( i: ? >> _ ) : void = i + 1
>
> fn test_chnge () : int = let
> var i = 0
> val () = chng_int_test(i)
> in
> i
> end
>
> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 47(line=2, offs=46):
> error(3): the dynamic expression cannot be assigned the type
> [S2Eapp(S2Ecst(g1uint_int_t0ype); S2Eextkind(atstype_size), S2EVar(0))].
> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 47(line=2, offs=46):
> 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(g1uint_int_t0ype);
> S2Eextkind(atstype_size), S2EVar(0))
> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 51(line=2, offs=50):
> error(3): the linear dynamic variable [i$view$74(-1)] is preserved but with
> an incompatible type.
> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 51(line=2, offs=50):
> 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))
> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 51(line=2, offs=50):
> error(3): mismatch of static terms (tyleq):
> The actual term is: S2Eat(S2Etop(knd=0; S2Eapp(S2Ecst(g0int_t0ype);
> S2Eextkind(atstype_int))); S2Evar(i(4314)))
> The needed term is: S2Eat(S2Eapp(S2Ecst(g0int_t0ype);
> S2Eextkind(atstype_int)); S2Evar(i(4314)))
> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 51(line=2, offs=50):
> error(3): the dynamic expression cannot be assigned the type
> [S2Ecst(atsvoid_t0ype)].
> /tmp/patsopt_tcats_SwYDb2: 46(line=2, offs=45) -- 51(line=2, offs=50):
> error(3): mismatch of static terms (tyleq):
> The actual term is: S2Eapp(S2Ecst(g1uint_int_t0ype);
> S2Eextkind(atstype_size), S2Eapp(S2Ecst(add_int_int); S2EVar(0),
> S2Eintinf(1)))
> The needed term is: S2Ecst(atsvoid_t0ype)
> /tmp/patsopt_tcats_SwYDb2: 78(line=4, offs=26) -- 138(line=9, offs=4):
> error(3): the linear dynamic variable [i$view$75(-1)] is preserved but with
> an incompatible type.
> /tmp/patsopt_tcats_SwYDb2: 78(line=4, offs=26) -- 138(line=9, offs=4):
> error(3): mismatch of static terms (tyleq):
> The actual term is: S2Eapp(S2Ecst(g0int_t0ype); S2Eextkind(atstype_int))
> The needed term is: S2Eapp(S2Ecst(g1int_int_t0ype);
> S2Eextkind(atstype_int), S2Eintinf(0))
> /tmp/patsopt_tcats_SwYDb2: 78(line=4, offs=26) -- 138(line=9, offs=4):
> 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: S2Etop(knd=0; S2Eapp(S2Ecst(g1int_int_t0ype);
> S2Eextkind(atstype_int), S2Eintinf(0)))
> /tmp/patsopt_tcats_SwYDb2: 78(line=4, offs=26) -- 138(line=9, offs=4):
> error(3): mismatch of static terms (tyleq):
> The actual term is: S2Eat(S2Etop(knd=0; S2Eapp(S2Ecst(g0int_t0ype);
> S2Eextkind(atstype_int))); S2Evar(i(4313)))
> The needed term is: S2Eat(S2Etop(knd=0; S2Eapp(S2Ecst(g1int_int_t0ype);
> S2Eextkind(atstype_int), S2Eintinf(0))); S2Evar(i(4313)))
> patsopt(TRANS3): there are [4] errors in total.
> exit(ATS): uncaught exception:
> _2home_2hwxi_2Research_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
>
> --
> 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/b7580da8-275c-4d17-b796-90e81404ee5dn%40googlegroups.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/CAPPSPLreL%3DOzDipN%3DKh4EYZPpRFHRebS4aeJURfGw6TSvaR45Q%40mail.gmail.com.

Re: Support for OOP in some ATS3 extension (2)

I think I misunderstood your earlier message.

If I understand you correctly this time, then what you mentioned in this
message
can already be done in ATS2 (you need ats2cpp for using g++ on the generated
code):

https://github.com/githwxi/ATS-Postiats/tree/master/contrib/ats2cpp
https://github.com/githwxi/ATS-Postiats/tree/master/contrib/ats2cpp/STL

The code in STL shows a way to wrap linear and dependent types around
various
STL functions (stack, deque, etc.).

By the way, this is also what is planned for xats2cc, which aims at
compiling XATSCML to C/C++.


On Thu, Jan 21, 2021 at 5:36 PM Dambaev Alexander 
wrote:

> And that is why I dream about an ability to be able to render classes to
> Java/C++: as soon as we might have a XATSCML->Java / XATSCML->C++ translator
> Ie, to be able to render something like this:
>
>
> ```
>
> UCLASS()class AMyActor : public AActor{
> GENERATED_BODY()public:
>
> UPROPERTY(EditAnywhere, BlueprintReadWrite, Category="Damage")
> int32 TotalDamage;
>
> UPROPERTY(EditAnywhere, BlueprintReadWrite, Category="Damage")
> float DamageTimeInSeconds;
>
> UPROPERTY(BlueprintReadOnly, VisibleAnywhere, Transient, 
> Category="Damage")
> float DamagePerSecond;
>
> ...};
> ```
> https://docs.unrealengine.com/en-US/ProgrammingAndScripting/ProgrammingWithCPP/IntroductionToCPP/index.html
>
> Such that we should able to inject things like `UCLASS` into output or 
> `UPROPERTY`.
>
> At the same time, this means, that we can have a part of program, that is 
> written on a C++ and part, which had been rendered to C++ by ATS, such that 
> to use rendered parts borderlessly, we need to be able to describe 
> host-languages types in ATS, like:
> ```
>
> typedef std_vector(a:t0ype, n:int) = $extype_struct"std::vector"
>
> ```
>
> and then we should be able to use, say `push_back` either by using $extfcall 
> or being able to describe it in statics:
>
> ```
>
> extern fn {a:t0ype} push_back{n:nat} ( v: !std_vector(a, n) >> std_vector(a, 
> n+1), value: a): void
>
> ```
>
> but this means, that ATS should be able to render
> ```
>
>   val vec = (* some constructor *)
>
>   val () = push_back( vec, 1)
>
> ```
>
> into
> ```
>
>std::vector v;
>
>v. push_back( 1)
>
> ```
>
> Otherwise, ATS should render structures into host language and either make it 
> easy to use from target or we will have to marshall the data between target 
> language and ATS, but why do we need a translator into a target language
> if we still have to spent development time and CPU cycles to marshal data 
> from/to ATS? :)
>
>
> So what I mean is that there are a lot of 'mainstream' OOP languages, which 
> are being used for production, say Java and C++ and currently, in order to 
> write, say, non-C++ for Unreal Engine development, or non C# for Unity3D or
> non-Java for Android development, you sign for a pain of marshalling data and 
> writing a lot of bindings (for both sides: target language and higher level 
> language), ie, loosing the time in fighting against the platform in pursuit 
> of using
>  something more, that platform is not able to provide.
>
> So for me, it is clear, that ATS2 does the great job to eliminate the 
> fighting against C to a some extent: ie, ATS requires no marshalling and we 
> have $extfcall(), so in the case of 'I need to finish this today', we can use 
> a bunch of $extfcall()s for C libraries and it will
> not be a fighting against the C target.
> But, no matter how sad it is, I see a trend, where C API becomes obsolete. 
> Even GCC is now using C++ as a language of implementation. Many sources say 
> 'use Golang instead of C for most of your tasks' and C slowly becomes 
> 'language for kernel API
> or embedded' development, which means, that very few projects now provide C 
> libraries, which I can use a an ATS developer. For example: I know, that only 
> Godot engine provides C library, but neither Unity nor Unreal Engine. (or 
> maybe I'm wrong?)
> But if we imagine that someone had developed a translator to C++/Java/C#/Go - 
> will ATS-developer still be fighting against the platform? I think he will 
> fight against OOP platforms at least, as it will still require to manually 
> create classes at least, from which
>
> he will be able to call functions, rendered by ATS. And things like 
> std::vector, std::string and etc may require marshalling to/from ATS, even if 
> ATS itself renders into a target language...
>
>
>
> --
> 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/CAHjn2KzpLfvckjhsWqyOxEVTPy1avB_B0znx8YDz_4Obz_xD%3Dw%40mail.gmail.com
>

Re: Support for OOP in some ATS3 extension (2)

I simply meant 'don't-write-non-portable-code`.

Clearly, one can always write hard-to-port code in ATS.

I think that the real question is what kind of code one really wants to
port in the first place.

An executable ATS program looks like this: ATS-generic-stuff +
Target-language-runtime.
The first part is 100% portable, and the second part can be chosen
according to the target
language.

On Thu, Jan 21, 2021 at 1:01 PM Raoul Duke  wrote:

> How can that be when the methods for any given type in the host language
> are different across languages, sdks?
>
> On Thu, Jan 21, 2021 at 9:58 AM Hongwei Xi  wrote:
>
>> 100%, I suppose :)
>>
>>
>> On Thu, Jan 21, 2021 at 12:57 PM Raoul Duke  wrote:
>>
>>> To what degree are programs written in ATS expected to be portable
>>> across host languages?
>>>
>>> On Thu, Jan 21, 2021 at 9:54 AM Hongwei Xi  wrote:
>>>
>>>> Strictly speaking, ATS is an "abstract" language; the language itself
>>>> does not have primitive data types. When compiled to C, it uses the
>>>> data types defined by C; when to JS, it uses the data types defined
>>>> by JS; etc.
>>>>
>>>> On Thu, Jan 21, 2021 at 11:50 AM Raoul Duke  wrote:
>>>>
>>>>> $0.02
>>>>>
>>>>> In my limited/humble experience with FFI's the thing is not just being
>>>>> able to call out from the guest language to the host language, it is
>>>>> the return paths and the full round tripping and the overall semantics
>>>>> and the inevitable impedance mismatches that all sum up to make it an
>>>>> exercise in uselessness. Worst case things are like when the host
>>>>> string type != the guest string type, etc., etc, all the way up of
>>>>> course to bigger concepts like the host class implementation != the
>>>>> guest class implementation. Either there's a lot of extra cpu cycles
>>>>> spent on transmogriphying back and forth, or maybe things are worse
>>>>> and there ends up being 2 parallel things in the guest language and i
>>>>> have to manually convert.
>>>>>
>>>>> I do wish there were a master's thesis that studied the levels of
>>>>> integration among languages, both historically and in terms of
>>>>> technical possibilities, and specifically examined the end-developer
>>>>> UI and UX implications thereof, as well as the *ity issues like
>>>>> performance, security, et. al.
>>>>
>>>>
>>>>>
>>>>> --
>>>>> 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/CAJ7XQb6j28exxf1t%3D%3DceCLJFxDKf237R618ZkX2H0BxKmo4ZEQ%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/CAPPSPLoK34G7g3RSnKf5JXH3z8NewA_ZVaeXRxrqo3A5KGu7KQ%40mail.gmail.com
>>>> <https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoK34G7g3RSnKf5JXH3z8NewA_ZVaeXRxrqo3A5KGu7KQ%40mail.gmail.com?utm_medium=email_source=footer>
>>>> .
>>>>
>>> --
>>>
>> 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/snZWQK2YePY/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/CAJ7XQb4Fvt%2BjPWa2%3D%2BKsL_TKZ9dV4vVwyodW8KD8gi9Qkp9F7w%40mail.gmail.com
>>> <https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb4Fvt%2BjPWa2%3D%2BKsL_TKZ9dV4vVwyodW8KD8gi9Qkp9F7w%40mail.gmail.com?utm_medium=email_source=footer>
>>> .
>>&g

Re: Support for OOP in some ATS3 extension (2)

100%, I suppose :)


On Thu, Jan 21, 2021 at 12:57 PM Raoul Duke  wrote:

> To what degree are programs written in ATS expected to be portable across
> host languages?
>
> On Thu, Jan 21, 2021 at 9:54 AM Hongwei Xi  wrote:
>
>> Strictly speaking, ATS is an "abstract" language; the language itself
>> does not have primitive data types. When compiled to C, it uses the
>> data types defined by C; when to JS, it uses the data types defined
>> by JS; etc.
>>
>> On Thu, Jan 21, 2021 at 11:50 AM Raoul Duke  wrote:
>>
>>> $0.02
>>>
>>> In my limited/humble experience with FFI's the thing is not just being
>>> able to call out from the guest language to the host language, it is
>>> the return paths and the full round tripping and the overall semantics
>>> and the inevitable impedance mismatches that all sum up to make it an
>>> exercise in uselessness. Worst case things are like when the host
>>> string type != the guest string type, etc., etc, all the way up of
>>> course to bigger concepts like the host class implementation != the
>>> guest class implementation. Either there's a lot of extra cpu cycles
>>> spent on transmogriphying back and forth, or maybe things are worse
>>> and there ends up being 2 parallel things in the guest language and i
>>> have to manually convert.
>>>
>>> I do wish there were a master's thesis that studied the levels of
>>> integration among languages, both historically and in terms of
>>> technical possibilities, and specifically examined the end-developer
>>> UI and UX implications thereof, as well as the *ity issues like
>>> performance, security, et. al.
>>
>>
>>>
>>> --
>>> 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/CAJ7XQb6j28exxf1t%3D%3DceCLJFxDKf237R618ZkX2H0BxKmo4ZEQ%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/CAPPSPLoK34G7g3RSnKf5JXH3z8NewA_ZVaeXRxrqo3A5KGu7KQ%40mail.gmail.com
>> <https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoK34G7g3RSnKf5JXH3z8NewA_ZVaeXRxrqo3A5KGu7KQ%40mail.gmail.com?utm_medium=email_source=footer>
>> .
>>
> --
> 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/snZWQK2YePY/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/CAJ7XQb4Fvt%2BjPWa2%3D%2BKsL_TKZ9dV4vVwyodW8KD8gi9Qkp9F7w%40mail.gmail.com
> <https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb4Fvt%2BjPWa2%3D%2BKsL_TKZ9dV4vVwyodW8KD8gi9Qkp9F7w%40mail.gmail.com?utm_medium=email_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/CAPPSPLo_QPzjfX3YUkqpJ13O2dNJ-3s5LUarSPXdUFs6vGpGTQ%40mail.gmail.com.

Re: Support for OOP in some ATS3 extension (2)

Strictly speaking, ATS is an "abstract" language; the language itself
does not have primitive data types. When compiled to C, it uses the
data types defined by C; when to JS, it uses the data types defined
by JS; etc.

On Thu, Jan 21, 2021 at 11:50 AM Raoul Duke  wrote:

> $0.02
>
> In my limited/humble experience with FFI's the thing is not just being
> able to call out from the guest language to the host language, it is
> the return paths and the full round tripping and the overall semantics
> and the inevitable impedance mismatches that all sum up to make it an
> exercise in uselessness. Worst case things are like when the host
> string type != the guest string type, etc., etc, all the way up of
> course to bigger concepts like the host class implementation != the
> guest class implementation. Either there's a lot of extra cpu cycles
> spent on transmogriphying back and forth, or maybe things are worse
> and there ends up being 2 parallel things in the guest language and i
> have to manually convert.
>
> I do wish there were a master's thesis that studied the levels of
> integration among languages, both historically and in terms of
> technical possibilities, and specifically examined the end-developer
> UI and UX implications thereof, as well as the *ity issues like
> performance, security, et. al.
>
> --
> 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/CAJ7XQb6j28exxf1t%3D%3DceCLJFxDKf237R618ZkX2H0BxKmo4ZEQ%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/CAPPSPLoK34G7g3RSnKf5JXH3z8NewA_ZVaeXRxrqo3A5KGu7KQ%40mail.gmail.com.

Re: Support for OOP in some ATS3 extension (2)

2021-01-18 Thread Hongwei Xi

> > This time I would like to do something a bit more interesting:
> >
> > class
> >  > , b:type>
> > mygpair(a, b)
> > *snip*
>
> Do we need to say both  and (a,b)?  It seems redundant,
> since we already know the class is parametrized according to a and b, but
> maybe I'm missing something?
>

Again this is an issue with the OOP syntax. We have the following
possibilities
for the interface of mygpair_copy:

fun mypair_copy{a:type,b:type}(obj: !mypair(a, b)): mypair(a, b)
fun mypair_copy(obj: !mypair(a, b)): mypair(a, b)

Given that OOP syntax is quite restrictive anyway, we could decide to always
choose the second possibility. If so, we can just write:

class mypair(a:type, b:type) {
   ...
}

--Hongwei

On Mon, Jan 18, 2021 at 3:51 AM Elijah Stone  wrote:

> On Sun, 17 Jan 2021, gmhwxi wrote:
>
> > This time I would like to do something a bit more interesting:
> >
> > class
> >  > , b:type>
> > mygpair(a, b)
> > *snip*
>
> Do we need to say both  and (a,b)?  It seems redundant,
> since we already know the class is parametrized according to a and b, but
> maybe I'm missing something?
>
>
> > The mygpair(T1, T2) is a so-called generic class parameterized over
> > types T1 and T2. For an object of the type mygpair(T, T), a method for
> > swapping the fst and snd components of the object can be supported. But
> > this is difficult to do with the OOP syntax. BTW, how would be done in
> > Java? Such a method can be readily implemented with the following
> > syntax:
> >
> > fun
> > 
> > swap(pp: mygpair(a, a)): void =
> > let
> > val tmp = pp.fst in pp.fst := pp.snd; pp.snd := tmp
> > end
>
> Hmmm.  In a language like c++ where templates are not checked until
> they're instantiated, you would be able to just make that a template
> method.  That doesn't work so well in practice, however...
>
> One possible solution is subtyping.  As in:
>
> class  mypair(a, b) {
> var fst: a
> var snd: b
> //...
> }
>
> class  mysamepair(a): mypair(a, a) {
> method swap(): void = ...
> }
>
>   -E
>
> --
> 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/snZWQK2YePY/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/7e9a72f0-b2ee-af5f-b297-57f929179ebd%40elronnd.net
> .
>

-- 
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/CAPPSPLpW_mO6tV1CqmBpYppL8Z558P5jKYk4aV%2By%2BPmuJU5h7w%40mail.gmail.com.

Re: Support for OOP in some ATS3 extension (2)

2021-01-18 Thread Hongwei Xi

> class  mysamepair(a): mypair(a, a) {
> method swap(): void = ...
> }
>

I feel that this is a serious problem with typed OOP. Let me
give another example which I think no current OOP syntax can
handle.

Say we have an object of the type myrectangle(x, y), where
x and y are of the sort int (for width and height). Imagine a method
for doubling the width:

fun
double_width
(obj: !myrectangle(x, y) >> myrectangle(2*x, y)): void

This cannot be handled with OOP syntax because OOP syntax all
implicitly assumes that the type of 'this' cannot be changed by a method
call.

Also, one cannot introduce mysquare(x) as a subclass of myrectangle(x, x)
because double_with turns a square (of non-zero length)  into a non-square
rectangle.

--Hongwei


On Mon, Jan 18, 2021 at 3:51 AM Elijah Stone  wrote:

> On Sun, 17 Jan 2021, gmhwxi wrote:
>
> > This time I would like to do something a bit more interesting:
> >
> > class
> >  > , b:type>
> > mygpair(a, b)
> > *snip*
>
> Do we need to say both  and (a,b)?  It seems redundant,
> since we already know the class is parametrized according to a and b, but
> maybe I'm missing something?
>
>
> > The mygpair(T1, T2) is a so-called generic class parameterized over
> > types T1 and T2. For an object of the type mygpair(T, T), a method for
> > swapping the fst and snd components of the object can be supported. But
> > this is difficult to do with the OOP syntax. BTW, how would be done in
> > Java? Such a method can be readily implemented with the following
> > syntax:
> >
> > fun
> > 
> > swap(pp: mygpair(a, a)): void =
> > let
> > val tmp = pp.fst in pp.fst := pp.snd; pp.snd := tmp
> > end
>
> Hmmm.  In a language like c++ where templates are not checked until
> they're instantiated, you would be able to just make that a template
> method.  That doesn't work so well in practice, however...
>
> One possible solution is subtyping.  As in:
>
> class  mypair(a, b) {
> var fst: a
> var snd: b
> //...
> }
>
> class  mysamepair(a): mypair(a, a) {
> method swap(): void = ...
> }
>
>   -E
>
> --
> 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/snZWQK2YePY/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/7e9a72f0-b2ee-af5f-b297-57f929179ebd%40elronnd.net
> .
>

-- 
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/CAPPSPLqCwvGL_2Um%2B45tZSW8HNA%3D4Rir2kTah-1oZNqRHz_Lbw%40mail.gmail.com.

Re: Learn ATS in Y minutes -- request for documentation review

2021-01-17 Thread Hongwei Xi

Thanks, Mark!

I took a quick read.

Your description of various ATS2 features is accurate.

To be honest, I myself often forget how certain things are done in ATS2 and
have to use 'grep' to find code examples helping me figure out. For example,
I find the information in Part 5 particularly helpful!

Given the scarcity of ATS2 documentation, I am also quite amazed by your
being
able to figure out some very intricate features of ATS2 on your own.

Cheers!

--Hongwei

On Sun, Jan 17, 2021 at 1:30 AM mark.l@gmail.com <
mark.l.barb...@gmail.com> wrote:

> Hi all,
>
> Learn X in Y Minutes  has community-made
> documentation for programming languages and tools, as example-driven
> "whirlwind tours" of each languages' features.  I made one for ATS, since
> none existed and I think it's a great documentation format to have.  Here's 
> the
> rendered markdown
> ,
> and the associated PR
> .  It's
> about 500 lines of well-commented ATS, and introduces language features as
> you read it.
>
> I'm still relatively inexperienced in ATS, so I'd appreciate reviews to
> make sure all the explanations are sound and to make the code more
> idiomatic.  Reviews from less experienced ATS users would also be
> particularly welcome, to make sure it addresses the confusions you had when
> first using ATS.
>
> Learn X in Y Minutes has been really helpful to me in the past learning
> other languages, since reading good code can be a great way to learn.  I
> hope we can make this equally helpful to new ATS programmers.
>
> Thanks,
>
> -Mark Barbone
>
> --
> 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/2f2cad00-f229-491a-bf7d-a064d5ec452en%40googlegroups.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/CAPPSPLpWWB0qZ2o6-Tf44-i%2BNkOTO6vwF8PJV%3DPPr%3DOqVEdhXw%40mail.gmail.com.

Re: Is It Possible to Pass a Function Template as a Parameter?

2021-01-02 Thread Hongwei Xi

Yes, I would like to see an example of this kind.


On Sat, Jan 2, 2021 at 9:19 PM d4v3y_5c0n3s  wrote:

> So, I know that  it's possible to pass a function to another function as a
> parameter, but what if I want to pass a function template specifically?  If
> anyone would like some clarification, I can try to provide some examples of
> what I'm trying to achieve.
>
> --
> 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/96fc4ec0-8355-4b32-883a-30f2293b4861n%40googlegroups.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/CAPPSPLoc7cF_sAjb0a%2Bkz6UJyW8NLzkVFpm_N4HiRG0EHxyvUw%40mail.gmail.com.

Re: Building ATS2 from Github head.

2020-12-31 Thread Hongwei Xi

This is an issue of the ATS2/Postiats compiler because it uses the absolute
path of a file
to create a name during compilation for the package stored in the file.
This is not a reliable
approach. Hopefully, something better can be used for ATS3. One possibility
is to just follow
what Java does.


On Thu, Dec 31, 2020 at 7:50 PM Steinway Wu  wrote:

> It is so weird, turns out that
>
> ATSHOME=/some/path/with/../../in/it make -f Makefile_devl all
>
> will fail, but
>
> ATSHOME=/some/absolute/path/with/no/dot make -f Makefile_devl all
>
> works.
>
> Any idea what could have caused that? Is it a Make issue or is it an ATS
> compiler issue?
>
>
>
> *Steinway Wu*
>
> *吴翰文*
>
> *Google Cloud*
>
> *I'm not a coder.*
> *I'm an artist of life.*
>
>
> On Dec 31, 2020 at 1:31:10 PM, gmhwxi  wrote:
>
>>
>> Maybe this has something to do with where the ATS2 package is stored on
>> your computer.
>> Could you try something like:
>>
>> cd /tmp
>> wget
>> http://downloads.sourceforge.net/project/ats-lang/ats-lang/anairiats-0.2.12/ats-lang-anairiats-0.2.12.tgz
>> tar xf ats-lang-anairiats-0.2.12.tgz
>> cd ats-lang-anairiats-0.2.12/
>> export ATSHOME=${PWD}
>> export ATSHOMERELOC=ATS-0.2.12
>> ./configure && make all
>>
>> Just tried. This script works for me.
>>
>> On Thursday, December 31, 2020 at 12:18:22 PM UTC-5 stein...@gmail.com
>> wrote:
>>
>>> Hi,
>>>
>>> It seems the documentation at
>>> https://github.com/githwxi/ATS-Postiats/wiki/Building-and-installing as
>>> well as scripts at
>>> https://github.com/ats-lang/ats-lang.github.io/blob/master/SCRIPT/C9-ATS2-install-latest.sh
>>> are outdated. I’m trying both and encountered link errors.
>>>
>>> Here’s what I did.
>>>
>>> # installing ats1
>>> wget …
>>> ./configure —prefix=…
>>> make all_ngc
>>> make install
>>>
>>> # installing ats2
>>> git clone …
>>> export ATSHOME=…
>>> export ATSHOMERELOC=ATS-0.2.12
>>> make -f Makefile_devl
>>>
>>> The errors I see is undefined reference to symbols like
>>> _2root_2parts_2ats1_2build_2libatsdoc_... Using nm to view the symbols
>>> of libatsdoc.a, I can see they are named like
>>> ATS_2d0_2e2_2e12_2libatsdoc_... instead.
>>>
>>> There was a post
>>> https://groups.google.com/g/ats-lang-users/c/uKlIX4jcL0Y/m/nKf8oezDBAAJ with
>>> the same error, but I believe I correctly set ATSHOMERELOC
>>>
>>> Any idea what I’m missing?
>>>
>>>
>>> --
>> 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/W62cWGzt0AI/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/87cbe011-5997-4d96-a439-2522ced8e8adn%40googlegroups.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/CAL-Unv9pvBNQtcQwK_wJ-wVdzmS-2HmnmZzKLr_SoTKonBVPmA%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/CAPPSPLpQkrw%3DdNn6miFquKPG4wqfXAObVsw8tEPOeSN9LZ7-RA%40mail.gmail.com.

Re: ignoring the datavtype

2020-12-30 Thread Hongwei Xi

Yes, if a linear value matches the wildcard pattern '_', it is leaked.
It is not a bug, though; it is by design.

This is probably a poor design of mine. It is already abandoned in ATS3.

--Hongwei

On Wed, Dec 30, 2020 at 7:34 AM Dambaev Alexander 
wrote:

> here is the repo of the minimum example where such issue is being
> reproduced: https://github.com/dambaev/ats-datavtype-leak
>
> and in particular test3:
> https://github.com/dambaev/ats-datavtype-leak/blob/master/src/TEST/test3.dats#L46-L53
> which is compilable and leaking resource
>
> ср, 30 дек. 2020 г. в 16:31, Dambaev Alexander :
>
>> Hi,
>>
>> milis is a datavtype `Bytestring_vtype`described at
>> https://github.com/dambaev/ats-bytestring/blob/master/SATS/bytestring.sats#L8
>> and in this particular case, being instantiated by `pack_int64' from
>> https://github.com/dambaev/ats-bytestring/blob/master/SATS/bytestring.sats#L184-L190
>>
>> ср, 30 дек. 2020 г. в 16:21, Artyom Shalkhakov <
>> artyom.shalkha...@gmail.com>:
>>
>>> Hi Alex,
>>>
>>> What's the type of [millis]?
>>>
>>> ср, 30 дек. 2020 г. в 10:04, Dambaev Alexander :
>>>
 Hi all,

 today I spotted an error in my code. Here is the snippet:
 ```
 val millis = $BS.pack( msecs_i64 + ($UN.cast{int64}
 msecs) ) // + $UN.cast{int32} msecs )
 val env = ( hws, millis)
 val () = list_vt_foreach_funenv0< ( $BS.BytestringNSH1,
 $BS.BytestringNSH1) ><($BS.BytestringNSH1,$BS.BytestringNSH1)>{void}( () |
 kvs, env, print_json) where {
   fn
 print_json
 ( pf: !void
 | x: &(@($BS.BytestringNSH1, $BS.BytestringNSH1))
 , env: !($BS.BytestringNSH1, $BS.BytestringNSH1)
 ): void = {
   val (hws, millis) = env
   val bs = $BS.pack "{ \"tenant\": \"demo\",
 \"buildingId\": \"demo\", "
 + $BS.pack "\"metadata\": { \"name\": \"" +!
 x.0 + $BS.pack "\"}, "
 + $BS.pack "\"value\": " +! x.1 + $BS.pack ", "
 + $BS.pack "\"timestamp\": " +! millis +
 $BS.pack ", "
 + $BS.pack "\"deviceId\": \"" +! hws + $BS.pack
 "\""
 + $BS.pack "}"
   val () = $BS.printlnC( bs)
   prval () = env := (hws, millis)
 }
 }
 *val (hws1, _) = env (* here I can just ignore the
 'millis'  and cause a memory leak *)*
 prval () = hws := hws1
 val () = list_vt_freelin_fun<@($BS.BytestringNSH1,
 $BS.BytestringNSH1)> (kvs, cleaner) where {
   fn cleaner( x: &($BS.BytestringNSH1,
 $BS.BytestringNSH1) >> ($BS.BytestringNSH1, $BS.BytestringNSH1)?):void = {
 val () = $BS.free x.0
 val () = $BS.free x.1
   }
 }
 val () = $BS.free( time)
 val () = $BS.free( rawpayload)
 val () = $BS.free( hws)
 ```
 and the compiler hasn't bite my hands with this: it has typechecked and
 compiled this code without issues. Only valgrind had.
 And here is the correct snippet, which is compiling without issues as
 well.

 ```
 val millis = $BS.pack( msecs_i64 + ($UN.cast{int64}
 msecs) ) // + $UN.cast{int32} msecs )
 val env = ( hws, millis)
 val () = list_vt_foreach_funenv0< ( $BS.BytestringNSH1,
 $BS.BytestringNSH1) ><($BS.BytestringNSH1,$BS.BytestringNSH1)>{void}( () |
 kvs, env, print_json) where {
   fn
 print_json
 ( pf: !void
 | x: &(@($BS.BytestringNSH1, $BS.BytestringNSH1))
 , env: !($BS.BytestringNSH1, $BS.BytestringNSH1)
 ): void = {
   val (hws, millis) = env
   val bs = $BS.pack "{ \"tenant\": \"demo\",
 \"buildingId\": \"demo\", "
 + $BS.pack "\"metadata\": { \"name\": \"" +!
 x.0 + $BS.pack "\"}, "
 + $BS.pack "\"value\": " +! x.1 + $BS.pack ", "
 + $BS.pack "\"timestamp\": " +! millis +
 $BS.pack ", "
 + $BS.pack "\"deviceId\": \"" +! hws + $BS.pack
 "\""
 + $BS.pack "}"
   val () = $BS.printlnC( bs)
   prval () = env := (hws, millis)
 }
 }
 *val (hws1, millis1) = env*
 prval () = hws := hws1
 *prval () = millis :=

Re: Can arrayptr_freelin() cause a memory leak?

2020-12-15 Thread Hongwei Xi

>>Okay, so what you are saying is that in order for the code to compile, I
will need to implement the template for the given type.

That's right.

Hopefully, such a template can be automatically generated in ATS3 based on
the given (or inferred) type
information. There should be a substantial component in ATS3 to support
this kind of type-based meta-programming.

On Tue, Dec 15, 2020 at 11:43 AM d4v3y_5c0n3s  wrote:

> Okay, so what you are saying is that in order for the code to compile, I
> will need to implement the template for the given type.  That makes sense,
> thanks for the explanation! :)
>
> On Tuesday, December 15, 2020 at 10:57:09 AM UTC-5 gmhwxi wrote:
>
>> It should not as arrayptr_freelin calls array_uninitize$clear to free all
>> the stored elements.
>> It is your obligation to implement the latter.
>>
>>
>> On Tue, Dec 15, 2020 at 9:54 AM d4v3y_5c0n3s  wrote:
>>
>>> I just have a question about using arrayptr_freelin() (which frees
>>> an arrayptr that contains a vt@ype.)  I have an arrayptr which contains
>>> datavtypes, and these datavtypes act like a list in that they can contain a
>>> reference to another of the same datavtype.  The typechecker lets me simply
>>> call arrayptr_freelin() on the arrayptr, but does this cause a memory
>>> leak?  Do I need to free the individual datavtypes first?
>>> I can provide a code example if anyone reading this doesn't
>>> understand what I am talking about.  The types and functions that I am
>>> using are all in the prelude.
>>>
>>> --
>>> 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/84121c93-a043-405c-be86-e7cc74903f68n%40googlegroups.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/b6d0bb1a-cfa2-4c1d-aca5-3d669d827016n%40googlegroups.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/CAPPSPLr23TN7MhK3nyGczRpJw%2B-WQM%3Dwz%2Bpp-jEG2Dvf-UVGHQ%40mail.gmail.com.

Re: Can arrayptr_freelin() cause a memory leak?

2020-12-15 Thread Hongwei Xi

It should not as arrayptr_freelin calls array_uninitize$clear to free all
the stored elements.
It is your obligation to implement the latter.


On Tue, Dec 15, 2020 at 9:54 AM d4v3y_5c0n3s  wrote:

> I just have a question about using arrayptr_freelin() (which frees an
> arrayptr that contains a vt@ype.)  I have an arrayptr which contains
> datavtypes, and these datavtypes act like a list in that they can contain a
> reference to another of the same datavtype.  The typechecker lets me simply
> call arrayptr_freelin() on the arrayptr, but does this cause a memory
> leak?  Do I need to free the individual datavtypes first?
> I can provide a code example if anyone reading this doesn't understand
> what I am talking about.  The types and functions that I am using are all
> in the prelude.
>
> --
> 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/84121c93-a043-405c-be86-e7cc74903f68n%40googlegroups.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/CAPPSPLphUMfuFkR2UVPCTFYycDtTA4%2BXyySA2iuQm3ytButYQA%40mail.gmail.com.

Re: symintr and staload

2020-11-28 Thread Hongwei Xi

This behavior is intended.

In ATS, a fixity declaration like the following one has no effect
outside the module (that is, file) where it is declared:

infixl (+) +++

By the way, symintr is no longer needed in ATS2; it is not even
supported in ATS3.


On Sat, Nov 28, 2020 at 8:47 AM Dambaev Alexander 
wrote:

> Hi,
> I have noticed, that I am not able to introduce new symbol inside sats
> file and use it in dats file, like this:
> file1.sats
> ```
>
> fn operator( a: int, b: int): int
>
> symintr +++
> infixl (+) +++
> overload +++ with operator
> ```
> main.dats:
>
> ```
> #include "share/atspre_staload.hats"
>
> #define ATS_DYNLOADFLAG 0
>
> (* if I uncomment those lines before staload, then main.dats will be
> compiled as expected. Otherwise, patscc will say, that it is unable to
> resolve +++
> symintr +++
> infixl (+) +++
> *)
> staload "file1.sats"
>
> implement main0() = println!( "1 +++ 2 = ", 1 +++ 2)
> ```
>
> I found a walkaround by introducing symbol and it's precedence before
> staload, but it seems like a bug for me
>
> --
> 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/CAHjn2KzsVTfFbMm_VX9vzvE-aPGem1eqVyDR2DCkXh-AAypF%2Bw%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/CAPPSPLp2NFK5DyJ5DALefCec5Z6gpdoB3TM_T5Ep4mJLgoZgkw%40mail.gmail.com.

Re: Read IO and Write IO

2020-11-24 Thread Hongwei Xi

>>Would it still be better to include the effects in the source file,

If we look at a bigger picture, it may not even be practical to require
that this kind of information be stored
in the source. Today it is effect-tracking, and tomorrow it will surely be
something else. And there is only so
much that you can put in the source file without causing conflicts.

On Tue, Nov 24, 2020 at 2:23 PM Brandon Barker 
wrote:

> Would it still be better to include the effects in the source file, and
> then pass to the compiler (or 3rd party tool) which effects are to be
> tracked, and possibly how they are tracked?
>
> Advantages of this approach to me seem that:
>  - Easily viewable from the source (as was already mentioned)
>  - If an effect isn't being used, though it is listed in the source, the
> effect checker could emit a warning or error (configurable).
>  - Encourages use of effects: I worry that without effect tracking, we
> gain less confidence in the rest of the ATS3 ecosystem. This is similar to
> the state of play with Mypy and Python's gradual typing (and I'll note that
> there, types are annotated in the code as one would expect), except we're
> only talking about effect types and not types in general: most python
> libraries don't use typings, so even if you are vigilant in your own code,
> it is much harder to sometimes understand what effects are happening in
> libraries. Of course, ultimately much of what we do is built on FFIs of
> some sort, and a certain degree of trust has to be exercised at that level,
> but I feel like without some degree of standardization with regard to a
> basic set of effects, and encouraging their use, it could result in them
> not being very useful due to fractured use within the ATS3 ecosystem.
>
> On Tuesday, November 24, 2020 at 1:24:10 AM UTC-5 gmhwxi wrote:
>
>> Thanks for the message!
>>
>> What I said is not in conflict with what you described in the message.
>>
>> An external tool for tracking effects can be quite useful in large scale
>> programming.
>> Deciding what effects should be tracked is often open-ended; what is
>> decided today
>> may not be what is wanted tomorrow.
>>
>> The type-based approach you described becomes quite burdensome once
>> higher-order
>> functions are present. A big difficulty in effect-tracking lies precisely
>> in handling higher-order
>> functions.
>>
>> On Monday, November 23, 2020 at 10:57:41 PM UTC-5 ice.r...@gmail.com
>> wrote:
>>
>>> Maintaining some external file seems to me as something, which is easy
>>> to ignore or easy to forget about and without some scatch of of example of
>>> usage, I can't see how it will be helpful at all.
>>>
>>> For example:
>>> ```
>>> fn foo(): void = println!("hello")
>>> implement main0() = foo()
>>> ```
>>> and the external file contains:
>>> ```
>>> console: println
>>> ```
>>> Do you mean, that such external tool should require foo and main0 to be
>>> listed in such file?
>>> In this case, it will still be absent in types so it will be hard to
>>> answer a questions like: "what effects contains foo?" or main0 as well.
>>>
>>> In contrast, by using proof arguments you will actually see, that in
>>> order to use foo you need to pass IO:
>>> so it is clearer to understand, but more verbose as well, as main0 will
>>> be probably a source of all kind of effects, like:
>>> ```
>>> extern prfn use_console( !IO): Console
>>> fn
>>>   foo
>>>   ( console: !Console
>>>   |
>>>   ): void = println!( console, "hello")
>>> implement main0(io | ) = {
>>>   prval console = use_console( io)
>>>   val () = foo( console | )
>>> }
>>> ```
>>>
>>> another interesting approach will be to wrap the exceptions (ie, the
>>> goal is to see in types which exceptions are possible to be thrown from
>>> function), so $raise should have type like:
>>> ```
>>> extern fn
>>>   $raise
>>>   {a:type}{b:type| // is there an exception sort?
>>>   ( !Throws(a)
>>>   | a
>>>   ): b
>>> ```
>>> then `try` should require `!IO` and bring `Throws(a)` for all branches
>>> in `with`, like:
>>> ```
>>> fn
>>>foo
>>>   ( Throws( DivisionByZero)
>>>   , Throws(FileNotFound)
>>>   | a: int
>>>   , b :int
>>>   ): int = a / b
>>>
>>> implement main0() =
>>> try
>>>   ( try foo() with // I am not sure if foo() will be able to use
>>> Throws(..) implicitely
>>>   | ~DivisionByZero() => ... // this brings Throws(DivisionByZero) into
>>> the scope and only within this block of try ... with
>>>   ) with
>>>   | ~FileNotFound() => ... // this brings Throws(FileNotFound) into the
>>> scope
>>> ```
>>> but of course, this looks like Haskell's typeclasses from
>>> https://www.well-typed.com/blog/2015/07/checked-exceptions/
>>>
>> --
> 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/HtsSq9thpk8/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to
>

Re: Current Status of ATS3 (2020-11-22)

2020-11-23 Thread Hongwei Xi

>>Can I guess that XATSCL0 is basically the same as the C-file that we have
now during compilation with patscc? Otherwise, what is the purpose of it?

Patscc generates code that contains goto statements. This time I would
exclude goto's in XATSCL0. In this way, compilers for ATS3 targeting other
languages can also benefit from using XATSCL0.

>>Does this mean that currently ATS3 just ignores code related to
linear/dependent types?

Yes, it ignores completely.

-- 

On Sun, Nov 22, 2020 at 11:47 PM Dambaev Alexander 
wrote:

> Glad to hear news about ATS3 implementation!
>
>
> XATSOPT:
>>
>> Xatsopt is a functioning compiler implemented in ATS2 for translating
>> ATS3 into a typed intermediate language of the name XATSCML, which is
>> both C-like and ML-like. It is planned for xatsopt to further
>> translate XATSCML into XATSCL0, a low-level C-like language. I now
>> primarily see xatsopt as a library (libxatsopt) for implementing tools
>> to support programming with ATS3.
>>
> Can I guess that XATSCL0 is basically the same as the C-file that we have
> now during compilation with patscc? Otherwise, what is the purpose of it?
>
>
>>
>> Documenting Xatsopt:
>>
>> This has been assigned a high priority. It is hoped that other
>> people interested in ATS3 can start developing tools for ATS3 after
>> a minimal amount of documentation on xatsopt is made available.
>>
> The more documentation - the better :)
>
>
>> Advanced Type-Checking:
>>
>> While one can specify with linear types and dependent types in ATS3,
>> there is no type-checking for such advanced types in xatsopt. I plan
>> to concentrate on implementing support for such type-checking in the
>> next phase of ATS3 development.
>>
>
> Does this mean that currently ATS3 just ignores code related to
> linear/dependent types?
>
> --
> 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/CAHjn2Kxekq4Phu1%3DEFWxTVgjRm2pczK5ZsLeAy7DN%2BGzuuyA8A%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/CAPPSPLqmUjH7eLeO8iaAp0DE_Hp6RHadu%2BuKyTcLu2TPc_rq7Q%40mail.gmail.com.

Re: Current Status of ATS3 (2020-11-22)

2020-11-22 Thread Hongwei Xi

>>What is the final vision for XATSCL0?  Will it be compiled into c?  Or
directly into native code (via custom backend, or llvm/similar)?

XATSCL0 should most likely be a subset of C.

To get into native code, one needs to remove function calls of C-style in
XATSCL0.

>>What is the effect on compilation speed of having (at least) two full
intermediate languages?

Right now, it is not a big concern as xatsopt does not do time-consuming
optimizations. I suspect that
more time is likely spent on the phase of compiling XATSCL0 to native code.

>>JS doesn't have integers.  So how will code that uses integers be
compiled?  Is code compiled to js is limited to 32-bit integers, since they
can fit into the range of a double?

When compiled to JS, the int type in ATS is interpreted by some JS
functions in a small library dabbed 'runtime'.
For instance, integer division is given the following implementation:

function
XATS2JS_gint_div_sint_sint
  (x1, x2)
{
//
  let q0 = x1 / x2;
//
  if
  (q0 >= 0)
  {
return Math.floor(q0);
  }
  else
  {
return Math.ceil( q0 );
  }
}

On Sun, Nov 22, 2020 at 6:31 PM Elronnd _  wrote:

> On Sun, 22 Nov 2020, gmhwxi
> wrote:
>
>
>
> > As of today, I am pleased to announce that ATS3 has reached a stage
> where it can be realistically used in software construction. This is
> achieved after slightly more than two and one-half years of continual
> development by yours truly
> :)
>
>
>
> Great to
> hear!
>
>
>
>
>
> > Xatsopt is a functioning compiler implemented in ATS2 for translating
> ATS3 into a typed intermediate language of the name XATSCML, which is both
> C-like and ML-like. It is planned for xatsopt to further translate XATSCML
> into XATSCL0, a low-level C-like
> language.
>
>
>
> What is the final vision for XATSCL0?  Will it be compiled into c?  Or
> directly into native code (via custom backend, or
> llvm/similar)?
>
>
>
> What is the effect on compilation speed of having (at least) two full
> intermediate
> languages?
>
>
>
>
>
> > Xats2js is a functioning compiler implemented in ATS2 for translating
> XATSCML into
> JavaScript
>
>
>
> JS doesn't have integers.  So how will code that uses integers be
> compiled?  Is code compiled to js is limited to 32-bit integers, since they
> can fit into the range of a
> double?
>
>
>
>  -E
>
>
> --
> 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/ca34ad8d-77db-4e91-b548-400c3111c8c9n%40googlegroups.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/CAPPSPLq6bS2tuU-WF3-TBjen36hfydPZ-4HHu%2BMfiZMeukRQDw%40mail.gmail.com.

Re: Current Status of ATS3 (2020-11-22)

2020-11-22 Thread Hongwei Xi

I could only manage one write-up so far:

https://github.com/xanadu-lang/xats2js/tree/master/docgen/CodeBook/Hello

I plan to implement some word games to showcase this style of
co-programming.

Cheers!


On Sun, Nov 22, 2020 at 1:30 PM Hongwei Xi  wrote:

> I will do a few examples today of co-programming with ATS3 and JS.
>
> Conceptually, it is straightforward: ATS code is compiled to JS via xats2js
> and the generated JS code can be directly combined with other JS code.
> There is a very small library of JS code needed for running the generated
> JS code.
>
> In practice, it is equally straightforward :)
>
> By the way, I would like to emphasize that xats2js is NOT meant to be an
> optimizing compiler; it is more like a reference implementation of some
> sort.
> The JS code generated by xats2js is currently not of high quality in terms
> of
> efficiency (time-wise or memory-wise).
>
> On Sun, Nov 22, 2020 at 12:38 PM Brandon Barker 
> wrote:
>
>> Hi Hongwei,
>>
>> That's exciting to hear. If and when they are available, could you point
>> to any FFI examples or documentation for JavaScript? Perhaps, but not
>> necessarily, related to DOM APIs in the browser (just as a common example)?
>> On Sunday, November 22, 2020 at 9:31:16 AM UTC-5 gmhwxi wrote:
>>
>>>
>>>
>>> Hi, there,
>>>
>>> HX-2020-11-22:
>>>
>>> (*
>>> HX-2018-04-07: Let us get started!!!
>>> *)
>>>
>>> As of today, I am pleased to announce that ATS3 has reached a stage
>>> where it can be realistically used in software construction. This is
>>> achieved after slightly more than two and one-half years of continual
>>> development by yours truly :)
>>>
>>> ##
>>> #
>>> # The current status
>>> #
>>> ##
>>>
>>> XATSOPT:
>>>
>>> Xatsopt is a functioning compiler implemented in ATS2 for translating
>>> ATS3 into a typed intermediate language of the name XATSCML, which is
>>> both C-like and ML-like. It is planned for xatsopt to further
>>> translate XATSCML into XATSCL0, a low-level C-like language. I now
>>> primarily see xatsopt as a library (libxatsopt) for implementing tools
>>> to support programming with ATS3.
>>>
>>> XATS2JS:
>>>
>>> Xats2js is a functioning compiler implemented in ATS2 for translating
>>> XATSCML into JavaScript (or JS for short). It should be noted that
>>> xats2js can compile tail-recursive calls into local jumps, effectively
>>> supporting the common practice in functional programming of writing
>>> loops as tail-recursive functions.
>>>
>>> I will give detailed explanation elsewhere on using xats2js. Generally
>>> speaking, one can now practice a form of co-programming with ATS3 and
>>> JS. The JS code generated by xats2js from compiling ATS3 source can be
>>> directly combined with other JS code (as if the generated code were
>>> manually written in JS)
>>>
>>> ##
>>> #
>>> # Future Development
>>> #
>>> ##
>>>
>>> Documenting Xatsopt:
>>>
>>> This has been assigned a high priority. It is hoped that other
>>> people interested in ATS3 can start developing tools for ATS3 after
>>> a minimal amount of documentation on xatsopt is made available.
>>>
>>> Advanced Type-Checking:
>>>
>>> While one can specify with linear types and dependent types in ATS3,
>>> there is no type-checking for such advanced types in xatsopt. I plan
>>> to concentrate on implementing support for such type-checking in the
>>> next phase of ATS3 development.
>>>
>>> ##
>>> #
>>> # A little history of ATS3
>>> #
>>> ##
>>>
>>> Essentially, ATS3 refers to the third edition of ATS, and ATS/Xanadu
>>> is currently the only implementation of ATS3. Note that the names ATS3
>>> and ATS/Xanadu are often used interchangeably.
>>>
>>> In the ATS family of languages, the first implementation is named
>>> ATS/Proto (2004) and the language it implements is referred to as
>>> ATS0. Please note that the implementation of ATS/Proto is written in
>>> OCaml. The next implementation is ATS/Geizella (2007), which is also
>>> written in OCaml. And the language implemented by ATS/Geizella is
>>> referred to as ATS1. ATS/Anairiats (2008) is an implementation of ATS1
>>> in itself; the implementation is first compiled by ATS/Geizella and
>

Re: Current Status of ATS3 (2020-11-22)

2020-11-22 Thread Hongwei Xi

I will do a few examples today of co-programming with ATS3 and JS.

Conceptually, it is straightforward: ATS code is compiled to JS via xats2js
and the generated JS code can be directly combined with other JS code.
There is a very small library of JS code needed for running the generated
JS code.

In practice, it is equally straightforward :)

By the way, I would like to emphasize that xats2js is NOT meant to be an
optimizing compiler; it is more like a reference implementation of some
sort.
The JS code generated by xats2js is currently not of high quality in terms
of
efficiency (time-wise or memory-wise).

On Sun, Nov 22, 2020 at 12:38 PM Brandon Barker 
wrote:

> Hi Hongwei,
>
> That's exciting to hear. If and when they are available, could you point
> to any FFI examples or documentation for JavaScript? Perhaps, but not
> necessarily, related to DOM APIs in the browser (just as a common example)?
> On Sunday, November 22, 2020 at 9:31:16 AM UTC-5 gmhwxi wrote:
>
>>
>>
>> Hi, there,
>>
>> HX-2020-11-22:
>>
>> (*
>> HX-2018-04-07: Let us get started!!!
>> *)
>>
>> As of today, I am pleased to announce that ATS3 has reached a stage
>> where it can be realistically used in software construction. This is
>> achieved after slightly more than two and one-half years of continual
>> development by yours truly :)
>>
>> ##
>> #
>> # The current status
>> #
>> ##
>>
>> XATSOPT:
>>
>> Xatsopt is a functioning compiler implemented in ATS2 for translating
>> ATS3 into a typed intermediate language of the name XATSCML, which is
>> both C-like and ML-like. It is planned for xatsopt to further
>> translate XATSCML into XATSCL0, a low-level C-like language. I now
>> primarily see xatsopt as a library (libxatsopt) for implementing tools
>> to support programming with ATS3.
>>
>> XATS2JS:
>>
>> Xats2js is a functioning compiler implemented in ATS2 for translating
>> XATSCML into JavaScript (or JS for short). It should be noted that
>> xats2js can compile tail-recursive calls into local jumps, effectively
>> supporting the common practice in functional programming of writing
>> loops as tail-recursive functions.
>>
>> I will give detailed explanation elsewhere on using xats2js. Generally
>> speaking, one can now practice a form of co-programming with ATS3 and
>> JS. The JS code generated by xats2js from compiling ATS3 source can be
>> directly combined with other JS code (as if the generated code were
>> manually written in JS)
>>
>> ##
>> #
>> # Future Development
>> #
>> ##
>>
>> Documenting Xatsopt:
>>
>> This has been assigned a high priority. It is hoped that other
>> people interested in ATS3 can start developing tools for ATS3 after
>> a minimal amount of documentation on xatsopt is made available.
>>
>> Advanced Type-Checking:
>>
>> While one can specify with linear types and dependent types in ATS3,
>> there is no type-checking for such advanced types in xatsopt. I plan
>> to concentrate on implementing support for such type-checking in the
>> next phase of ATS3 development.
>>
>> ##
>> #
>> # A little history of ATS3
>> #
>> ##
>>
>> Essentially, ATS3 refers to the third edition of ATS, and ATS/Xanadu
>> is currently the only implementation of ATS3. Note that the names ATS3
>> and ATS/Xanadu are often used interchangeably.
>>
>> In the ATS family of languages, the first implementation is named
>> ATS/Proto (2004) and the language it implements is referred to as
>> ATS0. Please note that the implementation of ATS/Proto is written in
>> OCaml. The next implementation is ATS/Geizella (2007), which is also
>> written in OCaml. And the language implemented by ATS/Geizella is
>> referred to as ATS1. ATS/Anairiats (2008) is an implementation of ATS1
>> in itself; the implementation is first compiled by ATS/Geizella and
>> then by itself, succeeding in so-called bootstrapping. The next
>> edition of ATS is ATS2, which is given an implementation of the name
>> ATS/Postiats (2013) written in ATS1.
>>
>> ATS/Xanadu implements ATS3 and the implementation is written in ATS2.
>> While there is currently no plan to bootstrap ATS3 by implementing it
>> in itself, it is perceivable that ATS/Xanadu can be readily translated
>> (manually) into such an implementation since the difference between
>> ATS2 and ATS3 in terms of both syntax and semantics is fairly minor
>> (for the part being used in compiler implementation).
>>
>> ##
>>
>> Cheers!
>>
>> --Hongwei
>>
>> ##
>>
>> For previously post messages:
>>
>> https://github.com/githwxi/ATS-Xanadu/tree/master/docgen/NOTES
>> ##
>>
>>
>> --
> 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/4Pb6GAuBiY4/unsubscribe.
> To

Fwd: [ats-lang-users] ATS2-0.4.2 released

2020-11-14 Thread Hongwei Xi

FYI.

-- Forwarded message -

Hi,

It is my pleasure to announce the release
of ATS2-0.4.2. Note that this is the version
currently needed for compiling the ongoing
implementation of ATS3 (ATS/Xanadu).

ATS-Postiats-0.4.2.tgz:
The same as ATS-Postiats-int-0.4.2.tgz
MD5:
900c43b69f544ddff738ebf864f98b06
SHA1:
76b7c817c3439858e42c4ff74edc226578e0ea1b
--
ATS2-Postiats-gmp-0.4.2.tgz:
MD5:
e2f0f6c38868bb6b85f77fd1d9222b23
SHA1:
a869ba92d673082cd30fc6c2368d3948eef772fa
--
ATS2-Postiats-int-0.4.2.tgz:
MD5:
900c43b69f544ddff738ebf864f98b06
SHA1:
76b7c817c3439858e42c4ff74edc226578e0ea1b

This is the 53rd release of ATS2, the successor of the
ATS programming language. The compiler for ATS2 is given
the name ATS/Positats, ATS2/Postiats or simply Postiats.

The official website for ATS is:

http://www.ats-lang.org

ATS-Postiats is hosted at github:

https://github.com/githwxi/ATS-Postiats

Major releases of ATS2 are available at:

https://sourceforge.net/projects/ats2-lang/

Major releases of external packages for ATS2 are available at:

https://sourceforge.net/projects/ats2-lang-contrib/

Here is a list of major additions and changes since the last release:

There are only a few minor modifications, which are primarily
needed for compiling the current (2020-11-01) implementation of ATS3.

1. Fixing the handling of an issue causing the compiler crash:
the proof of the at-view of a local variable is not restored
at the end of its scope.
Please visit the following link for more details:
https://groups.google.com/g/ats-lang-users/c/f9QVilhHMEM

2. Fixing bug-2020-10-14
(for the omission of handling records when the exhaustiveness of
pattern matching is tested)
Kudos to Alex Dambaev for reporting it!

Please note that in this release, there are two variants of
the package released: The "gmp" variant depends on the GMP library and
the "int" variant does not depend on the GMP library. In this release
ATS2-Postiats-0.4.2.tgz is just the same as
ATS2-Postiats-int-0.4.2.tgz.

Cheers,

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

___
ats-lang-users mailing list
ats-lang-us...@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/ats-lang-users

--
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/CAPPSPLqqh46i7_UjVSqv1iGG5ejwj5m-X%2BAk-2613RSJt7Jncg%40mail.gmail.com.

Re: Building ATS that uses uint8

2020-10-23 Thread Hongwei Xi

The error message says that gint2uint is not implemented for the type uint8.
Of course, you can just implement it. Or you can just use the following
unsafe
approach to circumvent the issue:

#include "share/atspre_staload.hats"
#include "share/atspre_define.hats"

val
twelve =
$UNSAFE.cast(12): uint8(12)

implement main0 () = print!("twelve is ", twelve, "\n")


On Fri, Oct 23, 2020 at 5:36 PM Mark Barbone 
wrote:

>
> Hi all,
>
> I'm new to ATS, and trying to use the uint8 type.  However, when I do, I
> get long errors from GCC, involving PMVtmpltcstmat and friends:
> https://gist.github.com/mb64/eb9d194f3dedffd06d5cd075db316899
>
> The command I'm using to compile is:
> patscc -DATS_MEMALLOC_LIBC -o uint8_test uint8_test.dats
>
> How should I compile such a file using uint8?  Are there other files to
> #include, staload, or pass as command-line arguments?
> Or is my ATS installation completely borked?
>
> Thanks!
>
> --
> 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/339ebe1e-8cd0-4192-a1ab-a66f24da36d1n%40googlegroups.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/CAPPSPLoDYbKZ2h3RNE4uiEHzCNhjziJG7Lq_COP1n0Ya6h1ZGg%40mail.gmail.com.

Re: feature request: showing location of failed constraint

2020-10-17 Thread Hongwei Xi

Have already kept a note of this request.


On Fri, Oct 2, 2020 at 9:13 AM Dambaev Alexander 
wrote:

> Hi,
>
> I found, that it is difficult to locate constraint, that had been failed
> to be solved.
> For example, I got error message like this:
> ```
> /data/devel/ats2/bytestring/DATS/bytestring_flat.dats: 12395(line=442,
> offs=49) -- 12409(line=442, offs=63): error(3): unsolved constraint:
> C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(>=); S2EVar(5829), S2Eintinf(0)))
> ```
>
> which shows me where the constraint failed to be satisfied, but does not
> shows which constraint I need to debug.
> In this particular case, there are 11 lines of constraints for me and I
> required to be very careful to found which one had issue.
>
> I hope, that at least ATS3 will be able to provide location of constraint
> definition to debug
>
> --
> 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/CAHjn2KzZuP5E3yiaoaTVFSN9Wng-QGrWOMJjt_w0pf_eKePJLw%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/CAPPSPLqdLxkjFYxAtKDx4705Ek4yV5Wj1rdTM3gZ5RZKDhjV_w%40mail.gmail.com.

Re: non-exhaustive pattern match in case+ expression

2020-10-17 Thread Hongwei Xi

Thanks for reporting it.

Finally got some time fixing this issue. Basically, records were not
handled. They are now handled.
The changes should go into the next release.

On Wed, Oct 14, 2020 at 5:48 AM Dambaev Alexander 
wrote:

> Hi,
> I have the following example:
> ```
> #include "share/atspre_define.hats"
> #include "share/atspre_staload.hats"
>
> #define ATS_DYNLOADFLAG 0
>
> implement main0() = {
>   val a = (Some_vt(0), None_vt())
>   val b =
> case+ a:(Option_vt(int), Option_vt(int)) of (* *9* *)
> | @( ~Some_vt(_), ~Some_vt(_)):(Option_vt(int), Option_vt(int)) => 0
> | @( ~Some_vt(_), ~None_vt()):(Option_vt(int), Option_vt(int)) => 1
> | @( ~None_vt(), ~Some_vt(_)):(Option_vt(int), Option_vt(int)) => 2
> | @( ~None_vt(), ~None_vt()):(Option_vt(int), Option_vt(int)) => 3 (*
> *13* *)
> }
> ```
> which produces the following error
> ```
> /data/devel/ats2/issue/main.dats: 172(line=9, offs=5) -- 503(line=13,
> offs=71): error(3): pattern match is nonexhaustive:
> @{0= Some_vt(_), 1= None_vt()}
> /data/devel/ats2/issue/main.dats: 172(line=9, offs=5) -- 503(line=13,
> offs=71): error(3): pattern match is nonexhaustive:
> @{0= None_vt()}
> typechecking has failed: there are some unsolved constraints: please
> inspect the above reported error message(s) for information.
> exit(ATS): uncaught exception:
> _2tmp_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
> ```
> I guess it is related to the same "weak type inference" thing, but type
> annotations are not helpful here. Replacing with '*case-*' helps, of
> course, but I would like to know how can I use case+ instead
>
> --
> 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/CAHjn2KzL02cZTA7CP_aWMet_Hk%2BtYkMxAAZgejcTjC3%2B36Y8ZA%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/CAPPSPLrmyUxpzbuwsKF1b%3DCZN_kELm1iqxLenVN9R%2ByjhptX3Q%40mail.gmail.com.

Re: case expressions in let binding and dataviewtypes

2020-10-13 Thread Hongwei Xi

The support for type inference in ATS2 is weak.
Often you need a type annotation for a case-expression
(or an if-expression):

implement main0() = {
  val a = 0
  val b =
(
case+ a of
| 0 => Some_vt(0) *(* 9 *)*
| _ => None_vt()  *(* 10 *)*
) : Option_vt(int)
  val () =
case+ b of
| ~None_vt() => ()
| ~Some_vt(_) => ()
}

On Tue, Oct 13, 2020 at 10:09 AM Dambaev Alexander 
wrote:

> Hi,
>
> In this example, I am trying to define a binding of type Option_vt(int),
>
> ```
> #include "share/atspre_staload.hats"
>
> #define ATS_DYNLOADFLAG 0
>
> implement main0() = {
>   val a = 0
>   val b =
> case+ a of
> | 0 => Some_vt(0) *(* 9 *)*
> | _ => None_vt()  *(* 10 *)*
>   val () =
> case+ b of
> | ~None_vt() => ()
> | ~Some_vt(_) => ()
> }
> ```
> but I get the following error from the compiler:
> ```
> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -o issue   main.dats
> /data/devel/ats2/issue/main.dats: 136(line=9, offs=12) -- 146(line=9,
> offs=22): error(3): the dynamic expression cannot be assigned the type
> [S2EVar(5243)].
> /data/devel/ats2/issue/main.dats: 136(line=9, offs=12) -- 146(line=9,
> offs=22): error(3): mismatch of sorts in unification:
> The sort of variable is: S2RTbas(S2RTBASimp(1; t@ype))
> The sort of solution is: S2RTbas(S2RTBASimp(2; viewtype))
> /data/devel/ats2/issue/main.dats: 136(line=9, offs=12) -- 146(line=9,
> offs=22): error(3): mismatch of static terms (tyleq):
> The actual term is: S2Eapp(S2Ecst(option_vt0ype_bool_vtype);
> S2Eapp(S2Ecst(g1int_int_t0ype); S2Eextkind(atstype_int), S2Eintinf(0)),
> S2Ecst(true_bool))
> The needed term is: S2EVar(5243)
> /data/devel/ats2/issue/main.dats: 158(line=10, offs=12) -- 167(line=10,
> offs=21): error(3): the dynamic expression cannot be assigned the type
> [S2EVar(5243)].
> /data/devel/ats2/issue/main.dats: 158(line=10, offs=12) -- 167(line=10,
> offs=21): error(3): mismatch of sorts in unification:
> The sort of variable is: S2RTbas(S2RTBASimp(1; t@ype))
> The sort of solution is: S2RTbas(S2RTBASimp(2; viewtype))
> /data/devel/ats2/issue/main.dats: 158(line=10, offs=12) -- 167(line=10,
> offs=21): error(3): mismatch of static terms (tyleq):
> The actual term is: S2Eapp(S2Ecst(option_vt0ype_bool_vtype); S2EVar(5245),
> S2Ecst(false_bool))
> The needed term is: S2EVar(5243)
> /data/devel/ats2/issue/main.dats: 200(line=13, offs=7) -- 210(line=13,
> offs=17): error(3): the constructor pattern cannot be assigned the type
> [S2EVar(5243)].
> /data/devel/ats2/issue/main.dats: 223(line=14, offs=7) -- 234(line=14,
> offs=18): error(3): the constructor pattern cannot be assigned the type
> [S2EVar(5243)].
> ```
> what is wrong with this example?
>
> Instead, this example is working:
> ```
> #include "share/atspre_staload.hats"
>
> #define ATS_DYNLOADFLAG 0
>
> implement main0() = {
>   val a = 0
>   val b =
> * f(a) where {fn f(a:int):<> Option_vt(int) =*
> case+ a of
> | 0 => Some_vt(0)
> | _ => None_vt()
>   }
>   val () =
> case+ b of
> | ~None_vt() => ()
> | ~Some_vt(_) => ()
> ```
> I have tried to reread the tutorial, but haven't found something related
> to this behavior
>
> --
> 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/CAHjn2KxcKRHMZxWkZZTqy7yQLLbx3LQ_FeTGrSn76xvXWh4%2BeQ%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/CAPPSPLot_wFq%2BbqZT4PAUoUM8EEgv_N_uc1FMYb%3Dbn9fhDs%2BEg%40mail.gmail.com.

Re: performance considerations of patsopt

2020-10-04 Thread Hongwei Xi

In this case, the long time compilation of your ATS code is most likely
caused
by constraint-solving. You may try to use the following flag to skip
constraint-solving:

--constraint-ignore

This will tell you if constraint-solving is indeed the culprit here.

Using an external constraint-solver like Z3 may improve. However,
constraint-solving
is inherently of exponential-time.



On Sun, Oct 4, 2020 at 8:15 AM Dambaev Alexander 
wrote:

> Hi,
> I have noticed, that patsopt takes huge amount of time, to compile
> relatively small library https://github.com/dambaev/ats-bytestring
>
> ``
> [nix-shell:/data/devel/ats2/bytestring]$ $(which time) make test1
> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -c -o SATS/bytestring_sats.o
> SATS/bytestring.sats
> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -c -o
> DATS/bytestring_flat_dats.o DATS/bytestring_flat.dats
> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -o test1
> SATS/bytestring_sats.o DATS/bytestring_flat_dats.o TEST/test1.dats
> 39.00user 0.43system *0:39.44*elapsed 99%CPU (0avgtext+0avgdata *215060*
> maxresident)k
> 0inputs+1024outputs (0major+140589minor)pagefaults 0swaps
> ```
>
> and one project, that uses this library take forever to compile:
>
> ```
> $ $(which time) make
> make -C src
> make[1]: Entering directory '/data/devel/smartplants/lora2mqtt/src'
> patscc -O2 -DATS_MEMALLOC_LIBC
> -I"/nix/store/cqynqsas6nwk3gbn8m2pi9lx4m0shr0y-ats2-0.3.13/lib/ats2-postiats-0.3.13/contrib/atscntrb/"
> -I"../libs/" -c -o DATS/logging_dats.o DATS/logging.dats
> /data/devel/smartplants/lora2mqtt/src/DATS/logging.dats: 3255(line=92,
> offs=24) -- 3255(line=92, offs=24): error(3): unsolved constraint:
> C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(>);
> S2EVar(5345->S2Evar(refcnt$8767$8777$8786$8794$8801$8807$8812$8816$8819(14823))),
> S2Eintinf(0)))
> ^Cmake[1]: *** [Makefile:71: DATS/logging_dats.o] Error 1
> make: *** [Makefile:2: all] Interrupt
> Command terminated by signal 2
> 202.80user 0.28system *3:23.13*elapsed 99%CPU (0avgtext+0avgdata *384768*
> maxresident)k
> 0inputs+0outputs (0major+97710minor)pagefaults 0swaps
>
> $ cat src/DATS/logging.dats | wc -l
> 120
> ```
> I had interrupted when the first error had been reported.
>
> What are the best practice to get reasonable performance of patsopt?
>
> --
> 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/CAHjn2KwdMZNSdJhtypDjpZyLDfqR2zZpca8LH-81UYyrk4UMzQ%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/CAPPSPLoy0jdo884-_JD%3DmHLdad7ytsSiWg%2BMsGjp5iH9BM2Yng%40mail.gmail.com.

Re: changing the value of vtype

2020-10-03 Thread Hongwei Xi

By the way, if 'i' is call-by-value, then it cannot be updated. If it needs
to be updated,
then it cannot be call-by-value.


On Sun, Oct 4, 2020 at 1:01 AM Hongwei Xi  wrote:

> The following line caused the issue:
>
> val () = i := build( () | (len, offset, cap, i2sz 0, refcnt + i2sz 1,
> dynamic, p)) // restore i
>
> It should be changed to
>
> prval () = i := build( () | (len, offset, cap, i2sz 0, refcnt + i2sz 1,
> dynamic, p)) // restore i
>
> Only a linear proof call-by-value argument can be a left-value. So 'i' is
> treated as a proof,
> and its erasure is of the type 'void'.
>
>
> On Sat, Oct 3, 2020 at 11:32 PM Dambaev Alexander 
> wrote:
>
>> Hi,
>>
>> I have a viewtype, defined like this:
>> ```
>> absvt0ype
>>   Bytestring_vtype
>>   ( len:int (* size in bytes, which occupied by data *)
>>   , offset: int (* the offset from base pointer at which data of length
>> len starts *)
>>   , cap: int (* capacity of the buffer *)
>>   , ucap: int (* how much unused bytes of buffer available after this
>> bytestring *)
>>   , refcnt:int (* how many other bytestrings refer to this bytestring *)
>>   , dynamically_allocated: bool (* if false, then base pointer is
>> statically allocated *)
>>   , base: addr (* base pointer *)
>>   ) =
>>   ( void
>>   | ( size_t (* len *)
>> , size_t (* offset *)
>> , size_t (* capacity *)
>> , size_t (* available capacity *)
>> , size_t (* refcnt *)
>> , bool (* is dynamically allocated *)
>> , ptr
>> )
>>   )
>>
>> (* bytestring, which backend memory is not shared with other bytestrings
>> *)
>> vtypedef
>>   BytestringNSH0 =
>>   [len: nat][offset,cap,ucap:nat][dynamically_allocated:bool][l:agz]
>>   Bytestring_vtype( len, offset, cap, ucap, 0, dynamically_allocated,l)
>>
>> ```
>>
>> In many functions, I would like to modify argument's type and value in
>> order to modify reference count, the simplified example of usage is:
>> ```
>> fn
>>   test1(): $BS.BytestringNSH0 = bs1 where {
>>   val bs = $BS.pack "hello world"
>>   val bs1 = $BS.incref_bs bs
>>   // do some stuff like val bs2 = $BS.take( i2sz 2, bs1)...
>>   val () = $BS.decref_bs( bs, bs1) // consume bs and decref for bs1
>> }
>> ```
>> where incref_bs and decref_bs defined like this:
>> ```
>> fn
>>   decref_bs
>>   {c_len, c_offset, cap, c_ucap: nat}{dynamic:bool}{l:addr}
>>   {p_len, p_offset, p_ucap, p_refcnt: nat | *p_refcnt > 0*}
>>   ( consume: Bytestring_vtype( c_len, c_offset, cap, c_ucap, *1*,
>> dynamic, l) // consume bytestring with refcounter = 1
>>   , preserve: !Bytestring_vtype( p_len, p_offset, cap, p_ucap, *p_refcnt*,
>> dynamic, l) >> Bytestring_vtype( p_len, p_offset, cap, p_ucap, *p_refcnt
>> - 1*, dynamic, l) // and decrease refcounter for one, that should be
>> preserved
>>   ):
>>   void
>> fn
>>   incref_bs
>>   {len, offset, cap, ucap, refcnt: nat}{dynamic:bool}{l:addr}
>>   ( i: !Bytestring_vtype( len, offset, cap, ucap, *refcnt*, dynamic, l)
>> >> Bytestring_vtype( len, offset, cap, 0, *refcnt + 1*, dynamic, l) //
>> increase reference counter on original bytestring
>>   ):
>>   Bytestring_vtype( len, offset, cap, ucap, *1*, dynamic, l) // produce
>> the same string with refcount == 1
>> ```
>> and the implementation of incref_bs is (decref_bs is similar to it):
>> ```
>> implement incref_bs( i) = res where {
>>   extern castfn
>> explode
>> { len, offset, cap, ucap, refcnt:nat}{dynamic:bool}{l:addr}
>> ( i: Bytestring_vtype( len, offset, cap, ucap, refcnt, dynamic, l)
>> ):<> ( size_t(len), size_t(offset), size_t(cap), size_t(ucap),
>> size_t(refcnt), bool(dynamic) ptr(l))
>>   extern castfn
>> build
>> { len, offset, cap, ucap, refcnt:nat}{dynamic:bool}{l:addr}
>> ( void
>> | ( size_t(len), size_t(offset), size_t(cap), size_t(ucap),
>> size_t(refcnt), bool(dynamic), ptr(l) )
>> ):<> Bytestring_vtype( len, offset, cap, ucap, refcnt, dynamic, l)
>>   val (len, offset, cap, ucap, refcnt, dynamic, p) = explode(i) //
>> consume i
>>   val res = build( () | (len, offset, cap, ucap, i2sz 1, dynamic, p))
>>   val () = i := build( () | (len, offset, cap, i2sz 0, refcnt + i2sz 1,
>> dynamic, p)) // restore i
>> }
>> ```
>> this implementation typechecks, but C's generated code can't be compiled
>> with error:
>> ```
>>
>> /nix/store/

Re: changing the value of vtype

2020-10-03 Thread Hongwei Xi

The following line caused the issue:

val () = i := build( () | (len, offset, cap, i2sz 0, refcnt + i2sz 1,
dynamic, p)) // restore i

It should be changed to

prval () = i := build( () | (len, offset, cap, i2sz 0, refcnt + i2sz 1,
dynamic, p)) // restore i

Only a linear proof call-by-value argument can be a left-value. So 'i' is
treated as a proof,
and its erasure is of the type 'void'.


On Sat, Oct 3, 2020 at 11:32 PM Dambaev Alexander 
wrote:

> Hi,
>
> I have a viewtype, defined like this:
> ```
> absvt0ype
>   Bytestring_vtype
>   ( len:int (* size in bytes, which occupied by data *)
>   , offset: int (* the offset from base pointer at which data of length
> len starts *)
>   , cap: int (* capacity of the buffer *)
>   , ucap: int (* how much unused bytes of buffer available after this
> bytestring *)
>   , refcnt:int (* how many other bytestrings refer to this bytestring *)
>   , dynamically_allocated: bool (* if false, then base pointer is
> statically allocated *)
>   , base: addr (* base pointer *)
>   ) =
>   ( void
>   | ( size_t (* len *)
> , size_t (* offset *)
> , size_t (* capacity *)
> , size_t (* available capacity *)
> , size_t (* refcnt *)
> , bool (* is dynamically allocated *)
> , ptr
> )
>   )
>
> (* bytestring, which backend memory is not shared with other bytestrings *)
> vtypedef
>   BytestringNSH0 =
>   [len: nat][offset,cap,ucap:nat][dynamically_allocated:bool][l:agz]
>   Bytestring_vtype( len, offset, cap, ucap, 0, dynamically_allocated,l)
>
> ```
>
> In many functions, I would like to modify argument's type and value in
> order to modify reference count, the simplified example of usage is:
> ```
> fn
>   test1(): $BS.BytestringNSH0 = bs1 where {
>   val bs = $BS.pack "hello world"
>   val bs1 = $BS.incref_bs bs
>   // do some stuff like val bs2 = $BS.take( i2sz 2, bs1)...
>   val () = $BS.decref_bs( bs, bs1) // consume bs and decref for bs1
> }
> ```
> where incref_bs and decref_bs defined like this:
> ```
> fn
>   decref_bs
>   {c_len, c_offset, cap, c_ucap: nat}{dynamic:bool}{l:addr}
>   {p_len, p_offset, p_ucap, p_refcnt: nat | *p_refcnt > 0*}
>   ( consume: Bytestring_vtype( c_len, c_offset, cap, c_ucap, *1*,
> dynamic, l) // consume bytestring with refcounter = 1
>   , preserve: !Bytestring_vtype( p_len, p_offset, cap, p_ucap, *p_refcnt*,
> dynamic, l) >> Bytestring_vtype( p_len, p_offset, cap, p_ucap, *p_refcnt
> - 1*, dynamic, l) // and decrease refcounter for one, that should be
> preserved
>   ):
>   void
> fn
>   incref_bs
>   {len, offset, cap, ucap, refcnt: nat}{dynamic:bool}{l:addr}
>   ( i: !Bytestring_vtype( len, offset, cap, ucap, *refcnt*, dynamic, l)
> >> Bytestring_vtype( len, offset, cap, 0, *refcnt + 1*, dynamic, l) //
> increase reference counter on original bytestring
>   ):
>   Bytestring_vtype( len, offset, cap, ucap, *1*, dynamic, l) // produce
> the same string with refcount == 1
> ```
> and the implementation of incref_bs is (decref_bs is similar to it):
> ```
> implement incref_bs( i) = res where {
>   extern castfn
> explode
> { len, offset, cap, ucap, refcnt:nat}{dynamic:bool}{l:addr}
> ( i: Bytestring_vtype( len, offset, cap, ucap, refcnt, dynamic, l)
> ):<> ( size_t(len), size_t(offset), size_t(cap), size_t(ucap),
> size_t(refcnt), bool(dynamic) ptr(l))
>   extern castfn
> build
> { len, offset, cap, ucap, refcnt:nat}{dynamic:bool}{l:addr}
> ( void
> | ( size_t(len), size_t(offset), size_t(cap), size_t(ucap),
> size_t(refcnt), bool(dynamic), ptr(l) )
> ):<> Bytestring_vtype( len, offset, cap, ucap, refcnt, dynamic, l)
>   val (len, offset, cap, ucap, refcnt, dynamic, p) = explode(i) // consume
> i
>   val res = build( () | (len, offset, cap, ucap, i2sz 1, dynamic, p))
>   val () = i := build( () | (len, offset, cap, i2sz 0, refcnt + i2sz 1,
> dynamic, p)) // restore i
> }
> ```
> this implementation typechecks, but C's generated code can't be compiled
> with error:
> ```
>
> /nix/store/cqynqsas6nwk3gbn8m2pi9lx4m0shr0y-ats2-0.3.13/lib/ats2-postiats-0.3.13/ccomp/runtime/pats_ccomp_instrset.h:339:39:*
> error: invalid use of void expression*
>  #define ATSINSstore(pmv1, pmv2) (pmv1 = pmv2)
>^
> bytestring_flat_dats.c:5417:1: note: in expansion of macro ‘ATSINSstore’
>  ATSINSstore(ATSderef(arg0, atsvoid_t0ype), ATSPMVcastfn(build,
> postiats_tyrec_0, tmp311)) ;
> ```
> and the generated code for incref_bs is:
> ```
> /*
> local:
> global: incref_bs$80$0(level=0)
> local:
> global:
> */
> ATSextern()
> postiats_tyrec_0
> bytestring__incref_bs(*atsrefarg0_type*(postiats_tyrec_0) arg0)
> {
> /* tmpvardeclst(beg) */
> ATStmpdec(tmpret301, postiats_tyrec_0) ;
> ATStmpdec(tmp302, atstkind_t0ype(atstype_size)) ;
> ATStmpdec(tmp303, atstkind_t0ype(atstype_size)) ;
> ATStmpdec(tmp304, atstkind_t0ype(atstype_size)) ;
> ATStmpdec(tmp305, atstkind_t0ype(atstype_size)) ;
> ATStmpdec(tmp306, atstkind_t0ype(atstype_size)) ;
> ATStmpdec(tmp307,

Re: Freestanding ATS

2020-10-03 Thread Hongwei Xi

In the past, I did use ATS2 to experiment with a kernel implementation:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/KernelBuilding

Basically, you can just use some compile-time flags to get rid of various
includes in the generated
C code. The following Makefile should be telling:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/KernelBuilding/singpolyma-kernel/Part1/Makefile

As for ATS3, I plan to support a scripting language for this kind of
configuration. Will do this very soon.


On Fri, Oct 2, 2020 at 9:10 PM Elronnd _  wrote:

> I'm trying to use ATS for OS development.  This means: no dependence on
> any feature of the host environment; nothing from libc.
>
> It looks like the parts of the prelude that implement basic types and
> language features are the same as the parts that interface with the host
> libc (for e.g. exit, malloc, etc.).  Is there something I'm missing?  If
> not, is there any chance official, integrated support can be added for a
> freestanding mode?  Happy to contribute on that count, FWIW; just want to
> gauge interest.
>
> --
> 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/9bf84c7c-c99d-4c72-8cca-392e41106576o%40googlegroups.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/CAPPSPLrQP-byQrkRvR9Sz6%2Bkx4xz2znr%3Dzr34P-cXtb9Zvd0iw%40mail.gmail.com.

Re: using #[] only for changing type of the argument's vtype

2020-09-28 Thread Hongwei Xi

I believe that #[...] must be at the leading position. Please try to change
each [...] to #[...].

On Mon, Sep 28, 2020 at 11:16 PM Dambaev Alexander 
wrote:

> Hi.
>
> I want to write a spec for a function 'append', which purpose is to append
> content of the second argument into the end of the content of the first one.
> I came to this:
> ```
> (* creates new bytestring with content of r appended to l. does not
> consumes l and r
>   in case if 'l' has enough unused capacity to fit 'r', it will copy
> content of 'r' into this unused space, incrementing reference counter of l
> and result
> *)
> fn
>   append
>   {l_len, l_offset, l_cap, l_ucap, l_refcnt: nat}{l_dynamic:bool}{l_p:addr}
>   {r_len, r_offset, r_cap, r_ucap, r_refcnt: nat}{r_dynamic:bool}{r_p:addr}
>   ( l: !Bytestring_vtype(l_len, l_offset, l_cap, l_ucap, l_refcnt,
> l_dynamic, l_p) >> Bytestring_vtype( l_len, l_offset, l_cap, *rl_ucap*,
> *rl_refcnt*, l_dynamic, l_p)
>   , r: !Bytestring_vtype(r_len, r_offset, r_cap, r_ucap, r_refcnt,
> r_dynamic, r_p)
>   ):
>   [reused_l: bool | (l_ucap >= r_len && reused_l == true) || reused_l ==
> false]
>   [offset:nat | (reused_l && offset == l_offset) || (reused_l == false &&
> offset == 0)]
>   [cap:nat | (reused_l && cap == l_cap) || (reused_l == false && cap ==
> l_len + r_len)]
>   [ucap:nat | (reused_l && ucap == l_ucap - r_len) || (reused_l == false
> && ucap == 0)]
>   *#[rl_ucap: nat | (reused_l && rl_ucap == 0) || (reused_l == false &&
> rl_ucap == l_ucap)]*
>   [refcnt:nat | (reused_l && refcnt == l_refcnt + 1) || (reused_l == false
> && refcnt == 0)]
>
> *#[rl_refcnt:nat | (reused_l && rl_refcnt == l_refcnt + 1) || (reused_l ==
> false && rl_refcnt == l_refcnt)]*  [dynamic:bool | (reused_l && dynamic
> == l_dynamic) || (reused_l == false && dynamic == true) ]
>   [l:addr | (reused_l && l == l_p) || (reused_l == false && l != l_p) ]
>   Bytestring_vtype( l_len+r_len, offset, cap, ucap, refcnt, dynamic, l)
> ```
> but compiler says, that I can't do it:
>
> ```
> /data/devel/ats2/bytestring/SATS/bytestring.sats: 6235(line=195, offs=3)
> -- 6765(line=200, offs=72): error(2): incorrect use of the existential
> quantifier #[...]
> /data/devel/ats2/bytestring/SATS/bytestring.sats: 6418(line=197, offs=3)
> -- 6765(line=200, offs=72): error(2): incorrect use of the existential
> quantifier #[...]
> /data/devel/ats2/bytestring/SATS/bytestring.sats: 5764(line=188, offs=129)
> -- 5771(line=188, offs=136): error(2): the static identifier [rl_ucap] is
> unrecognized.
> /data/devel/ats2/bytestring/SATS/bytestring.sats: 5773(line=188, offs=138)
> -- 5782(line=188, offs=147): error(2): the static identifier [rl_refcnt] is
> unrecognized.
> ```
> I guess, that rl_ucap and rl_refcnt have to be actually used in the type
> of the result, right?
>
> --
> 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/CAHjn2KwK0mE2DnApk9vMPkPZHGn3T0ELSyMr9pt4qDYc4hgiAw%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/CAPPSPLr70JeoTC6fmesLpgYH1kfPyLA95p36p_XtecVbEijsGQ%40mail.gmail.com.

Re: spotted compiler assert failure

2020-09-28 Thread Hongwei Xi

I just modified the code base to issue an error message in this case
(instead of just reporting a line number of with a compiler crash).

On Mon, Sep 28, 2020 at 7:36 AM Hongwei Xi  wrote:

> >>I expected, that there will be typechecking error, saying, that  buf_pf
> is being preserved with wrong type, forcing me to restore it, but instead I
> got error above.
>
> I have seen this issue before.
>
> Basically. for each stack-allocated variable ('buf' in this case), there
> should be a proof of
> some at-view associated with the variable at the end of its life. In this
> case, the proof associated
> with 'buf' is turned into a proof of the view Bytestring_v, which is not
> an at-view (of the form T@l).
>
>
> On Mon, Sep 28, 2020 at 4:13 AM Dambaev Alexander 
> wrote:
>
>> Hi,
>> I got assert failure:
>> ```
>> exit(ATS): [assert] failed:
>> /tmp/ATS-Postiats/src/pats_trans3_env_dvar.dats: 14625(line=619, offs=20)
>> -- 14641(line=619, offs=36)
>> ```
>> from this code
>> SATS file:
>> ```
>> (* abstract viewtype, that describes Bytestring with capacity and size *)
>> absvt0ype
>>   Bytestring_vtype
>>   ( len:int (* size in bytes, which occupied by data *)
>>   , offset: int (* the offset from base pointer at which data of length
>> len starts *)
>>   , cap: int (* capacity of the buffer *)
>>   , ucap: int (* how much unused bytes of buffer available after this
>> bytestring *)
>>   , refcnt:int (* how many other bytestrings refer to this bytestring *)
>>   , dynamically_allocated: bool (* if false, then base pointer is
>> statically allocated *)
>>   , base: addr (* base pointer *)
>>   ) =
>>   ( void
>>   | ( size_t (* len *)
>> , size_t (* offset *)
>> , size_t (* capacity *)
>> , size_t (* available capacity *)
>> , size_t (* refcnt *)
>> , bool (* is dynamically allocated *)
>> , ptr
>> )
>>   )
>> (* abstract viewtype, that describes Bytestring with capacity and size *)
>> absvt0ype
>>   Bytestring_vtype
>>   ( len:int (* size in bytes, which occupied by data *)
>>   , offset: int (* the offset from base pointer at which data of length
>> len starts *)
>>   , cap: int (* capacity of the buffer *)
>>   , ucap: int (* how much unused bytes of buffer available after this
>> bytestring *)
>>   , refcnt:int (* how many other bytestrings refer to this bytestring *)
>>   , dynamically_allocated: bool (* if false, then base pointer is
>> statically allocated *)
>>   , base: addr (* base pointer *)
>>   ) =
>>   ( void
>>   | ( size_t (* len *)
>> , size_t (* offset *)
>> , size_t (* capacity *)
>> , size_t (* available capacity *)
>> , size_t (* refcnt *)
>> , bool (* is dynamically allocated *)
>> , ptr
>> )
>>   )
>> vtypedef
>>   Bytestring(len) =
>>   {len:
>> nat}[offset,cap,ucap,refcnt:nat][dynamically_allocated:bool][l:agz]
>>   Bytestring_vtype( len, offset, cap, ucap, refcnt,
>> dynamically_allocated,l)
>>
>> absview
>>   Bytestring_v(a:t0ype, len:int, offset:int, cap: int, ucap: int,
>> refcnt:int, dynamically_allocated:bool, l:addr)
>>
>> (* non-empty bytestring *)
>> vtypedef
>>   Bytestring1 =
>>   [len:
>> pos][offset,cap,ucap,refcnt:nat][dynamically_allocated:bool][l:agz]
>>   Bytestring_vtype( len, offset, cap, ucap, refcnt,
>> dynamically_allocated,l)
>>
>> fn
>>   pack_chars_static
>>   {n:nat}{l:agz}{a:t0ype}
>>   ( !array_v( a, l, n) >> Bytestring_v(a, n, 0, n, 0, 0, false, l)
>>   | i: ptr l
>>   , sz: size_t n
>>   ):
>>   Bytestring_vtype( n, 0, n, 0, 0, false, l)
>>
>> overload pack with pack_chars_static
>> ```
>> DATS file:
>> ```
>> #include "share/atspre_staload.hats"
>>
>> #define ATS_DYNLOADFLAG 0
>>
>> staload BS="SATS/bytestring.sats"
>> staload "DATS/bytestring_flat.dats"
>>
>> implement pack_chars_static{n}{l}{a}(pf | p, sz) =
>> let
>>   extern castfn
>> believeme
>> {n,offset,cap,ucap,refcnt:nat}{dynamic:bool}{l:agz}
>> ( !array_v( a, l, cap) >> Bytestring_v(a, n, offset, cap, ucap,
>> refcnt, dynamic, l)
>> | ( size_t(n)
>>   , size_t(offset)
>>   , size_t(cap)
>>   , size_t(ucap)
>>   , size_t(refcnt)
>>   , bool(dynamic)
>>   , ptr(l)
>>   )
>> ):<>
>> Bytestring_vtype(n, offset, cap, u

Re: symbol overloading resolution and statics

2020-09-27 Thread Hongwei Xi

Yes, that is correct. Overloading resolution
only uses type erasures (that is, types without indices) and arity
information.

BTW.

In ATS2, template resolution uses dependent types (that is, types with
indices)
to select template implementation. This caused a nightmare in terms of
usability :(
In ATS3, template resolution only uses type erasures.

--Hongwei


On Sun, Sep 27, 2020 at 4:32 AM Dambaev Alexander 
wrote:

> Hi,
>
> I have 2 functions:
> ```
> fn
>   free_static
>   {len, offset, cap: nat}{l:addr}
>   ( v: Bytestring_vtype(len, offset, cap, 0, *false*, l)
>   ): void
> fn
>   free_dynamic
>   {len, offset, cap: nat}{l:addr}
>   ( v: Bytestring_vtype(len, offset, cap, 0, *true*, l)
>   ): void
> ```
> where false means "not dynamic" and true - dynamic
> I was hoping, that this difference will be enough to differentiate those
> functions for overloading like this:
> ```
> symintr free
> overload free with free_static
> overload free with free_dynamic
> ```
> but compiler complains with:
> ```
> /data/devel/ats2/bytestring/TEST/test9.dats: 418(line=19, offs=12) --
> 428(line=19, offs=22): error(3): the symbol [$BS.free] cannot be resolved
> due to too many matches:
> D2ITMcst(free_dynamic) of 0
> D2ITMcst(free_static) of 0
> ```
> am I correct to assume, that in this case compiler is only looking on a
> type of arguments and arity of given alternatives to choose which function
> to resolve to?
>
> --
> 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/CAHjn2KyVjgjoXbX97ALw8R5HhaVhMyimrBqpuRBKgNGFSLH_Eg%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/CAPPSPLrktgMRPTMoZo9am4BLe92Td6nk78e9oT3Hae56Q2UoZQ%40mail.gmail.com.

Re: resolving overloaded operators and staload

2020-09-24 Thread Hongwei Xi

Yes, you are correct.

An overload declaration in a package is available only when the package is
opened.

>>is it ok to have such 2 staloads or are there any other good practice to
staload only overloaded symbols? Maybe, there is a way to staload only some
of symbols (like in haskell's 'import' command like this:

Staloading is idempotent. It is totally okay to overload it multiple times.

I often just add the following line in the file where appendC is used:

overload + with $BS.appendC

Supporting haskell-like imports should be straightforward. Let me postpone
this until ATS3 is ready.

--Hongwei



On Thu, Sep 24, 2020 at 12:11 AM Dambaev Alexander 
wrote:

> Hi,
> I want to confirm what I see in practice:
> 1. I had defined abstract vtype Bytesting and overloaded '+' operator for
> it like this:
> ```
> (* the same as append, but consumes arguments in order to make caller's
> code clear from bunch of val's and free()
>  *)
> fn
>   appendC
>   {l_n, r_n, l_cap, r_cap: nat}
>   ( l: Bytestring(l_n, l_cap)
>   , r: Bytestring(r_n, r_cap)
>   ):
>   [res_cap: nat | res_cap >= l_n + r_n]
>   Bytestring( l_n+r_n, res_cap)
>
> overload + with appendC
> ```
> in the SATS file
>
> 2. I want to have an alias for symbols from this SATS file, so I am
> staloading it like this:
> ```
> staload BS="{$LIBS}/ats-bytestring/SATS/bytestring.sats"
> ```
> 3. but this is not enough to bring overloading of '+' into the scope and I
> have to add another staload:
> ```
> staload "{$LIBS}/ats-bytestring/SATS/bytestring.sats" (* for operator
> overloading in scope *)
> ```
>
> am I correct to assume, that I need the second staload to add overloading
> info into the global scope?
> Because without second staload, I can't write:
> ```
> val one = $BS.pack "one"
> val two = $BS.pack "two"
> val three = one + two (* failes to resolve + here without second staload *)
> ```
>
> is it ok to have such 2 staloads or are there any other good practice to
> staload only overloaded symbols? Maybe, there is a way to staload only some
> of symbols (like in haskell's 'import' command like this:
> ```
> import Data.ByteString (ByteString) -- imports only ByteString type into
> global scope
> import qualified Data.ByteString as BS -- the rest are being accessed only
> through alias BS
> ```
> )
>
>
> --
> 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/CAHjn2KyUefdSgSMyunE_QYDHCp1L6uUdRt-sbBKjWgWNKxHZJg%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/CAPPSPLpn6PjWcoP49opMnwzL2q0BMT%2BHz3NWwFqfEtuO-pZSAw%40mail.gmail.com.

Re: How to avoid to return uninitialized value on ATS2?

2020-09-16 Thread Hongwei Xi

It works because the type for sbuf_bcat allows it:

val () = sbuf_bcat{elf_thrmisc_t}(pf_thrmisc | addr_thrmisc) // fails
val () = sbuf_bcat{elf_thrmisc_t?}(pf_thrmisc | addr_thrmisc) // succeeds


On Wed, Sep 16, 2020 at 3:10 AM Kiwamu Okabe  wrote:

> Dear all,
>
> I try to avoid following issue using ATS2:
>
> * Security Advisory:
> https://www.freebsd.org/security/advisories/FreeBSD-SA-20:03.thrmisc.asc
> * Patch
> https://github.com/freebsd/freebsd/commit/685a165c4c0b975cb2819b7042e1ddbc6eb79c5d
>
> This issue is caused by returning uninitialized value into user space
> from FreeBSD kernel.
> Then I wrote following pseudo code:
>
>
> https://github.com/metasepi/postmortem/blob/master/Security-Advisory/FreeBSD-kernel/FreeBSD-SA-20:03.thrmisc/Resolution/ATS2/error/main.dats
>
> Above code can't avoid this issue with at-view.
>
> * `!a? @ l >> a @ l` means to initialize uninitialized value
> * `!a @ l` means to take and keep initialized or uninitialized value
>
> How to explain to take "uninitialized value" as type?
>
> 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%3Dkyay10uEqkyzgJoWOYe-ToHGtLv08m2QREbp%2BbWLt-w%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/CAPPSPLo2t6VD_-pTnzZXV0j18zmsP3gGc0z%3D5bcRdtfgA_TpHw%40mail.gmail.com.

Re: What is the difference between the two ways of declaring parameters?

2020-09-14 Thread Hongwei Xi

 >> fn add2 (x, y: int): int = x * x + y * y

ATS2 does very little of type-inference. Every argument of
a function needs to be given a type in principle.


On Mon, Sep 14, 2020 at 11:54 AM Timmy Jose  wrote:

>
> Suppose I have this simple function:
>
> fn add1 (x: int, y: int): int = x * x + y * y
>
> This works as expected.
>
> However, if I define the parameters so:
>
> fn add2 (x, y: int): int = x * x + y * y
>
> where I bunch up the parameters together, I get the following error (not a
> syntax error):
>
> 6| fn add2 (x, y: int): int = x * x + y * y
>   ^
>error: the symbol [*] cannot be resolved due to too many matches:
>   D2ITMcst(mul_size1_int1) of 22
>   D2ITMcst(mul_int1_size1) of 22
>
> 6| fn add2 (x, y: int): int = x * x + y * y
>   ^
>error: the symbol [+] cannot be resolved due to too many matches:
>   D2ITMcst(add_double_int) of 0
>   D2ITMcst(add_float_int) of 0
>
>error: the dynamic expression cannot be assigned the type
>   [g0int(# atstype_int)]
>
>error: mismatch of static terms (tyleq):
>   actual:  errexp
>   needed:  g0int(# atstype_int)
>
> patsopt(TRANS3): there are [3] errors in total.
>   exit(ATS): (1025)
>
> So what exactly is going on in this case? Is this not legal, or does this
> mean something else from what I'm using it as? Is this a  bug?
>
> Thanks!
>
> Timmy
>
> --
> 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/7fbabd9c-fd3d-4cef-8a14-8e8a23f81257n%40googlegroups.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/CAPPSPLqLgHf37qjnAYuX2%2BRzEw1fHd3bjckL-0HCkAP-hnwo9g%40mail.gmail.com.

Re: How to Free a Pointer to a viewt@ype

2020-09-02 Thread Hongwei Xi

The type-checker has quite a few limitations in handling existential
quantifiers.
Here is a way to circumvent the problem:

  implement
  mesh_delete( mpf, mpff | m ) =
  let
val m1 = !m
  in
arrayptr_free(m1.vap);
arrayptr_free(m1.tap);
ptr_free(mpff, mpf | m)
  end


  implement
  mesh_delete( mpf, mpff | m ) =
  let
val m1 = !m
  in
arrayptr_free(m1.vap);
arrayptr_free(m1.tap);
ptr_free(mpff, mpf | m)
  end



On Wed, Sep 2, 2020 at 11:04 PM d4v3y_5c0n3s  wrote:

> So, I've got the following code:
> absvt@ype mesh
>
> assume mesh =
> [v,t:int]
> [vl,tl:addr]
> @{
>   v=int v, t=int t, vap=arrayptr(vertex, vl, v), tap=arrayptr(uint32, tl,
> t)
> }
>
> fun mesh_delete {l:addr} ( mpf: mesh @ l, mpff: mfree_gc_v(l) | m: ptr l )
> : void = "sta#%"
>
> implement mesh_delete ( mpf, mpff | m ) =
> (
>   arrayptr_free(!m.vap);
>   arrayptr_free(!m.tap);
>   ptr_free(mpff, mpf | m)
> )
>
> However, I'm getting the following error:
> patscc -tcats /home/tmj90/Goldelish-Engine/source/g_engine.dats
> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 69182(line=2426,
> offs=18) -- 69185(line=2426, offs=21): error(3): the dynamic expression
> cannot be assigned the type [S2Eat(S2EVar(7167), S2Evar(l$3392(8793)))].
> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 69182(line=2426,
> offs=18) -- 69185(line=2426, offs=21): error(3): mismatch of sorts in
> unification:
> The sort of variable is: S2RTbas(S2RTBASimp(1; t@ype))
> The sort of solution is: S2RTbas(S2RTBASimp(3; viewt0ype))
> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 69182(line=2426,
> offs=18) -- 69185(line=2426, offs=21): error(3): mismatch of static terms
> (tyleq):
> The actual term is: S2Etyrec(flt0; npf=-1; v=S2Eapp(S2Ecst(int);
> S2Evar(v$10840(16813))), t=S2Eapp(S2Ecst(int); S2Evar(t$10841(16814))),
> vap=S2Ecst(ptr_type), tap=S2Ecst(ptr_type))
> The needed term is: S2EVar(7167)
>
> I can allocate a pointer to mesh using ptr_alloc just fine, so why is
> ptr_free not working?  Do I need to get rid of the view to deallocate,
> perhaps using unsafe casting/functions?  Any help is appreciated, and if
> you'd like to see more of the code then please, ask me,
>
> --
> 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/3a5cd9b9-2ef3-4d32-8513-a4e952c09d26n%40googlegroups.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/CAPPSPLqLgv-Dbez04yHHyd1bH5HdTJTE%3Dt%2BXdUvQVQTThL9cuA%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.

Re: Solving compiler error

2020-08-30 Thread Hongwei Xi

This means that gpointer is declared more than once in your code.
You need to check various 'staload' declarations in your code.

On Sun, Aug 30, 2020 at 9:47 PM Dambaev Alexander 
wrote:

> Hi
> Usually, I am able to parse and solve compiler errors, but now I need help:
>
> ```
>   macdef GSIGNAL_CANCELLED = $extval( $GLIB.gsignal, "cancelled")
>   fn foo( p: $GLIB.gpointer): void = ()
>   val p = $GLIB.gpointer the_null_ptr
>   prval _ = $showtype p
>   val _ = $GLIB.g_signal_connect( cancellable, GSIGNAL_CANCELLED,
> $GLIB.G_CALLBACK(foo), p)
> }
> ```
>
> I get:
>
> ```
> **SHOWTYPE[UP]**(/data/devel/cacaoweb/folders/libfm/base/DATS/folders.dats:
> 664(line=31, offs=23) -- 665(line=31, offs=24)): S2Ecst(gpointer):
> S2RTbas(S2RTBASimp(0; type))
> /data/devel/cacaoweb/folders/libfm/base/DATS/folders.dats: 755(line=32,
> offs=90) -- 756(line=32, offs=91): error(3): the dynamic expression cannot
> be assigned the type [S2Ecst(gpointer)].
> /data/devel/cacaoweb/folders/libfm/base/DATS/folders.dats: 755(line=32,
> offs=90) -- 756(line=32, offs=91): error(3): mismatch of static terms
> (tyleq):
> The actual term is: S2Ecst(gpointer)
> The needed term is: S2Ecst(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/CAHjn2KxgmRqw9vsZKdTAh6ygegsEKb8mQhPgN9zXepGAR8QJOg%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/CAPPSPLpwni%3DNDOgJRVio6iq8QmCooy%2B5PYicacRGPdVWPraxJw%40mail.gmail.com.

Re: How to assign a `shared` value onto a member of vtype?

2020-08-29 Thread Hongwei Xi

Well, you did not prove that the one returned is the same as the one
borrowed :)


On Sat, Aug 29, 2020 at 9:05 PM Kiwamu Okabe  wrote:

> Dear Hongwei,
> thank you for your reply.
>
> On Sat, Aug 29, 2020 at 11:05 PM Hongwei Xi  wrote:
> > In the following code, the proof of the view associated with opts is
> > stored in inp.sh. This proof needs to be taken out and put back into
> view@opts
> > before the function main0 can exit.
> >
> > implement main0 () = let
> > var opts: ip6_pktopts
> > var inp: inpcb
> > val () = inp.in6p_outputopts := addr@opts
> > val () = inp.sh := shared_make(view@opts | addr@opts)
> >   in
> > ignoret(usleep(1000u))
> >   end
>
> So I think I miss-understanded `ignoret`.
> Then I tried to use `shared_unref` to return `view@opts`.
> But the code causes the other error:
>
>
> https://github.com/metasepi/postmortem/commit/cb97cf86f5cdb766b7b6123db674f58b95ed793c
>
> ```ats
> implement main0 () = let
> var opts: ip6_pktopts
> var inp: inpcb
> val () = inp.in6p_outputopts := addr@opts
> val () = inp.sh := shared_make(view@opts | addr@opts)
> val (pf_oopts | x, count) = shared_unref(inp.sh)
> val () = assertloc(count <= 1)
> prval Some_v(pf_opts) = pf_oopts
> prval () = view@opts := pf_opts
>   in
> ignoret(usleep(1000u))
>   end
> ```
>
> ```
> $ patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC main.dats -lpthread
> ../main.dats: 2867(line=106, offs=16) -- 2887(line=106, offs=36):
> error(3): viewat-restoration cannot be performed: mismatch of bef/aft
> locations of atviews:
> bef: [S2Evar(opts(8626))]
> aft: [S2Evar(l$8797$8799(14588))]
> ```
>
> Are `view@opts` and return from `shared_unref` not the same?
>
> 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%3DGfoVn7yJveTeiKpmOd0Kz%2Bkn_nCHQf3kfQJ-JkRtprw%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/CAPPSPLp5dtGpg%3DdkML6ZjVcKp91hCAGKBDNFd5aDtCXHi%3Dbm%3Dw%40mail.gmail.com.

Re: How to assign a `shared` value onto a member of vtype?

2020-08-29 Thread Hongwei Xi

In the following code, the proof of the view associated with opts is
stored in inp.sh. This proof needs to be taken out and put back into
view@opts
before the function main0 can exit.

implement main0 () = let
var opts: ip6_pktopts
var inp: inpcb
val () = inp.in6p_outputopts := addr@opts
val () = inp.sh := shared_make(view@opts | addr@opts)
  in
ignoret(usleep(1000u))
  end

On Sat, Aug 29, 2020 at 4:31 AM Kiwamu Okabe  wrote:

> Dear all,
>
> There is a security issue on FreeBSD:
>
> * Security Advisory:
> https://www.freebsd.org/security/advisories/FreeBSD-SA-20:20.ipv6.asc
> * The patch:
> https://github.com/freebsd/freebsd/commit/5707de0ed806712f53752acd433313a39f63f15c
>
> I'm writing following ATS code to try to avoid the issue:
>
>
> https://github.com/metasepi/postmortem/blob/master/Security-Advisory/FreeBSD-kernel/FreeBSD-SA-20:20.ipv6/Resolution/ATS2/error/main.dats
>
> But the code causes following error:
>
> ```
> $ patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC main.dats -lpthread
> .../FreeBSD-SA-20:20.ipv6/Resolution/ATS2/error/main.dats:
> 2574(line=98, offs=22) -- 2764(line=105, offs=6):
> error(3): the linear dynamic variable [opts$view$5659(-1)] is
> preserved but with an incompatible type.
> ```
>
> How to assign a `shared` value onto a member of vtype?
>
> 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%3DDxDQ4hNty%3DXA6t12Ge2LDuMQpv7C_wRLNsXUY_-t78w%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/CAPPSPLogy7PexTYTuNpYsyzPxAP0UuGy19HHeRRw9oYOWC_CmA%40mail.gmail.com.

Re: Segmentation fault in Braun Tree example (modified)

2020-08-20 Thread Hongwei Xi

When I encounter a segfault, it is usually caused by recursion depth being
over some kind of limit.

In your code, the 'aux' function is defined but never called. Here is a
fixed version:

fun
{a: t@ype}
brauntest1 (t0: tree a): bool =
  let exception Negative of ()
  fun aux (t0: tree a): bool =
case+ t0 of
  | tree_nil () => true
  | tree_cons (tl, _, tr) =>
  let val szl = size (tl)
  val szr = size (tr)
  in
if abs (szl - szr) > 1 then $raise Negative ()
  else aux(tl) andalso aux(tr)
  end
  in
try aux(t0) with ~Negative () => false
  end

On Thu, Aug 20, 2020 at 6:46 AM Timmy Jose  wrote:

>
>
> Hi,
>
> I have a variation of the Braun Tree test (where the size of the left and
> right subtrees differ by at most 1 at every level) from the tutorials, and
> this one, for some reason gives a segmentation fault.
>
> Here is the snippet:
>
> fun
> {a: t@ype}
> brauntest1 (t0: tree a): bool =
>   let exception Negative of ()
>   fun aux (t0: tree a): bool =
> case+ t0 of
>   | tree_nil () => true
>   | tree_cons (tl, _, tr) =>
>   let val szl = size (tl)
>   val szr = size (tr)
>   in
> if abs (szl - szr) > 1 then $raise Negative ()
>   else brauntest1 (tl) andalso brauntest1 (tr)
>   end
>   in
> try brauntest1 (t0) with ~Negative () => false
>   end
>
> And here is the output from `lldb` (gdb has some code-signing issues on
> macOS).
>
> $ lldb braun
> (lldb) target create "braun"
> Current executable set to 'braun' (x86_64).
> (lldb) r
> Process 28137 launched: '/braun' (x86_64)
> Process 28137 stopped
> * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS
> (code=2, address=0x7ffeef3fff68)
> frame #0: 0x00011577 braun`brauntest1_3__3__1 + 39
> braun`brauntest1_3__3__1:
> ->  0x11577 <+39>: callq  0x11c3a   ; symbol stub for:
> setjmp
> 0x1157c <+44>: testl  %eax, %eax
> 0x1157e <+46>: je 0x115de   ; <+142>
> 0x11580 <+48>: movq   0xb31(%rip), %rcx ;
> my_atsexnframe_getref.my_atsexnframe
> Target 0: (braun) stopped.
> (lldb)
>
> Anybody seen this before, or have an idea what might be going wrong?
>
> Thanks!
>
> Timmy
>
> --
> 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/ad557181-8986-4784-a724-2f2bba9cd5d9n%40googlegroups.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/CAPPSPLqhKexD7BhuSSGF9EUZ9cqz%2BZJ-nWg-2s1Tz7JeZWFwMA%40mail.gmail.com.

Re: A small query about closures

2020-08-11 Thread Hongwei Xi

The following header:

fn
linum (): void - void =

should be changed to

fn
linum (): () - void =

But this does not give what you expected.

You could use a reference:

fn
linum (): () - void=
let
val
line = ref(0)
in
lam () =>
let
val () = !line := !line + 1
in
println! ("Current line number = ", !line);
end
end

implement
main0() =
{
val f0 = linum()
val () = f0()
val () = f0()
val f1 = linum()
val () = f1()
val () = f1()
}


On Tue, Aug 11, 2020 at 10:10 AM Timmy Jose  wrote:

> Hello,
>
> I have a small closure implementation in Rust which looks like so:
>
> fn linum() -> impl FnMut() {
> let mut line = 0;
>
> Box::new(move || {
> line = line + 1;
> println!("Current line number is {}", line);
> })
> }
>
> fn main() {
> let mut l = linum();
> for _ in 0..5 {
> l();
> }
>
> l = linum();
> for _ in 0..5 {
> l();
> }
> }
>
> Basically, I simply want to capture the line variable in my closure.
> Running it:
>
> $ rustc linum.rs && ./linum
> Current line number is 1
> Current line number is 2
> Current line number is 3
> Current line number is 4
> Current line number is 5
> Current line number is 1
> Current line number is 2
> Current line number is 3
> Current line number is 4
> Current line number is 5
>
> as expected. Now, I was trying to replicate this behaviour in ATS (please
> note that I am totally new to ATS) using the chapter on functions, and this
> was my attempt:
>
> fn
> linum (): void - void=
>   let val line = 0
>   in
>lam () =>
>   let val line = line + 1
>   in
>println! ("Current line number = ", line);
>   end
>   end
>
> which gives the following errors:
>
> $ make
> acc pc -DATS_MEMALLOC_LIBC -O3 -o closures closures.dats
>
> /Users/z0ltan/dev/study/ats/introduction_to_programming_in_ats/revision/chapter3/closures.dats:
> 12:4-16:10
>
>error(3): dynamic arity mismatch: more arguments are expected.
>
> patsopt(TRANS3): there are [1] errors in total.
>   exit(ATS): (1025)
> make: *** [closures] Error 1
>
> Can someone help me understand what the problem is? I'm pretty sure my
> knowledge of ATS is not enough right now to maybe fully implement this the
> way I want it, but I would like some pointers on this error message and
> maybe a nudge in the right direction to be able to implement this!
>
> Thanks!
>
> Best Regards,
>
> Timmy
>
> (P.S: I hope it's all right if I keep posting questions every so often? I
> tried the IRC channel, but it appears to be inactive. Please let me know
> otherwise, in which case I'll bunch up my questions after having finished
> the basic tutorials!).
>
>
> --
> 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/92bd27f3-5d34-48dc-ac71-b9924ec58b4dn%40googlegroups.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/CAPPSPLrBOjAAEjptkwTu5o0UXVhMhdHkf%2B7jQGfWPDB%2Bj6b06w%40mail.gmail.com.

Re: Structural typing in ATS?

2020-08-08 Thread Hongwei Xi

Yes. But datatypes are nominal.

Often one uses abstract types to hide information. For example,

abst@ype Point2D

#extern
fun Point2D_get_x(Point2D): double

local

absimpl
Point2D = @{x=double,y=double}

in

implement Point2D_get_x(p) = p.x

end


On Sat, Aug 8, 2020 at 11:33 AM Timmy Jose  wrote:

>
> Hello,
>
> I was trying out some experiments as part of my learning process. The
> small program below typechecks and runs correctly:
>
> typedef
> point2D = @{ x = double, y = double }
>
> typedef
> coord = @{ x = double, y = double }
>
> fn
> display_point (name: string, p: point2D): void =
>   (println! ("[", name , "] x = ", p.x, "y = ", p.y))
>
> implement main0 () = {
>   val origin = @{ x = 0.0, y = 0.0 }: point2D
>   val () = display_point ("origin", origin)
>   val () = println! ("x = ", origin.x, ", y = ", origin.y)
>
>   val coord0 = @{ x = 0.0, y = 0.0 }: coord
>   val () = display_point ("coord0", coord0)
> }
>
> So I'm assuming that typing in ATS is structural instead of nominative
> since the `display_point` functions works for both `point2D` and `coord`
> values?
>
> Just wanted to confirm this. Thanks!
>
> Best,
>
> Timmy
>
> --
> 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/0d2e897a-5693-40f8-b268-60da5b71ac26n%40googlegroups.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/CAPPSPLrn_hDuaYvnWygByVgdBodvy-_qd8J6V-KHpBCdLOR9KQ%40mail.gmail.com.

Re: The current status of ATS3

2020-08-05 Thread Hongwei Xi

  >>1. Will ATS3 syntax and semantics diverge significantly from ATS2? (It
looks like it's mostly going to be similar, but please correct me if I'm
wrong), and

The syntax of ATS3 is very similar to that of ATS2.

Here is some code in ATS3:

https://github.com/xanadu-lang/xinterp/tree/master/srcgen/TEST

I would say that ATS2 and ATS3 share 95% of the syntax or more.

  2. Will there be an added focus on making ATS a production-capable
language with ATS3? (Again, looks to be the case from what I could figure
out, but please correct me again!)

Certainly. To program is to program productively. If we just talk about
using ATS with emacs (or other editors) to produce C (or JS) code of
quality, it won't take too
long. If we talk about an IDE of some sort, I don't feel I have the energy
and/or the expertise. But hopefully others may.

When compared to C, ATS2 and ATS3 use the same data representation (for
values of datatypes). As a consequence, the C code generated by ATS2 is
compatible with the C code generated by ATS3. Not only your learnings but
also your code can be carried forward :)

Cheers!

--Hongwei


On Wed, Aug 5, 2020 at 9:56 AM Timmy Jose  wrote:

> Hello all,
>
> I am learning the ATS language right now, and have a couple of questions:
>
>   1. Will ATS3 syntax and semantics diverge significantly from ATS2? (It
> looks like it's mostly going to be similar, but please correct me if I'm
> wrong), and
>   2. Will there be an added focus on making ATS a production-capable
> language with ATS3? (Again, looks to be the case from what I could figure
> out, but please correct me again!)
>
> I have a vested interest in asking these questions - as you yourselves
> acknowledge, the learning curve is not very smooth, but I'm enjoying it so
> far, and have hopes of using it as a production language in the near
> future, or at least for some serious projects. I just want to make sure
> than my learnings from
> ATS2 will carry forward as much as possible! :-)
>
> Best Regards,
>
> Timmy
>
> On Thursday, July 9, 2020 at 10:11:23 PM UTC+5:30 zuercher...@outlook.com
> wrote:
>
>>
>>
>> On Friday, July 3, 2020 at 8:03:08 AM UTC-5, Matthias Wolff wrote:
>>>
>>> C++ templates restricted to functions show only one half oft the truth.
>>>
>>> template
>>> struct function;
>>>
>>> struct XXX;
>>>
>>> template<>
>>> struct function {
>>>
>>> template
>>> void operator()(std::ostream& s, const A&... a) {
>>>(s  << ... << a);
>>> }
>>> };
>>>
>>> struct YYY;
>>>
>>> template<>
>>> struct function {
>>>
>>> template
>>> void operator()(const A&... a) {
>>>(s td::cout << ... << a
>>> );
>>> }
>>> };
>>>
>>> int main()
>>> {
>>>
>>> //using function object - additional constructor parenthesis
>>> function()(std::cout,"a",1);
>>>
>>> function()(1,"a");
>>>
>>> return 0;
>>>
>>> }
>>>
>>> Template power in c++ starts with structs or classes and templated
>>> normal functions
>>> are often used to redirect the call to templated structs and their
>>> specializations. Where
>>> structs/classes may have many also templated methods and many inner
>>> classes and
>>> yes a function - I think - can have inner structs:
>>>
>>> void my_function()
>>> {
>>> struct abc { void print() { std::cout << "ok" << std::endl; } };
>>>
>>> abc().print();
>>> }
>>> Variadic templates are really powerful "template struct
>>> mystruct" and next
>>> template type deduction.
>>>
>>> Template are not a weak point in C++. But if you look in direction of
>>> category theory, one can
>>> very quickly recognize, that this topic is a black hole. C++ has no
>>> mathematical inspiration
>>>
>>
>> Prior to Stroustrup's work on concept maps in concepts, C++ templates'
>> inspiration was almost entirely a proper subset of Ada generics (but
>> without Ada's option of shared implementation of machine code among all
>> expansions/type-instantiations).  C++ concepts without concept-maps has no
>> feature of which I am aware that Ada generics have not already had for
>> since either 1983 or 1995 editions of the Ada language.  The history of C++
>> prior to C++11 is almost entirely a multidecade critique of Ada:  C++ as
>> Ada done right was the mantra (which might be factually correct if
>> restricting* Ada to only Ada83 which was rather half-baked, because Ada95,
>> Ada2005, and especially Ada2012 are better examples of the Ada school of
>> thought done right—and they differ quite substantially in their definition
>> of “Ada done right” that C++'s definition of “Ada done right”).
>>
>> * The vast majority of DoD & aerospace usage of Ada in 2020 (i.e., what
>> remains extant in production, not transliterated into either Java or C++
>> with the historic Ada implementation abandoned) is strictly limited to
>> Ada83, prohibiting all later features, which is why AdaCore and other Ada
>> compiler vendors charge a premium for

Re: error messages

2020-08-03 Thread Hongwei Xi

By the way, an ifcase-expression should be used in place of the
case-expression
in your code. Also, I would like to point out that templates are a shining
feature of ATS :)

##

datatype
bstree(a:t@ype) =
| E of ()
| B of (bstree(a), a, bstree(a))

fun
{a:t@ype}
bstree_search
(
 t0: bstree(a),
 k0: a
) : bool =
case+ t0 of
| E () => false
| B (t1, k, t2) =>
  let
  val sgn =
  gcompare_val_val(k0, k)
  in
  ifcase
  | sgn < 0 => bstree_search (t1, k0)
  | sgn > 0 => bstree_search (t2, k0)
  | _ (* else *) => true
  end


On Mon, Aug 3, 2020 at 10:43 AM Hongwei Xi  wrote:

> There is a COMMA following 'false' that should be removed.
>
> BTW, the syntax of ATS is heavily influenced by Standard ML.
>
> On Mon, Aug 3, 2020 at 10:21 AM Timmy Jose  wrote:
>
>>
>> Hello,
>>
>> I've been trying to learn ATS from the official tutorials, and while I
>> like the language so far, and think that it is quite logical (if different
>> from many other languages in the same categories),  one thing that keeps
>> annoying me is getting some strange error messages.
>>
>> For instance, why is this a problem:
>>
>> fun
>> bstree_search (
>>   t0: bstree,
>>   k0: string
>> ): bool =
>> case+ t0 of
>>   | E () => false,
>>   | B (t1, k, t2) =>
>> let val sgn = compare (k0, k)
>> in case+ 0 of
>>   | _ when sgn < 0 => bstree_search (t1, k0)
>>   | _ when sgn > 0 => bstree_search (t2, k0)
>>   | _ => true
>> end
>>
>> I would expect that the return types of all sub-expressions are `void`
>> anyway, so why does the compiler complain:
>>
>> $ patscc -DATS_MEMALLOC_LIBC -o bst bst.dats && ./bst
>> /Users/z0ltan/dev/study/ats/introduction_to_programming_in_ats/chapter4/bst.dats:
>> 1022(line=53, offs=22) -- 1023(line=53, offs=23): error(parsing): the token
>> is discarded.
>> /Users/z0ltan/dev/study/ats/introduction_to_programming_in_ats/chapter4/bst.dats:
>> 1096(line=56, offs=9) -- 1098(line=56, offs=11): error(parsing): the token
>> is discarded.
>> exit(ATS): uncaught exception:
>> _2home_2hwxi_2Research_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
>>
>> The ATS FAQ recommends wrapping expressions with parentheses for such
>> errors, but doing so in this case does not get rid of the errors, and
>> secondly why is that even needed?
>>
>> Right now, this is the biggest thing that keeps tripping me up -
>> seemingly random "token discarded" error messages as well as some strange
>> "} keyword needed" error message etc. Experimenting randomly seems to fix
>> them most times, but is there any reason to this madness?
>>
>> Can anyone give me general guidelines to avoid seeing these sort of
>> trivial errors?
>>
>> Best,
>>
>> Timmy
>>
>> --
>> 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/71b5daaa-c80b-42d6-983a-72d8ab59b0ean%40googlegroups.com
>> <https://groups.google.com/d/msgid/ats-lang-users/71b5daaa-c80b-42d6-983a-72d8ab59b0ean%40googlegroups.com?utm_medium=email_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/CAPPSPLp869w2YMiaheMAranfUTk2s4ei9sdC_Y9zDvaRN1374Q%40mail.gmail.com.

Re: error messages

2020-08-03 Thread Hongwei Xi

There is a COMMA following 'false' that should be removed.

BTW, the syntax of ATS is heavily influenced by Standard ML.

On Mon, Aug 3, 2020 at 10:21 AM Timmy Jose  wrote:

>
> Hello,
>
> I've been trying to learn ATS from the official tutorials, and while I
> like the language so far, and think that it is quite logical (if different
> from many other languages in the same categories),  one thing that keeps
> annoying me is getting some strange error messages.
>
> For instance, why is this a problem:
>
> fun
> bstree_search (
>   t0: bstree,
>   k0: string
> ): bool =
> case+ t0 of
>   | E () => false,
>   | B (t1, k, t2) =>
> let val sgn = compare (k0, k)
> in case+ 0 of
>   | _ when sgn < 0 => bstree_search (t1, k0)
>   | _ when sgn > 0 => bstree_search (t2, k0)
>   | _ => true
> end
>
> I would expect that the return types of all sub-expressions are `void`
> anyway, so why does the compiler complain:
>
> $ patscc -DATS_MEMALLOC_LIBC -o bst bst.dats && ./bst
> /Users/z0ltan/dev/study/ats/introduction_to_programming_in_ats/chapter4/bst.dats:
> 1022(line=53, offs=22) -- 1023(line=53, offs=23): error(parsing): the token
> is discarded.
> /Users/z0ltan/dev/study/ats/introduction_to_programming_in_ats/chapter4/bst.dats:
> 1096(line=56, offs=9) -- 1098(line=56, offs=11): error(parsing): the token
> is discarded.
> exit(ATS): uncaught exception:
> _2home_2hwxi_2Research_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
>
> The ATS FAQ recommends wrapping expressions with parentheses for such
> errors, but doing so in this case does not get rid of the errors, and
> secondly why is that even needed?
>
> Right now, this is the biggest thing that keeps tripping me up - seemingly
> random "token discarded" error messages as well as some strange "} keyword
> needed" error message etc. Experimenting randomly seems to fix them most
> times, but is there any reason to this madness?
>
> Can anyone give me general guidelines to avoid seeing these sort of
> trivial errors?
>
> Best,
>
> Timmy
>
> --
> 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/71b5daaa-c80b-42d6-983a-72d8ab59b0ean%40googlegroups.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/CAPPSPLqp1V-Su-LrsP5nuoaGcFjYTLn%2B2zswKztYtexFdtdNQQ%40mail.gmail.com.

Fwd: [ats-lang-users] ATS2-0.4.1 released

2020-08-02 Thread Hongwei Xi

-- Forwarded message -

Hi,

It is my pleasure to announce the release
of ATS2-0.4.1. Note that this is the version needed
(or may be needed in the future) for compiling the
ongoing implementation of ATS3 (ATS/Xanadu).


ATS-Postiats-0.4.1.tgz:
The same as ATS-Postiats-int-0.4.1.tgz
MD5: 99d99ea8296035abc7983fc3c21e1f05
SHA1: 1e1d2b33b2f89ca229689de6fc6b403d0d35b6fe
--
ATS2-Postiats-gmp-1.4.0.tgz:
MD5: 1f73c15ec2fcf0b6880f7a2b3d5da17c
SHA1: af6a943b49236f02fcc1fe671477dbff85197c6a
--
ATS2-Postiats-int-1.4.0.tgz:
MD5: 6bbdd92aa412dd7f70a9e56363b8b22f
SHA1: 6c9e4032514a297365ad1f92a17dd61ead70755f


This is the 52nd release of ATS2, the successor of the
ATS programming language. The compiler for ATS2 is given
the name ATS/Positats, ATS2/Postiats or simply Postiats.

The official website for ATS is:

http://www.ats-lang.org

ATS-Postiats is hosted at github:

https://github.com/githwxi/ATS-Postiats

Major releases of ATS2 are available at:

https://sourceforge.net/projects/ats2-lang/

Major releases of external packages for ATS2 are available at:

https://sourceforge.net/projects/ats2-lang-contrib/

##

Here is a list of major additions and changes since the last
release:

There are only a few minor modifications made to the last release;
however, these modifications are needed for compiling ATS3 in the
future.

##

Please note that there are two variants of the ATS2 package being
released:

The "gmp" variant depends on the GMP library and the "int" variant does
not depend on the GMP library. In this release
ATS2-Postiats-0.4.1.tgz is just the same as ATS2-Postiats-int-0.4.1.tgz.

##

Cheers,

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: h...@cs.bu.edu
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)



___
ats-lang-users mailing list
ats-lang-us...@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/ats-lang-users

-- 
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/CAPPSPLqEA1yZFFT63xSsnKDUtObL8nrrXeFS-0Ga6T_XmO98bw%40mail.gmail.com.

Re: ATS Linux - A Feedback

2020-07-26 Thread Hongwei Xi

I read some of your code in lib/string.dats. I suppose that you would soon
find that
handling structs can be a big challenge.

Even without using linear types, you could potentially find bugs involving
dereferencing
NULL pointers. For example, in the following code, pde_subdir_find
obviously assumes that
its argument 'dir' is not NULL. But is this assumption really met at all
the call sites of pde_subdir_find?

static struct proc_dir_entry *pde_subdir_find(struct proc_dir_entry *dir,
  const char *name,
  unsigned int len)
{
struct rb_node *node = dir->subdir.rb_node; // dir could potentially be 
NULL
...

}

I would not be surprised if bugs of this kind are uncovered with some
easy dependent type checking.

Furthermore, things can turn out to be more interesting if linear
types are used. For example, hidden
bugs potentially causing resource leaks can be uncovered with linear
type checking.

If you use linear types, handling structs can be quite a challenge.
Maybe it is a good idea to avoid using linear
types for now.


On Sun, Jul 26, 2020 at 8:57 PM Matthias Wolff 
wrote:

> Hi Hongwei,
>
> thanks for the feedback. Point 2 I perhaps misunderstand.
> I think the system is running with working ats code - respecting
> big endian, 32 bit coding, and memory alignment stuff. Between
> my mail and your response I wrote about 1300 lines of ats code.
> Working and running code. But for what I'm doing this. I can only
> express it with the name Schönfinkel, pure phantasy - or reality?
>
>
> Am 26.07.20 um 21:30 schrieb gmhwxi:
>
>
> Hi Matthias,
>
> Today I took a glance at your ats-linux project. Here are a few thoughts
> that I would like to share.
>
> 1. Please do not use the current library of ATS2. Instead, you should build
> a library of your own specifically for this project. Of course, you could
> use ATS2
> library at the beginning and then gradually replace the ATS library code
> with your
> own.
>
> 2. Please try to avoid using dependent types at the beginning. I would not
> until
> after I have got a running system. Think of dependent types as a way for
> you to
> do (static) debugging later.
>
> 3. Try to use abstract types a lot! Here is some code I wrote to show off
> the idea:
>
>
> https://github.com/xanadu-lang/xinterp/blob/master/srcgen/TEST/xatslib_githwxi/test-2020-07-26.dats
>
> For instance, argv is just an array of strings. But you can make it
> abstract. If you really need to make use
> of the fact that argv is an array of strings, you could just do a cast.
> Yes, this is unsafe but can be fixed later
> without much effort at all.
>
> 4. Try to use templates a lot! Probably you could study the code in
> ATS-Temptory (but don't use ATS-Temptory
> for your project as it is a quick experiment done and over at this point).
>
> Good luck!
>
> --Hongwei
>
> PS: Don't feel that I have time to contribute to your project at this
> moment. But I will be happy to make suggestions
> on translating C code into ATS.
>
>
> On Wednesday, July 1, 2020 at 9:29:58 PM UTC-4, matthias wrote:
>>
>> Hi,
>>
>> After half a year of experiencing ats (as a c++ developer) I changed my
>> point of view in how  to go forward in using ats. Comparing ats with other
>> "modern" languages is not very satisfying. Always having a position in the
>> middle - for the logical prove oriented people we have linear logic
>> (finally get control over resources, while the garbage collector solved
>> before such problems), for the machine programming oriented people linear
>> logic is like c-programming (nothing new, while garbage collection or
>> intelligent resource management may also solve serious problems) - is
>> difficult. Personally I Iike to have both - I can compare - cool. To come
>> to a point. I learned very much from this list and from the very good
>> documentation of the ats language. I started to change the linux kernel as
>> a private self teaching project. Looking from the viewpoint of a
>> c-programmer in direction to ats or alternatively to c++ is for me of
>> interest, For that, a minimal linux system of about 630 objects consists
>> now on 595 ats-dats files, may help to understand more. Sure, I haven't
>> migrated 595 c-files to real ats code. The integration is a first step
>> using the %{...%} pattern. The real migration must be done, one after the
>> other, by hand. It's a kind of training. If someone else has a personal
>> interest on linux kernel coding take my approach from git.bejocama.org.
>> It's totally open. Finally Thanks.
>>
>> Regards Matthias
>>
>> --
> 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
>

Re: ptr1 and v0tp

2020-07-26 Thread Hongwei Xi

As I suggested in my previous email, please try to build a library of your
own for this project.
Try to avoid using ptr and use cptr instead. Note that ptr is like void*
and cptr(T) is like T* in C.
Also try to avoid using dependent type at the beginning. Dependent types
can be introduced later
for the purpose of static debugging.

Personally, I feel that ATS3 would be a lot better for such a project, but
ATS2 is adequate. Once ATS3
becomes ready, the project can be readily translated from ATS2 into ATS3.

Cheers!

--Hongwei


On Sat, Jul 25, 2020 at 8:41 PM Matthias Wolff 
wrote:

> Your speed is impressing. I take all I can get. It's really an adventure.
> In my early stage of my playground "ats linux kernel" it helps to make
> good design decisions.
>
> Am 25.07.20 um 23:34 schrieb Hongwei Xi:
>
>
> #include "share/atspre_define.hats"
> #include "share/atspre_staload.hats"
> #staload UN = "prelude/SATS/unsafe.sats"
>
> #define ATS_DYNLOADFLAG 0
>
> (*
> Recursion is at the center of programming.
> And recursively defined concepts are occurring everywhere.
> For instance, the C-string concept is recursively defined.
> Let 'string(n)' be a type for C-strings of the size 'n'.
>
> We can readily implement the following three functions
> for recursively traversing a C-string:
> *)
>
> extern
> fun{}
> string_nilq
> {n:int}(string(n)): bool(n==0)
> extern
> fun{}
> string_head{n:pos}(string(n)): char
> extern
> fun{}
> string_tail{n:pos}(string(n)): string(n-1)
>
> (*
> For saving time, these three functions
> are given the following UNSAFE implementation
> *)
> implement
> string_nilq<>(cs) =
> $UN.cast
> (
> iseqz
> ($UN.ptr0_get(string2ptr(cs)))
> )
> //
> implement
> string_head<>(cs) =
> ($UN.ptr0_get(string2ptr(cs)))
> //
> implement
> string_tail<>(cs) =
> $UN.cast(ptr_succ(string2ptr(cs)))
>
> (*
> Then the length for C-strings can be implemented
> as follows:
> *)
>
> fun
> strlen
> {n:nat}
> (cs: string(n)): int(n) =
> loop(cs, 0) where
> {
> fun
> loop
> {i,j:nat|i+j==n}..
> (cs: string(i), j:int(j)): int(n) =
> if
> string_nilq(cs)
> then j else loop(string_tail(cs), j+1)
> }
>
> implement main0 () =
> let
> var s = @[char][4]('A','B','C','\0')
> val x = strlen($UN.cast{String0}(addr@(s)))
> in
> println!(x)
> end
>
> ##
>
> When compiled to assembly (after inlining), the strlen function implemented
> above is essentially the same as the one you did that uses pointers
> explicitly.
>
> Obviously, you can replace C-strings with other forms of sequences.
>
>
> On Sat, Jul 25, 2020 at 5:01 PM Matthias Wolff 
> wrote:
>
>> Surprising answer, because I don't understand the details at the moment.
>> It comes earlier than I expected. But I will take the chance. Thanks.
>> Am 25.07.20 um 21:32 schrieb Hongwei Xi:
>>
>> Your code should work if you add the following lines
>> at the beginning:
>>
>> prfun
>> lemma_char_size()
>> : [sizeof(char) > 0] void
>> prval () = lemma_char_size()
>>
>> These lines tell the type-checker that sizeof(char) is positive.
>>
>> Right now, the type system only knows that 'sizeof(char)' is an int.
>>
>>
>>
>> On Sat, Jul 25, 2020 at 9:59 AM matthias.wo...@bejocama.de <
>> matthias.wo...@bejocama.de> wrote:
>>
>>> Hi,
>>>
>>> after migrating the string functions in the lib of the linux kernel to
>>> ats I'm now starting to
>>> to improve the code in an ats sense. A first step was to change from
>>> ptr0_get/set to
>>> ptr1 (sure, still unsafe stuff - but better type checked regarding
>>> implicit type conversions).
>>>
>>> The code at the end demonstrates a little problem. ptr1_succ(pp)
>>> doesn't have the
>>> property l:agz even pp has it. Second, looking on the template parameter
>>> of ptr1_succ
>>> I get vt0p which stands for viewt@ype. I cannot actually get this in
>>> sync with documentation,
>>> because a viewt@ype should be something like vtypedef VT(T:t@ype,l:addr)
>>> = ( T@l | ptr(l) ).
>>> So I think the template parameter should be of t0p = t@ype. Otherwise I
>>> have wrong expectations
>>> in how to use these functions - and I don't really understand why my
>>> code compiles.
>>>
>>> Finally an last minute insight regarding the usage of ptr1_pred: l:addr
>>> | l > (null + sizeof(a)) .. works -
>>> without the null not. I know, in this case I should not be surprised.
&

Re: conditional expressions and branches

Forgot to mention that you need parentheses:

(a <= 5) * (b <= 5)

On Sat, Jul 25, 2020 at 10:55 PM Hongwei Xi  wrote:

>
> Please use ifcase-expressions:
>
> fun
> foo
> {n:int}
> (n:int(n)): void =
> ifcase
> | n = 0 => () where {prval () = prop_verify{n == 0}()}
> | n = 1 => () where {prval () = prop_verify{n == 1}()}
> | _ (*else*) => () where {prval () = prop_verify{n != 0 && n != 1}()}
>
> ##
>
> Also, you can use '+' and '*' for || and &&, respectively. For instance,
>
> if a <= 5 * b <= 5 then ... else ...
>
> And '+' and '*' have the types expected by you.
>
>
>
>
> On Sat, Jul 25, 2020 at 10:35 PM Dambaev Alexander 
> wrote:
>
>> Hi,
>>
>> We know, that ATS is able to keep information about check in appropriate
>> branch of 'if' expression, like:
>>
>> ```
>> fn foo( i: int): int =
>>   if i < 1
>>   then (* here typechecker knows, that i < 1*)
>>   else (* here typechecker knows, that i >= 1*)
>> ```
>>
>> But sometimes, you need to use more conditions and case expressions is
>> more convenient in this case, but currently, typechecker is not always able
>> to keep such info in branches of 'case', like:
>>
>> ```
>> fn foo( a: int, b: int): int =
>>   case+ 0 of
>>   | _ when a > 10 => ...
>>   | _ when a > 5 => ...
>>   | _ when b > 10 => ...
>>   | _ when b > 5 => ...
>>   | _ => (* 1 *)
>> ```
>>
>> It will be great, if, at least in ATS3, at mark 1 typechecker will know,
>> that a <= 5 and b <= 5, because currently, as far as I got, condition like:
>> ```
>> if a <= 5 && b <= 5
>> then (* 1 *)
>> else (* 2 *)
>> ```
>> will tell typechecker, that there is a proof 'a <= 5 && b <= 5', but
>> there are no separate proofs 'a <= 5' and 'b<=5' so you have to make a
>> nested if-expressions to get them, which is not so compact as 'case'
>> expressions
>>
>> --
>> 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/CAHjn2KxS8iGdxHRjVU2MJu_%2B5g143Lq6HKFo%2BRta06aF3ENdgg%40mail.gmail.com
>> <https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KxS8iGdxHRjVU2MJu_%2B5g143Lq6HKFo%2BRta06aF3ENdgg%40mail.gmail.com?utm_medium=email_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/CAPPSPLpks-nnuS8yd_6QfasOQP2dN%2B7LyC%2BDAbXPA5HEdf%3DShg%40mail.gmail.com.

Re: conditional expressions and branches

Please use ifcase-expressions:

fun
foo
{n:int}
(n:int(n)): void =
ifcase
| n = 0 => () where {prval () = prop_verify{n == 0}()}
| n = 1 => () where {prval () = prop_verify{n == 1}()}
| _ (*else*) => () where {prval () = prop_verify{n != 0 && n != 1}()}

##

Also, you can use '+' and '*' for || and &&, respectively. For instance,

if a <= 5 * b <= 5 then ... else ...

And '+' and '*' have the types expected by you.




On Sat, Jul 25, 2020 at 10:35 PM Dambaev Alexander 
wrote:

> Hi,
>
> We know, that ATS is able to keep information about check in appropriate
> branch of 'if' expression, like:
>
> ```
> fn foo( i: int): int =
>   if i < 1
>   then (* here typechecker knows, that i < 1*)
>   else (* here typechecker knows, that i >= 1*)
> ```
>
> But sometimes, you need to use more conditions and case expressions is
> more convenient in this case, but currently, typechecker is not always able
> to keep such info in branches of 'case', like:
>
> ```
> fn foo( a: int, b: int): int =
>   case+ 0 of
>   | _ when a > 10 => ...
>   | _ when a > 5 => ...
>   | _ when b > 10 => ...
>   | _ when b > 5 => ...
>   | _ => (* 1 *)
> ```
>
> It will be great, if, at least in ATS3, at mark 1 typechecker will know,
> that a <= 5 and b <= 5, because currently, as far as I got, condition like:
> ```
> if a <= 5 && b <= 5
> then (* 1 *)
> else (* 2 *)
> ```
> will tell typechecker, that there is a proof 'a <= 5 && b <= 5', but there
> are no separate proofs 'a <= 5' and 'b<=5' so you have to make a nested
> if-expressions to get them, which is not so compact as 'case' expressions
>
> --
> 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/CAHjn2KxS8iGdxHRjVU2MJu_%2B5g143Lq6HKFo%2BRta06aF3ENdgg%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/CAPPSPLoAtWmL0kRe1Hpd5P%3DPMazOkzg5VeZr2pVAn%2B%3D%3DF2teEQ%40mail.gmail.com.

Re: ptr1 and v0tp

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
#staload UN = "prelude/SATS/unsafe.sats"

#define ATS_DYNLOADFLAG 0

(*
Recursion is at the center of programming.
And recursively defined concepts are occurring everywhere.
For instance, the C-string concept is recursively defined.
Let 'string(n)' be a type for C-strings of the size 'n'.

We can readily implement the following three functions
for recursively traversing a C-string:
*)

extern
fun{}
string_nilq
{n:int}(string(n)): bool(n==0)
extern
fun{}
string_head{n:pos}(string(n)): char
extern
fun{}
string_tail{n:pos}(string(n)): string(n-1)

(*
For saving time, these three functions
are given the following UNSAFE implementation
*)
implement
string_nilq<>(cs) =
$UN.cast
(
iseqz
($UN.ptr0_get(string2ptr(cs)))
)
//
implement
string_head<>(cs) =
($UN.ptr0_get(string2ptr(cs)))
//
implement
string_tail<>(cs) =
$UN.cast(ptr_succ(string2ptr(cs)))

(*
Then the length for C-strings can be implemented
as follows:
*)

fun
strlen
{n:nat}
(cs: string(n)): int(n) =
loop(cs, 0) where
{
fun
loop
{i,j:nat|i+j==n}..
(cs: string(i), j:int(j)): int(n) =
if
string_nilq(cs)
then j else loop(string_tail(cs), j+1)
}

implement main0 () =
let
var s = @[char][4]('A','B','C','\0')
val x = strlen($UN.cast{String0}(addr@(s)))
in
println!(x)
end

##

When compiled to assembly (after inlining), the strlen function implemented
above is essentially the same as the one you did that uses pointers
explicitly.

Obviously, you can replace C-strings with other forms of sequences.


On Sat, Jul 25, 2020 at 5:01 PM Matthias Wolff 
wrote:

> Surprising answer, because I don't understand the details at the moment.
> It comes earlier than I expected. But I will take the chance. Thanks.
> Am 25.07.20 um 21:32 schrieb Hongwei Xi:
>
> Your code should work if you add the following lines
> at the beginning:
>
> prfun
> lemma_char_size()
> : [sizeof(char) > 0] void
> prval () = lemma_char_size()
>
> These lines tell the type-checker that sizeof(char) is positive.
>
> Right now, the type system only knows that 'sizeof(char)' is an int.
>
>
>
> On Sat, Jul 25, 2020 at 9:59 AM matthias.wo...@bejocama.de <
> matthias.wo...@bejocama.de> wrote:
>
>> Hi,
>>
>> after migrating the string functions in the lib of the linux kernel to
>> ats I'm now starting to
>> to improve the code in an ats sense. A first step was to change from
>> ptr0_get/set to
>> ptr1 (sure, still unsafe stuff - but better type checked regarding
>> implicit type conversions).
>>
>> The code at the end demonstrates a little problem. ptr1_succ(pp)
>> doesn't have the
>> property l:agz even pp has it. Second, looking on the template parameter
>> of ptr1_succ
>> I get vt0p which stands for viewt@ype. I cannot actually get this in
>> sync with documentation,
>> because a viewt@ype should be something like vtypedef VT(T:t@ype,l:addr)
>> = ( T@l | ptr(l) ).
>> So I think the template parameter should be of t0p = t@ype. Otherwise I
>> have wrong expectations
>> in how to use these functions - and I don't really understand why my code
>> compiles.
>>
>> Finally an last minute insight regarding the usage of ptr1_pred: l:addr |
>> l > (null + sizeof(a)) .. works -
>> without the null not. I know, in this case I should not be surprised. But
>> l,r:agz | r == (l + sizeof(a)) --
>> doesn't imply r >= l.
>>
>> Here is the code - c-style strlen - very often called by the kernel and
>> the performance seems
>> to be good. The ptr0 version works (and also my pointer type modification
>> pgz):
>>
>> #define ATS_DYNLOADFLAG 0
>> #include "share/atspre_define.hats"
>> #include "share/atspre_staload.hats"
>> staload "prelude/SATS/unsafe.sats"
>>
>> fn strlen{l:agz}(p:ptr(l)) : [r:nat] size_t(r) =
>> let
>>   fun loop{ll:agz| ll >= l}(pp:ptr(ll)) : [r:agz| r >= ll] ptr(r) =
>>   case+ ptr1_get(pp) = '\0' of
>> | true => pp
>> | false => loop(ptr1_succ(pp))
>> in
>>   g1ofg0(cast{size_t}(loop(p) - p))
>> end
>>
>> implement main0 () =
>> let
>> var s = @[char][4]('A','B','C','\0')
>> val x = strlen(addr@(s))
>> in
>> println!(x)
>> end
>>
>> --
>> 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-u

Re: ptr1 and v0tp

Your code should work if you add the following lines
at the beginning:

prfun
lemma_char_size()
: [sizeof(char) > 0] void
prval () = lemma_char_size()

These lines tell the type-checker that sizeof(char) is positive.

Right now, the type system only knows that 'sizeof(char)' is an int.



On Sat, Jul 25, 2020 at 9:59 AM matthias.wo...@bejocama.de <
matthias.wo...@bejocama.de> wrote:

> Hi,
>
> after migrating the string functions in the lib of the linux kernel to ats
> I'm now starting to
> to improve the code in an ats sense. A first step was to change from
> ptr0_get/set to
> ptr1 (sure, still unsafe stuff - but better type checked regarding
> implicit type conversions).
>
> The code at the end demonstrates a little problem. ptr1_succ(pp)
> doesn't have the
> property l:agz even pp has it. Second, looking on the template parameter
> of ptr1_succ
> I get vt0p which stands for viewt@ype. I cannot actually get this in sync
> with documentation,
> because a viewt@ype should be something like vtypedef VT(T:t@ype,l:addr)
> = ( T@l | ptr(l) ).
> So I think the template parameter should be of t0p = t@ype. Otherwise I
> have wrong expectations
> in how to use these functions - and I don't really understand why my code
> compiles.
>
> Finally an last minute insight regarding the usage of ptr1_pred: l:addr |
> l > (null + sizeof(a)) .. works -
> without the null not. I know, in this case I should not be surprised. But
> l,r:agz | r == (l + sizeof(a)) --
> doesn't imply r >= l.
>
> Here is the code - c-style strlen - very often called by the kernel and
> the performance seems
> to be good. The ptr0 version works (and also my pointer type modification
> pgz):
>
> #define ATS_DYNLOADFLAG 0
> #include "share/atspre_define.hats"
> #include "share/atspre_staload.hats"
> staload "prelude/SATS/unsafe.sats"
>
> fn strlen{l:agz}(p:ptr(l)) : [r:nat] size_t(r) =
> let
>   fun loop{ll:agz| ll >= l}(pp:ptr(ll)) : [r:agz| r >= ll] ptr(r) =
>   case+ ptr1_get(pp) = '\0' of
> | true => pp
> | false => loop(ptr1_succ(pp))
> in
>   g1ofg0(cast{size_t}(loop(p) - p))
> end
>
> implement main0 () =
> let
> var s = @[char][4]('A','B','C','\0')
> val x = strlen(addr@(s))
> in
> println!(x)
> end
>
> --
> 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/9e71a4f6-6be7-44ed-8e61-c7b44d260b34o%40googlegroups.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/CAPPSPLoo4t-5ZisDftmGV1rUuHLqnuLWiw_he%3DLQYY2PUww9ZA%40mail.gmail.com.

Re: constraint solving