File streams, fgets, in ATS2

Google Group
1

This is just a quick question on advice before starting something. I just
started out looking at ATS2 today, I noticed fgets functions seem to have
changed in several ways from ATS to ATS2. Chiefly, it seems that ATS1 has
FILE streams and ATS2 has FILEref and FILEptrs.

I want to write a function to read in matrices (tabular data) that will be
used going forward in ATS2, but I also need it now in ATS for (hopefully)
the last peg in the ATS-part of the project I’ve been working on. This
probably isn’t a terribly important feature for my program, but I may as
well get it over with now :). I guess the best thing to do would be to
just use fgets_err in ATS1, which seems to match up more with fgets in
ATS2. I am guessing that using the linear type would be best here, since it
would be part of a library function that others may use, so we can always
avoid forcing a GC requirement.

ATS2:
dataview
fgets_v (
sz:int, n0: int, addr, addr
) =
| {lbf:addr}
fgets_v_fail (sz, n0, lbf, null) of b0ytes(sz) @ lbf
| {n:nat | n < n0} {lbf:agz}
fgets_v_succ (sz, n0, lbf, lbf) of strbuf(sz, n) @ lbf
// end of [fgets_v]
*)
//
symintr fgets
//
fun fgets0
{sz:int}{n0:pos | n0 <= sz}
(
buf: &bytes(sz) >> _, n0: int n0, filr: FILEref
) :<!wrt> Ptr0 // = addr@(buf) or NULL

fun fgets1
{sz:int}{n0:pos | n0 <= sz}{m:fm}
(
pfm: fmlte (m, r)
| buf: &bytes(sz) >> _, n0: int n0, filp: !FILEptr1 (m)
) :<!wrt> Ptr0 // = addr@(buf) or NULL
//
overload fgets with fgets0
overload fgets with fgets1

ATS:
dataview
fgets_v (sz:int, n0: int, addr, addr) =
| {l_buf:addr}
fgets_v_fail (sz, n0, l_buf, null) of b0ytes (sz) @ l_buf
| {n:nat | n < n0} {l_buf:addr | l_buf > null}
fgets_v_succ (sz, n0, l_buf, l_buf) of strbuf (sz, n) @ l_buf
// end of [fgets_v]

fun fgets_err
{sz,n0:int | 0 < n0; n0 <= sz}
{m:fm} {l_buf:addr} (
pf_mod: file_mode_lte (m, r)
, pf_buf: b0ytes (sz) @ l_buf
| p: ptr l_buf, n0: int n0, f: &FILE m
) :<> [l:addr] (fgets_v (sz, n0, l_buf, l) | ptr l)
= “mac#atslib_fgets_err”
// end of [fgets_err]

//
// HX:
// this function returns an empty strbuf
// if EOF is reached but no character is read
//
fun fgets_exn
{sz,n0:int | 0 < n0; n0 <= sz}
{m:fm} {l_buf:addr} (
pf_mod: file_mode_lte (m, r),
pf_buf: !b0ytes (sz) @ l_buf >>
[n:nat | n < n0] strbuf (sz, n) @ l_buf
| p: ptr l_buf, n0: int n0, f: &FILE m
) :<!exn> void = “atslib_fgets_exn”
// end of [fgets_exn]

2

Ah, we were just discussing on IRC a week or so back on how to go about
specifying return values in ATS. This is nice to see.

3

In ATS2, please use ‘main0’ for ‘main’ in ATS.
The ‘main’ in ATS2 is the same as the ‘main’ in C: it returns an integer.

Also, I modified stdio.sats; so you need to update your ATS-Postiats.

Then go into ${PATSHOME} and do 'make -f codegen/Makefile_atslib"

A few more changes:

staload _(anon) = “libc/SATS/stdio.sats” // remove it
staload “libc/SATS/stdio.sats” // keep it

staload _(anon) = “prelude/DATS/integer.dats” // remove it

Add the following line:

#include “share/atspre_staload_tmpdef.hats”

This should fix your problem.

4

Thanks, I’m still getting a number of errors that I’m not very clear on. I
attached my full file if that helps.

/media/RAID5/share/ATS_learning/fcopy2.dats: 426(line=27, offs=18) –
429(line=27, offs=21): error(3):
[/home/hwxi/research/Postiats/git/doc/DISTRIB/ATS-Postiats/src/pats_trans3_util.dats]:
d3exp_trdn: the dynamic expression cannot be assigned the type
[S2Etyarr(S2Ecst(byte); S2EVar(420))].
/media/RAID5/share/ATS_learning/fcopy2.dats: 426(line=27, offs=18) –
429(line=27, offs=21): error(3): mismatch of static terms (tyleq):
The actual term is: S2Etop(knd=0; S2Ecst(byte_t0ype))
The needed term is: S2Ecst(byte_t0ype)
/media/RAID5/share/ATS_learning/fcopy2.dats: 426(line=27, offs=18) –
429(line=27, offs=21): error(3): mismatch of static terms (tyleq):
The actual term is: S2Etyarr(S2Etop(knd=0; S2Ecst(byte)); S2Evar(n(2906)))
The needed term is: S2Etyarr(S2Ecst(byte); S2EVar(420->S2Evar(n(2906))))
/media/RAID5/share/ATS_learning/fcopy2.dats: 791(line=50, offs=21) –
793(line=50, offs=23): error(3):
[/home/hwxi/research/Postiats/git/doc/DISTRIB/ATS-Postiats/src/pats_trans3_util.dats]:
d3exp_trdn: the dynamic expression cannot be assigned the type
[S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(int_kind))].
/media/RAID5/share/ATS_learning/fcopy2.dats: 791(line=50, offs=21) –
793(line=50, offs=23): error(3): mismatch of static terms (tyleq):
The actual term is: S2Ecst(atsvoid_t0ype)
The needed term is: S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(int_kind))
TRANS3: there are [2] errors in total.
exit(ATS): uncaught exception:
_2home_2hwxi_2research_2Postiats_2git_2doc_2DISTRIB_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorException(1025)

fcopy2_dats.txt (907 Bytes)

5

I have to say that fget_err is a bit hard to use. The lesson I learned in
the past few years is that you have to be able to write programs in order
to do program verification. I really think that I made the interface for
many C functions too hard to be used in practice. This is a mistake I am
trying to correct in ATS2. I wrote the following function in ATS2 for
copying files in a line-by-line manner:

fun fcopy2
(
filr: FILEref, filr2: FILEref
) : void = let
//
fun loop {n:pos}
(
buf: &b0ytes(n) >> bytes(n), n: int n, filr: FILEref, filr2: FILEref
) : void = let
val p = fgets (buf, n, filr)
in
//
if p > 0 then let
val () = fputs_exn ($UN.cast{string}§, filr2)
in
loop (buf, n, filr, filr2)
end else () // end of [if]
//
end // end of [loop]
//
val
(
pfat, pfgc | p
) = malloc_gc ((i2sz)N)
val () = loop (!p, N, filr, filr2)
val () = mfree_gc (pfat, pfgc | p)
//
in
// nothing
end (* end of [fcopy2] *)

You can do something similar in ATS1 (by making use of some unsafe
features).

6

You could also try this complete example: