The I/O is done in ATS/Anairiats by providing interfaces for various I/O functions in C. In particular, most functions declared in <stdio.h> have their counterparts declared in libc/SATS/stdio.sats.
There is a datasort file_mode and an abstract type constructor FILE in ATS that are declared as follows:
datasort file_mode = | file_mode_r | file_mode_w | file_mode_rw absviewt@ype FILE (file_mode) = $extype "ats_FILE_type"where the external type ats_FILE_type is an alias of the type FILE in C. We now use r, w and rw for file_mode_r, file_mode_w and file_mode_rw in the following presentation. If a file is assigned the type FILE(r), then it is read-only; if it is assigned the type FILE(w), then it is write-only; it is assigned the type FILE(rw), then it can be read from and also written to.
There is also an abstract type constructorfile_mode declared as follows:
abst@ype file_mode (file_mode)Note that file_mode is overloaded: it refers to a type constructor as well as a datasort. The following values are available that represent various file modes:
val file_mode_r : file_mode (r) // = "r" val file_mode_rr : file_mode (rw) // = "r+" val file_mode_w : file_mode (w) // = "w" val file_mode_ww : file_mode (rw) // = "w+" val file_mode_a : file_mode (w) // = "a" val file_mode_aa : file_mode (rw) // = "a+"
fun fopen_exn {m:file_mode}
(path: string, m: file_mode m): [l:addr] (FILE m @ l | ptr l)
Note that we use
_exn in the name of fopen_exn as a convention to indicate
that an exception is raised if a call to this function results in an error.
There is another function
fopen_err in ATS that is assigned the following type:
fun fopen_err {m:file_mode}
(path: string, m: file_mode m): [l:addr] (FILE_opt_v (m, l) | ptr l)
where FILE_opt_v (m, l) is defined as follows:
viewdef FILE_opt_v (m:file_mode, l:addr) = option_v (FILE m @ l, l <> null)The function fopen_err exactly corresponds to fopen in C: It returns a null pointer in case of error.
fun fclose_exn {m:file_mode} {l:addr} (pf: FILE m @ l | p: ptr l): void
The function fclose_exn raises an exception if a call to it results
in an error. There is another function
fclose_err that is assigned the following type:
fun fclose_exn {m:file_mode} {l:addr} (pf: FILE m @ l | p: ptr l): int
The function fclose_err exactly corresponds to fclose in C: It
returns 0 in case of success and EOF in case of error.
fun fgetc_err {m:file_mode}
(pf: file_mode_lte (m, r) | f: &FILE m): [i:int | i <= UCHAR_MAX] int i
where UCHAR_MAX is defined to be 255.
This function exactly corresponds to
fgetc in C: It returns the obtained character (cast into unsigned
char) if successful, or it returns EOF in case of failure. The file
argument of the function fgets_err, i.e., its first non-proof argument,
is passed as a reference (call-by-reference).
Note that file_mode_lte is a prop constructor. Given two file modes m1 and m2, if a proof of the prop file_mode_lte (m1, m2) can be formed, then m1 is less than or equal to m2. The following proofs are available:
prval file_mode_lte_r_r : file_mode_lte (r, r) prval file_mode_lte_rw_r : file_mode_lte (rw, r) prval file_mode_lte_w_w : file_mode_lte (w, w) prval file_mode_lte_rw_w : file_mode_lte (rw, w) prval file_mode_lte_rw_rw : file_mode_lte (rw, rw)In order to read from a file of the type FILE (m), it is necessary to prove that m is less than or equal to r.
There is currently no function fget_exn, which would be given the following type if defined:
fun fgetc_exn {m:file_mode}
(pf: file_mode_lte (m, r) | f: &FILE m): [i:nat | i <= UCHAR_MAX] int i
The problem with fgetc_exn is that it is not a function of much
use. If implemented, this function should probably be called on a file
after it is made certain (e.g., by calling feof) that the file has
not reached its end.
fun fputc_err {m:file_mode}
(pf: file_mode_lte (m, w) | c: char, f: &FILE m): [i:int | i <= UCHAR_MAX] int i
This function exactly corresponds to fputc in C: It returns the
charater being written in case of success, or EOF in case of failure. There
is another function fputc_exn that is assigned the following type:
fun fputc_exn {m:file_mode} (pf: file_mode_lte (m, w) | c: char, f: &FILE m): void
In case of failure, fputs_exn raises an exception.
#define i2c char_of_int1
fn filecopy_exn {m1,m2:file_mode} (
pf1: file_mode_lte (m1, r)
, pf2: file_mode_lte (m2, w)
| fil_s: &FILE m1, fil_d: &FILE m2
) : void = let
fun loop
(fil_s: &FILE m1, fil_d: &FILE m2): void = let
val c = fgetc_err (pf1 | fil_s)
in
if c >= 0 then begin
fputc_exn (pf2 | i2c c, fil_d); loop (fil_s, fil_d)
end // end of [if]
end // end of [loop]
in
loop (fil_s, fil_d)
end // end of [filecopy_exn]
In case of error, filecopy_exn raises an exception.
The following function filecopy_err is a variant of
filecopy_exn. Instead of raising an exception in case of error,
filecopy_err returns EOF.
fn filecopy_err {m1,m2:file_mode} (
pf1: file_mode_lte (m1, r)
, pf2: file_mode_lte (m2, w)
| fil_s: &FILE m1, fil_d: &FILE m2
) : int = let
fun loop
(fil_s: &FILE m1, fil_d: &FILE m2): void = let
val c = fgetc_err (pf1 | fil_s)
in
if c >= 0 then let
val err = fputc_err (pf2 | i2c c, fil_d)
in
loop (fil_s, fil_d)
end // end of [if]
end // end of [loop]
val () = loop (fil_s, fil_d)
in
if ferror (fil_d) = 0 then ~1 else 0
end // end of [filecopy_err]
We now use filecopy_err to implement as follows the functionality of
concatenating a list of files into a single one:
// concatenation of a list of files
implement main {n} (argc, argv) = let
val () = case+ argc of
| 1 => let
val (pf_stdin | p_stdin) = stdin_get ()
val (pf_stdout | p_stdout) = stdout_get ()
val _(*err*) = filecopy_err
(file_mode_lte_r_r, file_mode_lte_w_w | !p_stdin, !p_stdout)
val () = stdout_view_set (pf_stdout | (*none*))
val () = stdin_view_set (pf_stdin | (*none*))
in
// empty
end // end of [1]
| _ (*argc >= 2*) => loop (argc, argv, 1) where {
fun loop {i:nat | i <= n}
(argc: int n, argv: &(@[string][n]), i: int i): void =
if i < argc then let
val name = argv.[i]
val (pfopt | p_ifp) = fopen_err (name, file_mode_r)
in
if p_ifp <> null then let
prval Some_v (pf) = pfopt
val (pf_stdout | p_stdout) = stdout_get ()
val _(*err*) = filecopy_err
(file_mode_lte_r_r, file_mode_lte_w_w | !p_ifp, !p_stdout)
val () = stdout_view_set (pf_stdout | (*none*))
val () = fclose_exn (pf | p_ifp)
in
loop (argc, argv, i+1)
end else let
prval None_v () = pfopt
val () = prerrf ("%s: can't open [%s]\n", @(argv.[0], name))
in
exit {void} (1)
end // end of [if]
end // end of [if]
} // end of [_]
// end of [val]
val (pf_stdout | p_stdout) = stdout_get ()
val err = ferror (!p_stdout)
val () = stdout_view_set (pf_stdout | (*none*))
in
if (err <> 0) then begin
prerrf ("%s: error writing stdout\n", @(argv.[0])); exit {void} (2)
end else begin
exit {void} (0) // exit normally
end // end of [if]
end // end of [main]
The code used for illustration is available here.