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

[Yannick Duchêne]

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.

[Hongwei Xi]

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

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

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

[Yannick Duchêne]

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`?

[Hongwei Xi]

See: https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_dyn.sats

The proof you need is file_mode_lte_w_w:

val x = fflush(file_mode_lte_w_w | out)

--

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.