Simple Input and Output

Handling I/O in ATS properly requires the availability of both dependent types and linear types, which I will cover elsewhere. In this section, I only present a means for allowing the programmer to access certain very basic I/O functionalities.

A file handle essentially associates a stream (of bytes) with a file identifier (represented as an integer). In ATS, the type for file handles is FILEref. There are three standard file handles, which are listed as follows:

Various functions on file handles are declared in the file filebas.sats, which is automatically loaded by atsopt. For instance, the functions for opening and closing file handles have the following interfaces:

fun fileref_open_exn ( path: string, fm: file_mode ) : FILEref // endfun fun fileref_close(fil: FILEref): void

Note that these two functions abort immediately whenever an error occurs. The following function is an optional version of fileref_open_exn, and the caller needs to inspect the value returned by a call to fileref_open_opt to see if a file handle is actually obtained.

fun fileref_open_opt (path: string, fm: file_mode) : Option_vt(FILEref)

The type file_mode is for values representing file modes, which are listed as follows:

As an example, the following short program opens a file handle, outputs the string "Hello, world!" plus a newline into the stream associated with the file handle and then closes the file handle:

implement main0 () = { val out = fileref_open_exn("hello.txt", file_mode_w) val () = fprint_string(out, "Hello, world!n") val () = fileref_close(out) // } (* end of [main0] *)

After executing the program, we obtain a file of the name "hello.txt" in the current working directory containing the expected content. There are various fprint-functions in ATS for printing out data into the stream associated with a given file handle. Often the programmer can simply use the name fprint to refer to these functions due to the support for overloading in ATS.

Another common I/O function is given the following interface:

fun fileref_get_line_string(fil: FILEref): Strptr1

The function fileref_get_line_string reads a line from the stream associated with a given file handle, and it returns a value of the type Strptr1. For the moment, I will simply say that such a value is just like a string except that it needs to be freed explicitly. As an example, the following short program echos onto the standard output each line read from the standard input:

implement main0 ( // argumentless ) = loop() where { // fun loop(): void = let val isnot = fileref_isnot_eof(stdin_ref) // end of [val] in // if isnot then let val line = fileref_get_line_string(stdin_ref) val ((*void*)) = fprintln!(stdout_ref, line) val ((*void*)) = strptr_free(line) in loop((*void*)) end else ((*loop exits as the end-of-file is reached*)) // end (* end of [loop] *) // } (* end of [main0] *)

Note that the function strptr_free is called to free a linear string (of the type Strptr1). Often, typing the CTRL-D character can terminate the above program for echoing each line of input.