How to use gflist?

[Kiwamu Okabe]

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

[Hongwei Xi]

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

--
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.

[Hongwei Xi]

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

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLIB/libats_gflist.dats

Code involving gflist has not really been run until now. So far the primary use of gflist is for education

in program verification.

[Kiwamu Okabe]

Hi Hongwei,

On Wed, Jun 17, 2015 at 2:09 AM, Hongwei Xi <gmh...@gmail.com> wrote:
> I fixed the issue with gflist. Here is a small file for testing gflist:

My code is also available to be compiled.

[gmhwxi]

Where could I find your code?

[Kiwamu Okabe]

Hi Hongwei,

On Thu, Jun 18, 2015 at 2:02 AM, gmhwxi <gmh...@gmail.com> wrote:
> Where could I find your code?

It's found at here.

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

[Kiwamu Okabe]

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<int> 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, PMVtmpltcstmat[0](tostrptr_val<S2EVar(4429)>)(arg1)) ;
^

In future, it should be fixed?

[Kiwamu Okabe]

Hi all,

On Thu, Jun 18, 2015 at 7:00 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> On Thu, Jun 18, 2015 at 2:02 AM, gmhwxi <gmh...@gmail.com> wrote:
>> Where could I find your code?
>
> It's found at here.
>
> https://github.com/jats-ug/practice-ats/blob/master/test_gflist/main.dats

One using gflist_vt is found at following:

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

Thank's,

[gmhwxi]

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.

[Kiwamu Okabe]

Hi Hongwei,

On Fri, Jun 19, 2015 at 9:01 AM, gmhwxi <gmh...@gmail.com> 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,

[gmhwxi]

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

https://groups.google.com/forum/#!searchin/ats-lang-users/INV/ats-lang-users/ptwztS9IHWg/NcyCP1vjTB8J