Helping to flesh out ATSLIB in ATS2

There are a lot of nice library functions and succinct algorithms in ATS1’s
ATSLIB, while at the same time, many of these seem to be implemented in
ATS2 using templates where possible.
It can be helpful to check one’s understanding of the ATS1 code by
inspection and modification before attempting to port to ATS2.

One alternative is to use version control, but others may prefer to copy
and paste code into a single file with included tests. This may involve
copy from several files though.
I’ve put an example https://gist.github.com/bbarker/d068e38107e4b801b7c5of this up as a git gist for linset_union (copied to my_linset_union); feel
free to improve it or suggest changes.

Currently, there is a problem with the termination metric though (I don’t
know why yet).

The ‘ref’ in cloref does not mean ref-effect.

I suggest that you do not track effects as doing so is not very meaningful
in this case.
Use cloref1 instead of cloref.On Tuesday, January 14, 2014 8:25:41 PM UTC-5, Brandon Barker wrote:

There are a lot of nice library functions and succinct algorithms in
ATS1’s ATSLIB, while at the same time, many of these seem to be implemented
in ATS2 using templates where possible.
It can be helpful to check one’s understanding of the ATS1 code by
inspection and modification before attempting to port to ATS2.

One alternative is to use version control, but others may prefer to copy
and paste code into a single file with included tests. This may involve
copy from several files though.
I’ve put an example https://gist.github.com/bbarker/d068e38107e4b801b7c5of this up as a git gist for linset_union (copied to my_linset_union); feel
free to improve it or suggest changes.

Currently, there is a problem with the termination metric though (I don’t
know why yet).

That is good to know about (anything with a $ seems to be really handy).

I was trying to avoid using cloref1 or <1> cause I get:
error(3): the effects [exn, ntm] are disallowed

and it seemed easier to worry about 1 eff rather than 3.

Unfortunately, even with effmask_all, the termination metric problem still
occurs if the print_lvt statement is uncommented.https://gist.github.com/bbarker/d068e38107e4b801b7c5/33847f180cdf8ab36c27d9b05d2ef6bca1191aabOn Wednesday, January 15, 2014 10:38:32 AM UTC-5, gmhwxi wrote:

you can use $effmask_all(print(…)) to mask effects.

On Tuesday, January 14, 2014 8:25:41 PM UTC-5, Brandon Barker wrote:

There are a lot of nice library functions and succinct algorithms in
ATS1’s ATSLIB, while at the same time, many of these seem to be implemented
in ATS2 using templates where possible.
It can be helpful to check one’s understanding of the ATS1 code by
inspection and modification before attempting to port to ATS2.

One alternative is to use version control, but others may prefer to copy
and paste code into a single file with included tests. This may involve
copy from several files though.
I’ve put an examplehttps://gist.github.com/bbarker/d068e38107e4b801b7c5of this up as a git gist for linset_union (copied to my_linset_union); feel
free to improve it or suggest changes.

Currently, there is a problem with the termination metric though (I don’t
know why yet).

Try:

fn{a:t0p}
print_lvt{n:nat}(xsl: !list_vt (a,n)):<!ref> void = …On Wednesday, January 15, 2014 12:20:43 PM UTC-5, gmhwxi wrote:

This is because the type you assigned to print_lvt is not strong enough.
What happens if print_lvt actually increase the length of its argument?
You have
to say that the type-checker is doing its work very diligently :slight_smile:

My suggestion: please skip termination-checking.

On Wednesday, January 15, 2014 12:03:22 PM UTC-5, Brandon Barker wrote:

That is good to know about (anything with a $ seems to be really handy).

I was trying to avoid using cloref1 or <1> cause I get:
error(3): the effects [exn, ntm] are disallowed

and it seemed easier to worry about 1 eff rather than 3.

Unfortunately, even with effmask_all, the termination metric problem
still occurs if the print_lvt statement is uncommented.https://gist.github.com/bbarker/d068e38107e4b801b7c5/33847f180cdf8ab36c27d9b05d2ef6bca1191aab

On Wednesday, January 15, 2014 10:38:32 AM UTC-5, gmhwxi wrote:

you can use $effmask_all(print(…)) to mask effects.

On Tuesday, January 14, 2014 8:25:41 PM UTC-5, Brandon Barker wrote:

There are a lot of nice library functions and succinct algorithms in
ATS1’s ATSLIB, while at the same time, many of these seem to be implemented
in ATS2 using templates where possible.
It can be helpful to check one’s understanding of the ATS1 code by
inspection and modification before attempting to port to ATS2.

One alternative is to use version control, but others may prefer to
copy and paste code into a single file with included tests. This may
involve copy from several files though.
I’ve put an examplehttps://gist.github.com/bbarker/d068e38107e4b801b7c5of this up as a git gist for linset_union (copied to my_linset_union); feel
free to improve it or suggest changes.

Currently, there is a problem with the termination metric though (I
don’t know why yet).

This is because the type you assigned to print_lvt is not strong enough.
What happens if print_lvt actually increase the length of its argument? You
have
to say that the type-checker is doing its work very diligently :slight_smile:

My suggestion: please skip termination-checking.On Wednesday, January 15, 2014 12:03:22 PM UTC-5, Brandon Barker wrote:

That is good to know about (anything with a $ seems to be really handy).

I was trying to avoid using cloref1 or <1> cause I get:
error(3): the effects [exn, ntm] are disallowed

and it seemed easier to worry about 1 eff rather than 3.

Unfortunately, even with effmask_all, the termination metric problem still
occurs if the print_lvt statement is uncommented.https://gist.github.com/bbarker/d068e38107e4b801b7c5/33847f180cdf8ab36c27d9b05d2ef6bca1191aab

On Wednesday, January 15, 2014 10:38:32 AM UTC-5, gmhwxi wrote:

you can use $effmask_all(print(…)) to mask effects.

On Tuesday, January 14, 2014 8:25:41 PM UTC-5, Brandon Barker wrote:

There are a lot of nice library functions and succinct algorithms in
ATS1’s ATSLIB, while at the same time, many of these seem to be implemented
in ATS2 using templates where possible.
It can be helpful to check one’s understanding of the ATS1 code by
inspection and modification before attempting to port to ATS2.

One alternative is to use version control, but others may prefer to copy
and paste code into a single file with included tests. This may involve
copy from several files though.
I’ve put an examplehttps://gist.github.com/bbarker/d068e38107e4b801b7c5of this up as a git gist for linset_union (copied to my_linset_union); feel
free to improve it or suggest changes.

Currently, there is a problem with the termination metric though (I
don’t know why yet).

That does it. That makes sense, just like switching between string and
string(n) can give trouble.On Wednesday, January 15, 2014 12:22:29 PM UTC-5, gmhwxi wrote:

Try:

fn{a:t0p}
print_lvt{n:nat}(xsl: !list_vt (a,n)):<!ref> void = …

On Wednesday, January 15, 2014 12:20:43 PM UTC-5, gmhwxi wrote:

This is because the type you assigned to print_lvt is not strong enough.
What happens if print_lvt actually increase the length of its argument?
You have
to say that the type-checker is doing its work very diligently :slight_smile:

My suggestion: please skip termination-checking.

On Wednesday, January 15, 2014 12:03:22 PM UTC-5, Brandon Barker wrote:

That is good to know about (anything with a $ seems to be really handy).

I was trying to avoid using cloref1 or <1> cause I get:
error(3): the effects [exn, ntm] are disallowed

and it seemed easier to worry about 1 eff rather than 3.

Unfortunately, even with effmask_all, the termination metric problem
still occurs if the print_lvt statement is uncommented.https://gist.github.com/bbarker/d068e38107e4b801b7c5/33847f180cdf8ab36c27d9b05d2ef6bca1191aab

On Wednesday, January 15, 2014 10:38:32 AM UTC-5, gmhwxi wrote:

you can use $effmask_all(print(…)) to mask effects.

On Tuesday, January 14, 2014 8:25:41 PM UTC-5, Brandon Barker wrote:

There are a lot of nice library functions and succinct algorithms in
ATS1’s ATSLIB, while at the same time, many of these seem to be implemented
in ATS2 using templates where possible.
It can be helpful to check one’s understanding of the ATS1 code by
inspection and modification before attempting to port to ATS2.

One alternative is to use version control, but others may prefer to
copy and paste code into a single file with included tests. This may
involve copy from several files though.
I’ve put an examplehttps://gist.github.com/bbarker/d068e38107e4b801b7c5of this up as a git gist for linset_union (copied to my_linset_union); feel
free to improve it or suggest changes.

Currently, there is a problem with the termination metric though (I
don’t know why yet).

changing clo to “cloref” fixes this, but when the print_lvt statement is
uncommented, we are back to the termination metric issue:
/home/brand_000/linset_union/d068e38107e4b801b7c5/linset_ats1libtest.dats:
2218(line=89, offs=20) – 2222(line=89, offs=24): error(3): unsolved
constraint for termination metric being decreasing: C3STRprop(metric_dec;
S2Emetlt(S2Eapp(S2Ecst(+); S2EVar(2573), S2EVar(2574)), S2Eapp(S2Ecst(+);
S2Evar(n1(5415)), S2Evar(n2(5416)))))On Wednesday, January 15, 2014 10:28:27 AM UTC-5, Brandon Barker wrote:

In the current version where I try to combine clo and !refhttps://gist.github.com/bbarker/d068e38107e4b801b7c5/c3fd0f9d2a34557a2335e5e62d18a2332a88c027,
I get a gcc error, which indicates I’m probably not doing things in the
usual or correct way:

$ atscc linset_ats1libtest.dats
/home/brand_000/ats-lang-anairiats-0.2.11/bin/atsopt --output
linset_ats1libtest_dats.c --dynamic linset_ats1libtest.dats
gcc -I/home/brand_000/ats-lang-anairiats-0.2.11/
-I/home/brand_000/ats-lang-anairiats-0.2.11/ccomp/runtime/
-L/home/brand_000/ats-lang-anairiats-0.2.11/ccomp/lib/
/home/brand_000/ats-lang-anairiats-0.2.11/ccomp/runtime/ats_prelude.c
linset_ats1libtest_dats.c -lats
linset_ats1libtest_dats.c: In function ‘loop_8’:
linset_ats1libtest_dats.c:541:15: error: cannot convert to a pointer type
/* tmp36 = / ((ats_void_type()(ats_clo_ptr_type, ats_ptr_type,
ats_ptr_type, ats_ref_type))(ats_closure_fun(env1))) (env1, tmp35, arg1,
tmp30) ;
^
linset_ats1libtest_dats.c:541:15: error: incompatible type for argument 1
of ‘(ats_void_type (*)(struct ats_clo_type *, void *, void , void
))0u->closure_fun’
linset_ats1libtest_dats.c:541:15: note: expected ‘ats_clo_ptr_type’ but
argument is of type ‘ats_clo_type’
linset_ats1libtest_dats.c:547:15: error: cannot convert to a pointer type
/
tmp39 = / ((ats_void_type()(ats_clo_ptr_type, ats_ptr_type,
ats_ptr_type, ats_ref_type))(ats_closure_fun(env1))) (env1, arg0, tmp38,
tmp32) ;
^
linset_ats1libtest_dats.c:547:15: error: incompatible type for argument 1
of ‘(ats_void_type (
)(struct ats_clo_type *, void *, void , void
))0u->closure_fun’
linset_ats1libtest_dats.c:547:15: note: expected ‘ats_clo_ptr_type’ but
argument is of type ‘ats_clo_type’
linset_ats1libtest_dats.c:553:15: error: cannot convert to a pointer type
/
tmp42 = / ((ats_void_type()(ats_clo_ptr_type, ats_ptr_type,
ats_ptr_type, ats_ref_type))(ats_closure_fun(env1))) (env1, tmp40, tmp41,
tmp30) ;
^
linset_ats1libtest_dats.c:553:15: error: incompatible type for argument 1
of ‘(ats_void_type (
)(struct ats_clo_type *, void *, void *, void
))0u->closure_fun’
linset_ats1libtest_dats.c:553:15: note: expected ‘ats_clo_ptr_type’ but
argument is of type ‘ats_clo_type’
linset_ats1libtest_dats.c: In function
‘my_linset_union_02003_ats_int_type’:
linset_ats1libtest_dats.c:611:15: warning: passing argument 1 of
‘(ats_void_type (
)(struct ats_clo_type *, void *, void *, void *))((struct
ats_clo_type )ptrof_error(loop_8_closure_error()))->closure_fun’ makes
pointer from integer without a cast [enabled by default]
/
tmp44 = / ((ats_void_type()(ats_clo_ptr_type, ats_ptr_type,
ats_ptr_type,
ats_ref_type))(ats_closure_fun(ptrof_error(loop_8_closure_error ()))))
(ptrof_error(loop_8_closure_error ()), arg0, arg1, (&tmp43)) ;
^
linset_ats1libtest_dats.c:611:15: note: expected ‘ats_clo_ptr_type’ but
argument is of type ‘int’
Exit: [gcc] failed.

On Tuesday, January 14, 2014 8:25:41 PM UTC-5, Brandon Barker wrote:

There are a lot of nice library functions and succinct algorithms in
ATS1’s ATSLIB, while at the same time, many of these seem to be implemented
in ATS2 using templates where possible.
It can be helpful to check one’s understanding of the ATS1 code by
inspection and modification before attempting to port to ATS2.

One alternative is to use version control, but others may prefer to copy
and paste code into a single file with included tests. This may involve
copy from several files though.
I’ve put an examplehttps://gist.github.com/bbarker/d068e38107e4b801b7c5of this up as a git gist for linset_union (copied to my_linset_union); feel
free to improve it or suggest changes.

Currently, there is a problem with the termination metric though (I don’t
know why yet).

you can use $effmask_all(print(…)) to mask effects.On Tuesday, January 14, 2014 8:25:41 PM UTC-5, Brandon Barker wrote:

There are a lot of nice library functions and succinct algorithms in
ATS1’s ATSLIB, while at the same time, many of these seem to be implemented
in ATS2 using templates where possible.
It can be helpful to check one’s understanding of the ATS1 code by
inspection and modification before attempting to port to ATS2.

One alternative is to use version control, but others may prefer to copy
and paste code into a single file with included tests. This may involve
copy from several files though.
I’ve put an example https://gist.github.com/bbarker/d068e38107e4b801b7c5of this up as a git gist for linset_union (copied to my_linset_union); feel
free to improve it or suggest changes.

Currently, there is a problem with the termination metric though (I don’t
know why yet).

In the current version where I try to combine clo and !refhttps://gist.github.com/bbarker/d068e38107e4b801b7c5/c3fd0f9d2a34557a2335e5e62d18a2332a88c027,
I get a gcc error, which indicates I’m probably not doing things in the
usual or correct way:

$ atscc linset_ats1libtest.dats
/home/brand_000/ats-lang-anairiats-0.2.11/bin/atsopt --output
linset_ats1libtest_dats.c --dynamic linset_ats1libtest.dats
gcc -I/home/brand_000/ats-lang-anairiats-0.2.11/
-I/home/brand_000/ats-lang-anairiats-0.2.11/ccomp/runtime/
-L/home/brand_000/ats-lang-anairiats-0.2.11/ccomp/lib/
/home/brand_000/ats-lang-anairiats-0.2.11/ccomp/runtime/ats_prelude.c
linset_ats1libtest_dats.c -lats
linset_ats1libtest_dats.c: In function ‘loop_8’:
linset_ats1libtest_dats.c:541:15: error: cannot convert to a pointer type
/* tmp36 = / ((ats_void_type()(ats_clo_ptr_type, ats_ptr_type,
ats_ptr_type, ats_ref_type))(ats_closure_fun(env1))) (env1, tmp35, arg1,
tmp30) ;
^
linset_ats1libtest_dats.c:541:15: error: incompatible type for argument 1
of ‘(ats_void_type (*)(struct ats_clo_type *, void *, void , void
))0u->closure_fun’
linset_ats1libtest_dats.c:541:15: note: expected ‘ats_clo_ptr_type’ but
argument is of type ‘ats_clo_type’
linset_ats1libtest_dats.c:547:15: error: cannot convert to a pointer type
/
tmp39 = / ((ats_void_type()(ats_clo_ptr_type, ats_ptr_type,
ats_ptr_type, ats_ref_type))(ats_closure_fun(env1))) (env1, arg0, tmp38,
tmp32) ;
^
linset_ats1libtest_dats.c:547:15: error: incompatible type for argument 1
of ‘(ats_void_type (
)(struct ats_clo_type *, void *, void , void
))0u->closure_fun’
linset_ats1libtest_dats.c:547:15: note: expected ‘ats_clo_ptr_type’ but
argument is of type ‘ats_clo_type’
linset_ats1libtest_dats.c:553:15: error: cannot convert to a pointer type
/
tmp42 = / ((ats_void_type()(ats_clo_ptr_type, ats_ptr_type,
ats_ptr_type, ats_ref_type))(ats_closure_fun(env1))) (env1, tmp40, tmp41,
tmp30) ;
^
linset_ats1libtest_dats.c:553:15: error: incompatible type for argument 1
of ‘(ats_void_type (
)(struct ats_clo_type *, void *, void *, void
))0u->closure_fun’
linset_ats1libtest_dats.c:553:15: note: expected ‘ats_clo_ptr_type’ but
argument is of type ‘ats_clo_type’
linset_ats1libtest_dats.c: In function ‘my_linset_union_02003_ats_int_type’:
linset_ats1libtest_dats.c:611:15: warning: passing argument 1 of
‘(ats_void_type (
)(struct ats_clo_type *, void *, void *, void *))((struct
ats_clo_type )ptrof_error(loop_8_closure_error()))->closure_fun’ makes
pointer from integer without a cast [enabled by default]
/
tmp44 = / ((ats_void_type()(ats_clo_ptr_type, ats_ptr_type,
ats_ptr_type,
ats_ref_type))(ats_closure_fun(ptrof_error(loop_8_closure_error ()))))
(ptrof_error(loop_8_closure_error ()), arg0, arg1, (&tmp43)) ;
^
linset_ats1libtest_dats.c:611:15: note: expected ‘ats_clo_ptr_type’ but
argument is of type ‘int’
Exit: [gcc] failed.On Tuesday, January 14, 2014 8:25:41 PM UTC-5, Brandon Barker wrote:

There are a lot of nice library functions and succinct algorithms in
ATS1’s ATSLIB, while at the same time, many of these seem to be implemented
in ATS2 using templates where possible.
It can be helpful to check one’s understanding of the ATS1 code by
inspection and modification before attempting to port to ATS2.

One alternative is to use version control, but others may prefer to copy
and paste code into a single file with included tests. This may involve
copy from several files though.
I’ve put an example https://gist.github.com/bbarker/d068e38107e4b801b7c5of this up as a git gist for linset_union (copied to my_linset_union); feel
free to improve it or suggest changes.

Currently, there is a problem with the termination metric though (I don’t
know why yet).