Is there a linear file type is the ATS2 default library?

Google Group
1

Hi people,

I’m looking (back since some time) at “Chapter 13. Introduction to Views
and Viewtypes” and a question I already had in mind came back: is there a
linear file type in the default ATS2 library? I mean a file type you must
close after you’ve opened it.

2

Yes. It is FILEptr(l:addr, m:file_mode). See:

https://github.com/githwxi/ATS-Postiats/blob/master/libc/SATS/stdio.sats

If I may, I need a bit of a hint or help for a simple start.

If I do this:

 staload "libc/SATS/stdio.sats"
 val out = fopen_exn(FILE_NAME, file_mode_w)
 val x = fflush1(out)
 val () = fclose1_exn(out)

I get an error as fflush1 expects a proof argument. I feel to understand
it’s expected to be a proof out is in write‑mode. But neither fopen_exn
nor fopen returns this proof. How to get a proof out was opened with
file_mode_w?

3

Yes. It is FILEptr(l:addr, m:file_mode). See:

https://github.com/githwxi/ATS-Postiats/blob/master/libc/SATS/stdio.satsOn Tue, Feb 10, 2015 at 6:44 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Hi people,

I’m looking (back since some time) at “Chapter 13. Introduction to Views
and Viewtypes” and a question I already had in mind came back: is there a
linear file type in the default ATS2 library? I mean a file type you must
close after you’ve opened it.

–
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/507323ba-ddc5-43a0-8454-8d23a2fb7cce%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/507323ba-ddc5-43a0-8454-8d23a2fb7cce%40googlegroups.com?utm_medium=email&utm_source=footer
.

4

See:

The proof you need is file_mode_lte_w_w:

val x = fflush(file_mode_lte_w_w | out)On Wed, Feb 11, 2015 at 9:51 AM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le mercredi 11 février 2015 01:27:50 UTC+1, gmhwxi a écrit :

Yes. It is FILEptr(l:addr, m:file_mode). See:

https://github.com/githwxi/ATS-Postiats/blob/master/libc/SATS/stdio.sats

If I may, I need a bit of a hint or help for a simple start.

If I do this:

 staload "libc/SATS/stdio.sats"
 val out = fopen_exn(FILE_NAME, file_mode_w)
 val x = fflush1(out)
 val () = fclose1_exn(out)

I get an error as fflush1 expects a proof argument. I feel to understand
it’s expected to be a proof out is in write‑mode. But neither fopen_exn
nor fopen returns this proof. How to get a proof out was opened with
file_mode_w?

–
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/8c604662-020e-4bd6-8b40-b6f6727f24a5%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/8c604662-020e-4bd6-8b40-b6f6727f24a5%40googlegroups.com?utm_medium=email&utm_source=footer
.