How to use gflist?

Google Group
1

This one looks like a bug. Let me see if it can be easily fixed.On Tue, Jun 16, 2015 at 3:16 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

Hi all,

Now I’m writing some code using gflist.

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

staload "libats/SATS/ilist_prf.sats"
staload "libats/SATS/gflist.sats"
staload _ = "libats/DATS/gflist.dats"

implement main0 () = {
  val (pf1 | xs1) = list2gflist ($list{int}(1, 2, 3))
  val (pf2 | xs2) = list2gflist ($list{int}(4, 3, 2, 1))
  val (pf_append | xs3) = gflist_append (xs1, xs2)
}

However, the code has error on GCC side.

$ patscc test_gflist.dats -DATS_MEMALLOC_LIBC
In file included from test_gflist_dats.c:15:0:
test_gflist_dats.c: In function ‘loop_2__2__1’:
/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:260:35:
error: assignment to expression with array type
#define ATSINSmove(tmp, val) (tmp = val)
^
test_gflist_dats.c:910:1: note: in expansion of macro ‘ATSINSmove’
ATSINSmove(tmp10__1, ATSSELcon(arg0, postiats_tysum_0, atslab__0)) ;
^
/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:287:74:
warning: assignment makes integer from pointer without a cast
#define ATSINSstore_con1_ofs(tmp, tysum, lab, val) (((tysum*)(tmp))->lab
= val)
^
test_gflist_dats.c:939:1: note: in expansion of macro
‘ATSINSstore_con1_ofs’
ATSINSstore_con1_ofs(tmp12__1, postiats_tysum_3, atslab__0, tmp10__1) ;
^

How to use gflist?

Thank’s,

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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dmYKd5yV%2B2%2BFG%3DJXJ%2B31YFJj83863FCsoJrW0-CioXneg%40mail.gmail.com
.

2

I fixed the issue with gflist. Here is a small file for testing gflist:

Code involving gflist has not really been run until now. So far the primary
use of gflist is for education
in program verification.On Tue, Jun 16, 2015 at 4:01 AM, Hongwei Xi gmh...@gmail.com wrote:

This one looks like a bug. Let me see if it can be easily fixed.

On Tue, Jun 16, 2015 at 3:16 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

Hi all,

Now I’m writing some code using gflist.

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

staload "libats/SATS/ilist_prf.sats"
staload "libats/SATS/gflist.sats"
staload _ = "libats/DATS/gflist.dats"

implement main0 () = {
  val (pf1 | xs1) = list2gflist ($list{int}(1, 2, 3))
  val (pf2 | xs2) = list2gflist ($list{int}(4, 3, 2, 1))
  val (pf_append | xs3) = gflist_append (xs1, xs2)
}

However, the code has error on GCC side.

$ patscc test_gflist.dats -DATS_MEMALLOC_LIBC
In file included from test_gflist_dats.c:15:0:
test_gflist_dats.c: In function ‘loop_2__2__1’:
/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:260:35:
error: assignment to expression with array type
#define ATSINSmove(tmp, val) (tmp = val)
^
test_gflist_dats.c:910:1: note: in expansion of macro ‘ATSINSmove’
ATSINSmove(tmp10__1, ATSSELcon(arg0, postiats_tysum_0, atslab__0)) ;
^
/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:287:74:
warning: assignment makes integer from pointer without a cast
#define ATSINSstore_con1_ofs(tmp, tysum, lab, val) (((tysum*)(tmp))->lab
= val)

^
test_gflist_dats.c:939:1: note: in expansion of macro
‘ATSINSstore_con1_ofs’
ATSINSstore_con1_ofs(tmp12__1, postiats_tysum_3, atslab__0, tmp10__1) ;
^

How to use gflist?

Thank’s,

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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dmYKd5yV%2B2%2BFG%3DJXJ%2B31YFJj83863FCsoJrW0-CioXneg%40mail.gmail.com
.

3

Search INV in this forum, and you can find some explanation. For instance:

Redirecting to Google Groups Thursday, June 18, 2015 at 10:49:34 PM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Fri, Jun 19, 2015 at 9:01 AM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

extern
fun{a:t@ype}
gflist_append_length
{xs1,xs2:ilist}{n1,n2:int}
( pf1: LENGTH (xs1, n1), pf2: LENGTH (xs2, n2)
| xs1: gflist (INV(a), xs1), xs2: gflist (a, xs2)
): [res:ilist] (LENGTH (res, n1+n2), APPEND (xs1, xs2, res) | gflist (a,
res))

You use INV(a) to tell the typechecker how a type constraint should be
generated with respect xs1.

For my eye, INV(a) has no meaning.

abst@ype // S2Einvar
invar_t0ype_t0ype (a:t@ype) = a
vtypedef
INV (a: t@ype) = invar_t0ype_t0ype (a)

How does it work?

Regards,

Kiwamu Okabe at METASEPI DESIGN

4

Where could I find your code?On Wednesday, June 17, 2015 at 1:08:03 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Wed, Jun 17, 2015 at 2:09 AM, Hongwei Xi <gmh...@gmail.com <javascript:>> wrote:

I fixed the issue with gflist. Here is a small file for testing gflist:

My code is also available to be compiled.

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

5

extern fun{a:t@ype} gflist_append_length {xs1,xs2:ilist}{n1,n2:int} (pf1:
LENGTH (xs1, n1), pf2: LENGTH (xs2, n2) | xs1: gflist (a, xs1), xs2: gflist
(a, xs2)): [res:ilist] (LENGTH (res, n1+n2), APPEND (xs1, xs2, res) |
gflist (a, res))

changes to

extern
fun{a:t@ype}
gflist_append_length
{xs1,xs2:ilist}{n1,n2:int}
( pf1: LENGTH (xs1, n1), pf2: LENGTH (xs2, n2)
| xs1: gflist (INV(a), xs1), xs2: gflist (a, xs2)
): [res:ilist] (LENGTH (res, n1+n2), APPEND (xs1, xs2, res) | gflist (a, res
))

You use INV(a) to tell the typechecker how a type constraint should be
generated with respect xs1.On Thursday, June 18, 2015 at 6:04:18 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

https://github.com/jats-ug/practice-ats/blob/master/test_gflist/main.dats

I found an error, while change the main0 function as following:

$ git diff . | cat
diff --git a/test_gflist/main.dats b/test_gflist/main.dats
index dd058b3…a6e1ca3 100644
— a/test_gflist/main.dats
+++ b/test_gflist/main.dats
@@ -26,5 +26,5 @@ implement main0 () = {
val (pf2 | xs2) = list2gflist l2
val (pf_len, pf_append | xs3) = gflist_append_length (pf1, pf2 | xs1,
xs2)
val (pf3 | l3) = gflist2list xs3

  • val () = print_list l3
  • val () = print_list l3
    }
    $ patscc main.dats -DATS_MEMALLOC_LIBC
    In file included from main_dats.c:15:0:
    main_dats.c: In function ‘ATSLIB_056_prelude__fprint_val__27__1’:
    main_dats.c:2531:22: error: ‘PMVtmpltcstmat’ undeclared (first use in
    this function)
    ATSINSmove(tmp65__1, PMVtmpltcstmat0(arg1))
    ;
    ^

In future, it should be fixed?

Thank’s,

Kiwamu Okabe